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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
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
- CategoryTheory.Functor.preservesHomologyOfExact
- CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbModuleCategoryInstAddCommGroupCatLargeCategoryPreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategoryPreadditiveHasZeroMorphismsInstPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategoryForget₂ModuleConcreteCategoryConcreteCategoryHasForgetToAddCommGroupPreservesZeroMorphisms_of_additiveForget₂_addCommGroupCat_additive
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A functor which preserves homology preserves kernels.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A functor which preserves homology preserves cokernels.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.PreservesFiniteLimits F]
[CategoryTheory.Limits.PreservesFiniteColimits F]
:
Equations
- CategoryTheory.Functor.preservesHomologyOfExact F = { 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
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₃.- f' : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.ShortComplex.LeftHomologyData.f' h) 0) F
the functor preserves the cokernel of
h.f' : S.X₁ ⟶ h.K.
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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
:
Equations
- One or more equations did not get rendered due to their size.
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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
When a left homology data is preserved by a functor F, this functor
preserves the kernel of S.g : S.X₂ ⟶ S.X₃.
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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h 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'
@[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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.LeftHomologyData.map h 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.LeftHomologyData.map h 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.LeftHomologyData.map h 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.LeftHomologyData.map h 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
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.
@[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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy 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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ F]
:
(CategoryTheory.ShortComplex.LeftHomologyMapData.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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ F]
:
(CategoryTheory.ShortComplex.LeftHomologyMapData.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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂ 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
- CategoryTheory.ShortComplex.LeftHomologyMapData.map ψ F = { φK := F.map ψ.φK, φH := F.map ψ.φH, commi := ⋯, commf' := ⋯, commπ := ⋯ }
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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
:
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₂.- g' : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair (CategoryTheory.ShortComplex.RightHomologyData.g' h) 0) F
the functor preserves the kernel of
h.g' : h.Q ⟶ S.X₃.
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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
:
Equations
- One or more equations did not get rendered due to their size.
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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
When a right homology data is preserved by a functor F, this functor
preserves the cokernel of S.f : S.X₁ ⟶ S.X₂.
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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h 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'
@[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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.RightHomologyData.map h 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.RightHomologyData.map h 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.RightHomologyData.map h 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
(CategoryTheory.ShortComplex.RightHomologyData.map h 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
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.
@[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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
@[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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F]
:
(CategoryTheory.ShortComplex.RightHomologyMapData.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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ F]
:
(CategoryTheory.ShortComplex.RightHomologyMapData.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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂}
(ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂ 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
- CategoryTheory.ShortComplex.RightHomologyMapData.map ψ F = { φQ := F.map ψ.φQ, φH := F.map ψ.φH, commp := ⋯, commg' := ⋯, commι := ⋯ }
@[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 : CategoryTheory.ShortComplex.HomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F]
:
(CategoryTheory.ShortComplex.HomologyData.map h F).right = CategoryTheory.ShortComplex.RightHomologyData.map h.right 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 : CategoryTheory.ShortComplex.HomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F]
:
(CategoryTheory.ShortComplex.HomologyData.map h 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 : CategoryTheory.ShortComplex.HomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right 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 : CategoryTheory.ShortComplex.HomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h.right F]
:
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
- One or more equations did not get rendered due to their size.
@[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₁ : CategoryTheory.ShortComplex.HomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.HomologyData S₂}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right 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₁ : CategoryTheory.ShortComplex.HomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.HomologyData S₂}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right 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₁ : CategoryTheory.ShortComplex.HomologyData S₁}
{h₂ : CategoryTheory.ShortComplex.HomologyData S₂}
(ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right 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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(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 : CategoryTheory.ShortComplex.LeftHomologyData S) → CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F
the functor preserves all the left homology data of the short complex
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(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 : CategoryTheory.ShortComplex.RightHomologyData S) → CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F
the functor preserves all the right homology data of the short complex
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.Functor.PreservesHomology F]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.Functor.PreservesHomology F]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h F]
:
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.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.RightHomologyData S)
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h F]
:
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.
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₁ : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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₂ : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁)
(hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ 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₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁)
(hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ 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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁)
(hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ 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₁ : CategoryTheory.ShortComplex.RightHomologyData S₁)
(hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ 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₁ : CategoryTheory.ShortComplex.HomologyData S₁)
(h₂ : CategoryTheory.ShortComplex.HomologyData S₂)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₁.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₁.right F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy h₂.left F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy h₂.right 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F 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
- One or more equations did not get rendered due to their size.
@[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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
{Z : D}
(h : F.obj S.X₂ ⟶ Z)
:
@[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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
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
- One or more equations did not get rendered due to their size.
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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S]
[CategoryTheory.Functor.PreservesRightHomologyOf F 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 : CategoryTheory.ShortComplex.LeftHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F 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 : CategoryTheory.ShortComplex.RightHomologyData S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.cycles S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapCyclesIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.cycles (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.cyclesMap φ))
(CategoryTheory.ShortComplex.mapCyclesIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapCyclesIso S₁ F).inv
(CategoryTheory.ShortComplex.cyclesMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.leftHomology S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.leftHomology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasLeftHomology S₁]
[CategoryTheory.ShortComplex.HasLeftHomology S₂]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.leftHomologyMap φ))
(CategoryTheory.ShortComplex.mapLeftHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapLeftHomologyIso S₁ F).inv
(CategoryTheory.ShortComplex.leftHomologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.opcycles S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.opcycles (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ))
(CategoryTheory.ShortComplex.mapOpcyclesIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapOpcyclesIso S₁ F).inv
(CategoryTheory.ShortComplex.opcyclesMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.rightHomology S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.rightHomology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasRightHomology S₁]
[CategoryTheory.ShortComplex.HasRightHomology S₂]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.rightHomologyMap φ))
(CategoryTheory.ShortComplex.mapRightHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapRightHomologyIso S₁ F).inv
(CategoryTheory.ShortComplex.rightHomologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.homology S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapHomologyIso S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.ShortComplex.mapHomologyIso S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S₁ F).inv
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : F.obj (CategoryTheory.ShortComplex.homology S₂) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).map φ))
(CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
{Z : D}
(h : CategoryTheory.ShortComplex.homology (CategoryTheory.ShortComplex.map S₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₁ F)]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S₂ F)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
:
CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ))
(CategoryTheory.ShortComplex.mapHomologyIso' S₂ F).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso' S₁ F).inv
(CategoryTheory.ShortComplex.homologyMap ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
@[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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
(τ : F ⟶ 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π := ⋯ }
@[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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.RightHomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.RightHomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.RightHomologyData S)
(τ : F ⟶ 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ι := ⋯ }
@[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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.HomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.HomologyData S)
(τ : 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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
(h : CategoryTheory.ShortComplex.HomologyData S)
(τ : F ⟶ 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.
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}
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
[CategoryTheory.ShortComplex.HasHomology S]
(τ : F ⟶ G)
:
CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.mapNatTrans S τ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S F).hom
(CategoryTheory.CategoryStruct.comp (τ.app (CategoryTheory.ShortComplex.homology S))
(CategoryTheory.ShortComplex.mapHomologyIso S 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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[CategoryTheory.Functor.PreservesHomology F]
:
The natural isomorphism
F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F
for a functor F : C ⥤ D which preserves homology. -
Equations
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[CategoryTheory.Functor.PreservesHomology F]
:
The natural isomorphism
F.mapShortComplex ⋙ leftHomologyFunctor D ≅ leftHomologyFunctor C ⋙ F
for a functor F : C ⥤ D which preserves homology. -
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[CategoryTheory.Functor.PreservesHomology F]
:
The natural isomorphism
F.mapShortComplex ⋙ opcyclesFunctor D ≅ opcyclesFunctor C ⋙ F
for a functor F : C ⥤ D which preserves homology. -
Equations
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Limits.HasKernels C]
[CategoryTheory.Limits.HasCokernels C]
[CategoryTheory.Limits.HasKernels D]
[CategoryTheory.Limits.HasCokernels D]
[CategoryTheory.Functor.PreservesHomology F]
:
The natural isomorphism
F.mapShortComplex ⋙ rightHomologyFunctor D ≅ rightHomologyFunctor C ⋙ F
for a functor F : C ⥤ D which preserves homology. -
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.CategoryWithHomology C]
[CategoryTheory.CategoryWithHomology D]
[CategoryTheory.Functor.PreservesHomology F]
:
The natural isomorphism
F.mapShortComplex ⋙ homologyFunctor D ≅ homologyFunctor C ⋙ F
for a functor F : C ⥤ D which preserves homology. -
Equations
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{hl₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁}
{hl₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂}
(ψl : CategoryTheory.ShortComplex.LeftHomologyMapData φ hl₁ hl₂)
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₁ F]
[CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy hl₂ F]
:
CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
{φ : S₁ ⟶ S₂}
{hr₁ : CategoryTheory.ShortComplex.RightHomologyData S₁}
{hr₂ : CategoryTheory.ShortComplex.RightHomologyData S₂}
(ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂)
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₁ F]
[CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy hr₂ F]
:
CategoryTheory.ShortComplex.QuasiIso ((CategoryTheory.Functor.mapShortComplex F).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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
[CategoryTheory.ShortComplex.QuasiIso φ]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₁]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S₂]
[CategoryTheory.Functor.ReflectsIsomorphisms F]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
[CategoryTheory.ShortComplex.QuasiIso φ]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₁)]
[CategoryTheory.ShortComplex.HasHomology ((CategoryTheory.Functor.mapShortComplex F).obj S₂)]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₁]
[CategoryTheory.Functor.PreservesRightHomologyOf F S₂]
[CategoryTheory.Functor.ReflectsIsomorphisms F]
:
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
(hf : S.f = 0)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
(hg : S.g = 0)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F]
:
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
- One or more equations did not get rendered due to their size.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
(hg : S.g = 0)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair S.f 0) F]
:
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.
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)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
(S : CategoryTheory.ShortComplex C)
(hf : S.f = 0)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F]
:
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.
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)
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesLeftHomologyOf G S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf G S]
:
τ.app (CategoryTheory.ShortComplex.homology S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.mapHomologyIso S F).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.ShortComplex.homologyMap (CategoryTheory.ShortComplex.mapNatTrans S τ))
(CategoryTheory.ShortComplex.mapHomologyIso S G).hom)