From 07c7fee93fbe6eaa7c9f7c6d425eff2ab50e5589 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 20 Jul 2023 08:16:45 +0000 Subject: [PATCH] feat: left and right homology data are dual notions (#5674) This PR shows that left and right homology data of short complexes are dual notions. --- .../Homology/ShortComplex/RightHomology.lean | 174 +++++++++++++++++- Mathlib/CategoryTheory/Limits/Opposites.lean | 51 +++++ .../Limits/Shapes/ZeroMorphisms.lean | 6 + .../CategoryTheory/Preadditive/Opposite.lean | 10 - 4 files changed, 228 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean index 6c6fa8fbb510e..fd6fb602ae1ea 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean @@ -5,6 +5,7 @@ Authors: Joël Riou -/ import Mathlib.Algebra.Homology.ShortComplex.LeftHomology +import Mathlib.CategoryTheory.Limits.Opposites /-! RightHomology of short complexes @@ -32,7 +33,7 @@ open Category Limits namespace ShortComplex variable {C : Type _} [Category C] [HasZeroMorphisms C] - (S : ShortComplex C) + (S : ShortComplex C) {S₁ S₂ S₃ : ShortComplex C} /-- A right homology data for a short complex `S` consists of morphisms `p : S.X₂ ⟶ Q` and `ι : H ⟶ Q` such that `p` identifies `Q` to the kernel of `f : S.X₁ ⟶ S.X₂`, @@ -209,8 +210,8 @@ lemma ofZeros_g' (hf : S.f = 0) (hg : S.g = 0) : end RightHomologyData /-- A short complex `S` has right homology when there exists a `S.RightHomologyData` -/ -class HasRightHomology : Prop := -(condition : Nonempty S.RightHomologyData) +class HasRightHomology : Prop where + condition : Nonempty S.RightHomologyData /-- A chosen `S.RightHomologyData` for a short complex `S` that has right homology -/ noncomputable def rightHomologyData [HasRightHomology S] : @@ -240,6 +241,173 @@ instance of_zeros (X Y Z : C) : end HasRightHomology +namespace RightHomologyData + +/-- A right homology data for a short complex `S` induces a left homology data for `S.op`. -/ +@[simps] +def op (h : S.RightHomologyData) : S.op.LeftHomologyData where + K := Opposite.op h.Q + H := Opposite.op h.H + i := h.p.op + π := h.ι.op + wi := Quiver.Hom.unop_inj h.wp + hi := CokernelCofork.IsColimit.ofπOp _ _ h.hp + wπ := Quiver.Hom.unop_inj h.wι + hπ := KernelFork.IsLimit.ofιOp _ _ h.hι + +@[simp] lemma op_f' (h : S.RightHomologyData) : + h.op.f' = h.g'.op := rfl + +/-- A right homology data for a short complex `S` in the opposite category +induces a left homology data for `S.unop`. -/ +@[simps] +def unop {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : S.unop.LeftHomologyData where + K := Opposite.unop h.Q + H := Opposite.unop h.H + i := h.p.unop + π := h.ι.unop + wi := Quiver.Hom.op_inj h.wp + hi := CokernelCofork.IsColimit.ofπUnop _ _ h.hp + wπ := Quiver.Hom.op_inj h.wι + hπ := KernelFork.IsLimit.ofιUnop _ _ h.hι + +@[simp] lemma unop_f' {S : ShortComplex Cᵒᵖ} (h : S.RightHomologyData) : + h.unop.f' = h.g'.unop := rfl + +end RightHomologyData + +namespace LeftHomologyData + +/-- A left homology data for a short complex `S` induces a right homology data for `S.op`. -/ +@[simps] +def op (h : S.LeftHomologyData) : S.op.RightHomologyData where + Q := Opposite.op h.K + H := Opposite.op h.H + p := h.i.op + ι := h.π.op + wp := Quiver.Hom.unop_inj h.wi + hp := KernelFork.IsLimit.ofιOp _ _ h.hi + wι := Quiver.Hom.unop_inj h.wπ + hι := CokernelCofork.IsColimit.ofπOp _ _ h.hπ + +@[simp] lemma op_g' (h : S.LeftHomologyData) : + h.op.g' = h.f'.op := rfl + +/-- A left homology data for a short complex `S` in the opposite category +induces a right homology data for `S.unop`. -/ +@[simps] +def unop {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : S.unop.RightHomologyData where + Q := Opposite.unop h.K + H := Opposite.unop h.H + p := h.i.unop + ι := h.π.unop + wp := Quiver.Hom.op_inj h.wi + hp := KernelFork.IsLimit.ofιUnop _ _ h.hi + wι := Quiver.Hom.op_inj h.wπ + hι := CokernelCofork.IsColimit.ofπUnop _ _ h.hπ + +@[simp] lemma unop_g' {S : ShortComplex Cᵒᵖ} (h : S.LeftHomologyData) : + h.unop.g' = h.f'.unop := rfl + +end LeftHomologyData + +instance [S.HasLeftHomology] : HasRightHomology S.op := + HasRightHomology.mk' S.leftHomologyData.op + +instance [S.HasRightHomology] : HasLeftHomology S.op := + HasLeftHomology.mk' S.rightHomologyData.op + +lemma hasLeftHomology_iff_op (S : ShortComplex C) : + S.HasLeftHomology ↔ S.op.HasRightHomology := + ⟨fun _ => inferInstance, fun _ => HasLeftHomology.mk' S.op.rightHomologyData.unop⟩ + +lemma hasRightHomology_iff_op (S : ShortComplex C) : + S.HasRightHomology ↔ S.op.HasLeftHomology := + ⟨fun _ => inferInstance, fun _ => HasRightHomology.mk' S.op.leftHomologyData.unop⟩ + +lemma hasLeftHomology_iff_unop (S : ShortComplex Cᵒᵖ) : + S.HasLeftHomology ↔ S.unop.HasRightHomology := + S.unop.hasRightHomology_iff_op.symm + +lemma hasRightHomology_iff_unop (S : ShortComplex Cᵒᵖ) : + S.HasRightHomology ↔ S.unop.HasLeftHomology := + S.unop.hasLeftHomology_iff_op.symm + +section + +variable (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) + +/-- Given right homology data `h₁` and `h₂` for two short complexes `S₁` and `S₂`, +a `RightHomologyMapData` for a morphism `φ : S₁ ⟶ S₂` +consists of a description of the induced morphisms on the `Q` (opcycles) +and `H` (right homology) fields of `h₁` and `h₂`. -/ +structure RightHomologyMapData where + /-- the induced map on opcycles -/ + φQ : h₁.Q ⟶ h₂.Q + /-- the induced map on right homology -/ + φH : h₁.H ⟶ h₂.H + /-- commutation with `p` -/ + commp : h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p := by aesop_cat + /-- commutation with `g'` -/ + commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by aesop_cat + /-- commutation with `ι` -/ + commι : φH ≫ h₂.ι = h₁.ι ≫ φQ := by aesop_cat + +namespace RightHomologyMapData + +attribute [reassoc (attr := simp)] commp commg' commι +attribute [nolint simpNF] mk.injEq + +/-- The right homology map data associated to the zero morphism between two short complexes. -/ +@[simps] +def zero (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) : + RightHomologyMapData 0 h₁ h₂ where + φQ := 0 + φH := 0 + +/-- The right homology map data associated to the identity morphism of a short complex. -/ +@[simps] +def id (h : S.RightHomologyData) : RightHomologyMapData (𝟙 S) h h where + φQ := 𝟙 _ + φH := 𝟙 _ + +/-- The composition of right homology map data. -/ +@[simps] +def comp {φ : S₁ ⟶ S₂} {φ' : S₂ ⟶ S₃} {h₁ : S₁.RightHomologyData} + {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} + (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) : + RightHomologyMapData (φ ≫ φ') h₁ h₃ where + φQ := ψ.φQ ≫ ψ'.φQ + φH := ψ.φH ≫ ψ'.φH + +instance : Subsingleton (RightHomologyMapData φ h₁ h₂) := + ⟨fun ψ₁ ψ₂ => by + have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp] + have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ] + cases ψ₁ + cases ψ₂ + congr⟩ + +instance : Inhabited (RightHomologyMapData φ h₁ h₂) := ⟨by + let φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) (by rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]) + have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := + by rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc, + RightHomologyData.p_g', φ.comm₂₃, RightHomologyData.p_g'_assoc] + let φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) + (by rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]) + exact ⟨φQ, φH, by simp, commg', by simp⟩⟩ + +instance : Unique (RightHomologyMapData φ h₁ h₂) := Unique.mk' _ + +variable {φ h₁ h₂} + +lemma congr_φH {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH := by rw [eq] +lemma congr_φQ {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φQ = γ₂.φQ := by rw [eq] + +end RightHomologyMapData + +end + end ShortComplex end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/Opposites.lean b/Mathlib/CategoryTheory/Limits/Opposites.lean index 27c65ebe7bf21..10dae41a97a1e 100644 --- a/Mathlib/CategoryTheory/Limits/Opposites.lean +++ b/Mathlib/CategoryTheory/Limits/Opposites.lean @@ -5,6 +5,7 @@ Authors: Scott Morrison, Floris van Doorn -/ import Mathlib.CategoryTheory.Limits.Filtered import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts +import Mathlib.CategoryTheory.Limits.Shapes.Kernels import Mathlib.CategoryTheory.DiscreteCategory #align_import category_theory.limits.opposites from "leanprover-community/mathlib"@"ac3ae212f394f508df43e37aa093722fa9b65d31" @@ -707,4 +708,54 @@ theorem pushoutIsoUnopPullback_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [ end Pushout +section HasZeroMorphisms + +variable [HasZeroMorphisms C] + +/-- A colimit cokernel cofork gives a limit kernel fork in the opposite category -/ +def CokernelCofork.IsColimit.ofπOp {X Y Q : C} (p : Y ⟶ Q) {f : X ⟶ Y} + (w : f ≫ p = 0) (h : IsColimit (CokernelCofork.ofπ p w)) : + IsLimit (KernelFork.ofι p.op (show p.op ≫ f.op = 0 by rw [← op_comp, w, op_zero])) := + KernelFork.IsLimit.ofι _ _ + (fun x hx => (h.desc (CokernelCofork.ofπ x.unop (Quiver.Hom.op_inj hx))).op) + (fun x hx => Quiver.Hom.unop_inj (Cofork.IsColimit.π_desc h)) + (fun x hx b hb => Quiver.Hom.unop_inj (Cofork.IsColimit.hom_ext h + (by simpa only [Quiver.Hom.unop_op, Cofork.IsColimit.π_desc] using Quiver.Hom.op_inj hb))) + +/-- A colimit cokernel cofork in the opposite category gives a limit kernel fork +in the original category -/ +def CokernelCofork.IsColimit.ofπUnop {X Y Q : Cᵒᵖ} (p : Y ⟶ Q) {f : X ⟶ Y} + (w : f ≫ p = 0) (h : IsColimit (CokernelCofork.ofπ p w)) : + IsLimit (KernelFork.ofι p.unop (show p.unop ≫ f.unop = 0 by rw [← unop_comp, w, unop_zero])) := + KernelFork.IsLimit.ofι _ _ + (fun x hx => (h.desc (CokernelCofork.ofπ x.op (Quiver.Hom.unop_inj hx))).unop) + (fun x hx => Quiver.Hom.op_inj (Cofork.IsColimit.π_desc h)) + (fun x hx b hb => Quiver.Hom.op_inj (Cofork.IsColimit.hom_ext h + (by simpa only [Quiver.Hom.op_unop, Cofork.IsColimit.π_desc] using Quiver.Hom.unop_inj hb))) + +/-- A limit kernel fork gives a colimit cokernel cofork in the opposite category -/ +def KernelFork.IsLimit.ofιOp {K X Y : C} (i : K ⟶ X) {f : X ⟶ Y} + (w : i ≫ f = 0) (h : IsLimit (KernelFork.ofι i w)) : + IsColimit (CokernelCofork.ofπ i.op + (show f.op ≫ i.op = 0 by rw [← op_comp, w, op_zero])) := + CokernelCofork.IsColimit.ofπ _ _ + (fun x hx => (h.lift (KernelFork.ofι x.unop (Quiver.Hom.op_inj hx))).op) + (fun x hx => Quiver.Hom.unop_inj (Fork.IsLimit.lift_ι h)) + (fun x hx b hb => Quiver.Hom.unop_inj (Fork.IsLimit.hom_ext h (by + simpa only [Quiver.Hom.unop_op, Fork.IsLimit.lift_ι] using Quiver.Hom.op_inj hb))) + +/-- A limit kernel fork in the opposite category gives a colimit cokernel cofork +in the original category -/ +def KernelFork.IsLimit.ofιUnop {K X Y : Cᵒᵖ} (i : K ⟶ X) {f : X ⟶ Y} + (w : i ≫ f = 0) (h : IsLimit (KernelFork.ofι i w)) : + IsColimit (CokernelCofork.ofπ i.unop + (show f.unop ≫ i.unop = 0 by rw [← unop_comp, w, unop_zero])) := + CokernelCofork.IsColimit.ofπ _ _ + (fun x hx => (h.lift (KernelFork.ofι x.op (Quiver.Hom.unop_inj hx))).unop) + (fun x hx => Quiver.Hom.op_inj (Fork.IsLimit.lift_ι h)) + (fun x hx b hb => Quiver.Hom.op_inj (Fork.IsLimit.hom_ext h (by + simpa only [Quiver.Hom.op_unop, Fork.IsLimit.lift_ι] using Quiver.Hom.unop_inj hb))) + +end HasZeroMorphisms + end CategoryTheory.Limits diff --git a/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean b/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean index 946e2eac219cc..ca87b655876c4 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean @@ -132,6 +132,12 @@ section variable [HasZeroMorphisms C] +@[simp] lemma op_zero (X Y : C) : (0 : X ⟶ Y).op = 0 := rfl +#align category_theory.op_zero CategoryTheory.Limits.op_zero + +@[simp] lemma unop_zero (X Y : Cᵒᵖ) : (0 : X ⟶ Y).unop = 0 := rfl +#align category_theory.unop_zero CategoryTheory.Limits.unop_zero + theorem zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : f ≫ g = 0) : f = 0 := by rw [← zero_comp, cancel_mono] at h exact h diff --git a/Mathlib/CategoryTheory/Preadditive/Opposite.lean b/Mathlib/CategoryTheory/Preadditive/Opposite.lean index 9068d54f78160..6ab278b2eb79f 100644 --- a/Mathlib/CategoryTheory/Preadditive/Opposite.lean +++ b/Mathlib/CategoryTheory/Preadditive/Opposite.lean @@ -32,11 +32,6 @@ instance moduleEndLeft {X : Cᵒᵖ} {Y : C} : Module (End X) (unop X ⟶ Y) whe zero_smul _ := Limits.zero_comp #align category_theory.module_End_left CategoryTheory.moduleEndLeft -@[simp] -theorem unop_zero (X Y : Cᵒᵖ) : (0 : X ⟶ Y).unop = 0 := - rfl -#align category_theory.unop_zero CategoryTheory.unop_zero - @[simp] theorem unop_add {X Y : Cᵒᵖ} (f g : X ⟶ Y) : (f + g).unop = f.unop + g.unop := rfl @@ -52,11 +47,6 @@ theorem unop_neg {X Y : Cᵒᵖ} (f : X ⟶ Y) : (-f).unop = -f.unop := rfl #align category_theory.unop_neg CategoryTheory.unop_neg -@[simp] -theorem op_zero (X Y : C) : (0 : X ⟶ Y).op = 0 := - rfl -#align category_theory.op_zero CategoryTheory.op_zero - @[simp] theorem op_add {X Y : C} (f g : X ⟶ Y) : (f + g).op = f.op + g.op := rfl