diff --git a/Mathlib/Algebra/Homology/HomotopyCategory.lean b/Mathlib/Algebra/Homology/HomotopyCategory.lean index 8baf39506dd33..65409ca66e334 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory.lean @@ -77,10 +77,13 @@ instance : (quotient V c).Additive where open ZeroObject --- TODO upgrade this to `HasZeroObject`, presumably for any `quotient`. instance [HasZeroObject V] : Inhabited (HomotopyCategory V c) := ⟨(quotient V c).obj 0⟩ +instance [HasZeroObject V] : HasZeroObject (HomotopyCategory V c) := + ⟨(quotient V c).obj 0, by + rw [IsZero.iff_id_eq_zero, ← (quotient V c).map_id, id_zero, Functor.map_zero]⟩ + variable {V c} -- porting note: removed @[simp] attribute because it hinders the automatic application of the @@ -151,6 +154,15 @@ def homotopyEquivOfIso {C D : HomologicalComplex V c} (by rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]) #align homotopy_category.homotopy_equiv_of_iso HomotopyCategory.homotopyEquivOfIso +lemma isZero_quotient_obj_iff (C : HomologicalComplex V c) : + IsZero ((quotient _ _).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0) := by + rw [IsZero.iff_id_eq_zero] + constructor + · intro h + exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩ + · rintro ⟨h⟩ + simpa using (eq_of_homotopy _ _ h) + variable (V c) section diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean index 9facc663e86fb..3fadfdc8855a5 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean @@ -556,6 +556,7 @@ lemma δ_neg_one_cochain (z : Cochain F G (-1)) : rw [Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p-1) p by simp) (show (ComplexShape.up ℤ).Rel p (p+1) by simp)] abel + end HomComplex variable (F G) @@ -628,6 +629,10 @@ lemma coe_neg (z : Cocycle F G n) : lemma coe_smul (z : Cocycle F G n) (x : R) : (↑(x • z) : Cochain F G n) = x • (z : Cochain F G n) := rfl +@[simp] +lemma coe_units_smul (z : Cocycle F G n) (x : Rˣ) : + (↑(x • z) : Cochain F G n) = x • (z : Cochain F G n) := rfl + @[simp] lemma coe_sub (z₁ z₂ : Cocycle F G n) : (↑(z₁ - z₂) : Cochain F G n) = (z₁ : Cochain F G n) - (z₂ : Cochain F G n) := rfl @@ -703,10 +708,39 @@ def diff : Cocycle K K 1 := end Cocycle -namespace Cochain - variable {F G} +@[simp] +lemma δ_comp_zero_cocycle {n : ℤ} (z₁ : Cochain F G n) (z₂ : Cocycle G K 0) (m : ℤ) : + δ n m (z₁.comp z₂.1 (add_zero n)) = + (δ n m z₁).comp z₂.1 (add_zero m) := by + by_cases hnm : n + 1 = m + · simp [δ_comp_zero_cochain _ _ _ hnm] + · simp [δ_shape _ _ hnm] + +@[simp] +lemma δ_comp_ofHom {n : ℤ} (z₁ : Cochain F G n) (f : G ⟶ K) (m : ℤ) : + δ n m (z₁.comp (Cochain.ofHom f) (add_zero n)) = + (δ n m z₁).comp (Cochain.ofHom f) (add_zero m) := by + rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle] + + +@[simp] +lemma δ_zero_cocycle_comp {n : ℤ} (z₁ : Cocycle F G 0) (z₂ : Cochain G K n) (m : ℤ) : + δ n m (z₁.1.comp z₂ (zero_add n)) = + z₁.1.comp (δ n m z₂) (zero_add m) := by + by_cases hnm : n + 1 = m + · simp [δ_zero_cochain_comp _ _ _ hnm] + · simp [δ_shape _ _ hnm] + +@[simp] +lemma δ_ofHom_comp {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) : + δ n m ((Cochain.ofHom f).comp z (zero_add n)) = + (Cochain.ofHom f).comp (δ n m z) (zero_add m) := by + rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp] + +namespace Cochain + /-- Given two morphisms of complexes `φ₁ φ₂ : F ⟶ G`, the datum of an homotopy between `φ₁` and `φ₂` is equivalent to the datum of a `1`-cochain `z` such that `δ (-1) 0 z` is the difference of the zero cochains associated to `φ₂` and `φ₁`. -/ diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean index d0103b2dbd1c4..9828d433230c6 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean @@ -400,7 +400,7 @@ lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add, add_right_inj, smul_smul] congr 1 - rw [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc, + simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul] · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by linarith) rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero] diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean b/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean index 8728fcb936bc2..8f2441b963537 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean @@ -105,9 +105,13 @@ instance (n : ℤ) : variable {C} +@[simp] +lemma shiftFunctor_obj_X' (K : CochainComplex C ℤ) (n p : ℤ) : + ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X p = K.X (p + n) := rfl + @[simp] lemma shiftFunctor_map_f' {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n p : ℤ) : - ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p+n) := rfl + ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ).f p = φ.f (p + n) := rfl @[simp] lemma shiftFunctor_obj_d' (K : CochainComplex C ℤ) (n i j : ℤ) : @@ -283,4 +287,9 @@ noncomputable instance commShiftQuotient : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).CommShift ℤ := Quotient.functor_commShift (homotopic C (ComplexShape.up ℤ)) ℤ +instance (n : ℤ) : (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).Additive := by + have : ((quotient C (ComplexShape.up ℤ) ⋙ shiftFunctor _ n)).Additive := + Functor.additive_of_iso ((quotient C (ComplexShape.up ℤ)).commShiftIso n) + apply Functor.additive_of_full_essSurj_comp (quotient _ _ ) + end HomotopyCategory diff --git a/Mathlib/CategoryTheory/Triangulated/Basic.lean b/Mathlib/CategoryTheory/Triangulated/Basic.lean index c3eb9756dd927..f6bec1774ea29 100644 --- a/Mathlib/CategoryTheory/Triangulated/Basic.lean +++ b/Mathlib/CategoryTheory/Triangulated/Basic.lean @@ -162,6 +162,23 @@ lemma Triangle.hom_ext {A B : Triangle C} (f g : A ⟶ B) (h₁ : f.hom₁ = g.hom₁) (h₂ : f.hom₂ = g.hom₂) (h₃ : f.hom₃ = g.hom₃) : f = g := TriangleMorphism.ext _ _ h₁ h₂ h₃ +@[simp] +lemma id_hom₁ (A : Triangle C) : TriangleMorphism.hom₁ (𝟙 A) = 𝟙 _ := rfl +@[simp] +lemma id_hom₂ (A : Triangle C) : TriangleMorphism.hom₂ (𝟙 A) = 𝟙 _ := rfl +@[simp] +lemma id_hom₃ (A : Triangle C) : TriangleMorphism.hom₃ (𝟙 A) = 𝟙 _ := rfl + +@[simp, reassoc] +lemma comp_hom₁ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : + (f ≫ g).hom₁ = f.hom₁ ≫ g.hom₁ := rfl +@[simp, reassoc] +lemma comp_hom₂ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : + (f ≫ g).hom₂ = f.hom₂ ≫ g.hom₂ := rfl +@[simp, reassoc] +lemma comp_hom₃ {X Y Z : Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) : + (f ≫ g).hom₃ = f.hom₃ ≫ g.hom₃ := rfl + @[simps] def Triangle.homMk (A B : Triangle C) (hom₁ : A.obj₁ ⟶ B.obj₁) (hom₂ : A.obj₂ ⟶ B.obj₂) (hom₃ : A.obj₃ ⟶ B.obj₃) @@ -200,6 +217,26 @@ lemma Triangle.isIso_of_isIsos {A B : Triangle C} (f : A ⟶ B) (by simp) (by simp) (by simp) exact (inferInstance : IsIso e.hom) +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) : + e.hom.hom₁ ≫ e.inv.hom₁ = 𝟙 _ := by rw [← comp_hom₁, e.hom_inv_id, id_hom₁] +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) : + e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 _ := by rw [← comp_hom₂, e.hom_inv_id, id_hom₂] +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) : + e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 _ := by rw [← comp_hom₃, e.hom_inv_id, id_hom₃] + +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) : + e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 _ := by rw [← comp_hom₁, e.inv_hom_id, id_hom₁] +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) : + e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 _ := by rw [← comp_hom₂, e.inv_hom_id, id_hom₂] +@[reassoc (attr := simp)] +lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₃ {A B : Triangle C} (e : A ≅ B) : + e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 _ := by rw [← comp_hom₃, e.inv_hom_id, id_hom₃] + lemma Triangle.eqToHom_hom₁ {A B : Triangle C} (h : A = B) : (eqToHom h).hom₁ = eqToHom (by subst h; rfl) := by subst h; rfl lemma Triangle.eqToHom_hom₂ {A B : Triangle C} (h : A = B) :