From d412c821c9dd98524268d9023f528f98aff7980a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 27 Dec 2023 10:11:17 +0000 Subject: [PATCH] feat(Algebra/Homology): computation of the connecting homomorphism of the homology sequence (#8771) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a variant of a lemma introduced in #8512: `ShortComplex.SnakeInput.δ_apply'` computes the connecting homomorphism of the snake lemma in a concrete categoriy `C` with a phrasing based on the functor `forget₂ C Ab` rather than `forget C`. From this, the lemma `ShortComplex.ShortExact.δ_apply` is obtained in a new file `Algebra.Homology.ConcreteCategory`: it gives a computation in terms of (co)cycles of the connecting homomorphism in homology attached to a short exact sequence of homological complexes in `C`. This PR also adds a lemma which computes "up to refinements" the connecting homomorphism of the homology sequence in general abelian categories. --- Mathlib.lean | 1 + .../Algebra/Homology/ConcreteCategory.lean | 97 +++++++++++++++++++ .../Algebra/Homology/HomologySequence.lean | 26 +++++ Mathlib/Algebra/Homology/ShortComplex/Ab.lean | 7 ++ .../ShortComplex/ConcreteCategory.lean | 47 ++++++++- .../ShortComplex/PreservesHomology.lean | 5 + .../ConcreteCategory/Basic.lean | 9 ++ 7 files changed, 189 insertions(+), 3 deletions(-) create mode 100644 Mathlib/Algebra/Homology/ConcreteCategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index f4ac51bf7b43a..cbadc395b2594 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -231,6 +231,7 @@ import Mathlib.Algebra.HierarchyDesign import Mathlib.Algebra.Homology.Additive import Mathlib.Algebra.Homology.Augment import Mathlib.Algebra.Homology.ComplexShape +import Mathlib.Algebra.Homology.ConcreteCategory import Mathlib.Algebra.Homology.DifferentialObject import Mathlib.Algebra.Homology.Exact import Mathlib.Algebra.Homology.ExactSequence diff --git a/Mathlib/Algebra/Homology/ConcreteCategory.lean b/Mathlib/Algebra/Homology/ConcreteCategory.lean new file mode 100644 index 0000000000000..97b6277794839 --- /dev/null +++ b/Mathlib/Algebra/Homology/ConcreteCategory.lean @@ -0,0 +1,97 @@ +/- +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 +-/ +import Mathlib.Algebra.Homology.HomologySequence +import Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory + +/-! +# Homology of complexes in concrete categories + +The homology of short complexes in concrete categories was studied in +`Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory`. In this file, +we introduce specific definitions and lemmas for the homology +of homological complexes in concrete categories. In particular, +we give a computation of the connecting homomorphism of +the homology sequence in terms of (co)cycles. + +-/ + +open CategoryTheory + +universe v u + +variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] [HasForget₂ C Ab.{v}] + [Abelian C] [(forget₂ C Ab).Additive] [(forget₂ C Ab).PreservesHomology] + {ι : Type*} {c : ComplexShape ι} + +namespace HomologicalComplex + +variable (K : HomologicalComplex C c) + +/-- Constructor for cycles of a homological complex in a concrete category. -/ +noncomputable def cyclesMk {i : ι} (x : (forget₂ C Ab).obj (K.X i)) (j : ι) (hj : c.next i = j) + (hx : ((forget₂ C Ab).map (K.d i j)) x = 0) : + (forget₂ C Ab).obj (K.cycles i) := + (K.sc i).cyclesMk x (by subst hj; exact hx) + +@[simp] +lemma i_cyclesMk {i : ι} (x : (forget₂ C Ab).obj (K.X i)) (j : ι) (hj : c.next i = j) + (hx : ((forget₂ C Ab).map (K.d i j)) x = 0) : + ((forget₂ C Ab).map (K.iCycles i)) (K.cyclesMk x j hj hx) = x := by + subst hj + apply (K.sc i).i_cyclesMk + +end HomologicalComplex + +namespace CategoryTheory + +namespace ShortComplex + +namespace ShortExact + +variable {S : ShortComplex (HomologicalComplex C c)} + (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) + +lemma δ_apply' (x₃ : (forget₂ C Ab).obj (S.X₃.homology i)) + (x₂ : (forget₂ C Ab).obj (S.X₂.opcycles i)) + (x₁ : (forget₂ C Ab).obj (S.X₁.cycles j)) + (h₂ : (forget₂ C Ab).map (HomologicalComplex.opcyclesMap S.g i) x₂ = + (forget₂ C Ab).map (S.X₃.homologyι i) x₃) + (h₁ : (forget₂ C Ab).map (HomologicalComplex.cyclesMap S.f j) x₁ = + (forget₂ C Ab).map (S.X₂.opcyclesToCycles i j) x₂) : + (forget₂ C Ab).map (hS.δ i j hij) x₃ = (forget₂ C Ab).map (S.X₁.homologyπ j) x₁ := + (HomologicalComplex.HomologySequence.snakeInput hS i j hij).δ_apply' x₃ x₂ x₁ h₂ h₁ + +lemma δ_apply (x₃ : (forget₂ C Ab).obj (S.X₃.X i)) + (hx₃ : (forget₂ C Ab).map (S.X₃.d i j) x₃ = 0) + (x₂ : (forget₂ C Ab).obj (S.X₂.X i)) (hx₂ : (forget₂ C Ab).map (S.g.f i) x₂ = x₃) + (x₁ : (forget₂ C Ab).obj (S.X₁.X j)) + (hx₁ : (forget₂ C Ab).map (S.f.f j) x₁ = (forget₂ C Ab).map (S.X₂.d i j) x₂) + (k : ι) (hk : c.next j = k) : + (forget₂ C Ab).map (hS.δ i j hij) + ((forget₂ C Ab).map (S.X₃.homologyπ i) (S.X₃.cyclesMk x₃ j (c.next_eq' hij) hx₃)) = + (forget₂ C Ab).map (S.X₁.homologyπ j) (S.X₁.cyclesMk x₁ k hk (by + have := hS.mono_f + apply (Preadditive.mono_iff_injective (S.f.f k)).1 inferInstance + erw [← forget₂_comp_apply, ← HomologicalComplex.Hom.comm, forget₂_comp_apply, hx₁, + ← forget₂_comp_apply, HomologicalComplex.d_comp_d, Functor.map_zero, map_zero, + AddMonoidHom.zero_apply])) := by + refine hS.δ_apply' i j hij _ ((forget₂ C Ab).map (S.X₂.pOpcycles i) x₂) _ ?_ ?_ + · erw [← forget₂_comp_apply, ← forget₂_comp_apply, + HomologicalComplex.p_opcyclesMap, Functor.map_comp, comp_apply, + HomologicalComplex.homology_π_ι, forget₂_comp_apply, hx₂, HomologicalComplex.i_cyclesMk] + · apply (Preadditive.mono_iff_injective (S.X₂.iCycles j)).1 inferInstance + conv_lhs => + erw [← forget₂_comp_apply, HomologicalComplex.cyclesMap_i, forget₂_comp_apply, + HomologicalComplex.i_cyclesMk, hx₁] + conv_rhs => + erw [← forget₂_comp_apply, ← forget₂_comp_apply, + HomologicalComplex.pOpcycles_opcyclesToCycles_assoc, HomologicalComplex.toCycles_i] + +end ShortExact + +end ShortComplex + +end CategoryTheory diff --git a/Mathlib/Algebra/Homology/HomologySequence.lean b/Mathlib/Algebra/Homology/HomologySequence.lean index f6d4c08571308..1c673d44139b5 100644 --- a/Mathlib/Algebra/Homology/HomologySequence.lean +++ b/Mathlib/Algebra/Homology/HomologySequence.lean @@ -302,6 +302,32 @@ lemma homology_exact₂ : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i lemma homology_exact₃ : (ShortComplex.mk _ _ (comp_δ hS i j hij)).Exact := (snakeInput hS i j hij).L₁'_exact +lemma δ_eq' {A : C} (x₃ : A ⟶ S.X₃.homology i) (x₂ : A ⟶ S.X₂.opcycles i) + (x₁ : A ⟶ S.X₁.cycles j) + (h₂ : x₂ ≫ HomologicalComplex.opcyclesMap S.g i = x₃ ≫ S.X₃.homologyι i) + (h₁ : x₁ ≫ HomologicalComplex.cyclesMap S.f j = x₂ ≫ S.X₂.opcyclesToCycles i j) : + x₃ ≫ hS.δ i j hij = x₁ ≫ S.X₁.homologyπ j := + (snakeInput hS i j hij).δ_eq x₃ x₂ x₁ h₂ h₁ + +lemma δ_eq {A : C} (x₃ : A ⟶ S.X₃.X i) (hx₃ : x₃ ≫ S.X₃.d i j = 0) + (x₂ : A ⟶ S.X₂.X i) (hx₂ : x₂ ≫ S.g.f i = x₃) + (x₁ : A ⟶ S.X₁.X j) (hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j) + (k : ι) (hk : c.next j = k) : + S.X₃.liftCycles x₃ j (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i ≫ hS.δ i j hij = + S.X₁.liftCycles x₁ k hk (by + have := hS.mono_f + rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁, + d_comp_d, comp_zero, zero_comp]) ≫ S.X₁.homologyπ j := by + simpa only [assoc] using hS.δ_eq' i j hij (S.X₃.liftCycles x₃ j + (c.next_eq' hij) hx₃ ≫ S.X₃.homologyπ i) + (x₂ ≫ S.X₂.pOpcycles i) (S.X₁.liftCycles x₁ k hk _) + (by simp only [assoc, HomologicalComplex.p_opcyclesMap, + HomologicalComplex.homology_π_ι, + HomologicalComplex.liftCycles_i_assoc, reassoc_of% hx₂]) + (by rw [← cancel_mono (S.X₂.iCycles j), HomologicalComplex.liftCycles_comp_cyclesMap, + HomologicalComplex.liftCycles_i, assoc, assoc, opcyclesToCycles_iCycles, + HomologicalComplex.p_fromOpcycles, hx₁]) + end ShortExact end ShortComplex diff --git a/Mathlib/Algebra/Homology/ShortComplex/Ab.lean b/Mathlib/Algebra/Homology/ShortComplex/Ab.lean index 103da7c452f39..3d00fedbdac13 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/Ab.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/Ab.lean @@ -71,6 +71,13 @@ the abstract `S.cycles` of the homology API and the more concrete description as noncomputable def abCyclesIso : S.cycles ≅ AddCommGroupCat.of (AddMonoidHom.ker S.g) := S.abLeftHomologyData.cyclesIso +@[simp] +lemma abCyclesIso_inv_apply_iCycles (x : AddMonoidHom.ker S.g) : + S.iCycles (S.abCyclesIso.inv x) = x := by + dsimp only [abCyclesIso] + erw [← comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles] + rfl + /-- Given a short complex `S` of abelian groups, this is the isomorphism between the abstract `S.homology` of the homology API and the more explicit quotient of `AddMonoidHom.ker S.g` by the image of diff --git a/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean b/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean index a360bb51913b3..1d9489809dc7c 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean @@ -55,7 +55,7 @@ lemma Preadditive.mono_iff_injective' {X Y : C} (f : X ⟶ Y) : have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp) exact Arrow.isoOfNatIso e (Arrow.mk f) -lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) : +lemma Preadditive.epi_iff_surjective {X Y : C} (f : X ⟶ Y) : Epi f ↔ Function.Surjective ((forget₂ C Ab).map f) := by rw [← AddCommGroupCat.epi_iff_surjective] constructor @@ -65,7 +65,7 @@ lemma Preadditive.epi_iff_injective {X Y : C} (f : X ⟶ Y) : lemma Preadditive.epi_iff_surjective' {X Y : C} (f : X ⟶ Y) : Epi f ↔ Function.Surjective ((forget C).map f) := by - simp only [epi_iff_injective, ← CategoryTheory.epi_iff_surjective] + simp only [epi_iff_surjective, ← CategoryTheory.epi_iff_surjective] apply (MorphismProperty.RespectsIso.epimorphisms (Type w)).arrow_mk_iso_iff have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp) exact Arrow.isoOfNatIso e (Arrow.mk f) @@ -91,9 +91,25 @@ lemma ShortExact.injective_f (hS : S.ShortExact) : lemma ShortExact.surjective_g (hS : S.ShortExact) : Function.Surjective ((forget₂ C Ab).map S.g) := by - rw [← Preadditive.epi_iff_injective] + rw [← Preadditive.epi_iff_surjective] exact hS.epi_g +variable (S) + +/-- Constructor for cycles of short complexes in a concrete category. -/ +noncomputable def cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂) + (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) : + (forget₂ C Ab).obj S.cycles := + (S.mapCyclesIso (forget₂ C Ab)).hom ((ShortComplex.abCyclesIso _).inv ⟨x₂, hx₂⟩) + +@[simp] +lemma i_cyclesMk [S.HasHomology] (x₂ : (forget₂ C Ab).obj S.X₂) + (hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0) : + (forget₂ C Ab).map S.iCycles (S.cyclesMk x₂ hx₂) = x₂ := by + dsimp [cyclesMk] + erw [← comp_apply, S.mapCyclesIso_hom_iCycles (forget₂ C Ab), + ← comp_apply, abCyclesIso_inv_apply_iCycles ] + end ShortComplex end preadditive @@ -136,6 +152,31 @@ lemma δ_apply (x₃ : D.L₀.X₃) (x₂ : D.L₁.X₂) (x₁ : D.L₂.X₁) rw [Functor.map_comp, types_comp_apply, eq₁] exact h₁.symm +/-- This lemma allows the computation of the connecting homomorphism +`D.δ` when `D : SnakeInput C` and `C` is a concrete category. -/ +lemma δ_apply' (x₃ : (forget₂ C Ab).obj D.L₀.X₃) + (x₂ : (forget₂ C Ab).obj D.L₁.X₂) (x₁ : (forget₂ C Ab).obj D.L₂.X₁) + (h₂ : (forget₂ C Ab).map D.L₁.g x₂ = (forget₂ C Ab).map D.v₀₁.τ₃ x₃) + (h₁ : (forget₂ C Ab).map D.L₂.f x₁ = (forget₂ C Ab).map D.v₁₂.τ₂ x₂) : + (forget₂ C Ab).map D.δ x₃ = (forget₂ C Ab).map D.v₂₃.τ₁ x₁ := by + have e : forget₂ C Ab ⋙ forget Ab ≅ forget C := eqToIso (HasForget₂.forget_comp) + apply (mono_iff_injective (e.hom.app _)).1 inferInstance + refine (congr_hom (e.hom.naturality D.δ) x₃).trans + ((D.δ_apply (e.hom.app _ x₃) (e.hom.app _ x₂) (e.hom.app _ x₁) ?_ ?_ ).trans + (congr_hom (e.hom.naturality D.v₂₃.τ₁).symm x₁)) + · refine ((congr_hom (e.hom.naturality D.L₁.g) x₂).symm.trans ?_).trans + (congr_hom (e.hom.naturality D.v₀₁.τ₃) x₃) + dsimp + rw [comp_apply, comp_apply] + erw [h₂] + rfl + · refine ((congr_hom (e.hom.naturality D.L₂.f) x₁).symm.trans ?_).trans + (congr_hom (e.hom.naturality D.v₁₂.τ₂) x₂) + dsimp + rw [comp_apply, comp_apply] + erw [h₁] + rfl + end SnakeInput end ShortComplex diff --git a/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean index d01c63f06c307..7d8b6fa9fbfb8 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean @@ -400,6 +400,11 @@ noncomputable def mapCyclesIso [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] (S.map F).cycles ≅ F.obj S.cycles := (S.leftHomologyData.map F).cyclesIso +@[reassoc (attr := simp)] +lemma mapCyclesIso_hom_iCycles [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] : + (S.mapCyclesIso F).hom ≫ F.map S.iCycles = (S.map F).iCycles := by + apply LeftHomologyData.cyclesIso_hom_comp_i + /-- When a functor `F` preserves the left homology of a short complex `S`, this is the canonical isomorphism `(S.map F).leftHomology ≅ F.obj S.leftHomology`. -/ noncomputable def mapLeftHomologyIso [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] : diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index a3d280b47126b..19883fe435036 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -212,6 +212,15 @@ def forget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} HasForget₂.forget₂ #align category_theory.forget₂ CategoryTheory.forget₂ +attribute [local instance] ConcreteCategory.funLike ConcreteCategory.hasCoeToSort + +lemma forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C] [ConcreteCategory.{w} C] + [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] {X Y Z : C} + (f : X ⟶ Y) (g : Y ⟶ Z) (x : (forget₂ C D).obj X) : + ((forget₂ C D).map (f ≫ g) x) = + (forget₂ C D).map g ((forget₂ C D).map f x) := by + rw [Functor.map_comp, comp_apply] + instance forget₂_faithful (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C] [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : Faithful (forget₂ C D) := HasForget₂.forget_comp.faithful_of_comp