Functors which preserves homology #
If F : C ⥤ D
is a functor between categories with zero morphisms, we shall
say that F
preserves homology when F
preserves both kernels and cokernels.
This typeclass is named [F.PreservesHomology]
, and is automatically
satisfied when F
preserves both finite limits and finite colimits.
If S : ShortComplex C
and [F.PreservesHomology]
, then there is an
isomorphism S.mapHomologyIso F : (S.map F).homology ≅ F.obj S.homology
, which
is part of the natural isomorphism homologyFunctorIso F
between the functors
F.mapShortComplex ⋙ homologyFunctor D
and homologyFunctor C ⋙ F
.
A functor preserves homology when it preserves both kernels and cokernels.
- preservesKernels ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F
the functor preserves kernels
- preservesCokernels ⦃X Y : C⦄ (f : X ⟶ Y) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F
the functor preserves cokernels
Instances
A functor which preserves homology preserves kernels.
A functor which preserves homology preserves cokernels.
A left homology data h
of a short complex S
is preserved by a functor F
is
F
preserves the kernel of S.g : S.X₂ ⟶ S.X₃
and the cokernel of h.f' : S.X₁ ⟶ h.K
.
the functor preserves the kernel of
S.g : S.X₂ ⟶ S.X₃
.the functor preserves the cokernel of
h.f' : S.X₁ ⟶ h.K
.
Instances
When a left homology data is preserved by a functor F
, this functor
preserves the kernel of S.g : S.X₂ ⟶ S.X₃
.
When a left homology data h
is preserved by a functor F
, this functor
preserves the cokernel of h.f' : S.X₁ ⟶ h.K
.
When a left homology data h
of a short complex S
is preserved by a functor F
,
this is the induced left homology data h.map F
for the short complex S.map F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a left homology map data ψ : LeftHomologyMapData φ h₁ h₂
such that
both left homology data h₁
and h₂
are preserved by a functor F
, this is
the induced left homology map data for the morphism F.mapShortComplex.map φ
.
Equations
- ψ.map F = { φK := F.map ψ.φK, φH := F.map ψ.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }
Instances For
A right homology data h
of a short complex S
is preserved by a functor F
is
F
preserves the cokernel of S.f : S.X₁ ⟶ S.X₂
and the kernel of h.g' : h.Q ⟶ S.X₃
.
the functor preserves the cokernel of
S.f : S.X₁ ⟶ S.X₂
.the functor preserves the kernel of
h.g' : h.Q ⟶ S.X₃
.
Instances
When a right homology data is preserved by a functor F
, this functor
preserves the cokernel of S.f : S.X₁ ⟶ S.X₂
.
When a right homology data h
is preserved by a functor F
, this functor
preserves the kernel of h.g' : h.Q ⟶ S.X₃
.
When a right homology data h
of a short complex S
is preserved by a functor F
,
this is the induced right homology data h.map F
for the short complex S.map F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a right homology map data ψ : RightHomologyMapData φ h₁ h₂
such that
both right homology data h₁
and h₂
are preserved by a functor F
, this is
the induced right homology map data for the morphism F.mapShortComplex.map φ
.
Equations
- ψ.map F = { φQ := F.map ψ.φQ, φH := F.map ψ.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }
Instances For
When a homology data h
of a short complex S
is such that both h.left
and
h.right
are preserved by a functor F
, this is the induced homology data
h.map F
for the short complex S.map F
.
Equations
- h.map F = { left := h.left.map F, right := h.right.map F, iso := F.mapIso h.iso, comm := ⋯ }
Instances For
Given a homology map data ψ : HomologyMapData φ h₁ h₂
such that
h₁.left
, h₁.right
, h₂.left
and h₂.right
are all preserved by a functor F
, this is
the induced homology map data for the morphism F.mapShortComplex.map φ
.
Equations
- ψ.map F = { left := ψ.left.map F, right := ψ.right.map F }
Instances For
A functor preserves the left homology of a short complex S
if it preserves all the
left homology data of S
.
- isPreservedBy (h : S.LeftHomologyData) : h.IsPreservedBy F
the functor preserves all the left homology data of the short complex
Instances
A functor preserves the right homology of a short complex S
if it preserves all the
right homology data of S
.
- isPreservedBy (h : S.RightHomologyData) : h.IsPreservedBy F
the functor preserves all the right homology data of the short complex
Instances
If a functor preserves a certain left homology data of a short complex S
, then it
preserves the left homology of S
.
If a functor preserves a certain right homology data of a short complex S
, then it
preserves the right homology of S
.
When a functor F
preserves the left homology of a short complex S
, this is the
canonical isomorphism (S.map F).cycles ≅ F.obj S.cycles
.
Equations
- S.mapCyclesIso F = (S.leftHomologyData.map F).cyclesIso
Instances For
When a functor F
preserves the left homology of a short complex S
, this is the
canonical isomorphism (S.map F).leftHomology ≅ F.obj S.leftHomology
.
Equations
- S.mapLeftHomologyIso F = (S.leftHomologyData.map F).leftHomologyIso
Instances For
When a functor F
preserves the right homology of a short complex S
, this is the
canonical isomorphism (S.map F).opcycles ≅ F.obj S.opcycles
.
Equations
- S.mapOpcyclesIso F = (S.rightHomologyData.map F).opcyclesIso
Instances For
When a functor F
preserves the right homology of a short complex S
, this is the
canonical isomorphism (S.map F).rightHomology ≅ F.obj S.rightHomology
.
Equations
- S.mapRightHomologyIso F = (S.rightHomologyData.map F).rightHomologyIso
Instances For
When a functor F
preserves the left homology of a short complex S
, this is the
canonical isomorphism (S.map F).homology ≅ F.obj S.homology
.
Equations
- S.mapHomologyIso F = (S.homologyData.left.map F).homologyIso
Instances For
When a functor F
preserves the right homology of a short complex S
, this is the
canonical isomorphism (S.map F).homology ≅ F.obj S.homology
.
Equations
Instances For
Given a natural transformation τ : F ⟶ G
between functors C ⥤ D
which preserve
the left homology of a short complex S
, and a left homology data for S
,
this is the left homology map data for the morphism S.mapNatTrans τ
obtained by evaluating τ
.
Equations
- CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ = { φK := τ.app h.K, φH := τ.app h.H, commi := ⋯, commf' := ⋯, commπ := ⋯ }
Instances For
Given a natural transformation τ : F ⟶ G
between functors C ⥤ D
which preserve
the right homology of a short complex S
, and a right homology data for S
,
this is the right homology map data for the morphism S.mapNatTrans τ
obtained by evaluating τ
.
Equations
- CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ = { φQ := τ.app h.Q, φH := τ.app h.H, commp := ⋯, commg' := ⋯, commι := ⋯ }
Instances For
Given a natural transformation τ : F ⟶ G
between functors C ⥤ D
which preserve
the homology of a short complex S
, and a homology data for S
,
this is the homology map data for the morphism S.mapNatTrans τ
obtained by evaluating τ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural isomorphism
F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F
for a functor F : C ⥤ D
which preserves homology. -
Equations
- CategoryTheory.ShortComplex.cyclesFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapCyclesIso F) ⋯
Instances For
The natural isomorphism
F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F
for a functor F : C ⥤ D
which preserves homology. -
Equations
- CategoryTheory.ShortComplex.leftHomologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapLeftHomologyIso F) ⋯
Instances For
The natural isomorphism
F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F
for a functor F : C ⥤ D
which preserves homology. -
Equations
- CategoryTheory.ShortComplex.opcyclesFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapOpcyclesIso F) ⋯
Instances For
The natural isomorphism
F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F
for a functor F : C ⥤ D
which preserves homology. -
Equations
- CategoryTheory.ShortComplex.rightHomologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapRightHomologyIso F) ⋯
Instances For
The natural isomorphism
F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F
for a functor F : C ⥤ D
which preserves homology. -
Equations
- CategoryTheory.ShortComplex.homologyFunctorIso F = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.ShortComplex C) => S.mapHomologyIso F) ⋯
Instances For
If a short complex S
is such that S.f = 0
and that the kernel of S.g
is preserved
by a functor F
, then F
preserves the left homology of S
.
If a short complex S
is such that S.g = 0
and that the cokernel of S.f
is preserved
by a functor F
, then F
preserves the right homology of S
.
If a short complex S
is such that S.g = 0
and that the cokernel of S.f
is preserved
by a functor F
, then F
preserves the left homology of S
.
If a short complex S
is such that S.f = 0
and that the kernel of S.g
is preserved
by a functor F
, then F
preserves the right homology of S
.