Skip to content

Commit 1078957

Browse files
joelrioujoelriou
committed
fix
1 parent 9d4ae88 commit 1078957

File tree

1 file changed

+4
-18
lines changed

1 file changed

+4
-18
lines changed

‎Mathlib/CategoryTheory/Triangulated/TStructure/TruncLTGE.lean‎

Lines changed: 4 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,6 @@ namespace TStructure
3636

3737
variable (t : TStructure C)
3838

39-
set_option backward.isDefEq.respectTransparency false in
4039
/-- Two morphisms `T ⟶ T'` between distinguished triangles must coincide when
4140
they coincide on the middle object, and there are integers `a ≤ b` such that
4241
for a t-structure, we have `T.obj₁ ≤ a` and `T'.obj₃ ≥ b`. -/
@@ -212,7 +211,6 @@ is the `< n`-truncation functor. See also the natural transformation `truncLTι`
212211
noncomputable def truncLT (n : ℤ) : C ⥤ C :=
213212
TruncAux.triangleFunctor t n ⋙ Triangle.π₁
214213

215-
set_option backward.isDefEq.respectTransparency false in
216214
instance (n : ℤ) : (t.truncLT n).Additive where
217215
map_add {_ _ _ _} := by
218216
dsimp only [truncLT, Functor.comp_map]
@@ -229,7 +227,6 @@ is the `≥ n`-truncation functor. See also the natural transformation `truncGE
229227
noncomputable def truncGE (n : ℤ) : C ⥤ C :=
230228
TruncAux.triangleFunctor t n ⋙ Triangle.π₃
231229

232-
set_option backward.isDefEq.respectTransparency false in
233230
instance (n : ℤ) : (t.truncGE n).Additive where
234231
map_add {_ _ _ _} := by
235232
dsimp only [truncGE, Functor.comp_map]
@@ -305,18 +302,15 @@ lemma truncGEδLT_comp_truncLTι_app (n : ℤ) (X : C) :
305302
(t.truncGEδLT n).app X ≫ ((t.truncLTι n).app X)⟦(1 : ℤ)⟧' = 0 :=
306303
comp_distTriang_mor_zero₃₁ _ (t.triangleLTGE_distinguished n X)
307304

308-
set_option backward.isDefEq.respectTransparency false in
309305
@[reassoc (attr := simp)]
310306
lemma truncLTι_comp_truncGEπ (n : ℤ) :
311307
t.truncLTι n ≫ t.truncGEπ n = 0 := by
312308
cat_disch
313309

314-
set_option backward.isDefEq.respectTransparency false in
315310
@[reassoc (attr := simp)]
316311
lemma truncGEπ_comp_truncGEδLT (n : ℤ) :
317312
t.truncGEπ n ≫ t.truncGEδLT n = 0 := by cat_disch
318313

319-
set_option backward.isDefEq.respectTransparency false in
320314
@[reassoc (attr := simp)]
321315
lemma truncGEδLT_comp_truncLTι (n : ℤ) :
322316
t.truncGEδLT n ≫ Functor.whiskerRight (t.truncLTι n) (shiftFunctor C (1 : ℤ)) = 0 := by
@@ -337,7 +331,6 @@ lemma natTransTruncLTOfLE_ι_app (a b : ℤ) (h : a ≤ b) (X : C) :
337331
(t.natTransTruncLTOfLE a b h).app X ≫ (t.truncLTι b).app X = (t.truncLTι a).app X := by
338332
simpa using ((TruncAux.triangleFunctorNatTransOfLE t a b h).app X).comm₁.symm
339333

340-
set_option backward.isDefEq.respectTransparency false in
341334
@[reassoc (attr := simp)]
342335
lemma natTransTruncLTOfLE_ι (a b : ℤ) (h : a ≤ b) :
343336
t.natTransTruncLTOfLE a b h ≫ t.truncLTι b = t.truncLTι a := by
@@ -363,7 +356,6 @@ lemma truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE (a b : ℤ) (h : a ≤ b
363356
ext X
364357
exact t.truncGEδLT_comp_natTransTruncLTOfLE_app a b h X
365358

366-
set_option backward.isDefEq.respectTransparency false in
367359
@[reassoc (attr := simp)]
368360
lemma π_natTransTruncGEOfLE (a b : ℤ) (h : a ≤ b) :
369361
t.truncGEπ a ≫ t.natTransTruncGEOfLE a b h = t.truncGEπ b := by
@@ -372,12 +364,10 @@ lemma π_natTransTruncGEOfLE (a b : ℤ) (h : a ≤ b) :
372364
/-- The natural transformation `t.triangleLTGE a ⟶ t.triangleLTGE b`
373365
when `a ≤ b`. -/
374366
noncomputable def natTransTriangleLTGEOfLE (a b : ℤ) (h : a ≤ b) :
375-
t.triangleLTGE a ⟶ t.triangleLTGE b := by
376-
refine Triangle.functorHomMk' (t.natTransTruncLTOfLE a b h) (𝟙 _)
377-
((t.natTransTruncGEOfLE a b h)) ?_ ?_ ?_
378-
· simp
379-
· simp
380-
· exact t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE a b h
367+
t.triangleLTGE a ⟶ t.triangleLTGE b :=
368+
Triangle.functorHomMk' (t.natTransTruncLTOfLE a b h) (𝟙 _)
369+
((t.natTransTruncGEOfLE a b h)) (by simp) (by simp)
370+
(t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE a b h)
381371

382372
@[simp]
383373
lemma natTransTriangleLTGEOfLE_refl (a : ℤ) :
@@ -441,7 +431,6 @@ instance (n : ℤ) : t.IsLE (0 : C) n := t.isLE_of_isZero (isZero_zero C) n
441431

442432
instance (n : ℤ) : t.IsGE (0 : C) n := t.isGE_of_isZero (isZero_zero C) n
443433

444-
set_option backward.isDefEq.respectTransparency false in
445434
lemma isLE_iff_isIso_truncLTι_app (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X : C) :
446435
t.IsLE X n₀ ↔ IsIso (((t.truncLTι n₁)).app X) := by
447436
subst h
@@ -460,7 +449,6 @@ lemma isLE_iff_isIso_truncLTι_app (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) (X :
460449
rw [this]
461450
infer_instance
462451

463-
set_option backward.isDefEq.respectTransparency false in
464452
lemma isGE_iff_isIso_truncGEπ_app (n : ℤ) (X : C) :
465453
t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X) := by
466454
constructor
@@ -531,13 +519,11 @@ lemma to_truncLT_obj_ext {n : ℤ} {Y : C} {X : C}
531519
(by dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia)))
532520
rw [hg, hg', zero_comp]
533521

534-
set_option backward.isDefEq.respectTransparency false in
535522
@[reassoc]
536523
lemma truncLT_map_truncLTι_app (n : ℤ) (X : C) :
537524
(t.truncLT n).map ((t.truncLTι n).app X) = (t.truncLTι n).app ((t.truncLT n).obj X) :=
538525
t.to_truncLT_obj_ext (by simp)
539526

540-
set_option backward.isDefEq.respectTransparency false in
541527
@[reassoc]
542528
lemma truncGE_map_truncGEπ_app (n : ℤ) (X : C) :
543529
(t.truncGE n).map ((t.truncGEπ n).app X) = (t.truncGEπ n).app ((t.truncGE n).obj X) :=

0 commit comments

Comments
 (0)