Homology of short complexes #
In this file, we shall define the homology of short complexes S
, i.e. diagrams
f : X₁ ⟶ X₂
and g : X₂ ⟶ X₃
such that f ≫ g = 0
. We shall say that
[S.HasHomology]
when there exists h : S.HomologyData
. A homology data
for S
consists of compatible left/right homology data left
and right
. The
left homology data left
involves an object left.H
that is a cokernel of the canonical
map S.X₁ ⟶ K
where K
is a kernel of g
. On the other hand, the dual notion right.H
is a kernel of the canonical morphism Q ⟶ S.X₃
when Q
is a cokernel of f
.
The compatibility that is required involves an isomorphism left.H ≅ right.H
which
makes a certain pentagon commute. When such a homology data exists, S.homology
shall be defined as h.left.H
for a chosen h : S.HomologyData
.
This definition requires very little assumption on the category (only the existence of zero morphisms). We shall prove that in abelian categories, all short complexes have homology data.
Note: This definition arose by the end of the Liquid Tensor Experiment which
contained a structure has_homology
which is quite similar to S.HomologyData
.
After the category ShortComplex C
was introduced by J. Riou, A. Topaz suggested
such a structure could be used as a basis for the definition of homology.
a left homology data
a right homology data
- iso : s.left.H ≅ s.right.H
the compatibility isomorphism relating the two dual notions of
LeftHomologyData
andRightHomologyData
- comm : CategoryTheory.CategoryStruct.comp s.left.π (CategoryTheory.CategoryStruct.comp s.iso.hom s.right.ι) = CategoryTheory.CategoryStruct.comp s.left.i s.right.p
the pentagon relation expressing the compatibility of the left and right homology data
A homology data for a short complex consists of two compatible left and right homology data
Instances For
- left : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left
a left homology map data
- right : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right
a right homology map data
A homology map data for a morphism φ : S₁ ⟶ S₂
where both S₁
and S₂
are
equipped with homology data consists of left and right homology map data.
Instances For
A choice of the (unique) homology map data associated with a morphism
φ : S₁ ⟶ S₂
where both short complexes S₁
and S₂
are equipped with
homology data.
Instances For
When the first map S.f
is zero, this is the 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 homology data on S
given
by the chosen kernel S.g
Instances For
When the second map S.g
is zero, this is the 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 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 homology data on S
Instances For
If φ : S₁ ⟶ S₂
is a morphism of short complexes such that φ.τ₁
is epi, φ.τ₂
is an iso
and φ.τ₃
is mono, then a homology data for S₁
induces a homology data for S₂
.
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 homology data for S₂
induces a homology data for S₁
.
The inverse construction is ofEpiOfIsIsoOfMono
.
Instances For
If e : S₁ ≅ S₂
is an isomorphism of short complexes and h₁ : HomologyData S₁
,
this is the homology data for S₂
deduced from the isomorphism.
Instances For
A homology data for a short complex S
induces a homology data for S.op
.
Instances For
A homology data for a short complex S
in the opposite category
induces a homology data for S.unop
.
Instances For
- condition : Nonempty (CategoryTheory.ShortComplex.HomologyData S)
the condition that there exists a homology data
A short complex S
has homology when there exists a S.HomologyData
Instances
A chosen S.HomologyData
for a short complex S
that has homology
Instances For
The homology map data associated to the identity morphism of a short complex.
Instances For
The homology map data associated to the zero morphism between two short complexes.
Instances For
The composition of homology map data.
Instances For
A homology map data for a morphism of short complexes induces a homology map data in the opposite category.
Instances For
A homology map data for a morphism of short complexes in the opposite category induces a homology map data in the original category.
Instances For
When S₁.f
, S₁.g
, S₂.f
and S₂.g
are all zero, the action on 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 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 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 homology map
data (for the identity of S
) which relates the 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 homology map
data (for the identity of S
) which relates the homology data
HomologyData.ofIsLimitKernelFork
and ofZeros
.
Instances For
This homology map data expresses compatibilities of the homology data
constructed by HomologyData.ofEpiOfIsIsoOfMono
Instances For
This homology map data expresses compatibilities of the homology data
constructed by HomologyData.ofEpiOfIsIsoOfMono'
Instances For
The homology of a short complex is the left.H
field of a chosen homology data.
Instances For
When a short complex has homology, this is the canonical isomorphism
S.leftHomology ≅ S.homology
.
Instances For
When a short complex has homology, this is the canonical isomorphism
S.rightHomology ≅ S.homology
.
Instances For
When a short complex has homology, its homology can be computed using any left homology data.
Instances For
When a short complex has homology, its homology can be computed using any right homology data.
Instances For
Given a morphism φ : S₁ ⟶ S₂
of short complexes and homology data h₁
and h₂
for S₁
and S₂
respectively, this is the induced homology map h₁.left.H ⟶ h₁.left.H
.
Instances For
The homology map S₁.homology ⟶ S₂.homology
induced by a morphism
S₁ ⟶ S₂
of short complexes.
Instances For
Given an isomorphism S₁ ≅ S₂
of short complexes and homology data h₁
and h₂
for S₁
and S₂
respectively, this is the induced homology isomorphism h₁.left.H ≅ h₁.left.H
.
Instances For
The homology isomorphism S₁.homology ⟶ S₂.homology
induced by an isomorphism
S₁ ≅ S₂
of short complexes.
Instances For
If a short complex S
has both a left homology data h₁
and a right homology data h₂
,
this is the canonical morphism h₁.H ⟶ h₂.H
.
Instances For
If a short complex S
has both a left and right homology,
this is the canonical morphism S.leftHomology ⟶ S.rightHomology
.
Instances For
This is the homology data for a short complex S
that is obtained
from a left homology data h₁
and a right homology data h₂
when the comparison
morphism leftRightHomologyComparison' h₁ h₂ : h₁.H ⟶ h₂.H
is an isomorphism.
Instances For
- hasHomology : ∀ (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.HasHomology S
We shall say that a category C
is a category with homology when all short complexes
have homology.
Instances
The homology functor ShortComplex C ⥤ C
for a category C
with homology.
Instances For
The canonical morphism S.cycles ⟶ S.homology
for a short complex S
that has homology.
Instances For
The canonical morphism S.homology ⟶ S.opcycles
for a short complex S
that has homology.
Instances For
The homology S.homology
of a short complex is
the cokernel of the morphism S.toCycles : S.X₁ ⟶ S.cycles
.
Instances For
The homology S.homology
of a short complex is
the kernel of the morphism S.fromOpcycles : S.opcycles ⟶ S.X₃
.
Instances For
Given a morphism k : S.cycles ⟶ A
such that S.toCycles ≫ k = 0
, this is the
induced morphism S.homology ⟶ A
.
Instances For
Given a morphism k : A ⟶ S.opcycles
such that k ≫ S.fromOpcycles = 0
, this is the
induced morphism A ⟶ S.homology
.
Instances For
The homology of a short complex S
identifies to the kernel of the induced morphism
cokernel S.f ⟶ S.X₃
.
Instances For
The homology of a short complex S
identifies to the cokernel of the induced morphism
S.X₁ ⟶ kernel S.g
.
Instances For
The canonical isomorphism S.op.homology ≅ Opposite.op S.homology
when a short
complex S
has homology.
Instances For
The natural isomorphism (homologyFunctor C).op ≅ opFunctor C ⋙ homologyFunctor Cᵒᵖ
which relates the homology in C
and in Cᵒᵖ
.
Instances For
The canonical isomorphism S.cycles ≅ S.homology
when S.f = 0
.
Instances For
The canonical isomorphism S.homology ≅ S.opcycles
when S.g = 0
.