Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(AlgebraicTopology/SimplicialSet): 0-truncated paths #21331

Closed
wants to merge 94 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
94 commits
Select commit Hold shift + click to select a range
2e28429
Refactor StrictSegal defs through SSet.Truncated
gio256 Jan 11, 2025
a469764
Add SimplexCategory.Truncated macro [m]ₙ
gio256 Jan 12, 2025
f423198
fix: doc lints
gio256 Jan 12, 2025
08ac434
fix: instance lints
gio256 Jan 12, 2025
38def5d
fix: more instance lints
gio256 Jan 12, 2025
ef1fb9b
Improve leq_prefix tactic
gio256 Jan 12, 2025
5a6166f
Reuse truncated notations in HomotopyCat.lean
gio256 Jan 12, 2025
0bef460
Tweak leq tactic
gio256 Jan 12, 2025
330f44f
Add truncated simplicial notations
gio256 Jan 12, 2025
24f9711
Update scripts/noshake.json
gio256 Jan 12, 2025
6f2e291
Formatting
gio256 Jan 12, 2025
72e21fc
Formatting: indentation
gio256 Jan 12, 2025
fb62cb2
Move failure message into trunc tactic
gio256 Jan 12, 2025
0139c97
Add delaborator for SimplexCategory notation [m]ₙ
gio256 Jan 13, 2025
378fa76
Tweak SimplexCategory.delabMkNotation
gio256 Jan 14, 2025
99574d0
Add delaborators for SimplicialObject notations
gio256 Jan 14, 2025
42aecaa
doc: docstrings for SimplicialObject delaborators
gio256 Jan 14, 2025
7c89dd9
Clarify behavior of notations wrt metavariables
gio256 Jan 14, 2025
02aa8de
Merge branch 'gio/trunc-delab' (#20719)
gio256 Jan 14, 2025
a948233
fix: duplicate open in HomotopyCat.lean
gio256 Jan 14, 2025
acca59b
feat: CosimplicialObject.Truncated.trunc
gio256 Jan 14, 2025
e86382b
feat: SimplexCategory.Truncated.Hom.tr, fewer erws
gio256 Jan 16, 2025
29bab8b
fix: remove unused import
gio256 Jan 16, 2025
524b70a
fix: Remove some erws in Coskeletal.lean
gio256 Jan 16, 2025
257bdb6
fix: combine successive rewrites
gio256 Jan 17, 2025
5d41e60
fix(SimplexCategory): check valid subscript chars
gio256 Jan 17, 2025
f4d15c3
fix(SimplicialObject): check valid subscript chars
gio256 Jan 17, 2025
6076206
chore: Rename Meta.subscript and reduce footprint
gio256 Jan 17, 2025
a2a99a1
chore: style fixes
gio256 Jan 17, 2025
d7d008c
doc: backport changes from branch gio/trunc-delab
gio256 Jan 17, 2025
352317b
fix: scoped macro_rules
gio256 Jan 18, 2025
9f6f968
Merge branch 'master' into gio/trunc-macro
gio256 Jan 18, 2025
b306faa
doc: fix typo
gio256 Jan 18, 2025
9df7da9
Merge branch 'master' into gio/trunc-delab
gio256 Jan 18, 2025
daa9210
Merge branch 'master' into gio/trunc
gio256 Jan 18, 2025
0667d75
Merge branch 'gio/trunc-delab' into gio/trunc
gio256 Jan 18, 2025
99fb3cd
chore: clean up a goal
gio256 Jan 18, 2025
696b6a3
chore: style fixes
gio256 Jan 18, 2025
90b595f
doc: Update docstrings for Path.ext' lemmas
gio256 Jan 18, 2025
95ec5e4
Merge branch 'gio/trunc-delab' into gio/trunc
gio256 Jan 18, 2025
ac96b32
fix: spine_map_vertex lemmas
gio256 Jan 18, 2025
6182de8
chore: decided not to duplicate diagonal
gio256 Jan 18, 2025
bac7a43
chore: formatting of macro_rules
gio256 Jan 18, 2025
232614a
fix: backport changes from branch gio/trunc-delab
gio256 Jan 18, 2025
a0ef73e
Merge branch 'gio/trunc-delab' into gio/trunc
gio256 Jan 18, 2025
81ed7e1
Add class IsStrictSegal : Prop
gio256 Jan 18, 2025
c63cf41
chore: make IsStrictSegal param autoParam
gio256 Jan 18, 2025
65ea7e7
chore: clean up sections in StrictSegal.lean
gio256 Jan 18, 2025
48bb968
doc: Update doc for SimplicialSet/StrictSegal.lean
gio256 Jan 18, 2025
7a07689
chore: use explicit max func in spine_map_vertex
gio256 Jan 18, 2025
06edc34
feat: StrictSegal.spineToSimplex_map lemmas
gio256 Jan 18, 2025
24b638e
chore: use sx for term of type StrictSegal X
gio256 Jan 18, 2025
eee4fa5
fix: make isStrictSegal_of_strictSegal a lemma
gio256 Jan 18, 2025
8f2a98c
chore: simplify some proofs, try to avoid omega
gio256 Jan 19, 2025
50882fa
chore: simplify a proof
gio256 Jan 19, 2025
295ddad
feat: explicit spine_arrow and spine_vertex lemmas
gio256 Jan 19, 2025
98670c2
feat: explicit map_arrow and map_vertex lemmas
gio256 Jan 19, 2025
175a41c
feat: lemma SimplexCategory.Truncated.Hom.tr_comp
gio256 Jan 19, 2025
d05db46
feat: lemma SSet.StrictSegal.spineEquiv_coe_fn_mk
gio256 Jan 19, 2025
3ee7431
feat: simplify proofs in SimplicialSet/StrictSegal
gio256 Jan 19, 2025
fa89320
fix: remove simp lemmas for abbrevs in Path.lean
gio256 Jan 19, 2025
10dc3b6
feat: rename spineEquiv_coe_fn, simplify proof
gio256 Jan 19, 2025
55bb50a
feat: trunc_spine and truncation_spine lemmas
gio256 Jan 20, 2025
e04e653
feat: lemma spine_map_subinterval
gio256 Jan 20, 2025
39f6a5a
chore: update authors
gio256 Jan 20, 2025
266cabd
chore: clean up some proofs in Coskeletal.lean
gio256 Jan 20, 2025
a2e99a2
chore: explicit argument in rw
gio256 Jan 20, 2025
0c9a500
chore: rename spineEquiv_symm_coe_fn
gio256 Jan 20, 2025
2b396e9
chore: clean up some proofs in Coskeletal.lean
gio256 Jan 20, 2025
218da01
feat: make (X : SSet) implicit in Coskeletal.lean
gio256 Jan 20, 2025
b04302a
chore: simplify two proofs
gio256 Jan 20, 2025
dcf2d37
chore: style fixes
gio256 Jan 20, 2025
a6d960c
chore: rename lemma StrictSegal.isStrictSegal
gio256 Jan 20, 2025
c81f10f
feat: lemma spineToDiagonal_def
gio256 Jan 20, 2025
4a7364c
chore: make some arguments explicit in Path₁.map
gio256 Jan 20, 2025
36b5e84
fix: cheaper trunc tactic (defer to omega sooner)
gio256 Jan 21, 2025
8736801
Merge branch 'gio/trunc-macro' into gio/trunc-delab
gio256 Jan 21, 2025
32b95d3
Merge branch 'gio/trunc-delab' into gio/trunc
gio256 Jan 21, 2025
ec03ef2
Remove leq tactic
gio256 Jan 22, 2025
2591116
Give strArrowMk₂ an autoParam
gio256 Jan 22, 2025
b5bd7fd
feat: adjust autoParam usage
gio256 Jan 22, 2025
ff883fb
feat: try to tag spineToSimplex_spine_apply simp
gio256 Jan 22, 2025
6c775f3
fix: only one spineToSimplex_spine_apply simps
gio256 Jan 22, 2025
a89a1ac
chore: Update scripts/noshake.json
gio256 Jan 23, 2025
ce76d0f
Merge branch 'gio/trunc-delab' into gio/trunc
gio256 Jan 23, 2025
73b3e0e
Merge branch 'master' into gio/trunc
gio256 Jan 23, 2025
434a77e
fix: trailing whitespace
gio256 Jan 23, 2025
73e4f26
Merge branch 'master' into gio/trunc
gio256 Jan 25, 2025
4abc0d6
fix: merge conflict in SimplicialSet/Basic.lean
gio256 Jan 25, 2025
8262d32
feat: inductive def of SSet.Truncated.StrictSegal
gio256 Jan 26, 2025
3076bed
fix: improve failure message for trunc tactic
gio256 Jan 27, 2025
3060678
Merge branch 'gio/trunc-macro' into gio/trunc-delab
gio256 Jan 27, 2025
47245b0
Merge branch 'gio/trunc-delab' into gio/trunc-ind
gio256 Jan 27, 2025
53dc574
feat: 0-truncated path definition
gio256 Jan 27, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
chore: make some arguments explicit in Path₁.map
gio256 committed Jan 20, 2025
commit 4a7364c0b016676ea122cbf319cf863bb7307ff5
4 changes: 2 additions & 2 deletions Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
Original file line number Diff line number Diff line change
@@ -70,8 +70,8 @@ variable {X Y : SSet.Truncated.{u} 1} {n : ℕ}
/-- Maps of 1-truncated simplicial sets induce maps of paths. -/
@[simps]
def map (f : Path₁ X n) (σ : X ⟶ Y) : Path₁ Y n where
vertex i := σ.app _ (f.vertex i)
arrow i := σ.app _ (f.arrow i)
vertex i := σ.app (op [0]₁) (f.vertex i)
arrow i := σ.app (op [1]₁) (f.arrow i)
arrow_src i := by
simp only [← f.arrow_src i]
exact congr (σ.naturality (tr (δ 1)).op) rfl |>.symm