Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 5ed51dc

Browse files
joelrioujoelriou
committed
feat(algebraic_topology): variations on the statements of simplicial relations (#16957)
This PR introduces variations on the statements of simplicial relations which makes it easier to use. This is demonstrated in `algebraic_topology.dold_kan.faces`. The attribute `reassoc` is also added to the simplicial relations.
1 parent a4c2bd4 commit 5ed51dc

4 files changed

Lines changed: 184 additions & 42 deletions

File tree

‎src/algebraic_topology/dold_kan/faces.lean‎

Lines changed: 46 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,18 @@ def higher_faces_vanish {Y : C} {n : ℕ} (q : ℕ) (φ : Y ⟶ X _[n+1]) : Prop
5252

5353
namespace higher_faces_vanish
5454

55+
@[reassoc]
56+
lemma comp_δ_eq_zero {Y : C} {n : ℕ} {q : ℕ} {φ : Y ⟶ X _[n+1]}
57+
(v : higher_faces_vanish q φ) (j : fin (n+2)) (hj₁ : j ≠ 0) (hj₂ : n+2 ≤ (j : ℕ) + q) :
58+
φ ≫ X.δ j = 0 :=
59+
begin
60+
obtain ⟨i, hi⟩ := fin.eq_succ_of_ne_zero hj₁,
61+
subst hi,
62+
apply v i,
63+
rw [← @nat.add_le_add_iff_right 1, add_assoc],
64+
simpa only [fin.coe_succ, add_assoc, add_comm 1] using hj₂,
65+
end
66+
5567
lemma of_succ {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n+1]}
5668
(v : higher_faces_vanish (q+1) φ) : higher_faces_vanish q φ :=
5769
λ j hj, v j (by simpa only [← add_assoc] using le_add_right hj)
@@ -84,18 +96,16 @@ begin
8496
/- cleaning up the second sum -/
8597
rw [← fin.sum_congr' _ (hnaq_shift 3).symm, @fin.sum_trunc _ _ (a+3)], swap,
8698
{ rintros ⟨k, hk⟩,
87-
suffices : φ ≫ X.σ ⟨a+1, by linarith⟩ ≫ X.δ ⟨a+3+k, by linarith⟩ = 0,
88-
{ dsimp, rw [assoc, this, smul_zero], },
89-
let i : fin (n+1) := ⟨a+1+k, by linarith⟩,
90-
have h : fin.cast_succ (⟨a+1, by linarith⟩ : fin (n+1)) < i.succ,
91-
{ simp only [fin.lt_iff_coe_lt_coe, fin.cast_succ_mk, fin.coe_mk, fin.succ_mk],
99+
rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero],
100+
{ intro h,
101+
rw [fin.pred_eq_iff_eq_succ, fin.ext_iff] at h,
102+
dsimp at h,
92103
linarith, },
93-
have δσ_rel := δ_comp_σ_of_gt X h,
94-
conv_lhs at δσ_rel
95-
{ simp only [fin.cast_succ_mk, fin.succ_mk, show a+1+k+1+1 = a+3+k, by linarith], },
96-
rw [δσ_rel, ← assoc, v i, zero_comp],
97-
simp only [i, fin.coe_mk],
98-
linarith, },
104+
{ dsimp,
105+
simp only [fin.coe_pred, fin.coe_mk, succ_add_sub_one],
106+
linarith, },
107+
{ dsimp,
108+
linarith, }, },
99109
/- leaving out three specific terms -/
100110
conv_lhs { congr, skip, rw [fin.sum_univ_cast_succ, fin.sum_univ_cast_succ], },
101111
rw fin.sum_univ_cast_succ,
@@ -113,15 +123,10 @@ begin
113123
use a,
114124
linarith, },
115125
{ /- d+e = 0 -/
116-
let b : fin (n+2) := ⟨a+1, by linarith⟩,
117-
have eq₁ : X.σ b ≫ X.δ (fin.cast_succ b) = 𝟙 _ := δ_comp_σ_self _,
118-
have eq₂ : X.σ b ≫ X.δ b.succ = 𝟙 _ := δ_comp_σ_succ _,
119-
simp only [b, fin.cast_succ_mk, fin.succ_mk] at eq₁ eq₂,
120-
simp only [eq₁, eq₂, fin.last, assoc, fin.cast_succ_mk, fin.cast_le_mk, fin.coe_mk,
121-
comp_id, add_eq_zero_iff_eq_neg, ← neg_zsmul],
122-
congr,
123-
ring_exp,
124-
rw mul_one, },
126+
rw [assoc, assoc, X.δ_comp_σ_self' (fin.cast_succ_mk _ _ _).symm,
127+
X.δ_comp_σ_succ' (fin.succ_mk _ _ _).symm],
128+
simp only [comp_id, pow_add _ (a+1) 1, pow_one, mul_neg, mul_one, neg_smul,
129+
add_right_neg], },
125130
{ /- c+a = 0 -/
126131
rw ← finset.sum_add_distrib,
127132
apply finset.sum_eq_zero,
@@ -151,13 +156,17 @@ begin
151156
fin.coe_one, pow_one, neg_smul, comp_neg],
152157
erw [δ_comp_σ_self, δ_comp_σ_succ, add_right_neg], },
153158
{ intro j,
154-
simp only [comp_zsmul],
155-
convert zsmul_zero _,
156-
have h : fin.cast (by rw add_comm 2) (fin.nat_add 2 j) = j.succ.succ,
157-
{ ext, simp only [add_comm 2, fin.coe_cast, fin.coe_nat_add, fin.coe_succ], },
158-
rw [h, ← fin.cast_succ_zero, δ_comp_σ_of_gt X], swap,
159-
{ exact fin.succ_pos j, },
160-
simp only [← assoc, v j (by linarith), zero_comp], }, },
159+
rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero],
160+
{ intro h,
161+
rw [fin.pred_eq_iff_eq_succ, fin.ext_iff] at h,
162+
dsimp at h,
163+
linarith, },
164+
{ dsimp,
165+
simp only [fin.cast_nat_add, fin.coe_pred, fin.coe_add_nat, add_succ_sub_one],
166+
linarith, },
167+
{ rw fin.lt_iff_coe_lt_coe,
168+
dsimp,
169+
linarith, }, }, },
161170
end
162171

163172
lemma induction {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n+1]}
@@ -190,26 +199,22 @@ begin
190199
{ by_contradiction,
191200
rw [not_le, ← nat.succ_le_iff] at h,
192201
linarith, },
193-
have ineq₁ : (fin.cast_succ (⟨a, nat.lt_succ_iff.mpr ham⟩ : fin (m+1)) < j),
194-
{ rw fin.lt_iff_coe_lt_coe, exact haj, },
195-
have eq₁ := δ_comp_σ_of_gt X ineq₁,
196-
rw fin.cast_succ_mk at eq₁,
197-
rw eq₁,
202+
rw [X.δ_comp_σ_of_gt', j.pred_succ], swap,
203+
{ rw fin.lt_iff_coe_lt_coe,
204+
simpa only [fin.coe_mk, fin.coe_succ, add_lt_add_iff_right] using haj, },
198205
obtain (ham' | ham'') := ham.lt_or_eq,
199206
{ -- case where `a<m`
200-
have ineq₂ : (fin.cast_succ (⟨a+1, nat.succ_lt_succ ham'⟩ : fin (m+1)) ≤ j),
201-
{ simpa only [fin.le_iff_coe_le_coe] using nat.succ_le_iff.mpr haj, },
202-
have eq₂ := δ_comp_δ X ineq₂,
203-
simp only [fin.cast_succ_mk] at eq₂,
204-
slice_rhs 2 3 { rw ← eq₂, },
207+
rw ← X.δ_comp_δ''_assoc, swap,
208+
{ rw fin.le_iff_coe_le_coe,
209+
dsimp,
210+
linarith, },
205211
simp only [← assoc, v j (by linarith), zero_comp], },
206212
{ -- in the last case, a=m, q=1 and j=a+1
207-
have hq : q=1 := by rw [← add_left_inj a, ha, ham'', add_comm],
208-
have hj₄ : (⟨a+1, by linarith⟩ : fin (m+3)) = fin.cast_succ j,
213+
rw X.δ_comp_δ_self'_assoc, swap,
209214
{ ext,
210-
simp only [fin.coe_mk, fin.coe_cast_succ],
215+
dsimp,
216+
have hq : q = 1 := by rw [← add_left_inj a, ha, ham'', add_comm],
211217
linarith, },
212-
slice_rhs 2 3 { rw [hj₄, δ_comp_δ_self], },
213218
simp only [← assoc, v j (by linarith), zero_comp], },
214219
end
215220

‎src/algebraic_topology/simplex_category.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,11 +172,36 @@ begin
172172
split_ifs; { simp at *; linarith },
173173
end
174174

175+
lemma δ_comp_δ' {n} {i : fin (n+2)} {j : fin (n+3)} (H : i.cast_succ < j) :
176+
δ i ≫ δ j = δ (j.pred (λ hj, by simpa only [hj, fin.not_lt_zero] using H)) ≫ δ i.cast_succ :=
177+
begin
178+
rw ← δ_comp_δ,
179+
{ rw fin.succ_pred, },
180+
{ simpa only [fin.le_iff_coe_le_coe, ← nat.lt_succ_iff, nat.succ_eq_add_one, ← fin.coe_succ,
181+
j.succ_pred, fin.lt_iff_coe_lt_coe] using H, },
182+
end
183+
184+
lemma δ_comp_δ'' {n} {i : fin (n+3)} {j : fin (n+2)} (H : i ≤ j.cast_succ) :
185+
δ (i.cast_lt (nat.lt_of_le_of_lt (fin.le_iff_coe_le_coe.mp H) j.is_lt)) ≫ δ j.succ =
186+
δ j ≫ δ i :=
187+
begin
188+
rw δ_comp_δ,
189+
{ refl, },
190+
{ exact H, },
191+
end
192+
175193
/-- The special case of the first simplicial identity -/
194+
@[reassoc]
176195
lemma δ_comp_δ_self {n} {i : fin (n+2)} : δ i ≫ δ i.cast_succ = δ i ≫ δ i.succ :=
177196
(δ_comp_δ (le_refl i)).symm
178197

198+
@[reassoc]
199+
lemma δ_comp_δ_self' {n} {i : fin (n+2)} {j : fin (n+3)} (H : j = i.cast_succ) :
200+
δ i ≫ δ j = δ i ≫ δ i.succ :=
201+
by { subst H, rw δ_comp_δ_self, }
202+
179203
/-- The second simplicial identity -/
204+
@[reassoc]
180205
lemma δ_comp_σ_of_le {n} {i : fin (n+2)} {j : fin (n+1)} (H : i ≤ j.cast_succ) :
181206
δ i.cast_succ ≫ σ j.succ = σ j ≫ δ i :=
182207
begin
@@ -207,6 +232,7 @@ begin
207232
end
208233

209234
/-- The first part of the third simplicial identity -/
235+
@[reassoc]
210236
lemma δ_comp_σ_self {n} {i : fin (n+1)} :
211237
δ i.cast_succ ≫ σ i = 𝟙 [n] :=
212238
begin
@@ -220,7 +246,13 @@ begin
220246
split_ifs; { simp at *; linarith, },
221247
end
222248

249+
@[reassoc]
250+
lemma δ_comp_σ_self' {n} {j : fin (n+2)} {i : fin (n+1)} (H : j = i.cast_succ) :
251+
δ j ≫ σ i = 𝟙 [n] :=
252+
by { subst H, rw δ_comp_σ_self, }
253+
223254
/-- The second part of the third simplicial identity -/
255+
@[reassoc]
224256
lemma δ_comp_σ_succ {n} {i : fin (n+1)} :
225257
δ i.succ ≫ σ i = 𝟙 [n] :=
226258
begin
@@ -232,7 +264,13 @@ begin
232264
split_ifs; { simp at *; linarith, },
233265
end
234266

267+
@[reassoc]
268+
lemma δ_comp_σ_succ' {n} (j : fin (n+2)) (i : fin (n+1)) (H : j = i.succ) :
269+
δ j ≫ σ i = 𝟙 [n] :=
270+
by { subst H, rw δ_comp_σ_succ, }
271+
235272
/-- The fourth simplicial identity -/
273+
@[reassoc]
236274
lemma δ_comp_σ_of_gt {n} {i : fin (n+2)} {j : fin (n+1)} (H : j.cast_succ < i) :
237275
δ i.succ ≫ σ j.cast_succ = σ j ≫ δ i :=
238276
begin
@@ -270,9 +308,23 @@ begin
270308
all_goals { simp at h_1 h_2 ⊢; linarith, },
271309
end
272310

311+
@[reassoc]
312+
lemma δ_comp_σ_of_gt' {n} {i : fin (n+3)} {j : fin (n+2)} (H : j.succ < i) :
313+
δ i ≫ σ j = σ (j.cast_lt ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le
314+
(by simpa only [fin.val_eq_coe, ← fin.coe_succ]
315+
using fin.lt_iff_coe_lt_coe.mp H) i.is_le))) ≫
316+
δ (i.pred (λ hi, by simpa only [fin.not_lt_zero, hi] using H)) :=
317+
begin
318+
rw ← δ_comp_σ_of_gt,
319+
{ simpa only [fin.succ_pred], },
320+
{ rw [fin.cast_succ_cast_lt, ← fin.succ_lt_succ_iff, fin.succ_pred],
321+
exact H, },
322+
end
323+
273324
local attribute [simp] fin.pred_mk
274325

275326
/-- The fifth simplicial identity -/
327+
@[reassoc]
276328
lemma σ_comp_σ {n} {i j : fin (n+1)} (H : i ≤ j) :
277329
σ i.cast_succ ≫ σ j = σ j.succ ≫ σ i :=
278330
begin

‎src/algebraic_topology/simplicial_object.lean‎

Lines changed: 82 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,41 +70,81 @@ by { ext, simp [eq_to_iso], }
7070

7171

7272
/-- The generic case of the first simplicial identity -/
73+
@[reassoc]
7374
lemma δ_comp_δ {n} {i j : fin (n+2)} (H : i ≤ j) :
7475
X.δ j.succ ≫ X.δ i = X.δ i.cast_succ ≫ X.δ j :=
7576
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ H] }
7677

78+
@[reassoc]
79+
lemma δ_comp_δ' {n} {i : fin (n+2)} {j : fin (n+3)} (H : i.cast_succ < j) :
80+
X.δ j ≫ X.δ i = X.δ i.cast_succ ≫
81+
X.δ (j.pred (λ hj, by simpa only [hj, fin.not_lt_zero] using H)) :=
82+
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ' H] }
83+
84+
@[reassoc]
85+
lemma δ_comp_δ'' {n} {i : fin (n+3)} {j : fin (n+2)} (H : i ≤ j.cast_succ) :
86+
X.δ j.succ ≫ X.δ (i.cast_lt (nat.lt_of_le_of_lt (fin.le_iff_coe_le_coe.mp H) j.is_lt)) =
87+
X.δ i ≫ X.δ j :=
88+
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ'' H] }
89+
7790
/-- The special case of the first simplicial identity -/
91+
@[reassoc]
7892
lemma δ_comp_δ_self {n} {i : fin (n+2)} : X.δ i.cast_succ ≫ X.δ i = X.δ i.succ ≫ X.δ i :=
7993
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ_self] }
8094

95+
@[reassoc]
96+
lemma δ_comp_δ_self' {n} {j : fin (n+3)} {i : fin (n+2)} (H : j = i.cast_succ) :
97+
X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i :=
98+
by { subst H, rw δ_comp_δ_self, }
99+
81100
/-- The second simplicial identity -/
101+
@[reassoc]
82102
lemma δ_comp_σ_of_le {n} {i : fin (n+2)} {j : fin (n+1)} (H : i ≤ j.cast_succ) :
83103
X.σ j.succ ≫ X.δ i.cast_succ = X.δ i ≫ X.σ j :=
84104
by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_le H] }
85105

86106
/-- The first part of the third simplicial identity -/
107+
@[reassoc]
87108
lemma δ_comp_σ_self {n} {i : fin (n+1)} :
88109
X.σ i ≫ X.δ i.cast_succ = 𝟙 _ :=
89110
begin
90111
dsimp [δ, σ],
91112
simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_self, op_id, X.map_id],
92113
end
93114

115+
@[reassoc]
116+
lemma δ_comp_σ_self' {n} {j : fin (n+2)} {i : fin (n+1)} (H : j = i.cast_succ):
117+
X.σ i ≫ X.δ j = 𝟙 _ := by { subst H, rw δ_comp_σ_self, }
118+
94119
/-- The second part of the third simplicial identity -/
120+
@[reassoc]
95121
lemma δ_comp_σ_succ {n} {i : fin (n+1)} :
96122
X.σ i ≫ X.δ i.succ = 𝟙 _ :=
97123
begin
98124
dsimp [δ, σ],
99125
simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_succ, op_id, X.map_id],
100126
end
101127

128+
@[reassoc]
129+
lemma δ_comp_σ_succ' {n} {j : fin (n+2)} {i : fin (n+1)} (H : j = i.succ) :
130+
X.σ i ≫ X.δ j = 𝟙 _ := by { subst H, rw δ_comp_σ_succ, }
131+
102132
/-- The fourth simplicial identity -/
133+
@[reassoc]
103134
lemma δ_comp_σ_of_gt {n} {i : fin (n+2)} {j : fin (n+1)} (H : j.cast_succ < i) :
104135
X.σ j.cast_succ ≫ X.δ i.succ = X.δ i ≫ X.σ j :=
105136
by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_gt H] }
106137

138+
@[reassoc]
139+
lemma δ_comp_σ_of_gt' {n} {i : fin (n+3)} {j : fin (n+2)} (H : j.succ < i) :
140+
X.σ j ≫ X.δ i = X.δ (i.pred (λ hi, by simpa only [fin.not_lt_zero, hi] using H)) ≫
141+
X.σ (j.cast_lt ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le
142+
(by simpa only [fin.val_eq_coe, ← fin.coe_succ]
143+
using fin.lt_iff_coe_lt_coe.mp H) i.is_le))) :=
144+
by { dsimp [δ, σ], simpa only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_gt' H], }
145+
107146
/-- The fifth simplicial identity -/
147+
@[reassoc]
108148
lemma σ_comp_σ {n} {i j : fin (n+1)} (H : i ≤ j) :
109149
X.σ j ≫ X.σ i.cast_succ = X.σ i ≫ X.σ j.succ :=
110150
by { dsimp [δ, σ], simp only [←X.map_comp, ←op_comp, simplex_category.σ_comp_σ H] }
@@ -312,43 +352,84 @@ X.map_iso (eq_to_iso (by rw h))
312352
@[simp] lemma eq_to_iso_refl {n : ℕ} (h : n = n) : X.eq_to_iso h = iso.refl _ :=
313353
by { ext, simp [eq_to_iso], }
314354

315-
316355
/-- The generic case of the first cosimplicial identity -/
356+
@[reassoc]
317357
lemma δ_comp_δ {n} {i j : fin (n+2)} (H : i ≤ j) :
318358
X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ i.cast_succ :=
319359
by { dsimp [δ], simp only [←X.map_comp, simplex_category.δ_comp_δ H], }
320360

361+
@[reassoc]
362+
lemma δ_comp_δ' {n} {i : fin (n+2)} {j : fin (n+3)} (H : i.cast_succ < j) :
363+
X.δ i ≫ X.δ j = X.δ (j.pred (λ hj, by simpa only [hj, fin.not_lt_zero] using H)) ≫
364+
X.δ i.cast_succ :=
365+
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ' H] }
366+
367+
@[reassoc]
368+
lemma δ_comp_δ'' {n} {i : fin (n+3)} {j : fin (n+2)} (H : i ≤ j.cast_succ) :
369+
X.δ (i.cast_lt (nat.lt_of_le_of_lt (fin.le_iff_coe_le_coe.mp H) j.is_lt)) ≫ X.δ j.succ =
370+
X.δ j ≫ X.δ i :=
371+
by { dsimp [δ], simp only [←X.map_comp, ←op_comp, simplex_category.δ_comp_δ'' H] }
372+
321373
/-- The special case of the first cosimplicial identity -/
374+
@[reassoc]
322375
lemma δ_comp_δ_self {n} {i : fin (n+2)} : X.δ i ≫ X.δ i.cast_succ = X.δ i ≫ X.δ i.succ :=
323376
by { dsimp [δ], simp only [←X.map_comp, simplex_category.δ_comp_δ_self] }
324377

378+
@[reassoc]
379+
lemma δ_comp_δ_self' {n} {i : fin (n+2)} {j : fin (n+3)} (H : j = i.cast_succ) :
380+
X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ :=
381+
by { subst H, rw δ_comp_δ_self, }
382+
325383
/-- The second cosimplicial identity -/
384+
@[reassoc]
326385
lemma δ_comp_σ_of_le {n} {i : fin (n+2)} {j : fin (n+1)} (H : i ≤ j.cast_succ) :
327386
X.δ i.cast_succ ≫ X.σ j.succ = X.σ j ≫ X.δ i :=
328387
by { dsimp [δ, σ], simp only [←X.map_comp, simplex_category.δ_comp_σ_of_le H] }
329388

330389
/-- The first part of the third cosimplicial identity -/
390+
@[reassoc]
331391
lemma δ_comp_σ_self {n} {i : fin (n+1)} :
332392
X.δ i.cast_succ ≫ X.σ i = 𝟙 _ :=
333393
begin
334394
dsimp [δ, σ],
335395
simp only [←X.map_comp, simplex_category.δ_comp_σ_self, X.map_id],
336396
end
337397

398+
@[reassoc]
399+
lemma δ_comp_σ_self' {n} {j : fin (n+2)} {i : fin (n+1)} (H : j = i.cast_succ) :
400+
X.δ j ≫ X.σ i = 𝟙 _ :=
401+
by { subst H, rw δ_comp_σ_self, }
402+
338403
/-- The second part of the third cosimplicial identity -/
404+
@[reassoc]
339405
lemma δ_comp_σ_succ {n} {i : fin (n+1)} :
340406
X.δ i.succ ≫ X.σ i = 𝟙 _ :=
341407
begin
342408
dsimp [δ, σ],
343409
simp only [←X.map_comp, simplex_category.δ_comp_σ_succ, X.map_id],
344410
end
345411

412+
@[reassoc]
413+
lemma δ_comp_σ_succ' {n} {j : fin (n+2)} {i : fin (n+1)} (H : j = i.succ) :
414+
X.δ j ≫ X.σ i = 𝟙 _ :=
415+
by { subst H, rw δ_comp_σ_succ, }
416+
346417
/-- The fourth cosimplicial identity -/
418+
@[reassoc]
347419
lemma δ_comp_σ_of_gt {n} {i : fin (n+2)} {j : fin (n+1)} (H : j.cast_succ < i) :
348420
X.δ i.succ ≫ X.σ j.cast_succ = X.σ j ≫ X.δ i :=
349421
by { dsimp [δ, σ], simp only [←X.map_comp, simplex_category.δ_comp_σ_of_gt H] }
350422

423+
@[reassoc]
424+
lemma δ_comp_σ_of_gt' {n} {i : fin (n+3)} {j : fin (n+2)} (H : j.succ < i) :
425+
X.δ i ≫ X.σ j = X.σ (j.cast_lt ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le
426+
(by simpa only [fin.val_eq_coe, ← fin.coe_succ]
427+
using fin.lt_iff_coe_lt_coe.mp H) i.is_le))) ≫
428+
X.δ (i.pred (λ hi, by simpa only [fin.not_lt_zero, hi] using H)) :=
429+
by { dsimp [δ, σ], simpa only [←X.map_comp, ←op_comp, simplex_category.δ_comp_σ_of_gt' H], }
430+
351431
/-- The fifth cosimplicial identity -/
432+
@[reassoc]
352433
lemma σ_comp_σ {n} {i j : fin (n+1)} (H : i ≤ j) :
353434
X.σ i.cast_succ ≫ X.σ j = X.σ j.succ ≫ X.σ i :=
354435
by { dsimp [δ, σ], simp only [←X.map_comp, simplex_category.σ_comp_σ H] }

0 commit comments

Comments
 (0)