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 ι : H ⟶ Q
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
ι : H ⟶ Q
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₃
- Q : C
a choice of cokernel of
S.f : S.X₁ ⟶ S.X₂
- H : C
the projection from
S.X₂
the inclusion of the (right) homology in the chosen cokernel of
S.f
the cokernel condition for
p
- hp : Limits.IsColimit (Limits.CokernelCofork.ofπ self.p ⋯)
the kernel condition for
ι
- hι : Limits.IsLimit (Limits.KernelFork.ofι self.ι ⋯)
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
The morphism from the (right) homology attached to a morphism
k : S.X₂ ⟶ A
such that S.f ≫ k = 0
.
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₂
.
For h : S.RightHomologyData
, this is a restatement of h.hι
, saying that
ι : h.H ⟶ h.Q
is a kernel of h.g' : h.Q ⟶ S.X₃
.
The morphism A ⟶ H
induced by a morphism k : A ⟶ Q
such that k ≫ g' = 0
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
- condition : Nonempty 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
- CategoryTheory.ShortComplex.RightHomologyMapData.zero h₁ h₂ = { φQ := 0, φH := 0, commp := ⋯, commg' := ⋯, commι := ⋯ }
The right homology map data associated to the identity morphism of a short complex.
Equations
- CategoryTheory.ShortComplex.RightHomologyMapData.id h = { φQ := CategoryTheory.CategoryStruct.id h.Q, φH := CategoryTheory.CategoryStruct.id h.H, commp := ⋯, commg' := ⋯, commι := ⋯ }
The composition of right homology map data.
Equations
- ψ.comp ψ' = { φQ := CategoryTheory.CategoryStruct.comp ψ.φQ ψ'.φQ, φH := CategoryTheory.CategoryStruct.comp ψ.φH ψ'.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
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
- CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂ = { φQ := φ.τ₂, φH := φ.τ₂, commp := ⋯, commg' := ⋯, commι := ⋯ }
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
- CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm = { φQ := φ.τ₂, φH := f, commp := ⋯, commg' := ⋯, commι := ⋯ }
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
- CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm = { φQ := f, φH := f, commp := ⋯, commg' := ⋯, commι := ⋯ }
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
The canonical map S.rightHomology ⟶ S.opcycles
.
Equations
The projection S.X₂ ⟶ S.opcycles
.
Equations
The canonical map S.opcycles ⟶ X₃
.
Equations
When S.f = 0
, this is the canonical isomorphism S.opcycles ≅ S.X₂
induced by S.pOpcycles
.
Equations
When S.g = 0
, this is the canonical isomorphism S.opcycles ≅ S.rightHomology
induced
by S.rightHomologyι
.
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 (right) homology map S₁.rightHomology ⟶ S₂.rightHomology
induced by a morphism
S₁ ⟶ S₂
of short complexes.
The morphism S₁.opcycles ⟶ S₂.opcycles
induced by a morphism S₁ ⟶ S₂
of short complexes.
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.
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
- CategoryTheory.ShortComplex.opcyclesMapIso e = { hom := CategoryTheory.ShortComplex.opcyclesMap e.hom, inv := CategoryTheory.ShortComplex.opcyclesMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
The isomorphism S.rightHomology ≅ h.H
induced by a right homology data h
for a
short complex S
.
The isomorphism S.opcycles ≅ h.Q
induced by a right homology data h
for a
short complex S
.
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.rightHomology ⟶ S.opcycles
for all short complexes S
.
Equations
- CategoryTheory.ShortComplex.rightHomologyιNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.rightHomologyι, naturality := ⋯ }
The natural transformation S.X₂ ⟶ S.opcycles
for all short complexes S
.
Equations
- CategoryTheory.ShortComplex.pOpcyclesNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.pOpcycles, naturality := ⋯ }
The natural transformation S.opcycles ⟶ S.X₃
for all short complexes S
.
Equations
- CategoryTheory.ShortComplex.fromOpcyclesNatTrans C = { app := fun (S : CategoryTheory.ShortComplex C) => S.fromOpcycles, naturality := ⋯ }
A left homology map data for a morphism of short complexes induces a right homology map data in the opposite category.
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.
A right homology map data for a morphism of short complexes induces a left homology map data in the opposite category.
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.
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
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'
.
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
.
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.
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.
The opposite of the right homology functor is the left homology functor.
Equations
The opposite of the left homology functor is the right homology functor.
Equations
A morphism k : S.X₂ ⟶ A
such that S.f ≫ k = 0
descends to a morphism S.opcycles ⟶ A
.
Equations
- S.descOpcycles k hk = S.rightHomologyData.descQ k hk
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
- S.opcyclesIsoCokernel = { hom := S.descOpcycles (CategoryTheory.Limits.cokernel.π S.f) ⋯, inv := CategoryTheory.Limits.cokernel.desc S.f S.pOpcycles ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
The morphism S.rightHomology ⟶ A
obtained from a morphism k : S.X₂ ⟶ A
such that S.f ≫ k = 0.
Equations
- S.descRightHomology k hk = CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.descOpcycles k hk)
Via S.rightHomologyι : S.rightHomology ⟶ S.opcycles
, the object S.rightHomology
identifies
to the kernel of S.fromOpcycles : S.opcycles ⟶ S.X₃
.
Equations
The right homology of a short complex S
identifies to the kernel of the canonical
morphism cokernel S.f ⟶ S.X₃
.
The following lemmas and instance gives a sufficient condition for a morphism of short complexes to induce an isomorphism on opcycles.