diff --git a/Mathlib.lean b/Mathlib.lean index 5bbd36285ce929..e9801ad51c351e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -312,6 +312,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated import Mathlib.Algebra.Homology.HomotopyCategory.Shift import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence +import Mathlib.Algebra.Homology.HomotopyCategory.ShortExact import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated import Mathlib.Algebra.Homology.HomotopyCofiber @@ -322,6 +323,7 @@ import Mathlib.Algebra.Homology.Localization import Mathlib.Algebra.Homology.ModuleCat import Mathlib.Algebra.Homology.Opposite import Mathlib.Algebra.Homology.QuasiIso +import Mathlib.Algebra.Homology.Refinements import Mathlib.Algebra.Homology.ShortComplex.Ab import Mathlib.Algebra.Homology.ShortComplex.Abelian import Mathlib.Algebra.Homology.ShortComplex.Basic diff --git a/Mathlib/Algebra/Homology/HomologySequenceLemmas.lean b/Mathlib/Algebra/Homology/HomologySequenceLemmas.lean index 8ffb3c98e2f884..3964e891d02359 100644 --- a/Mathlib/Algebra/Homology/HomologySequenceLemmas.lean +++ b/Mathlib/Algebra/Homology/HomologySequenceLemmas.lean @@ -72,7 +72,7 @@ noncomputable def composableArrows₅ (i j : ι) (hij : c.Rel i j) : ComposableA mk₅ (homologyMap S₁.f i) (homologyMap S₁.g i) (hS₁.δ i j hij) (homologyMap S₁.f j) (homologyMap S₁.g j) -lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j): +lemma composableArrows₅_exact (i j : ι) (hij : c.Rel i j) : (composableArrows₅ hS₁ i j hij).Exact := exact_of_δ₀ (hS₁.homology_exact₂ i).exact_toComposableArrows (exact_of_δ₀ (hS₁.homology_exact₃ i j hij).exact_toComposableArrows diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean b/Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean index a210ec80c24cf5..ce44a12d846927 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean @@ -174,6 +174,17 @@ lemma ext_from_iff (i j : ℤ) (hij : j + 1 = i) {A : C} (f g : (mappingCone φ) · rintro ⟨h₁, h₂⟩ exact ext_from φ i j hij h₁ h₂ +lemma decomp_to {i : ℤ} {A : C} (f : A ⟶ (mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) : + ∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i), f = a ≫ (inl φ).v j i (by omega) + b ≫ (inr φ).f i := + ⟨f ≫ (fst φ).1.v i j hij, f ≫ (snd φ).v i i (add_zero i), + by apply ext_to φ i j hij <;> simp⟩ + +lemma decomp_from {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) : + ∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A), + f = (fst φ).1.v j i hij ≫ a + (snd φ).v j j (add_zero j) ≫ b := + ⟨(inl φ).v i j (by omega) ≫ f, (inr φ).f j ≫ f, + by apply ext_from φ i j hij <;> simp⟩ + lemma ext_cochain_to_iff (i j : ℤ) (hij : i + 1 = j) {K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain K (mappingCone φ) i} : γ₁ = γ₂ ↔ γ₁.comp (fst φ).1 hij = γ₂.comp (fst φ).1 hij ∧ diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean b/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean index 16a3bd8aef8812..dc10431f21fff5 100644 --- a/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean +++ b/Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean @@ -18,7 +18,7 @@ and `HomotopyCategory` namespaces. -/ -open CategoryTheory Category +open CategoryTheory Category ComplexShape Limits variable (C : Type*) [Category C] [Preadditive C] @@ -124,6 +124,34 @@ instance {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] : change IsIso (homologyMap φ _) infer_instance +variable (C) in +lemma homologyFunctor_shift (n : ℤ) : + (homologyFunctor C (ComplexShape.up ℤ) 0).shift n = + homologyFunctor C (ComplexShape.up ℤ) n := rfl + +@[reassoc] +lemma liftCycles_shift_homologyπ + (K : CochainComplex C ℤ) {A : C} {n i : ℤ} (f : A ⟶ (K⟦n⟧).X i) (j : ℤ) + (hj : (up ℤ).next i = j) (hf : f ≫ (K⟦n⟧).d i j = 0) (i' : ℤ) (hi' : n + i = i') (j' : ℤ) + (hj' : (up ℤ).next i' = j') : + (K⟦n⟧).liftCycles f j hj hf ≫ (K⟦n⟧).homologyπ i = + K.liftCycles (f ≫ (K.shiftFunctorObjXIso n i i' (by omega)).hom) j' hj' (by + simp only [next] at hj hj' + obtain rfl : i' = i + n := by omega + obtain rfl : j' = j + n := by omega + dsimp at hf ⊢ + simp only [Linear.comp_units_smul] at hf + apply (one_smul (M := ℤˣ) _).symm.trans _ + rw [← Int.units_mul_self n.negOnePow, mul_smul, comp_id, hf, smul_zero]) ≫ + K.homologyπ i' ≫ + ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n i i' hi').inv.app K := by + simp only [liftCycles, homologyπ, + shiftFunctorObjXIso, Functor.shiftIso, Functor.ShiftSequence.shiftIso, + ShiftSequence.shiftIso_inv_app, ShortComplex.homologyπ_naturality, + ShortComplex.liftCycles_comp_cyclesMap_assoc, shiftShortComplexFunctorIso_inv_app_τ₂, + assoc, Iso.hom_inv_id, comp_id] + rfl + end CochainComplex namespace HomotopyCategory @@ -147,4 +175,14 @@ lemma homologyShiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainCom (homologyFunctorFactors _ _ a').inv.app K := by apply Functor.ShiftSequence.induced_shiftIso_hom_app_obj +@[reassoc] +lemma homologyFunctor_shiftMap + {K L : CochainComplex C ℤ} {n : ℤ} (f : K ⟶ L⟦n⟧) (a a' : ℤ) (h : n + a = a') : + (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap + ((quotient _ _).map f ≫ ((quotient _ _).commShiftIso n).hom.app _) a a' h = + (homologyFunctorFactors _ _ a).hom.app K ≫ + (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫ + (homologyFunctorFactors _ _ a').inv.app L := by + apply Functor.ShiftSequence.induced_shiftMap + end HomotopyCategory diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean b/Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean new file mode 100644 index 00000000000000..2dc4694c7f66e6 --- /dev/null +++ b/Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean @@ -0,0 +1,146 @@ +/- +Copyright (c) 2024 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor +import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence +import Mathlib.Algebra.Homology.HomologySequenceLemmas +import Mathlib.Algebra.Homology.Refinements + +/-! +# The mapping cone of a monomorphism, up to a quasi-isomophism + +If `S` is a short exact short complex of cochain complexes in an abelian category, +we construct a quasi-isomorphism `descShortComplex S : mappingCone S.f ⟶ S.X₃`. + +We obtain this by comparing the homology sequence of `S` and the homology +sequence of the homology functor on the homotopy category, applied to the +distinguished triangle attached to the mapping cone of `S.f`. + +-/ + +open CategoryTheory Category ComplexShape HomotopyCategory Limits + HomologicalComplex.HomologySequence Pretriangulated Preadditive + +variable {C : Type*} [Category C] [Abelian C] + +namespace CochainComplex + +@[reassoc] +lemma homologySequenceδ_quotient_mapTriangle_obj + (T : Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : + (homologyFunctor C (up ℤ) 0).homologySequenceδ + ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h = + (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫ + (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ (by omega) ≫ + (homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by + apply homologyFunctor_shiftMap + +namespace mappingCone + +variable (S : ShortComplex (CochainComplex C ℤ)) (hS : S.ShortExact) + +/-- The canonical morphism `mappingCone S.f ⟶ S.X₃` when `S` is a short complex +of cochain complexes. -/ +noncomputable def descShortComplex : mappingCone S.f ⟶ S.X₃ := desc S.f 0 S.g (by simp) + +@[reassoc (attr := simp)] +lemma inr_descShortComplex : inr S.f ≫ descShortComplex S = S.g := by + simp [descShortComplex] + +@[reassoc (attr := simp)] +lemma inr_f_descShortComplex_f (n : ℤ) : (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n := by + simp [descShortComplex] + +@[reassoc (attr := simp)] +lemma inl_v_descShortComplex_f (i j : ℤ) (h : i + (-1) = j) : + (inl S.f).v i j h ≫ (descShortComplex S).f j = 0 := by + simp [descShortComplex] + +variable {S} + +lemma homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : + (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h = + (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫ + HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫ hS.δ n₀ n₁ h ≫ + (homologyFunctorFactors C (up ℤ) n₁).inv.app _ := by + /- We proceed by diagram chase. We test the identity on + cocycles `x' : A' ⟶ (mappingCone S.f).X n₀` -/ + dsimp + rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _), + assoc, assoc, assoc, Iso.inv_hom_id_app, + ← cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc] + apply yoneda.map_injective + ext ⟨A⟩ (x : A ⟶ _) + obtain ⟨A', π, _, x', w, hx'⟩ := + (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h) + erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h] + dsimp + rw [comp_id, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app] + erw [comp_id] + rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx', + HomologicalComplex.homologyπ_naturality_assoc, + HomologicalComplex.liftCycles_comp_cyclesMap_assoc] + /- We decompose the cocycle `x'` into two morphisms `a : A' ⟶ S.X₁.X n₁` + and `b : A' ⟶ S.X₂.X n₀` satisfying certain relations. -/ + obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h + rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc, + assoc, assoc, assoc, inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp, + d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg, neg_eq_zero, + add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp, + d_snd_v _ _ _ h, comp_add, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w + /- We simplify the RHS. -/ + conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f, + inl_v_descShortComplex_f, comp_zero, zero_add] + rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a) + (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)] + /- We simplify the LHS. -/ + dsimp [Functor.shiftMap, homologyFunctor_shift] + rw [HomologicalComplex.homologyπ_naturality_assoc, + HomologicalComplex.liftCycles_comp_cyclesMap_assoc, + S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by omega) (n₁ + 1) (by simp), + Iso.inv_hom_id_app] + dsimp [homologyFunctor_shift] + simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc, + shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg, comp_id, + inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero] + +open ComposableArrows + +set_option simprocs false + +lemma quasiIso_descShortComplex : QuasiIso (descShortComplex S) where + quasiIsoAt n := by + rw [quasiIsoAt_iff_isIso_homologyMap] + let φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ + (triangleh S.f) n _ rfl).δlast ⟶ (composableArrows₅ hS n _ rfl).δlast := + homMk₄ ((homologyFunctorFactors C (up ℤ) _).hom.app _) + ((homologyFunctorFactors C (up ℤ) _).hom.app _) + ((homologyFunctorFactors C (up ℤ) _).hom.app _ ≫ + HomologicalComplex.homologyMap (descShortComplex S) n) + ((homologyFunctorFactors C (up ℤ) _).hom.app _) + ((homologyFunctorFactors C (up ℤ) _).hom.app _) + ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f) + (by + erw [(homologyFunctorFactors C (up ℤ) n).hom.naturality_assoc] + dsimp + rw [← HomologicalComplex.homologyMap_comp, inr_descShortComplex]) + (by + dsimp + erw [homologySequenceδ_triangleh hS] + simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj, assoc, + Iso.inv_hom_id_app, comp_id]) + ((homologyFunctorFactors C (up ℤ) _).hom.naturality S.f) + have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫ + HomologicalComplex.homologyMap (descShortComplex S) n) := by + apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono + ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _ + (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast + (composableArrows₅_exact hS n _ rfl).δlast φ + all_goals dsimp [φ]; infer_instance + apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f)) + +end mappingCone + +end CochainComplex diff --git a/Mathlib/Algebra/Homology/Refinements.lean b/Mathlib/Algebra/Homology/Refinements.lean new file mode 100644 index 00000000000000..a2c442807fce7b --- /dev/null +++ b/Mathlib/Algebra/Homology/Refinements.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2024 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ + +import Mathlib.CategoryTheory.Abelian.Refinements +import Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex + +/-! +# Refinements + +This file contains lemmas about "refinements" that are specific to +the study of the homology of `HomologicalComplex`. General +lemmas about refinements and the case of `ShortComplex` appear +in the file `CategoryTheory.Abelian.Refinements`. + +-/ + +open CategoryTheory + +variable {C ι : Type*} [Category C] [Abelian C] {c : ComplexShape ι} + (K : HomologicalComplex C c) + +namespace HomologicalComplex + +lemma eq_liftCycles_homologyπ_up_to_refinements {A : C} {i : ι} (γ : A ⟶ K.homology i) + (j : ι) (hj : c.next i = j) : + ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ K.X i) (hz : z ≫ K.d i j = 0), + π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i := by + subst hj + exact (K.sc i).eq_liftCycles_homologyπ_up_to_refinements γ + +end HomologicalComplex diff --git a/Mathlib/CategoryTheory/Abelian/Refinements.lean b/Mathlib/CategoryTheory/Abelian/Refinements.lean index f566d9630f585d..90215bae9f07f9 100644 --- a/Mathlib/CategoryTheory/Abelian/Refinements.lean +++ b/Mathlib/CategoryTheory/Abelian/Refinements.lean @@ -110,4 +110,13 @@ lemma ShortComplex.Exact.exact_up_to_refinements rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS exact hS x₂ hx₂ +lemma ShortComplex.eq_liftCycles_homologyπ_up_to_refinements {A : C} (γ : A ⟶ S.homology) : + ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (z : A' ⟶ S.X₂) (hz : z ≫ S.g = 0), + π ≫ γ = S.liftCycles z hz ≫ S.homologyπ := by + obtain ⟨A', π, hπ, z, hz⟩ := surjective_up_to_refinements_of_epi S.homologyπ γ + refine ⟨A', π, hπ, z ≫ S.iCycles, by simp, ?_⟩ + rw [hz] + congr 1 + rw [← cancel_mono S.iCycles, liftCycles_i] + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean b/Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean index 33ad165e1dbd64..79ed69962f8581 100644 --- a/Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean +++ b/Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean @@ -119,6 +119,18 @@ lemma induced_shiftIso_hom_app_obj (n a a' : M) (ha' : n + a = a') (X : C) : (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X := by apply induced.shiftIso_hom_app_obj +@[reassoc] +lemma induced_shiftMap {n : M} {X Y : C} (f : X ⟶ Y⟦n⟧) (a a' : M) (h : n + a = a') : + letI := induced e M F' e' + F.shiftMap (L.map f ≫ (L.commShiftIso n).hom.app _) a a' h = + (e' a).hom.app X ≫ G.shiftMap f a a' h ≫ (e' a').inv.app Y := by + dsimp [shiftMap] + rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc] + nth_rw 2 [← Functor.map_comp_assoc] + simp only [comp_obj, Iso.hom_inv_id_app, map_id, id_comp] + rw [← NatTrans.naturality_assoc] + rfl + end ShiftSequence end Functor diff --git a/Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean b/Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean index 3d8c1c7c9bb182..e630e1c82993c0 100644 --- a/Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean +++ b/Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean @@ -7,6 +7,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Exact import Mathlib.CategoryTheory.Shift.ShiftSequence import Mathlib.CategoryTheory.Triangulated.Functor import Mathlib.CategoryTheory.Triangulated.Subcategory +import Mathlib.Algebra.Homology.ExactSequence /-! # Homological functors @@ -237,6 +238,21 @@ lemma mem_homologicalKernel_W_iff {X Y : C} (f : X ⟶ Y) : · intros constructor <;> infer_instance +open ComposableArrows + +/-- The exact sequence with six terms starting from `(F.shift n₀).obj T.obj₁` until +`(F.shift n₁).obj T.obj₃` when `T` is a distinguished triangle and `F` a homological functor. -/ +@[simp] noncomputable def homologySequenceComposableArrows₅ : ComposableArrows A 5 := + mk₅ ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) + (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ((F.shift n₁).map T.mor₂) + +lemma homologySequenceComposableArrows₅_exact : + (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact := + exact_of_δ₀ (F.homologySequence_exact₂ T hT n₀).exact_toComposableArrows + (exact_of_δ₀ (F.homologySequence_exact₃ T hT n₀ n₁ h).exact_toComposableArrows + (exact_of_δ₀ (F.homologySequence_exact₁ T hT n₀ n₁ h).exact_toComposableArrows + (F.homologySequence_exact₂ T hT n₁).exact_toComposableArrows)) + end end Functor