From 3328b729eadc3dc3f30f544db44f098e6b136c83 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 13:13:14 +0200 Subject: [PATCH 1/5] wip --- Mathlib.lean | 1 + Mathlib/Algebra/Homology/ComplexShape.lean | 7 + Mathlib/Algebra/Homology/HomotopyCofiber.lean | 19 +- Mathlib/Algebra/Homology/HomotopyFiber.lean | 162 ++++++++++++++++++ 4 files changed, 188 insertions(+), 1 deletion(-) create mode 100644 Mathlib/Algebra/Homology/HomotopyFiber.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3435a680bbbdec..0c5f6f54b148fb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -643,6 +643,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors public import Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject public import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated public import Mathlib.Algebra.Homology.HomotopyCofiber +public import Mathlib.Algebra.Homology.HomotopyFiber public import Mathlib.Algebra.Homology.ImageToKernel public import Mathlib.Algebra.Homology.LeftResolution.Basic public import Mathlib.Algebra.Homology.LeftResolution.Reduced diff --git a/Mathlib/Algebra/Homology/ComplexShape.lean b/Mathlib/Algebra/Homology/ComplexShape.lean index 66899bc1022026..7db47640aa55dd 100644 --- a/Mathlib/Algebra/Homology/ComplexShape.lean +++ b/Mathlib/Algebra/Homology/ComplexShape.lean @@ -94,6 +94,13 @@ def symm (c : ComplexShape ι) : ComplexShape ι where next_eq w w' := c.prev_eq w w' prev_eq w w' := c.next_eq w w' +/-- If `c : ComplexShape α` is such that `c.Rel` is decidable, it is also the +case of `c.symm.Rel`. -/ +@[implicit_reducible] +def decidableRelSymm {α : Type*} (c : ComplexShape α) [DecidableRel c.Rel] : + DecidableRel c.symm.Rel := + fun a b ↦ decidable_of_iff (c.Rel b a) Iff.rfl + @[simp] theorem symm_symm (c : ComplexShape ι) : c.symm.symm = c := rfl diff --git a/Mathlib/Algebra/Homology/HomotopyCofiber.lean b/Mathlib/Algebra/Homology/HomotopyCofiber.lean index 099b803017cf36..da1b6d6fafc5a4 100644 --- a/Mathlib/Algebra/Homology/HomotopyCofiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyCofiber.lean @@ -79,6 +79,16 @@ noncomputable def XIso (i : ι) (hi : ¬ c.Rel i (c.next i)) : X φ i ≅ G.X i := eqToIso (dif_neg hi) +lemma isZero_X (i : ι) (hG : IsZero (G.X i)) + (hF : ∀ (j : ι), c.Rel i j → IsZero (F.X j)) : + IsZero (X φ i) := by + by_cases h : c.Rel i (c.next i) + · haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ h + refine IsZero.of_iso ?_ (XIsoBiprod φ _ _ h) + simp only [biprod_isZero_iff] + exact ⟨hF _ h, hG⟩ + · exact hG.of_iso (XIso φ i h) + /-- The second projection `(homotopyCofiber φ).X i ⟶ G.X i`. -/ noncomputable def sndX (i : ι) : X φ i ⟶ G.X i := if hi : c.Rel i (c.next i) @@ -376,7 +386,13 @@ section variable (K) variable [∀ i, HasBinaryBiproduct (K.X i) (K.X i)] - [HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))] + +/-- Given a homological complex `K`, this is the property that the morphism +`K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K` has a cofiber, which allows +to define `K.cylinder` as this cofiber. -/ +abbrev HasCylinder : Prop := HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K)) + +variable [K.HasCylinder] /-- The cylinder object of a homological complex `K` is the homotopy cofiber of the morphism `biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K`. -/ @@ -525,6 +541,7 @@ noncomputable def πCompι₀Homotopy : Homotopy (π K ≫ ι₀ K) (𝟙 K.cyli (πCompι₀Homotopy.nullHomotopy K)) /-- The homotopy equivalence between `K.cylinder` and `K`. -/ +@[simps] noncomputable def homotopyEquiv : HomotopyEquiv K.cylinder K where hom := π K inv := ι₀ K diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean new file mode 100644 index 00000000000000..1177fc24304a14 --- /dev/null +++ b/Mathlib/Algebra/Homology/HomotopyFiber.lean @@ -0,0 +1,162 @@ +/- +Copyright (c) 2023 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.Algebra.Homology.HomotopyCofiber +public import Mathlib.Algebra.Homology.Opposite + +/-! The homotopy fiber of a morphism of homological complexes + +In this file, we construct the homotopy fiber of a morphism `φ : F ⟶ G` +between homological complexes. Moreover, we dualise the definition +of the cylinder (which is a particular case of a homotopy cofiber) +in order to define the path object of a homological complex. + +-/ + +@[expose] public section + +open CategoryTheory Category Limits Preadditive Opposite + +variable {C : Type*} [Category* C] [Preadditive C] + +namespace HomologicalComplex + +attribute [local instance] ComplexShape.decidableRelSymm + +variable {α : Type*} {c : ComplexShape α} {F G K : HomologicalComplex C c} (φ : F ⟶ G) + +variable [DecidableRel c.Rel] + +section + +/-- A morphism of homological complexes `φ : F ⟶ G` has a homotopy fiber if for all +indices `i` and `j` such that `c.Rel i j`, the binary biproduct `F.X i ⊞ G.X j` exists. -/ +class HasHomotopyFiber (φ : F ⟶ G) : Prop where + hasBinaryBiproduct (φ) (i j : α) (hij : c.Rel i j) : HasBinaryBiproduct (G.X i) (F.X j) + +instance [HasBinaryBiproducts C] : HasHomotopyFiber φ where + hasBinaryBiproduct _ _ _ := inferInstance + +variable [HasHomotopyFiber φ] [DecidableRel c.Rel] + +instance : HasHomotopyCofiber ((opFunctor C c).map φ.op) where + hasBinaryBiproduct i j hij := by + have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij + dsimp + infer_instance + +/-- The homotopy fiber of a morphism between homological complexes. -/ +noncomputable def homotopyFiber : HomologicalComplex C c := + (unopFunctor C c.symm).obj (op (homotopyCofiber ((opFunctor C c).map φ.op))) + +end + +variable (K) [∀ i, HasBinaryBiproduct (K.X i) (K.X i)] + +instance (i : α) : HasBinaryBiproduct (K.op.X i) (K.op.X i) := by + dsimp; infer_instance + +/-- The property that a homological complex `K` has a path object, +i.e. that the morphism `K ⟶ K ⊞ K` induced by `𝟙 K` and `-𝟙 K` +has a homotopy fiber. -/ +abbrev HasPathObject := HasHomotopyFiber (biprod.desc (𝟙 K) (-𝟙 K)) + +instance [K.HasPathObject] : + HasHomotopyCofiber (biprod.lift (𝟙 K.op) (-𝟙 K.op)) where + hasBinaryBiproduct i j hij := by + have := HasHomotopyFiber.hasBinaryBiproduct (biprod.desc (𝟙 K) (-𝟙 K)) j i hij + exact hasBinaryBiproduct_of_iso (Iso.refl _ : op (K.X j) ≅ K.op.X j) + (show op ((K ⊞ K).X i) ≅ (K.op ⊞ K.op).X i from + ((eval _ _ i).mapBiprod K K).op.symm ≪≫ biprod.opIso _ _ ≪≫ + ((eval _ _ i).mapBiprod K.op K.op).symm) + +variable [K.HasPathObject] + +/-- The path object of a homological complex is defined here by dualizing +the cylinder object of `K.op`. -/ +@[no_expose] +noncomputable def pathObject := (unopFunctor C c.symm).obj (op K.op.cylinder) + +namespace pathObject + +lemma isZero_X (i : α) (h₁ : IsZero (K.X i)) (h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)) : + IsZero (K.pathObject.X i) := by + apply IsZero.unop + dsimp [pathObject] + refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj)) + exact IsZero.of_iso (by simpa using h₁.op) + ((eval Cᵒᵖ c.symm i).mapBiprod K.op K.op) + +/-- The first projection `K.pathObject ⟶ K`. -/ +@[no_expose] +noncomputable def π₀ : K.pathObject ⟶ K := + (unopFunctor C c.symm).map (cylinder.ι₀ K.op).op + +/-- The second projection `K.pathObject ⟶ K`. -/ +@[no_expose] +noncomputable def π₁ : K.pathObject ⟶ K := + (unopFunctor C c.symm).map (cylinder.ι₁ K.op).op + +/-- The inclusion `K ⟶ K.pathObject`. -/ +@[no_expose] +noncomputable def ι : K ⟶ K.pathObject := + (unopFunctor C c.symm).map (cylinder.π K.op).op + +@[reassoc (attr := simp)] +lemma π₀_ι : ι K ≫ π₀ K = 𝟙 K := + Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_π K.op)) + +@[reassoc (attr := simp)] +lemma π₁_ι : ι K ≫ π₁ K = 𝟙 K := + Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_π K.op)) + +/-- The homotopy between `π₀ K ≫ ι K` and `𝟙 K.pathObject`. -/ +@[no_expose] +noncomputable def π₀CompιHomotopy (hc : ∀ (i : α), ∃ j, c.Rel i j) : + Homotopy (π₀ K ≫ ι K) (𝟙 K.pathObject) := + (cylinder.πCompι₀Homotopy K.op hc).unop + +/-- The homotopy equivalence between `K` and `K.pathObject`. -/ +@[simps] +noncomputable def homotopyEquiv (hc : ∀ (i : α), ∃ j, c.Rel i j) : + HomotopyEquiv K K.pathObject where + hom := ι K + inv := π₀ K + homotopyHomInvId := Homotopy.ofEq (by simp) + homotopyInvHomId := π₀CompιHomotopy K hc + +/-- The homotopy between `pathObject.ι₀ K` and `pathObject.ι₁ K`. -/ +@[no_expose] +noncomputable def homotopy₀₁ (hc : ∀ (i : α), ∃ j, c.Rel i j) : Homotopy (π₀ K) (π₁ K) := + (cylinder.homotopy₀₁ K.op hc).unop + +section + +variable {K} (φ₀ φ₁ : F ⟶ K) (h : Homotopy φ₀ φ₁) + +/-- The morphism `F ⟶ K.pathObject` that is induced by two morphisms `φ₀ φ₁ : F ⟶ K` +and a homotopy `h : Homotopy φ₀ φ₁`. -/ +@[no_expose] +noncomputable def lift : F ⟶ K.pathObject := + letI φ : K.op.cylinder ⟶ (opFunctor C c).obj (op F) := + cylinder.desc ((opFunctor C c).map φ₀.op) + ((opFunctor C c).map φ₁.op) h.op + (unopFunctor C c.symm).map φ.op + +@[reassoc (attr := simp)] +lemma lift_π₀ : lift φ₀ φ₁ h ≫ π₀ K = φ₀ := + Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₀_desc _ _ _)) + +@[reassoc (attr := simp)] +lemma lift_π₁ : lift φ₀ φ₁ h ≫ π₁ K = φ₁ := + Quiver.Hom.op_inj ((opFunctor C c).map_injective (cylinder.ι₁_desc _ _ _)) + +end + +end pathObject + +end HomologicalComplex From e3665cc2684da96c99b88363213e2e52c51c4a38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 13:14:35 +0200 Subject: [PATCH 2/5] feat(CategoryTheory/Limits): biprod.opIso --- .../Limits/Shapes/BinaryBiproducts.lean | 120 +++++++++++++++++- 1 file changed, 118 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean index 71801d9d2248dc..c36ca080e3ea6b 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean @@ -35,7 +35,7 @@ noncomputable section universe w w' v u -open CategoryTheory Functor +open CategoryTheory Functor Opposite namespace CategoryTheory.Limits @@ -157,7 +157,7 @@ end BinaryBicones namespace BinaryBicone -variable {P Q : C} +variable {P P' Q Q' : C} /-- Extract the cone from a binary bicone. -/ def toCone (c : BinaryBicone P Q) : Cone (pair P Q) := @@ -250,6 +250,30 @@ def toBiconeIsColimit {X Y : C} (b : BinaryBicone X Y) : IsColimit b.toBicone.toCocone ≃ IsColimit b.toCocone := IsColimit.equivIsoColimit <| Cocone.ext (Iso.refl _) fun ⟨as⟩ => by cases as <;> simp +/-- Transport a binary bicone via isomorphisms. -/ +@[simps] +def ofIso (b : BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q') : + BinaryBicone P' Q' where + pt := b.pt + fst := b.fst ≫ eP.hom + snd := b.snd ≫ eQ.hom + inl := eP.inv ≫ b.inl + inr := eQ.inv ≫ b.inr + +/-- The opposite of a binary bicone. -/ +@[simps] +protected def op (b : BinaryBicone P Q) : + BinaryBicone (op P) (op Q) where + pt := Opposite.op b.pt + fst := b.inl.op + snd := b.inr.op + inl := b.fst.op + inr := b.snd.op + inl_fst := Quiver.Hom.unop_inj (by simp) + inr_fst := Quiver.Hom.unop_inj (by simp) + inl_snd := Quiver.Hom.unop_inj (by simp) + inr_snd := Quiver.Hom.unop_inj (by simp) + end BinaryBicone namespace Bicone @@ -297,6 +321,26 @@ structure BinaryBicone.IsBilimit {P Q : C} (b : BinaryBicone P Q) where attribute [inherit_doc BinaryBicone.IsBilimit] BinaryBicone.IsBilimit.isLimit BinaryBicone.IsBilimit.isColimit +/-- If a binary bicone for `P` and `Q` is bilimit, then the binary bicone for `P'` and `Q'` +obtained using isomorphisms `P ≅ P'` and `Q ≅ Q'` is also bilimit. -/ +def BinaryBicone.IsBilimit.ofIso {P Q P' Q' : C} {b : BinaryBicone P Q} (hb : b.IsBilimit) + (eP : P ≅ P') (eQ : Q ≅ Q') : + (b.ofIso eP eQ).IsBilimit where + isLimit := by + refine (IsLimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isLimit + exact BinaryFan.ext (Iso.refl _) (by simp [BinaryFan.fst]) + (by simp [BinaryFan.snd]) + isColimit := by + refine (IsColimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isColimit + exact BinaryCofan.ext (Iso.refl _) (by simp [BinaryCofan.inl]) + (by simp [BinaryCofan.inr]) + +/-- The opposite of a bilimit binary bicone is bilimit. -/ +protected def BinaryBicone.IsBilimit.op {P Q : C} {b : BinaryBicone P Q} (h : b.IsBilimit) : + b.op.IsBilimit where + isLimit := BinaryCofan.IsColimit.op h.isColimit + isColimit := BinaryFan.IsLimit.op h.isLimit + /-- A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit. -/ def BinaryBicone.toBiconeIsBilimit {X Y : C} (b : BinaryBicone X Y) : b.toBicone.IsBilimit ≃ b.IsBilimit where @@ -319,9 +363,26 @@ structure BinaryBiproductData (P Q : C) where bicone : BinaryBicone P Q isBilimit : bicone.IsBilimit +initialize_simps_projections BinaryBiproductData (-isBilimit) + attribute [inherit_doc BinaryBiproductData] BinaryBiproductData.bicone BinaryBiproductData.isBilimit +/-- Transport a binary bicone data via isomorphisms. -/ +@[simps] +def BinaryBiproductData.ofIso {P Q P' Q' : C} (d : BinaryBiproductData P Q) + (eP : P ≅ P') (eQ : Q ≅ Q') : + BinaryBiproductData P' Q' where + bicone := d.bicone.ofIso eP eQ + isBilimit := d.isBilimit.ofIso _ _ + +/-- The opposite of a binary biproduct data. -/ +@[simps] +protected def BinaryBiproductData.op {P Q : C} (d : BinaryBiproductData P Q) : + BinaryBiproductData (op P) (op Q) where + bicone := d.bicone.op + isBilimit := d.isBilimit.op + /-- `HasBinaryBiproduct P Q` expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram `pair P Q`. -/ class HasBinaryBiproduct (P Q : C) : Prop where mk' :: @@ -357,6 +418,15 @@ def BinaryBiproduct.isColimit (P Q : C) [HasBinaryBiproduct P Q] : IsColimit (BinaryBiproduct.bicone P Q).toCocone := (getBinaryBiproductData P Q).isBilimit.isColimit +lemma hasBinaryBiproduct_of_iso {P Q P' Q' : C} [HasBinaryBiproduct P Q] + (eP : P ≅ P') (eQ : Q ≅ Q') : + HasBinaryBiproduct P' Q' where + exists_binary_biproduct := ⟨(getBinaryBiproductData P Q).ofIso eP eQ⟩ + +instance {P Q : C} [HasBinaryBiproduct P Q] : + HasBinaryBiproduct (op P) (op Q) where + exists_binary_biproduct := ⟨(getBinaryBiproductData P Q).op⟩ + section variable (C) @@ -378,6 +448,10 @@ theorem hasBinaryBiproducts_of_finite_biproducts [HasFiniteBiproducts C] : HasBi { bicone := (biproduct.bicone (pairFunction P Q)).toBinaryBicone isBilimit := (Bicone.toBinaryBiconeIsBilimit _).symm (biproduct.isBilimit _) } } +instance [HasBinaryBiproducts C] : HasBinaryBiproducts Cᵒᵖ where + has_binary_biproduct X Y := + inferInstanceAs (HasBinaryBiproduct (op X.unop) (op Y.unop)) + end variable {P Q : C} @@ -826,6 +900,44 @@ theorem biprod.inrCokernelCofork_π : Cofork.π (biprod.inrCokernelCofork X Y) = def biprod.isCokernelInrCokernelFork : IsColimit (biprod.inrCokernelCofork X Y) := BinaryBicone.isColimitInrCokernelCofork (BinaryBiproduct.isColimit _ _) +section + +variable (P Q) [HasBinaryBiproduct P Q] + +/-- The isomorphism `op (P ⊞ Q) ≅ op P ⊞ op Q`. -/ +def biprod.opIso : op (P ⊞ Q) ≅ op P ⊞ op Q := + biprod.uniqueUpToIso _ _ (getBinaryBiproductData P Q).op.isBilimit + +@[reassoc (attr := simp)] +lemma biprod.opIso_hom_fst : (opIso P Q).hom ≫ fst = inl.op := lift_fst _ _ + +@[reassoc (attr := simp)] +lemma biprod.opIso_hom_snd : (opIso P Q).hom ≫ snd = inr.op := lift_snd _ _ + +@[reassoc (attr := simp)] +lemma biprod.inl_opIso_inv : inl ≫ (opIso P Q).inv = fst.op := inl_desc _ _ + +@[reassoc (attr := simp)] +lemma biprod.inr_opIso_inv : inr ≫ (opIso P Q).inv = snd.op := inr_desc _ _ + +@[reassoc (attr := simp)] +lemma biprod.fst_op_opIso_hom : fst.op ≫ (opIso P Q).hom = inl := by + ext <;> simp [← op_comp] + +@[reassoc (attr := simp)] +lemma biprod.snd_op_opIso_hom : snd.op ≫ (opIso P Q).hom = inr := by + ext <;> simp [← op_comp] + +@[reassoc (attr := simp)] +lemma biprod.opIso_inv_inl_op : (opIso P Q).inv ≫ inl.op = fst := by + ext <;> simp [← op_comp] + +@[reassoc (attr := simp)] +lemma biprod.opIso_inv_inr_op : (opIso P Q).inv ≫ inr.op = snd := by + ext <;> simp [← op_comp] + +end + end HasBinaryBiproduct variable {X Y : C} [HasBinaryBiproduct X Y] @@ -972,6 +1084,8 @@ end Limits open CategoryTheory.Limits +section + -- TODO: -- If someone is interested, they could provide the constructions: -- HasBinaryBiproducts ↔ HasFiniteBiproducts @@ -1016,4 +1130,6 @@ theorem isIso_right_of_isIso_biprod_map {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z infer_instance isIso_left_of_isIso_biprod_map g f +end + end CategoryTheory From f4f9a1824b751062fadc288d33c9406a86fcc4da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 13:20:04 +0200 Subject: [PATCH 3/5] feat(Algebra/Homology): the homotopy fiber --- Mathlib/Algebra/Homology/Opposite.lean | 39 ++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean index 10e5d2d49f745b..6810dd4cd77228 100644 --- a/Mathlib/Algebra/Homology/Opposite.lean +++ b/Mathlib/Algebra/Homology/Opposite.lean @@ -160,6 +160,9 @@ def opEquivalence : (HomologicalComplex V c)ᵒᵖ ≌ HomologicalComplex Vᵒ opFunctor_map_f, Hom.isoOfComponents_hom_f] exact Category.comp_id _ +instance : (opFunctor V c).IsEquivalence := (opEquivalence V c).isEquivalence_functor +instance : (opInverse V c).IsEquivalence := (opEquivalence V c).isEquivalence_inverse + set_option backward.isDefEq.respectTransparency false in /-- Auxiliary definition for `unopEquivalence`. -/ @[simps] @@ -211,6 +214,9 @@ def unopEquivalence : (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≌ HomologicalComple simp only [comp_f] exact Category.comp_id _ +instance : (unopFunctor V c).IsEquivalence := (unopEquivalence V c).isEquivalence_functor +instance : (unopInverse V c).IsEquivalence := (unopEquivalence V c).isEquivalence_inverse + instance (K : HomologicalComplex V c) (i : ι) [K.HasHomology i] : K.op.HasHomology i := inferInstanceAs <| (K.sc i).op.HasHomology @@ -435,3 +441,36 @@ instance unopFunctor_additive : (@unopFunctor ι V _ c _).Additive where end end HomologicalComplex + +namespace Homotopy + +open HomologicalComplex + +variable {V : Type*} [Category* V] {ι : Type*} {c : ComplexShape ι} [Preadditive V] + +/-- The opposite of a homotopy between morphisms of homological complexes. -/ +@[simps] +def op {F G : HomologicalComplex V c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) : + Homotopy ((opFunctor V c).map φ₁.op) ((opFunctor V c).map φ₂.op) where + hom i j := (h.hom j i).op + zero i j hij := Quiver.Hom.unop_inj (h.zero _ _ hij) + comm n := Quiver.Hom.unop_inj (by + dsimp + rw [h.comm n] + nth_rw 2 [add_comm] + rfl) + +/-- The homotopy between morphisms of homological complexes that is deduced +from a homotopy in the opposite category. -/ +@[simps] +def unop {F G : HomologicalComplex Vᵒᵖ c} {φ₁ φ₂ : F ⟶ G} (h : Homotopy φ₁ φ₂) : + Homotopy ((unopFunctor V c).map φ₁.op) ((unopFunctor V c).map φ₂.op) where + hom i j := (h.hom j i).unop + zero i j hij := Quiver.Hom.op_inj (h.zero _ _ hij) + comm n := Quiver.Hom.op_inj (by + dsimp + rw [h.comm n] + nth_rw 2 [add_comm] + rfl) + +end Homotopy From a70792e231b45dbb6fb6f078ebd48b23d50f9298 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Thu, 7 May 2026 22:16:33 +0200 Subject: [PATCH 4/5] Update Mathlib/Algebra/Homology/HomotopyFiber.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/Algebra/Homology/HomotopyFiber.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean index 1177fc24304a14..d2b3a3e92d4d5e 100644 --- a/Mathlib/Algebra/Homology/HomotopyFiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyFiber.lean @@ -8,7 +8,8 @@ module public import Mathlib.Algebra.Homology.HomotopyCofiber public import Mathlib.Algebra.Homology.Opposite -/-! The homotopy fiber of a morphism of homological complexes +/-! +# The homotopy fiber of a morphism of homological complexes In this file, we construct the homotopy fiber of a morphism `φ : F ⟶ G` between homological complexes. Moreover, we dualise the definition From 86804b4ee6d0a71aca15441a37d36bfc2c2bc12a Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Thu, 7 May 2026 20:17:17 +0000 Subject: [PATCH 5/5] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Algebra/Homology/HomotopyFiber.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/HomotopyFiber.lean b/Mathlib/Algebra/Homology/HomotopyFiber.lean index d2b3a3e92d4d5e..e5efe421ca2e24 100644 --- a/Mathlib/Algebra/Homology/HomotopyFiber.lean +++ b/Mathlib/Algebra/Homology/HomotopyFiber.lean @@ -8,7 +8,7 @@ module public import Mathlib.Algebra.Homology.HomotopyCofiber public import Mathlib.Algebra.Homology.Opposite -/-! +/-! # The homotopy fiber of a morphism of homological complexes In this file, we construct the homotopy fiber of a morphism `φ : F ⟶ G`