Documentation

Mathlib.Algebra.Homology.ShortComplex.RightHomology

Right Homology of short complexes #

In this file, we define the dual notions to those defined in Algebra.Homology.ShortComplex.LeftHomology. In particular, if S : ShortComplex C is a short complex consisting of two composable maps f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ such that f ≫ g = 0, we define h : S.RightHomologyData to be the datum of morphisms p : X₂ ⟶ Q and ι : HQ such that Q identifies to the cokernel of f and H to the kernel of the induced map g' : Q ⟶ X₃.

When such a S.RightHomologyData exists, we shall say that [S.HasRightHomology] and we define S.rightHomology to be the H field of a chosen right homology data. Similarly, we define S.opcycles to be the Q field.

In Homology.lean, when S has two compatible left and right homology data (i.e. they give the same H up to a canonical isomorphism), we shall define [S.HasHomology] and S.homology.

A right homology data for a short complex S consists of morphisms p : S.X₂ ⟶ Q and ι : HQ such that p identifies Q to the kernel of f : S.X₁ ⟶ S.X₂, and that ι identifies H to the kernel of the induced map g' : Q ⟶ S.X₃

The chosen cokernels and kernels of the limits API give a RightHomologyData

Equations
  • One or more equations did not get rendered due to their size.

Any morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism Q ⟶ A

Equations

The morphism from the (right) homology attached to a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0.

Equations

The morphism h.Q ⟶ S.X₃ induced by S.g : S.X₂ ⟶ S.X₃ and the fact that h.Q is a cokernel of S.f : S.X₁ ⟶ S.X₂.

Equations

For h : S.RightHomologyData, this is a restatement of h., saying that ι : h.H ⟶ h.Q is a kernel of h.g' : h.Q ⟶ S.X₃.

Equations

The morphism A ⟶ H induced by a morphism k : A ⟶ Q such that k ≫ g' = 0

Equations

When the first map S.f is zero, this is the right homology data on S given by any limit kernel fork of S.g

Equations
  • One or more equations did not get rendered due to their size.

When the first map S.f is zero, this is the right homology data on S given by the chosen kernel S.g

Equations
  • One or more equations did not get rendered due to their size.

When the second map S.g is zero, this is the right homology data on S given by any colimit cokernel cofork of S.g

Equations
  • One or more equations did not get rendered due to their size.

When the second map S.g is zero, this is the right homology data on S given by the chosen cokernel S.f

Equations
  • One or more equations did not get rendered due to their size.

When both S.f and S.g are zero, the middle object S.X₂ gives a right homology data on S

Equations
  • One or more equations did not get rendered due to their size.

A short complex S has right homology when there exists a S.RightHomologyData

Instances

    A chosen S.RightHomologyData for a short complex S that has right homology

    Equations

    A right homology data for a short complex S induces a left homology data for S.op.

    Equations
    • One or more equations did not get rendered due to their size.

    A right homology data for a short complex S in the opposite category induces a left homology data for S.unop.

    Equations
    • One or more equations did not get rendered due to their size.

    A left homology data for a short complex S induces a right homology data for S.op.

    Equations
    • One or more equations did not get rendered due to their size.

    A left homology data for a short complex S in the opposite category induces a right homology data for S.unop.

    Equations
    • One or more equations did not get rendered due to their size.

    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₂.

    The right homology map data associated to the zero morphism between two short complexes.

    Equations

    The right homology map data associated to the identity morphism of a short complex.

    Equations
    def CategoryTheory.ShortComplex.RightHomologyMapData.comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) :

    The composition of right homology map data.

    Equations
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) :
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} {φ : S₁ S₂} {φ' : S₂ S₃} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {h₃ : S₃.RightHomologyData} (ψ : RightHomologyMapData φ h₁ h₂) (ψ' : RightHomologyMapData φ' h₂ h₃) :
    Equations
    • One or more equations did not get rendered due to their size.
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) :
    def CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :

    When S₁.f, S₁.g, S₂.f and S₂.g are all zero, the action on right homology of a morphism φ : S₁ ⟶ S₂ is given by the action φ.τ₂ on the middle objects.

    Equations
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
    (ofZeros φ hf₁ hg₁ hf₂ hg₂).φQ = φ.τ₂
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
    (ofZeros φ hf₁ hg₁ hf₂ hg₂).φH = φ.τ₂

    When S₁.f and S₂.f are zero and we have chosen limit kernel forks c₁ and c₂ for S₁.g and S₂.g respectively, the action on right homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι.

    Equations
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (c₁ : Limits.KernelFork S₁.g) (hc₁ : Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : Limits.KernelFork S₂.g) (hc₂ : Limits.IsLimit c₂) (f : c₁.pt c₂.pt) (comm : CategoryStruct.comp (Limits.Fork.ι c₁) φ.τ₂ = CategoryStruct.comp f (Limits.Fork.ι c₂)) :
    (ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φQ = φ.τ₂
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hf₁ : S₁.f = 0) (c₁ : Limits.KernelFork S₁.g) (hc₁ : Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : Limits.KernelFork S₂.g) (hc₂ : Limits.IsLimit c₂) (f : c₁.pt c₂.pt) (comm : CategoryStruct.comp (Limits.Fork.ι c₁) φ.τ₂ = CategoryStruct.comp f (Limits.Fork.ι c₂)) :
    (ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f

    When S₁.g and S₂.g are zero and we have chosen colimit cokernel coforks c₁ and c₂ for S₁.f and S₂.f respectively, the action on right homology of a morphism φ : S₁ ⟶ S₂ of short complexes is given by the unique morphism f : c₁.pt ⟶ c₂.pt such that φ.τ₂ ≫ c₂.π = c₁.π ≫ f.

    Equations
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φH {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hg₁ : S₁.g = 0) (c₁ : Limits.CokernelCofork S₁.f) (hc₁ : Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : Limits.CokernelCofork S₂.f) (hc₂ : Limits.IsColimit c₂) (f : c₁.pt c₂.pt) (comm : CategoryStruct.comp φ.τ₂ (Limits.Cofork.π c₂) = CategoryStruct.comp (Limits.Cofork.π c₁) f) :
    (ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (hg₁ : S₁.g = 0) (c₁ : Limits.CokernelCofork S₁.f) (hc₁ : Limits.IsColimit c₁) (hg₂ : S₂.g = 0) (c₂ : Limits.CokernelCofork S₂.f) (hc₂ : Limits.IsColimit c₂) (f : c₁.pt c₂.pt) (comm : CategoryStruct.comp φ.τ₂ (Limits.Cofork.π c₂) = CategoryStruct.comp (Limits.Cofork.π c₁) f) :
    (ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φQ = f

    When both maps S.f and S.g of a short complex S are zero, this is the right homology map data (for the identity of S) which relates the right homology data RightHomologyData.ofIsLimitKernelFork and ofZeros .

    Equations
    • One or more equations did not get rendered due to their size.

    When both maps S.f and S.g of a short complex S are zero, this is the right homology map data (for the identity of S) which relates the right homology data ofZeros and ofIsColimitCokernelCofork.

    Equations
    • One or more equations did not get rendered due to their size.

    The right homology of a short complex, given by the H field of a chosen right homology data.

    Equations

    The "opcycles" of a short complex, given by the Q field of a chosen right homology data. This is the dual notion to cycles.

    Equations

    When S.f = 0, this is the canonical isomorphism S.opcycles ≅ S.X₂ induced by S.pOpcycles.

    Equations

    The (unique) right homology map data associated to a morphism of short complexes that are both equipped with right homology data.

    Equations

    Given a morphism φ : S₁ ⟶ S₂ of short complexes and right homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced right homology map h₁.H ⟶ h₁.H.

    Equations

    Given a morphism φ : S₁ ⟶ S₂ of short complexes and right homology data h₁ and h₂ for S₁ and S₂ respectively, this is the induced morphism h₁.K ⟶ h₁.K on opcycles.

    Equations

    The morphism S₁.opcycles ⟶ S₂.opcycles induced by a morphism S₁ ⟶ S₂ of short complexes.

    Equations
    theorem CategoryTheory.ShortComplex.rightHomologyMap'_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ S₂) (φ₂ : S₂ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
    rightHomologyMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryStruct.comp (rightHomologyMap' φ₁ h₁ h₂) (rightHomologyMap' φ₂ h₂ h₃)
    theorem CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ S₂) (φ₂ : S₂ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.H Z) :
    theorem CategoryTheory.ShortComplex.opcyclesMap'_comp {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ S₂) (φ₂ : S₂ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
    opcyclesMap' (CategoryStruct.comp φ₁ φ₂) h₁ h₃ = CategoryStruct.comp (opcyclesMap' φ₁ h₁ h₂) (opcyclesMap' φ₂ h₂ h₃)
    theorem CategoryTheory.ShortComplex.opcyclesMap'_comp_assoc {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ S₃ : ShortComplex C} (φ₁ : S₁ S₂) (φ₂ : S₂ S₃) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.Q Z) :

    An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the H fields of right homology data of S₁ and S₂.

    Equations
    • One or more equations did not get rendered due to their size.

    An isomorphism of short complexes S₁ ≅ S₂ induces an isomorphism on the Q fields of right homology data of S₁ and S₂.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    @[simp]

    The isomorphism S₁.rightHomology ≅ S₂.rightHomology induced by an isomorphism of short complexes S₁ ≅ S₂.

    Equations
    • One or more equations did not get rendered due to their size.

    The isomorphism S₁.opcycles ≅ S₂.opcycles induced by an isomorphism of short complexes S₁ ≅ S₂.

    Equations

    The right homology functor ShortComplex C ⥤ C, where the right homology of a short complex S is understood as a kernel of the obvious map S.fromOpcycles : S.opcycles ⟶ S.X₃ where S.opcycles is a cokernel of S.f : S.X₁ ⟶ S.X₂.

    Equations
    • One or more equations did not get rendered due to their size.

    The opcycles functor ShortComplex C ⥤ C which sends a short complex S to S.opcycles which is a cokernel of S.f : S.X₁ ⟶ S.X₂.

    Equations
    • One or more equations did not get rendered due to their size.

    The natural transformation S.X₂ ⟶ S.opcycles for all short complexes S.

    Equations

    The natural transformation S.opcycles ⟶ S.X₃ for all short complexes S.

    Equations

    A left homology map data for a morphism of short complexes induces a right homology map data in the opposite category.

    Equations
    • ψ.op = { φQ := ψ.φK.op, φH := ψ.φH.op, commp := , commg' := , commι := }

    A left homology map data for a morphism of short complexes in the opposite category induces a right homology map data in the original category.

    Equations

    A right homology map data for a morphism of short complexes induces a left homology map data in the opposite category.

    Equations
    • ψ.op = { φK := ψ.φQ.op, φH := ψ.φH.op, commi := , commf' := , commπ := }

    A right homology map data for a morphism of short complexes in the opposite category induces a left homology map data in the original category.

    Equations

    The right homology in the opposite category of the opposite of a short complex identifies to the left homology of this short complex.

    Equations

    The left homology in the opposite category of the opposite of a short complex identifies to the right homology of this short complex.

    Equations

    The opcycles in the opposite category of the opposite of a short complex identifies to the cycles of this short complex.

    Equations

    The cycles in the opposite category of the opposite of a short complex identifies to the opcycles of this short complex.

    Equations
    @[simp]
    @[simp]

    If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₁ induces a right homology data for S₂ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono'. The inverse construction is ofEpiOfIsIsoOfMono'.

    Equations

    If φ : S₁ ⟶ S₂ is a morphism of short complexes such that φ.τ₁ is epi, φ.τ₂ is an iso and φ.τ₃ is mono, then a right homology data for S₂ induces a right homology data for S₁ with the same Q and H fields. This is obtained by dualising LeftHomologyData.ofEpiOfIsIsoOfMono. The inverse construction is ofEpiOfIsIsoOfMono.

    Equations

    If e : S₁ ≅ S₂ is an isomorphism of short complexes and h₁ : RightomologyData S₁, this is the right homology data for S₂ deduced from the isomorphism.

    Equations

    This right homology map data expresses compatibilities of the right homology data constructed by RightHomologyData.ofEpiOfIsIsoOfMono

    Equations
    • One or more equations did not get rendered due to their size.

    This right homology map data expresses compatibilities of the right homology data constructed by RightHomologyData.ofEpiOfIsIsoOfMono'

    Equations
    • One or more equations did not get rendered due to their size.

    If a morphism of short complexes φ : S₁ ⟶ S₂ is such that φ.τ₁ is epi, φ.τ₂ is an iso, and φ.τ₃ is mono, then the induced morphism on right homology is an isomorphism.

    A morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.opcycles ⟶ A.

    Equations

    Via S.pOpcycles : S.X₂ ⟶ S.opcycles, the object S.opcycles identifies to the cokernel of S.f : S.X₁ ⟶ S.X₂.

    Equations

    The canonical isomorphism S.opcycles ≅ cokernel S.f.

    Equations

    The morphism S.rightHomology ⟶ A obtained from a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0.

    Equations

    The following lemmas and instance gives a sufficient condition for a morphism of short complexes to induce an isomorphism on opcycles.

    theorem CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (h₂ : IsIso φ.τ₂) (h₁ : Epi φ.τ₁) (h₁✝ : S₁.RightHomologyData) (h₂✝ : S₂.RightHomologyData) :
    IsIso (opcyclesMap' φ h₁✝ h₂✝)