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 homology data for a short complex consists of two compatible left and right homology data
- left : S.LeftHomologyData
a left homology data
- right : S.RightHomologyData
a right homology data
- iso : self.left.H ≅ self.right.H
the compatibility isomorphism relating the two dual notions of
LeftHomologyData
andRightHomologyData
- comm : CategoryTheory.CategoryStruct.comp self.left.π (CategoryTheory.CategoryStruct.comp self.iso.hom self.right.ι) = CategoryTheory.CategoryStruct.comp self.left.i self.right.p
the pentagon relation expressing the compatibility of the left and right homology data
Instances For
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.
- 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
Instances For
Equations
- CategoryTheory.ShortComplex.HomologyMapData.instInhabited = { default := { left := default, right := default } }
Equations
- CategoryTheory.ShortComplex.HomologyMapData.instUnique = Unique.mk' (CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
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.
Equations
- CategoryTheory.ShortComplex.HomologyMapData.homologyMapData φ h₁ h₂ = default
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
When the first map S.f
is zero, this is the homology data on S
given
by the chosen kernel S.g
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
When the second map S.g
is zero, this is the homology data on S
given by
the chosen cokernel S.f
Equations
- One or more equations did not get rendered due to their size.
Instances For
When both S.f
and S.g
are zero, the middle object S.X₂
gives a homology data on S
Equations
- One or more equations did not get rendered due to their size.
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'
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
Instances For
A homology data for a short complex S
induces a homology data for S.op
.
Equations
- h.op = { left := h.right.op, right := h.left.op, iso := h.iso.op, comm := ⋯ }
Instances For
A homology data for a short complex S
in the opposite category
induces a homology data for S.unop
.
Equations
- h.unop = { left := h.right.unop, right := h.left.unop, iso := h.iso.unop, comm := ⋯ }
Instances For
A short complex S
has homology when there exists a S.HomologyData
- condition : Nonempty S.HomologyData
the condition that there exists a homology data
Instances
A chosen S.HomologyData
for a short complex S
that has homology
Equations
- S.homologyData = ⋯.some
Instances For
The homology map data associated to the identity morphism of a short complex.
Equations
- CategoryTheory.ShortComplex.HomologyMapData.id h = { left := CategoryTheory.ShortComplex.LeftHomologyMapData.id h.left, right := CategoryTheory.ShortComplex.RightHomologyMapData.id h.right }
Instances For
The homology map data associated to the zero morphism between two short complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composition of homology map data.
Equations
- ψ.comp ψ' = { left := ψ.left.comp ψ'.left, right := ψ.right.comp ψ'.right }
Instances For
A homology map data for a morphism of short complexes induces a homology map data in the opposite category.
Equations
- ψ.op = { left := ψ.right.op, right := ψ.left.op }
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.
Equations
- ψ.unop = { left := ψ.right.unop, right := ψ.left.unop }
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.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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₂.ι
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
This homology map data expresses compatibilities of the homology data
constructed by HomologyData.ofEpiOfIsIsoOfMono
Equations
- One or more equations did not get rendered due to their size.
Instances For
This homology map data expresses compatibilities of the homology data
constructed by HomologyData.ofEpiOfIsIsoOfMono'
Equations
- One or more equations did not get rendered due to their size.
Instances For
The homology of a short complex is the left.H
field of a chosen homology data.
Equations
- S.homology = S.homologyData.left.H
Instances For
When a short complex has homology, this is the canonical isomorphism
S.leftHomology ≅ S.homology
.
Equations
- S.leftHomologyIso = CategoryTheory.ShortComplex.leftHomologyMapIso' (CategoryTheory.Iso.refl S) S.leftHomologyData S.homologyData.left
Instances For
When a short complex has homology, this is the canonical isomorphism
S.rightHomology ≅ S.homology
.
Equations
- S.rightHomologyIso = CategoryTheory.ShortComplex.rightHomologyMapIso' (CategoryTheory.Iso.refl S) S.rightHomologyData S.homologyData.right ≪≫ S.homologyData.iso.symm
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
.
Equations
- CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ h₁.left h₂.left
Instances For
The homology map S₁.homology ⟶ S₂.homology
induced by a morphism
S₁ ⟶ S₂
of short complexes.
Equations
- CategoryTheory.ShortComplex.homologyMap φ = CategoryTheory.ShortComplex.homologyMap' φ S₁.homologyData S₂.homologyData
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The homology isomorphism S₁.homology ⟶ S₂.homology
induced by an isomorphism
S₁ ≅ S₂
of short complexes.
Equations
- CategoryTheory.ShortComplex.homologyMapIso e = { hom := CategoryTheory.ShortComplex.homologyMap e.hom, inv := CategoryTheory.ShortComplex.homologyMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
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
.
Equations
- CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ = h₂.liftH (h₁.descH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯
Instances For
If a short complex S
has both a left and right homology,
this is the canonical morphism S.leftHomology ⟶ S.rightHomology
.
Equations
- S.leftRightHomologyComparison = CategoryTheory.ShortComplex.leftRightHomologyComparison' S.leftHomologyData S.rightHomologyData
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
We shall say that a category C
is a category with homology when all short complexes
have homology.
- hasHomology : ∀ (S : CategoryTheory.ShortComplex C), S.HasHomology
Instances
The homology functor ShortComplex C ⥤ C
for a category C
with homology.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical morphism S.cycles ⟶ S.homology
for a short complex S
that has homology.
Equations
- S.homologyπ = CategoryTheory.CategoryStruct.comp S.leftHomologyπ S.leftHomologyIso.hom
Instances For
The canonical morphism S.homology ⟶ S.opcycles
for a short complex S
that has homology.
Equations
- S.homologyι = CategoryTheory.CategoryStruct.comp S.rightHomologyIso.inv S.rightHomologyι
Instances For
The homology S.homology
of a short complex is
the cokernel of the morphism S.toCycles : S.X₁ ⟶ S.cycles
.
Equations
- S.homologyIsCokernel = S.leftHomologyIsCokernel.ofIsoColimit (CategoryTheory.Limits.Cofork.ext S.leftHomologyIso ⋯)
Instances For
The homology S.homology
of a short complex is
the kernel of the morphism S.fromOpcycles : S.opcycles ⟶ S.X₃
.
Equations
- S.homologyIsKernel = S.rightHomologyIsKernel.ofIsoLimit (CategoryTheory.Limits.Fork.ext S.rightHomologyIso ⋯)
Instances For
Given a morphism k : S.cycles ⟶ A
such that S.toCycles ≫ k = 0
, this is the
induced morphism S.homology ⟶ A
.
Equations
- S.descHomology k hk = S.homologyIsCokernel.desc (CategoryTheory.Limits.CokernelCofork.ofπ k hk)
Instances For
Given a morphism k : A ⟶ S.opcycles
such that k ≫ S.fromOpcycles = 0
, this is the
induced morphism A ⟶ S.homology
.
Equations
- S.liftHomology k hk = S.homologyIsKernel.lift (CategoryTheory.Limits.KernelFork.ofι k hk)
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
.
Equations
Instances For
The canonical isomorphism S.op.homology ≅ Opposite.op S.homology
when a short
complex S
has homology.
Equations
Instances For
The natural isomorphism (homologyFunctor C).op ≅ opFunctor C ⋙ homologyFunctor Cᵒᵖ
which relates the homology in C
and in Cᵒᵖ
.
Equations
- CategoryTheory.ShortComplex.homologyFunctorOpNatIso C = CategoryTheory.NatIso.ofComponents (fun (S : (CategoryTheory.ShortComplex C)ᵒᵖ) => (Opposite.unop S).homologyOpIso.symm) ⋯
Instances For
The canonical isomorphism S.cycles ≅ S.homology
when S.f = 0
.
Equations
- S.asIsoHomologyπ hf = CategoryTheory.asIso S.homologyπ
Instances For
The canonical isomorphism S.homology ≅ S.opcycles
when S.g = 0
.
Equations
- S.asIsoHomologyι hg = CategoryTheory.asIso S.homologyι