Left Homology of short complexes #
Given a short complex S : ShortComplex C
, which consists of two composable
maps f : X₁ ⟶ X₂
and g : X₂ ⟶ X₃
such that f ≫ g = 0
, we shall define
here the "left homology" S.leftHomology
of S
. For this, we introduce the
notion of "left homology data". Such an h : S.LeftHomologyData
consists of the
data of morphisms i : K ⟶ X₂
and π : K ⟶ H
such that i
identifies
K
with the kernel of g : X₂ ⟶ X₃
, and that π
identifies H
with the cokernel
of the induced map f' : X₁ ⟶ K
.
When such a S.LeftHomologyData
exists, we shall say that [S.HasLeftHomology]
and we define S.leftHomology
to be the H
field of a chosen left homology data.
Similarly, we define S.cycles
to be the K
field.
The dual notion is defined in RightHomologyData.lean
. 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
.
- K : C
a choice of kernel of
S.g : S.X₂ ⟶ S.X₃
- H : C
- i : s.K ⟶ S.X₂
the inclusion of cycles in
S.X₂
- π : s.K ⟶ s.H
the projection from cycles to the (left) homology
- wi : CategoryTheory.CategoryStruct.comp s.i S.g = 0
the kernel condition for
i
- hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι s.i (_ : CategoryTheory.CategoryStruct.comp s.i S.g = 0))
- wπ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift s.hi (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) s.π = 0
the cokernel condition for
π
- hπ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ s.π (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.IsLimit.lift s.hi (CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))) s.π = 0))
A left homology data for a short complex S
consists of morphisms i : K ⟶ S.X₂
and
π : K ⟶ H
such that i
identifies K
to the kernel of g : S.X₂ ⟶ S.X₃
,
and that π
identifies H
to the cokernel of the induced map f' : S.X₁ ⟶ K
Instances For
The chosen kernels and cokernels of the limits API give a LeftHomologyData
Instances For
Any morphism k : A ⟶ S.X₂
that is a cycle (i.e. k ≫ S.g = 0
) lifts
to a morphism A ⟶ K
Instances For
The (left) homology class A ⟶ H
attached to a cycle k : A ⟶ S.X₂
Instances For
Given h : LeftHomologyData S
, this is morphism S.X₁ ⟶ h.K
induced
by S.f : S.X₁ ⟶ S.X₂
and the fact that h.K
is a kernel of S.g : S.X₂ ⟶ S.X₃
.
Instances For
For h : S.LeftHomologyData
, this is a restatement of h.hπ
, saying that
π : h.K ⟶ h.H
is a cokernel of h.f' : S.X₁ ⟶ h.K
.
Instances For
The morphism H ⟶ A
induced by a morphism k : K ⟶ A
such that f' ≫ k = 0
Instances For
When the second map S.g
is zero, this is the left homology data on S
given
by any colimit cokernel cofork of S.f
Instances For
When the second map S.g
is zero, this is the left homology data on S
given by
the chosen cokernel S.f
Instances For
When the first map S.f
is zero, this is the left 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 left homology data on S
given
by the chosen kernel S.g
Instances For
When both S.f
and S.g
are zero, the middle object S.X₂
gives a left homology data on S
Instances For
- condition : Nonempty (CategoryTheory.ShortComplex.LeftHomologyData S)
A short complex S
has left homology when there exists a S.LeftHomologyData
Instances
A chosen S.LeftHomologyData
for a short complex S
that has left homology
Instances For
- φK : h₁.K ⟶ h₂.K
the induced map on cycles
- φH : h₁.H ⟶ h₂.H
the induced map on left homology
- commi : CategoryTheory.CategoryStruct.comp s.φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂
commutation with
i
- commf' : CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.LeftHomologyData.f' h₁) s.φK = CategoryTheory.CategoryStruct.comp φ.τ₁ (CategoryTheory.ShortComplex.LeftHomologyData.f' h₂)
commutation with
f'
- commπ : CategoryTheory.CategoryStruct.comp h₁.π s.φH = CategoryTheory.CategoryStruct.comp s.φK h₂.π
commutation with
π
Given left homology data h₁
and h₂
for two short complexes S₁
and S₂
,
a LeftHomologyMapData
for a morphism φ : S₁ ⟶ S₂
consists of a description of the induced morphisms on the K
(cycles)
and H
(left homology) fields of h₁
and h₂
.
Instances For
The left homology map data associated to the zero morphism between two short complexes.
Instances For
The left homology map data associated to the identity morphism of a short complex.
Instances For
The composition of left homology map data.
Instances For
When S₁.f
, S₁.g
, S₂.f
and S₂.g
are all zero, the action on left homology of a
morphism φ : S₁ ⟶ S₂
is given by the action φ.τ₂
on the middle objects.
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 left 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 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 left 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 both maps S.f
and S.g
of a short complex S
are zero, this is the left homology map
data (for the identity of S
) which relates the left homology data ofZeros
and
ofIsColimitCokernelCofork
.
Instances For
When both maps S.f
and S.g
of a short complex S
are zero, this is the left homology map
data (for the identity of S
) which relates the left homology data
LeftHomologyData.ofIsLimitKernelFork
and ofZeros
.
Instances For
The left homology of a short complex, given by the H
field of a chosen left homology data.
Instances For
The cycles of a short complex, given by the K
field of a chosen left homology data.
Instances For
The "homology class" map S.cycles ⟶ S.leftHomology
.
Instances For
The inclusion S.cycles ⟶ S.X₂
.
Instances For
The "boundaries" map S.X₁ ⟶ S.cycles
. (Note that in this homology API, we make no use
of the "image" of this morphism, which under some categorical assumptions would be a subobject
of S.X₂
contained in S.cycles
.)
Instances For
When S.g = 0
, this is the canonical isomorphism S.cycles ≅ S.X₂
induced by S.iCycles
.
Instances For
When S.f = 0
, this is the canonical isomorphism S.cycles ≅ S.leftHomology
induced
by S.leftHomologyπ
.
Instances For
The (unique) left homology map data associated to a morphism of short complexes that are both equipped with left homology data.
Instances For
Given a morphism φ : S₁ ⟶ S₂
of short complexes and left homology data h₁
and h₂
for S₁
and S₂
respectively, this is the induced left homology map h₁.H ⟶ h₁.H
.
Instances For
Given a morphism φ : S₁ ⟶ S₂
of short complexes and left homology data h₁
and h₂
for S₁
and S₂
respectively, this is the induced morphism h₁.K ⟶ h₁.K
on cycles.
Instances For
The (left) homology map S₁.leftHomology ⟶ S₂.leftHomology
induced by a morphism
S₁ ⟶ S₂
of short complexes.
Instances For
The morphism S₁.cycles ⟶ S₂.cycles
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 left homology data of S₁
and S₂
.
Instances For
An isomorphism of short complexes S₁ ≅ S₂
induces an isomorphism on the K
fields
of left homology data of S₁
and S₂
.
Instances For
The isomorphism S₁.leftHomology ≅ S₂.leftHomology
induced by an isomorphism of
short complexes S₁ ≅ S₂
.
Instances For
The isomorphism S₁.cycles ≅ S₂.cycles
induced by an isomorphism
of short complexes S₁ ≅ S₂
.
Instances For
The isomorphism S.leftHomology ≅ h.H
induced by a left homology data h
for a
short complex S
.
Instances For
The isomorphism S.cycles ≅ h.K
induced by a left homology data h
for a
short complex S
.
Instances For
The left homology functor ShortComplex C ⥤ C
, where the left homology of a
short complex S
is understood as a cokernel of the obvious map S.toCycles : S.X₁ ⟶ S.cycles
where S.cycles
is a kernel of S.g : S.X₂ ⟶ S.X₃
.
Instances For
The cycles functor ShortComplex C ⥤ C
which sends a short complex S
to S.cycles
which is a kernel of S.g : S.X₂ ⟶ S.X₃
.
Instances For
The natural transformation S.cycles ⟶ S.leftHomology
for all short complexes S
.
Instances For
The natural transformation S.cycles ⟶ S.X₂
for all short complexes S
.
Instances For
The natural transformation S.X₁ ⟶ S.cycles
for all short complexes S
.
Instances For
If φ : S₁ ⟶ S₂
is a morphism of short complexes such that φ.τ₁
is epi, φ.τ₂
is an iso
and φ.τ₃
is mono, then a left homology data for S₁
induces a left homology data for S₂
with
the same K
and H
fields. 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 left homology data for S₂
induces a left homology data for S₁
with
the same K
and H
fields. The inverse construction is ofEpiOfIsIsoOfMono
.
Instances For
If e : S₁ ≅ S₂
is an isomorphism of short complexes and h₁ : LeftHomologyData S₁
,
this is the left homology data for S₂
deduced from the isomorphism.
Instances For
This left homology map data expresses compatibilities of the left homology data
constructed by LeftHomologyData.ofEpiOfIsIsoOfMono
Instances For
This left homology map data expresses compatibilities of the left homology data
constructed by LeftHomologyData.ofEpiOfIsIsoOfMono'
Instances For
If a morphism of short complexes φ : S₁ ⟶ S₂
is such that φ.τ₁
is epi, φ.τ₂
is an iso,
and φ.τ₃
is mono, then the induced morphism on left homology is an isomorphism.
A morphism k : A ⟶ S.X₂
such that k ≫ S.g = 0
lifts to a morphism A ⟶ S.cycles
.
Instances For
Via S.iCycles : S.cycles ⟶ S.X₂
, the object S.cycles
identifies to the
kernel of S.g : S.X₂ ⟶ S.X₃
.
Instances For
The canonical isomorphism S.cycles ≅ kernel S.g
.
Instances For
The morphism A ⟶ S.leftHomology
obtained from a morphism k : A ⟶ S.X₂
such that k ≫ S.g = 0.
Instances For
Via S.leftHomologyπ : S.cycles ⟶ S.leftHomology
, the object S.leftHomology
identifies
to the cokernel of S.toCycles : S.X₁ ⟶ S.cycles
.
Instances For
The left homology of a short complex S
identifies to the cokernel of the canonical
morphism S.X₁ ⟶ kernel S.g
.
Instances For
The following lemmas and instance gives a sufficient condition for a morphism of short complexes to induce an isomorphism on cycles.