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
.
- Q : C
a choice of cokernel of
S.f : S.X₁ ⟶ S.X₂
- H : C
- p : S.X₂ ⟶ s.Q
the projection from
S.X₂
- ι : s.H ⟶ s.Q
the inclusion of the (right) homology in the chosen cokernel of
S.f
- wp : CategoryTheory.CategoryStruct.comp S.f s.p = 0
the cokernel condition for
p
- hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ s.p (_ : CategoryTheory.CategoryStruct.comp S.f s.p = 0))
- wι : CategoryTheory.CategoryStruct.comp s.ι (CategoryTheory.Limits.IsColimit.desc s.hp (CategoryTheory.Limits.CokernelCofork.ofπ S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) = 0
the kernel condition for
ι
- hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι s.ι (_ : CategoryTheory.CategoryStruct.comp s.ι (CategoryTheory.Limits.IsColimit.desc s.hp (CategoryTheory.Limits.CokernelCofork.ofπ S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) = 0))
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₃
Instances For
The chosen cokernels and kernels of the limits API give a RightHomologyData
Instances For
Any morphism k : S.X₂ ⟶ A
such that S.f ≫ k = 0
descends
to a morphism Q ⟶ A
Instances For
The morphism from the (right) homology attached to a morphism
k : S.X₂ ⟶ A
such that S.f ≫ k = 0
.
Instances For
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₂
.
Instances For
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₃
.
Instances For
The morphism A ⟶ H
induced by a morphism k : A ⟶ Q
such that k ≫ g' = 0
Instances For
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
Instances For
When the first map S.f
is zero, this is the right homology data on S
given by
the chosen kernel S.g
Instances For
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
Instances For
When the second map S.g
is zero, this is the right homology data on S
given
by the chosen cokernel S.f
Instances For
When both S.f
and S.g
are zero, the middle object S.X₂
gives a right homology data on S
Instances For
- condition : Nonempty (CategoryTheory.ShortComplex.RightHomologyData S)
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
Instances For
A right homology data for a short complex S
induces a left homology data for S.op
.
Instances For
A right homology data for a short complex S
in the opposite category
induces a left homology data for S.unop
.
Instances For
A left homology data for a short complex S
induces a right homology data for S.op
.
Instances For
A left homology data for a short complex S
in the opposite category
induces a right homology data for S.unop
.
Instances For
- φQ : h₁.Q ⟶ h₂.Q
the induced map on opcycles
- φH : h₁.H ⟶ h₂.H
the induced map on right homology
- commp : CategoryTheory.CategoryStruct.comp h₁.p s.φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p
commutation with
p
- commg' : CategoryTheory.CategoryStruct.comp s.φQ (CategoryTheory.ShortComplex.RightHomologyData.g' h₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.RightHomologyData.g' h₁) φ.τ₃
commutation with
g'
- commι : CategoryTheory.CategoryStruct.comp s.φH h₂.ι = CategoryTheory.CategoryStruct.comp h₁.ι s.φQ
commutation with
ι
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₂
.
Instances For
The right homology map data associated to the zero morphism between two short complexes.
Instances For
The right homology map data associated to the identity morphism of a short complex.
Instances For
The composition of right homology map data.
Instances For
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.
Instances For
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₂.ι
.
Instances For
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
.
Instances For
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
.
Instances For
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
.
Instances For
The right homology of a short complex,
given by the H
field of a chosen right homology data.
Instances For
The "opcycles" of a short complex, given by the Q
field of a chosen right homology data.
This is the dual notion to cycles.
Instances For
The canonical map S.rightHomology ⟶ S.opcycles
.
Instances For
The projection S.X₂ ⟶ S.opcycles
.
Instances For
The canonical map S.opcycles ⟶ X₃
.
Instances For
When S.f = 0
, this is the canonical isomorphism S.opcycles ≅ S.X₂
induced by S.pOpcycles
.
Instances For
When S.g = 0
, this is the canonical isomorphism S.opcycles ≅ S.rightHomology
induced
by S.rightHomologyι
.
Instances For
The (unique) right homology map data associated to a morphism of short complexes that are both equipped with right homology data.
Instances For
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
.
Instances For
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.
Instances For
The (right) homology map S₁.rightHomology ⟶ S₂.rightHomology
induced by a morphism
S₁ ⟶ S₂
of short complexes.
Instances For
The morphism S₁.opcycles ⟶ S₂.opcycles
induced by a morphism S₁ ⟶ S₂
of short complexes.
Instances For
An isomorphism of short complexes S₁ ≅ S₂
induces an isomorphism on the H
fields
of right homology data of S₁
and S₂
.
Instances For
An isomorphism of short complexes S₁ ≅ S₂
induces an isomorphism on the Q
fields
of right homology data of S₁
and S₂
.
Instances For
The isomorphism S₁.rightHomology ≅ S₂.rightHomology
induced by an isomorphism of
short complexes S₁ ≅ S₂
.
Instances For
The isomorphism S₁.opcycles ≅ S₂.opcycles
induced by an isomorphism
of short complexes S₁ ≅ S₂
.
Instances For
The isomorphism S.rightHomology ≅ h.H
induced by a right homology data h
for a
short complex S
.
Instances For
The isomorphism S.opcycles ≅ h.Q
induced by a right homology data h
for a
short complex S
.
Instances For
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₂
.
Instances For
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₂
.
Instances For
The natural transformation S.rightHomology ⟶ S.opcycles
for all short complexes S
.
Instances For
The natural transformation S.X₂ ⟶ S.opcycles
for all short complexes S
.
Instances For
The natural transformation S.opcycles ⟶ S.X₃
for all short complexes S
.
Instances For
A left homology map data for a morphism of short complexes induces a right homology map data in the opposite category.
Instances For
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.
Instances For
A right homology map data for a morphism of short complexes induces a left homology map data in the opposite category.
Instances For
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.
Instances For
The right homology in the opposite category of the opposite of a short complex identifies to the left homology of this short complex.
Instances For
The left homology in the opposite category of the opposite of a short complex identifies to the right homology of this short complex.
Instances For
The opcycles in the opposite category of the opposite of a short complex identifies to the cycles of this short complex.
Instances For
The cycles in the opposite category of the opposite of a short complex identifies to the opcycles of this short complex.
Instances For
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'
.
Instances For
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
.
Instances For
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.