Exact short complexes #
When S : ShortComplex C, this file defines a structure
S.Exact which expresses the exactness of S, i.e. there
exists a homology data h : S.HomologyData such that
h.left.H is zero. When [S.HasHomology], it is equivalent
to the assertion IsZero S.homology.
Almost by construction, this notion of exactness is self dual,
see Exact.op and Exact.unop.
structure
CategoryTheory.ShortComplex.Exact
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C)
:
The assertion that the short complex S : ShortComplex C is exact.
- condition : ∃ (h : CategoryTheory.ShortComplex.HomologyData S), CategoryTheory.Limits.IsZero h.left.H
the condition that there exists an homology data whose
left.Hfield is zero
Instances For
theorem
CategoryTheory.ShortComplex.HomologyData.exact_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.HomologyData S)
:
theorem
CategoryTheory.ShortComplex.HomologyData.exact_iff'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.HomologyData S)
:
theorem
CategoryTheory.ShortComplex.exact_of_iso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(e : S₁ ≅ S₂)
(h : CategoryTheory.ShortComplex.Exact S₁)
:
theorem
CategoryTheory.ShortComplex.exact_iff_of_iso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(e : S₁ ≅ S₂)
:
theorem
CategoryTheory.ShortComplex.exact_and_mono_f_iff_of_iso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(e : S₁ ≅ S₂)
:
theorem
CategoryTheory.ShortComplex.exact_and_epi_g_iff_of_iso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(e : S₁ ≅ S₂)
:
theorem
CategoryTheory.ShortComplex.exact_of_isZero_X₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C)
(h : CategoryTheory.Limits.IsZero S.X₂)
:
theorem
CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.Epi φ.τ₁]
[CategoryTheory.IsIso φ.τ₂]
[CategoryTheory.Mono φ.τ₃]
:
theorem
CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.HomologyData S)
:
CategoryTheory.ShortComplex.Exact S ↔ CategoryTheory.CategoryStruct.comp h.left.i h.right.p = 0
theorem
CategoryTheory.ShortComplex.exact_iff_i_p_zero
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
(h₁ : CategoryTheory.ShortComplex.LeftHomologyData S)
(h₂ : CategoryTheory.ShortComplex.RightHomologyData S)
:
theorem
CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Limits.HasKernel S.g]
[CategoryTheory.Limits.HasCokernel S.f]
:
theorem
CategoryTheory.exact_iff_shortComplex_exact
{A : Type u_3}
[CategoryTheory.Category.{u_4, u_3} A]
[CategoryTheory.Abelian A]
(S : CategoryTheory.ShortComplex A)
:
The notion of exactness given by ShortComplex.Exact is equivalent to
the one given by the previous API CategoryTheory.Exact in the case of
abelian categories.
@[simp]
@[simp]
theorem
CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff
{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.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.map S F) ↔ CategoryTheory.Limits.IsZero (F.toPrefunctor.obj h.H)
theorem
CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff
{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.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.map S F) ↔ CategoryTheory.Limits.IsZero (F.toPrefunctor.obj h.H)
theorem
CategoryTheory.ShortComplex.Exact.map_of_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]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Exact S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
theorem
CategoryTheory.ShortComplex.Exact.map_of_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]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Exact S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
theorem
CategoryTheory.ShortComplex.Exact.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.Exact S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
:
theorem
CategoryTheory.ShortComplex.exact_map_iff_of_faithful
{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)
[CategoryTheory.ShortComplex.HasHomology S]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesLeftHomologyOf F S]
[CategoryTheory.Functor.PreservesRightHomologyOf F S]
[CategoryTheory.Faithful F]
:
theorem
CategoryTheory.ShortComplex.Exact.comp_eq_zero_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Exact S)
{X : C}
{Y : C}
{a : X ⟶ S.X₂}
(ha : CategoryTheory.CategoryStruct.comp a S.g = 0)
{b : S.X₂ ⟶ Y}
(hb : CategoryTheory.CategoryStruct.comp S.f b = 0)
{Z : C}
(h : Y ⟶ Z)
:
theorem
CategoryTheory.ShortComplex.Exact.comp_eq_zero
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Exact S)
{X : C}
{Y : C}
{a : X ⟶ S.X₂}
(ha : CategoryTheory.CategoryStruct.comp a S.g = 0)
{b : S.X₂ ⟶ Y}
(hb : CategoryTheory.CategoryStruct.comp S.f b = 0)
:
theorem
CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}
(ex : CategoryTheory.ShortComplex.Exact S)
(hf : S.f = 0)
(hg : S.g = 0)
:
theorem
CategoryTheory.ShortComplex.exact_iff_mono
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.Limits.HasZeroObject C]
(hf : S.f = 0)
:
theorem
CategoryTheory.ShortComplex.exact_iff_epi
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.Limits.HasZeroObject C]
(hg : S.g = 0)
:
theorem
CategoryTheory.ShortComplex.Exact.epi_f'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
:
theorem
CategoryTheory.ShortComplex.Exact.mono_g'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
(h : CategoryTheory.ShortComplex.RightHomologyData S)
:
theorem
CategoryTheory.ShortComplex.Exact.epi_toCycles
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.ShortComplex.HasLeftHomology S]
:
theorem
CategoryTheory.ShortComplex.Exact.mono_fromOpcycles
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.ShortComplex.HasRightHomology S]
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(kf : CategoryTheory.Limits.KernelFork S.g)
(hkf : CategoryTheory.Limits.IsLimit kf)
:
(CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork hS kf hkf).K = kf.pt
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(kf : CategoryTheory.Limits.KernelFork S.g)
(hkf : CategoryTheory.Limits.IsLimit kf)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(kf : CategoryTheory.Limits.KernelFork S.g)
(hkf : CategoryTheory.Limits.IsLimit kf)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(kf : CategoryTheory.Limits.KernelFork S.g)
(hkf : CategoryTheory.Limits.IsLimit kf)
:
noncomputable def
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(kf : CategoryTheory.Limits.KernelFork S.g)
(hkf : CategoryTheory.Limits.IsLimit kf)
:
Given an exact short complex S and a limit kernel fork kf for S.g, this is the
left homology data for S with K := kf.pt and H := 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(cc : CategoryTheory.Limits.CokernelCofork S.f)
(hcc : CategoryTheory.Limits.IsColimit cc)
:
(CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork hS cc hcc).Q = cc.pt
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(cc : CategoryTheory.Limits.CokernelCofork S.f)
(hcc : CategoryTheory.Limits.IsColimit cc)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(cc : CategoryTheory.Limits.CokernelCofork S.f)
(hcc : CategoryTheory.Limits.IsColimit cc)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(cc : CategoryTheory.Limits.CokernelCofork S.f)
(hcc : CategoryTheory.Limits.IsColimit cc)
:
noncomputable def
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Limits.HasZeroObject C]
(cc : CategoryTheory.Limits.CokernelCofork S.f)
(hcc : CategoryTheory.Limits.IsColimit cc)
:
Given an exact short complex S and a colimit cokernel cofork cc for S.f, this is the
right homology data for S with Q := cc.pt and H := 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ShortComplex.exact_iff_epi_toCycles
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
:
theorem
CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Limits.HasKernel S.g]
:
CategoryTheory.ShortComplex.Exact S ↔ CategoryTheory.Epi (CategoryTheory.Limits.kernel.lift S.g S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))
theorem
CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
[CategoryTheory.ShortComplex.HasHomology S]
[CategoryTheory.Limits.HasCokernel S.f]
:
CategoryTheory.ShortComplex.Exact S ↔ CategoryTheory.Mono (CategoryTheory.Limits.cokernel.desc S.f S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))
theorem
CategoryTheory.ShortComplex.QuasiIso.exact_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
[CategoryTheory.ShortComplex.HasHomology S₁]
[CategoryTheory.ShortComplex.HasHomology S₂]
[CategoryTheory.ShortComplex.QuasiIso φ]
:
theorem
CategoryTheory.ShortComplex.exact_of_f_is_kernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
(hS : CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0)))
[CategoryTheory.ShortComplex.HasHomology S]
:
theorem
CategoryTheory.ShortComplex.exact_of_g_is_cokernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
(hS : CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.CokernelCofork.ofπ S.g (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0)))
[CategoryTheory.ShortComplex.HasHomology S]
:
theorem
CategoryTheory.ShortComplex.Exact.mono_g
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
(hf : S.f = 0)
:
theorem
CategoryTheory.ShortComplex.Exact.epi_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
(hg : S.g = 0)
:
theorem
CategoryTheory.ShortComplex.Exact.mono_g_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
:
CategoryTheory.Mono S.g ↔ S.f = 0
theorem
CategoryTheory.ShortComplex.Exact.epi_f_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
:
CategoryTheory.Epi S.f ↔ S.g = 0
theorem
CategoryTheory.ShortComplex.Exact.isZero_X₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
(hf : S.f = 0)
(hg : S.g = 0)
:
theorem
CategoryTheory.ShortComplex.Exact.isZero_X₂_iff
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
:
CategoryTheory.Limits.IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0
structure
CategoryTheory.ShortComplex.Splitting
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
:
Type u_3
A splitting for a short complex S consists of the data of a retraction r : X₂ ⟶ X₁
of S.f and section s : X₃ ⟶ X₂ of S.g which satisfy r ≫ S.f + S.g ≫ s = 𝟙 _
- r : S.X₂ ⟶ S.X₁
a retraction of
S.f - s : S.X₃ ⟶ S.X₂
a section of
S.g - f_r : CategoryTheory.CategoryStruct.comp S.f self.r = CategoryTheory.CategoryStruct.id S.X₁
the condition that
ris a retraction ofS.f - s_g : CategoryTheory.CategoryStruct.comp self.s S.g = CategoryTheory.CategoryStruct.id S.X₃
the condition that
sis a section ofS.g - id : CategoryTheory.CategoryStruct.comp self.r S.f + CategoryTheory.CategoryStruct.comp S.g self.s = CategoryTheory.CategoryStruct.id S.X₂
the compatibility between the given section and retraction
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.f_r_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(self : CategoryTheory.ShortComplex.Splitting S)
{Z : C}
(h : S.X₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp S.f (CategoryTheory.CategoryStruct.comp self.r h) = h
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.s_g_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(self : CategoryTheory.ShortComplex.Splitting S)
{Z : C}
(h : S.X₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp self.s (CategoryTheory.CategoryStruct.comp S.g h) = h
theorem
CategoryTheory.ShortComplex.Splitting.r_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
{Z : C}
(h : S.X₂ ⟶ Z)
:
theorem
CategoryTheory.ShortComplex.Splitting.r_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
theorem
CategoryTheory.ShortComplex.Splitting.g_s_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
{Z : C}
(h : S.X₂ ⟶ Z)
:
theorem
CategoryTheory.ShortComplex.Splitting.g_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.splitMono_f_retraction
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.splitMono_f s).retraction = s.r
def
CategoryTheory.ShortComplex.Splitting.splitMono_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
Given a splitting of a short complex S, this shows that S.f is a split monomorphism.
Instances For
theorem
CategoryTheory.ShortComplex.Splitting.isSplitMono_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
theorem
CategoryTheory.ShortComplex.Splitting.mono_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.splitEpi_g_section_
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.splitEpi_g s).section_ = s.s
def
CategoryTheory.ShortComplex.Splitting.splitEpi_g
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
Given a splitting of a short complex S, this shows that S.g is a split epimorphism.
Instances For
theorem
CategoryTheory.ShortComplex.Splitting.isSplitEpi_g
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
theorem
CategoryTheory.ShortComplex.Splitting.epi_g
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.s_r_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
{Z : C}
(h : S.X₁ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.s_r
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
:
CategoryTheory.CategoryStruct.comp s.s s.r = 0
theorem
CategoryTheory.ShortComplex.Splitting.ext_r
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
(s' : CategoryTheory.ShortComplex.Splitting S)
(h : s.r = s'.r)
:
s = s'
theorem
CategoryTheory.ShortComplex.Splitting.ext_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
(s' : CategoryTheory.ShortComplex.Splitting S)
(h : s.s = s'.s)
:
s = s'
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def
CategoryTheory.ShortComplex.Splitting.leftHomologyData
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
The left homology data on a short complex equipped with a splitting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
noncomputable def
CategoryTheory.ShortComplex.Splitting.rightHomologyData
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
The right homology data on a short complex equipped with a splitting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
noncomputable def
CategoryTheory.ShortComplex.Splitting.homologyData
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
The homology data on a short complex equipped with a splitting.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ShortComplex.Splitting.exact
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
A short complex equipped with a splitting is exact.
noncomputable def
CategoryTheory.ShortComplex.Splitting.fIsKernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))
If a short complex S is equipped with a splitting, then S.X₁ is the kernel of S.g.
Equations
Instances For
noncomputable def
CategoryTheory.ShortComplex.Splitting.gIsCokernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Limits.HasZeroObject C]
(s : CategoryTheory.ShortComplex.Splitting S)
:
If a short complex S is equipped with a splitting, then S.X₃ is the cokernel of S.f.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.map_r
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.Additive F]
:
(CategoryTheory.ShortComplex.Splitting.map s F).r = F.toPrefunctor.map s.r
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.map_s
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.Additive F]
:
(CategoryTheory.ShortComplex.Splitting.map s F).s = F.toPrefunctor.map s.s
def
CategoryTheory.ShortComplex.Splitting.map
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{S : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.Additive F]
:
If a short complex S has a splitting and F is an additive functor, then
S.map F also has a splitting.
Equations
- CategoryTheory.ShortComplex.Splitting.map s F = CategoryTheory.ShortComplex.Splitting.mk (F.toPrefunctor.map s.r) (F.toPrefunctor.map s.s)
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.ofIso_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S₁)
(e : S₁ ≅ S₂)
:
(CategoryTheory.ShortComplex.Splitting.ofIso s e).s = CategoryTheory.CategoryStruct.comp e.inv.τ₃ (CategoryTheory.CategoryStruct.comp s.s e.hom.τ₂)
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.ofIso_r
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S₁)
(e : S₁ ≅ S₂)
:
(CategoryTheory.ShortComplex.Splitting.ofIso s e).r = CategoryTheory.CategoryStruct.comp e.inv.τ₂ (CategoryTheory.CategoryStruct.comp s.r e.hom.τ₁)
def
CategoryTheory.ShortComplex.Splitting.ofIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(s : CategoryTheory.ShortComplex.Splitting S₁)
(e : S₁ ≅ S₂)
:
A splitting on a short complex induces splittings on isomorphic short complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(X₁ : C)
(X₂ : C)
[CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂]
:
CategoryTheory.ShortComplex.Splitting
(CategoryTheory.ShortComplex.mk CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryBiproduct.bicone X₁ X₂).inl
(CategoryTheory.Limits.BinaryBiproduct.bicone X₁ X₂).snd = 0))
The obvious splitting of the short complex X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂.
Equations
- CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct X₁ X₂ = CategoryTheory.ShortComplex.Splitting.mk CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inr
Instances For
noncomputable def
CategoryTheory.ShortComplex.Splitting.ofIsZeroOfIsIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
(hf : CategoryTheory.Limits.IsZero S.X₁)
(hg : CategoryTheory.IsIso S.g)
:
The obvious splitting of a short complex when S.X₁ is zero and S.g is an isomorphism.
Equations
Instances For
noncomputable def
CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C)
(hf : CategoryTheory.IsIso S.f)
(hg : CategoryTheory.Limits.IsZero S.X₃)
:
The obvious splitting of a short complex when S.f is an isomorphism and S.X₃ is zero.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.op_r
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.op h).r = h.s.op
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.op_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.op h).s = h.r.op
def
CategoryTheory.ShortComplex.Splitting.op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
:
The splitting of the short complex S.op deduced from a splitting of S.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.unop_r
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex Cᵒᵖ}
(h : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.unop h).r = h.s.unop
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.unop_s
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex Cᵒᵖ}
(h : CategoryTheory.ShortComplex.Splitting S)
:
(CategoryTheory.ShortComplex.Splitting.unop h).s = h.r.unop
def
CategoryTheory.ShortComplex.Splitting.unop
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex Cᵒᵖ}
(h : CategoryTheory.ShortComplex.Splitting S)
:
The splitting of the short complex S.unop deduced from a splitting of S.
Equations
- CategoryTheory.ShortComplex.Splitting.unop h = CategoryTheory.ShortComplex.Splitting.mk h.s.unop h.r.unop
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
[CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃]
:
@[simp]
theorem
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_inv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
[CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃]
:
noncomputable def
CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
(h : CategoryTheory.ShortComplex.Splitting S)
[CategoryTheory.Limits.HasBinaryBiproduct S.X₁ S.X₃]
:
The isomorphism S.X₂ ≅ S.X₁ ⊞ S.X₃ induced by a splitting of the short complex S.
Equations
Instances For
theorem
CategoryTheory.ShortComplex.Exact.isIso_f'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
(h : CategoryTheory.ShortComplex.LeftHomologyData S)
[CategoryTheory.Mono S.f]
:
theorem
CategoryTheory.ShortComplex.Exact.isIso_toCycles
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Mono S.f]
[CategoryTheory.ShortComplex.HasLeftHomology S]
:
theorem
CategoryTheory.ShortComplex.Exact.isIso_g'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
(h : CategoryTheory.ShortComplex.RightHomologyData S)
[CategoryTheory.Epi S.g]
:
theorem
CategoryTheory.ShortComplex.Exact.isIso_fromOpcycles
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Epi S.g]
[CategoryTheory.ShortComplex.HasRightHomology S]
:
noncomputable def
CategoryTheory.ShortComplex.Exact.fIsKernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Mono S.f]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι S.f (_ : CategoryTheory.CategoryStruct.comp S.f S.g = 0))
In a balanced category, if a short complex S is exact and S.f is a mono, then
S.X₁ is the kernel of S.g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
noncomputable def
CategoryTheory.ShortComplex.Exact.gIsCokernel
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
[CategoryTheory.Epi S.g]
:
In a balanced category, if a short complex S is exact and S.g is an epi, then
S.X₃ is the cokernel of S.g.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.ShortComplex.Exact.map_of_epi_of_preservesCokernel
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.ShortComplex.HasHomology (CategoryTheory.ShortComplex.map S F)]
:
noncomputable def
CategoryTheory.ShortComplex.Exact.lift
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
[CategoryTheory.Mono S.f]
:
A ⟶ S.X₁
If a short complex S in a balanced category is exact and such that S.f is a mono,
then a morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0 lifts to a morphism A ⟶ S.X₁.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.lift_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
[CategoryTheory.Mono S.f]
{Z : C}
(h : S.X₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.lift_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
[CategoryTheory.Mono S.f]
:
theorem
CategoryTheory.ShortComplex.Exact.lift'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
[CategoryTheory.Mono S.f]
:
∃ (l : A ⟶ S.X₁), CategoryTheory.CategoryStruct.comp l S.f = k
noncomputable def
CategoryTheory.ShortComplex.Exact.desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
[CategoryTheory.Epi S.g]
:
S.X₃ ⟶ A
If a short complex S in a balanced category is exact and such that S.g is an epi,
then a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.X₃ ⟶ A.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.g_desc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
[CategoryTheory.Epi S.g]
{Z : C}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.g_desc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
[CategoryTheory.Epi S.g]
:
theorem
CategoryTheory.ShortComplex.Exact.desc'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}
[CategoryTheory.Balanced C]
(hS : CategoryTheory.ShortComplex.Exact S)
{A : C}
(k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
[CategoryTheory.Epi S.g]
:
∃ (l : S.X₃ ⟶ A), CategoryTheory.CategoryStruct.comp S.g l = k
theorem
CategoryTheory.ShortComplex.mono_τ₂_of_exact_of_mono
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Balanced C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(h₁ : CategoryTheory.ShortComplex.Exact S₁)
[CategoryTheory.Mono S₁.f]
[CategoryTheory.Mono S₂.f]
[CategoryTheory.Mono φ.τ₁]
[CategoryTheory.Mono φ.τ₃]
:
CategoryTheory.Mono φ.τ₂
theorem
CategoryTheory.ShortComplex.epi_τ₂_of_exact_of_epi
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Balanced C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(h₂ : CategoryTheory.ShortComplex.Exact S₂)
[CategoryTheory.Epi S₁.g]
[CategoryTheory.Epi S₂.g]
[CategoryTheory.Epi φ.τ₁]
[CategoryTheory.Epi φ.τ₃]
:
CategoryTheory.Epi φ.τ₂
theorem
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hf₁ : S₁.f = 0)
(hg₁ : S₁.g = 0)
(hf₂ : S₂.f = 0)
:
CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.ShortComplex.Exact
(CategoryTheory.ShortComplex.mk φ.τ₂ S₂.g (_ : CategoryTheory.CategoryStruct.comp φ.τ₂ S₂.g = 0)) ∧ CategoryTheory.Mono φ.τ₂
Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.f
and S₁.g are zero (e.g. when S₁ is of the form 0 ⟶ S₁.X₂ ⟶ 0) and S₂.f = 0
(e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ S₂.X₃), then φ is a quasi-isomorphism iff
the obvious short complex S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃ is exact and φ.τ₂ is a mono).
theorem
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S₁ : CategoryTheory.ShortComplex C}
{S₂ : CategoryTheory.ShortComplex C}
(φ : S₁ ⟶ S₂)
(hg₁ : S₁.g = 0)
(hf₂ : S₂.f = 0)
(hg₂ : S₂.g = 0)
:
CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.ShortComplex.Exact
(CategoryTheory.ShortComplex.mk S₁.f φ.τ₂ (_ : CategoryTheory.CategoryStruct.comp S₁.f φ.τ₂ = 0)) ∧ CategoryTheory.Epi φ.τ₂
Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.g = 0
(e.g when S₁ is of the form S₁.X₁ ⟶ S₁.X₂ ⟶ 0) and both S₂.f and S₂.g are zero
(e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ 0), then φ is a quasi-isomorphism iff
the obvious short complex S₁.X₂ ⟶ S₁.X₂ ⟶ S₂.X₂ is exact and φ.τ₂ is an epi).
noncomputable def
CategoryTheory.ShortComplex.Exact.descToInjective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{J : C}
(f : S.X₂ ⟶ J)
[CategoryTheory.Injective J]
(hf : CategoryTheory.CategoryStruct.comp S.f f = 0)
:
S.X₃ ⟶ J
If S is an exact short complex and f : S.X₂ ⟶ J is a morphism to an injective object J
such that S.f ≫ f = 0, this is a morphism φ : S.X₃ ⟶ J such that S.g ≫ φ = f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.comp_descToInjective_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{J : C}
(f : S.X₂ ⟶ J)
[CategoryTheory.Injective J]
(hf : CategoryTheory.CategoryStruct.comp S.f f = 0)
{Z : C}
(h : J ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.comp_descToInjective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{J : C}
(f : S.X₂ ⟶ J)
[CategoryTheory.Injective J]
(hf : CategoryTheory.CategoryStruct.comp S.f f = 0)
:
noncomputable def
CategoryTheory.ShortComplex.Exact.liftFromProjective
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{P : C}
(f : P ⟶ S.X₂)
[CategoryTheory.Projective P]
(hf : CategoryTheory.CategoryStruct.comp f S.g = 0)
:
P ⟶ S.X₁
If S is an exact short complex and f : P ⟶ S.X₂ is a morphism from a projective object P
such that f ≫ S.g = 0, this is a morphism φ : P ⟶ S.X₁ such that φ ≫ S.f = f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{P : C}
(f : P ⟶ S.X₂)
[CategoryTheory.Projective P]
(hf : CategoryTheory.CategoryStruct.comp f S.g = 0)
{Z : C}
(h : S.X₂ ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C}
(hS : CategoryTheory.ShortComplex.Exact S)
{P : C}
(f : P ⟶ S.X₂)
[CategoryTheory.Projective P]
(hf : CategoryTheory.CategoryStruct.comp f S.g = 0)
:
instance
CategoryTheory.Functor.instPreservesMonomorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
:
Equations
instance
CategoryTheory.Functor.instReflectsMonomorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
[CategoryTheory.Faithful F]
[CategoryTheory.CategoryWithHomology C]
:
Equations
instance
CategoryTheory.Functor.instPreservesEpimorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
:
Equations
instance
CategoryTheory.Functor.instReflectsEpimorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Preadditive C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
[CategoryTheory.Functor.PreservesZeroMorphisms F]
[CategoryTheory.Functor.PreservesHomology F]
[CategoryTheory.Faithful F]
[CategoryTheory.CategoryWithHomology C]
:
Equations
noncomputable def
CategoryTheory.ShortComplex.Splitting.ofExactOfSection
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Balanced C]
(S : CategoryTheory.ShortComplex C)
(hS : CategoryTheory.ShortComplex.Exact S)
(s : S.X₃ ⟶ S.X₂)
(s_g : CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
(hf : CategoryTheory.Mono S.f)
:
This is the splitting of a short complex S in a balanced category induced by
a section of the morphism S.g : S.X₂ ⟶ S.X₃
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Balanced C]
(S : CategoryTheory.ShortComplex C)
(hS : CategoryTheory.ShortComplex.Exact S)
(r : S.X₂ ⟶ S.X₁)
(f_r : CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
(hg : CategoryTheory.Epi S.g)
:
This is the splitting of a short complex S in a balanced category induced by
a retraction of the morphism S.f : S.X₁ ⟶ S.X₂
Equations
- One or more equations did not get rendered due to their size.