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)
:
- condition : ∃ h, CategoryTheory.Limits.IsZero h.left.H
the condition that there exists an homology data whose
left.H
field is zero
The assertion that the short complex S : ShortComplex C
is exact.
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_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
@[simp]
@[simp]