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.
class
CategoryTheory.Functor.PreservesHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
:
Type (max (max (max u_1 u_2) u_3) u_4)
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
def
CategoryTheory.Functor.PreservesHomology.preservesKernel
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesHomology]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A functor which preserves homology preserves kernels.
Equations
Instances For
def
CategoryTheory.Functor.PreservesHomology.preservesCokernel
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesHomology]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A functor which preserves homology preserves cokernels.
Equations
Instances For
noncomputable instance
CategoryTheory.Functor.preservesHomologyOfExact
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.PreservesFiniteLimits F]
[CategoryTheory.Limits.PreservesFiniteColimits F]
:
F.PreservesHomology
Equations
- F.preservesHomologyOfExact = { preservesKernels := inferInstance, preservesCokernels := inferInstance }
class
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
:
Type (max (max (max u_1 u_2) u_3) u_4)
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
noncomputable instance
CategoryTheory.ShortComplex.LeftHomologyData.isPreservedByOfPreservesHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesHomology]
:
h.IsPreservedBy F
Equations
- h.isPreservedByOfPreservesHomology F = { g := CategoryTheory.Functor.PreservesHomology.preservesKernel F S.g, f' := CategoryTheory.Functor.PreservesHomology.preservesCokernel F h.f' }
def
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hg
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
When a left homology data is preserved by a functor F, this functor
preserves the kernel of S.g : S.X₂ ⟶ S.X₃.
Equations
Instances For
def
CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
When a left homology data h is preserved by a functor F, this functor
preserves the cokernel of h.f' : S.X₁ ⟶ h.K.
Equations
- CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.hf' h F = CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f'
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_i
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).i = F.map h.i
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_K
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).K = F.obj h.K
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_H
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).H = F.obj h.H
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_π
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).π = F.map h.π
noncomputable def
CategoryTheory.ShortComplex.LeftHomologyData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(S.map F).LeftHomologyData
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
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_f'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).f' = F.map h.f'
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.LeftHomologyData}
{h₂ : S₂.LeftHomologyData}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
(ψ.map F).φH = F.map ψ.φH
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.LeftHomologyData}
{h₂ : S₂.LeftHomologyData}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
(ψ.map F).φK = F.map ψ.φK
def
CategoryTheory.ShortComplex.LeftHomologyMapData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.LeftHomologyData}
{h₂ : S₂.LeftHomologyData}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
CategoryTheory.ShortComplex.LeftHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
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
class
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
:
Type (max (max (max u_1 u_2) u_3) u_4)
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
noncomputable instance
CategoryTheory.ShortComplex.RightHomologyData.isPreservedByOfPreservesHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesHomology]
:
h.IsPreservedBy F
Equations
- h.isPreservedByOfPreservesHomology F = { f := CategoryTheory.Functor.PreservesHomology.preservesCokernel F S.f, g' := CategoryTheory.Functor.PreservesHomology.preservesKernel F h.g' }
def
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hf
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
When a right homology data is preserved by a functor F, this functor
preserves the cokernel of S.f : S.X₁ ⟶ S.X₂.
Equations
Instances For
def
CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
When a right homology data h is preserved by a functor F, this functor
preserves the kernel of h.g' : h.Q ⟶ S.X₃.
Equations
- CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.hg' h F = CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g'
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_H
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).H = F.obj h.H
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_Q
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).Q = F.obj h.Q
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_p
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).p = F.map h.p
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_ι
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).ι = F.map h.ι
noncomputable def
CategoryTheory.ShortComplex.RightHomologyData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(S.map F).RightHomologyData
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
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_g'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.IsPreservedBy F]
:
(h.map F).g' = F.map h.g'
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyMapData.map_φH
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.RightHomologyData}
{h₂ : S₂.RightHomologyData}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
(ψ.map F).φH = F.map ψ.φH
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.RightHomologyData}
{h₂ : S₂.RightHomologyData}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
(ψ.map F).φQ = F.map ψ.φQ
def
CategoryTheory.ShortComplex.RightHomologyMapData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.RightHomologyData}
{h₂ : S₂.RightHomologyData}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.IsPreservedBy F]
[h₂.IsPreservedBy F]
:
CategoryTheory.ShortComplex.RightHomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
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
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyData.map_right
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.HomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.left.IsPreservedBy F]
[h.right.IsPreservedBy F]
:
(h.map F).right = h.right.map F
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyData.map_iso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.HomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.left.IsPreservedBy F]
[h.right.IsPreservedBy F]
:
(h.map F).iso = F.mapIso h.iso
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyData.map_left
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.HomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.left.IsPreservedBy F]
[h.right.IsPreservedBy F]
:
(h.map F).left = h.left.map F
noncomputable def
CategoryTheory.ShortComplex.HomologyData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h : S.HomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h.left.IsPreservedBy F]
[h.right.IsPreservedBy F]
:
(S.map F).HomologyData
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
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyMapData.map_right
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.HomologyData}
{h₂ : S₂.HomologyData}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.left.IsPreservedBy F]
[h₁.right.IsPreservedBy F]
[h₂.left.IsPreservedBy F]
[h₂.right.IsPreservedBy F]
:
(ψ.map F).right = ψ.right.map F
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyMapData.map_left
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.HomologyData}
{h₂ : S₂.HomologyData}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.left.IsPreservedBy F]
[h₁.right.IsPreservedBy F]
[h₂.left.IsPreservedBy F]
[h₂.right.IsPreservedBy F]
:
(ψ.map F).left = ψ.left.map F
def
CategoryTheory.ShortComplex.HomologyMapData.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{h₁ : S₁.HomologyData}
{h₂ : S₂.HomologyData}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.left.IsPreservedBy F]
[h₁.right.IsPreservedBy F]
[h₂.left.IsPreservedBy F]
[h₂.right.IsPreservedBy F]
:
CategoryTheory.ShortComplex.HomologyMapData (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
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
class
CategoryTheory.Functor.PreservesLeftHomologyOf
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
:
Type (max (max (max u_1 u_2) u_3) u_4)
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
class
CategoryTheory.Functor.PreservesRightHomologyOf
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
:
Type (max (max (max u_1 u_2) u_3) u_4)
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
noncomputable instance
CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
[F.PreservesHomology]
:
F.PreservesLeftHomologyOf S
Equations
- CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf F S = { isPreservedBy := inferInstance }
noncomputable instance
CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
[F.PreservesHomology]
:
F.PreservesRightHomologyOf S
Equations
- CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf F S = { isPreservedBy := inferInstance }
def
CategoryTheory.Functor.PreservesLeftHomologyOf.mk'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S : CategoryTheory.ShortComplex C}
(h : S.LeftHomologyData)
[h.IsPreservedBy F]
:
F.PreservesLeftHomologyOf S
If a functor preserves a certain left homology data of a short complex S, then it
preserves the left homology of S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Functor.PreservesRightHomologyOf.mk'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S : CategoryTheory.ShortComplex C}
(h : S.RightHomologyData)
[h.IsPreservedBy F]
:
F.PreservesRightHomologyOf S
If a functor preserves a certain right homology data of a short complex S, then it
preserves the right homology of S.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.ShortComplex.LeftHomologyData.isPreservedByOfPreserves
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h₁ : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
:
h₁.IsPreservedBy F
Equations
- h₁.isPreservedByOfPreserves F = CategoryTheory.Functor.PreservesLeftHomologyOf.isPreservedBy h₁
instance
CategoryTheory.ShortComplex.RightHomologyData.isPreservedByOfPreserves
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(h₂ : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[F.PreservesRightHomologyOf S]
:
h₂.IsPreservedBy F
Equations
- h₂.isPreservedByOfPreserves F = CategoryTheory.Functor.PreservesRightHomologyOf.isPreservedBy h₂
instance
CategoryTheory.ShortComplex.hasLeftHomology_of_preserves
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
(S.map F).HasLeftHomology
Equations
- ⋯ = ⋯
instance
CategoryTheory.ShortComplex.hasLeftHomology_of_preserves'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
(F.mapShortComplex.obj S).HasLeftHomology
Equations
- ⋯ = ⋯
instance
CategoryTheory.ShortComplex.hasRightHomology_of_preserves
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
(S.map F).HasRightHomology
Equations
- ⋯ = ⋯
instance
CategoryTheory.ShortComplex.hasRightHomology_of_preserves'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
(F.mapShortComplex.obj S).HasRightHomology
Equations
- ⋯ = ⋯
instance
CategoryTheory.ShortComplex.hasHomology_of_preserves
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[F.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
:
(S.map F).HasHomology
Equations
- ⋯ = ⋯
instance
CategoryTheory.ShortComplex.hasHomology_of_preserves'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[F.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
:
(F.mapShortComplex.obj S).HasHomology
Equations
- ⋯ = ⋯
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hl₁ : S₁.LeftHomologyData)
(hl₂ : S₂.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[hl₁.IsPreservedBy F]
[hl₂.IsPreservedBy F]
:
F.map (CategoryTheory.ShortComplex.cyclesMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
theorem
CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hl₁ : S₁.LeftHomologyData)
(hl₂ : S₂.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[hl₁.IsPreservedBy F]
[hl₂.IsPreservedBy F]
:
F.map (CategoryTheory.ShortComplex.leftHomologyMap' φ hl₁ hl₂) = CategoryTheory.ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hr₁ : S₁.RightHomologyData)
(hr₂ : S₂.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[hr₁.IsPreservedBy F]
[hr₂.IsPreservedBy F]
:
F.map (CategoryTheory.ShortComplex.opcyclesMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.opcyclesMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
theorem
CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hr₁ : S₁.RightHomologyData)
(hr₂ : S₂.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[hr₁.IsPreservedBy F]
[hr₂.IsPreservedBy F]
:
F.map (CategoryTheory.ShortComplex.rightHomologyMap' φ hr₁ hr₂) = CategoryTheory.ShortComplex.rightHomologyMap' (F.mapShortComplex.map φ) (hr₁.map F) (hr₂.map F)
theorem
CategoryTheory.ShortComplex.HomologyData.map_homologyMap'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(h₁ : S₁.HomologyData)
(h₂ : S₂.HomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[h₁.left.IsPreservedBy F]
[h₁.right.IsPreservedBy F]
[h₂.left.IsPreservedBy F]
[h₂.right.IsPreservedBy F]
:
F.map (CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂) = CategoryTheory.ShortComplex.homologyMap' (F.mapShortComplex.map φ) (h₁.map F) (h₂.map F)
noncomputable def
CategoryTheory.ShortComplex.mapCyclesIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
(S.map F).cycles ≅ F.obj S.cycles
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
@[simp]
theorem
CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
{Z : D}
(h : F.obj S.X₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (CategoryTheory.CategoryStruct.comp (F.map S.iCycles) h) = CategoryTheory.CategoryStruct.comp (S.map F).iCycles h
@[simp]
theorem
CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (F.map S.iCycles) = (S.map F).iCycles
noncomputable def
CategoryTheory.ShortComplex.mapLeftHomologyIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
(S.map F).leftHomology ≅ F.obj S.leftHomology
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
noncomputable def
CategoryTheory.ShortComplex.mapOpcyclesIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
(S.map F).opcycles ≅ F.obj S.opcycles
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
noncomputable def
CategoryTheory.ShortComplex.mapRightHomologyIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
(S.map F).rightHomology ≅ F.obj S.rightHomology
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
noncomputable def
CategoryTheory.ShortComplex.mapHomologyIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[(S.map F).HasHomology]
[F.PreservesLeftHomologyOf S]
:
(S.map F).homology ≅ F.obj S.homology
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
noncomputable def
CategoryTheory.ShortComplex.mapHomologyIso'
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[(S.map F).HasHomology]
[F.PreservesRightHomologyOf S]
:
(S.map F).homology ≅ F.obj S.homology
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
theorem
CategoryTheory.ShortComplex.LeftHomologyData.mapCyclesIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hl : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.LeftHomologyData.mapLeftHomologyIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hl : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasLeftHomology]
[F.PreservesLeftHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.RightHomologyData.mapOpcyclesIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hr : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.RightHomologyData.mapRightHomologyIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hr : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasRightHomology]
[F.PreservesRightHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.LeftHomologyData.mapHomologyIso_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hl : S.LeftHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[(S.map F).HasHomology]
[F.PreservesLeftHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.RightHomologyData.mapHomologyIso'_eq
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
(hr : S.RightHomologyData)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[(S.map F).HasHomology]
[F.PreservesRightHomologyOf S]
:
theorem
CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : F.obj S₂.cycles ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapCyclesIso F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapCyclesIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
(S₂.mapCyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).hom (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
theorem
CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : (S₂.map F).cycles ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapCyclesIso F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapCyclesIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ)) (S₂.mapCyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapCyclesIso F).inv
(CategoryTheory.ShortComplex.cyclesMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : F.obj S₂.leftHomology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapLeftHomologyIso F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapLeftHomologyIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
(S₂.mapLeftHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).hom
(F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
theorem
CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : (S₂.map F).leftHomology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapLeftHomologyIso F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapLeftHomologyIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasLeftHomology]
[S₂.HasLeftHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
(S₂.mapLeftHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapLeftHomologyIso F).inv
(CategoryTheory.ShortComplex.leftHomologyMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : F.obj S₂.opcycles ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapOpcyclesIso F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapOpcyclesIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
(S₂.mapOpcyclesIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).hom (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
theorem
CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : (S₂.map F).opcycles ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapOpcyclesIso F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (S₂.mapOpcyclesIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv
(CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : F.obj S₂.rightHomology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapRightHomologyIso F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapRightHomologyIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
(S₂.mapRightHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).hom
(F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
theorem
CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : (S₂.map F).rightHomology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapRightHomologyIso F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapRightHomologyIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasRightHomology]
[S₂.HasRightHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
(S₂.mapRightHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapRightHomologyIso F).inv
(CategoryTheory.ShortComplex.rightHomologyMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : F.obj S₂.homology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
(S₂.mapHomologyIso F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
theorem
CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
{Z : D}
(h : (S₂.map F).homology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapHomologyIso_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).inv
(CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : F.obj S₂.homology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso' F).hom h) = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom
(CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
theorem
CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
(S₂.mapHomologyIso' F).hom = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom (F.map (CategoryTheory.ShortComplex.homologyMap φ))
theorem
CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality_assoc
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
{Z : D}
(h : (S₂.map F).homology ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso' F).inv h) = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ)) h)
theorem
CategoryTheory.ShortComplex.mapHomologyIso'_inv_naturality
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S₁.HasHomology]
[S₂.HasHomology]
[(S₁.map F).HasHomology]
[(S₂.map F).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) (S₂.mapHomologyIso' F).inv = CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).inv
(CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
theorem
CategoryTheory.ShortComplex.mapHomologyIso'_eq_mapHomologyIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[S.HasHomology]
[F.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
:
S.mapHomologyIso' F = S.mapHomologyIso F
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
(h : S.LeftHomologyData)
(τ : F ⟶ G)
:
(CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φH = τ.app h.H
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
(h : S.LeftHomologyData)
(τ : F ⟶ G)
:
(CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φK = τ.app h.K
def
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
(h : S.LeftHomologyData)
(τ : F ⟶ G)
:
CategoryTheory.ShortComplex.LeftHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
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
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.RightHomologyData)
(τ : F ⟶ G)
:
(CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φQ = τ.app h.Q
@[simp]
theorem
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.RightHomologyData)
(τ : F ⟶ G)
:
(CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp h τ).φH = τ.app h.H
def
CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.RightHomologyData)
(τ : F ⟶ G)
:
CategoryTheory.ShortComplex.RightHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
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
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.HomologyData)
(τ : F ⟶ G)
:
@[simp]
theorem
CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.HomologyData)
(τ : F ⟶ G)
:
def
CategoryTheory.ShortComplex.HomologyMapData.natTransApp
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{S : CategoryTheory.ShortComplex C}
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
(h : S.HomologyData)
(τ : F ⟶ G)
:
CategoryTheory.ShortComplex.HomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
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
theorem
CategoryTheory.ShortComplex.homologyMap_mapNatTrans
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(S : CategoryTheory.ShortComplex C)
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
[S.HasHomology]
(τ : F ⟶ G)
:
CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ) = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).hom
(CategoryTheory.CategoryStruct.comp (τ.app S.homology) (S.mapHomologyIso G).inv)
noncomputable def
CategoryTheory.ShortComplex.cyclesFunctorIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[F.PreservesHomology]
:
F.mapShortComplex.comp (CategoryTheory.ShortComplex.cyclesFunctor D) ≅ (CategoryTheory.ShortComplex.cyclesFunctor C).comp F
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
noncomputable def
CategoryTheory.ShortComplex.leftHomologyFunctorIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[F.PreservesHomology]
:
F.mapShortComplex.comp (CategoryTheory.ShortComplex.leftHomologyFunctor D) ≅ (CategoryTheory.ShortComplex.leftHomologyFunctor C).comp F
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
noncomputable def
CategoryTheory.ShortComplex.opcyclesFunctorIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[F.PreservesHomology]
:
F.mapShortComplex.comp (CategoryTheory.ShortComplex.opcyclesFunctor D) ≅ (CategoryTheory.ShortComplex.opcyclesFunctor C).comp F
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
noncomputable def
CategoryTheory.ShortComplex.rightHomologyFunctorIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[F.PreservesHomology]
:
F.mapShortComplex.comp (CategoryTheory.ShortComplex.rightHomologyFunctor D) ≅ (CategoryTheory.ShortComplex.rightHomologyFunctor C).comp F
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
noncomputable def
CategoryTheory.ShortComplex.homologyFunctorIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[F.PreservesHomology]
:
F.mapShortComplex.comp (CategoryTheory.ShortComplex.homologyFunctor D) ≅ (CategoryTheory.ShortComplex.homologyFunctor C).comp F
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
theorem
CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_map_iff
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{hl₁ : S₁.LeftHomologyData}
{hl₂ : S₂.LeftHomologyData}
(ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂)
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[hl₁.IsPreservedBy F]
[hl₂.IsPreservedBy F]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψl.φH)
theorem
CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_map_iff
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{hr₁ : S₁.RightHomologyData}
{hr₂ : S₂.RightHomologyData}
(ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂)
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[hr₁.IsPreservedBy F]
[hr₂.IsPreservedBy F]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψr.φH)
instance
CategoryTheory.ShortComplex.quasiIso_map_of_preservesLeftHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[S₁.HasHomology]
[S₂.HasHomology]
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
[CategoryTheory.ShortComplex.QuasiIso φ]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
Equations
- ⋯ = ⋯
theorem
CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesLeftHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[S₁.HasHomology]
[S₂.HasHomology]
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[F.PreservesLeftHomologyOf S₁]
[F.PreservesLeftHomologyOf S₂]
[F.ReflectsIsomorphisms]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
instance
CategoryTheory.ShortComplex.quasiIso_map_of_preservesRightHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[S₁.HasHomology]
[S₂.HasHomology]
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
[CategoryTheory.ShortComplex.QuasiIso φ]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ)
Equations
- ⋯ = ⋯
theorem
CategoryTheory.ShortComplex.quasiIso_map_iff_of_preservesRightHomology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[S₁.HasHomology]
[S₂.HasHomology]
[(F.mapShortComplex.obj S₁).HasHomology]
[(F.mapShortComplex.obj S₂).HasHomology]
[F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂]
[F.ReflectsIsomorphisms]
:
CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.ShortComplex.QuasiIso φ
noncomputable def
CategoryTheory.Functor.preservesLeftHomologyOfZerof
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
(hf : S.f = 0)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F]
:
F.PreservesLeftHomologyOf 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 left homology of S.
Equations
- F.preservesLeftHomologyOfZerof S hf = { isPreservedBy := fun (h : S.LeftHomologyData) => { g := inferInstance, f' := CategoryTheory.Limits.preservesCokernelZero' F h.f' ⋯ } }
Instances For
noncomputable def
CategoryTheory.Functor.preservesRightHomologyOfZerog
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
(hg : S.g = 0)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F]
:
F.PreservesRightHomologyOf 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.
Equations
- F.preservesRightHomologyOfZerog S hg = { isPreservedBy := fun (h : S.RightHomologyData) => { f := inferInstance, g' := CategoryTheory.Limits.preservesKernelZero' F h.g' ⋯ } }
Instances For
noncomputable def
CategoryTheory.Functor.preservesLeftHomologyOfZerog
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
(hg : S.g = 0)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F]
:
F.PreservesLeftHomologyOf 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Functor.preservesRightHomologyOfZerof
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[F.PreservesZeroMorphisms]
(S : CategoryTheory.ShortComplex C)
(hf : S.f = 0)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F]
:
F.PreservesRightHomologyOf 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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.NatTrans.app_homology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroMorphisms D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(τ : F ⟶ G)
(S : CategoryTheory.ShortComplex C)
[S.HasHomology]
[F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms]
[F.PreservesLeftHomologyOf S]
[G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S]
[G.PreservesRightHomologyOf S]
:
τ.app S.homology = CategoryTheory.CategoryStruct.comp (S.mapHomologyIso F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (S.mapNatTrans τ))
(S.mapHomologyIso G).hom)