Documentation

Mathlib.Algebra.Homology.ShortComplex.Ab

Homology and exactness of short complexes of abelian groups #

In this file, the homology of a short complex S of abelian groups is identified with the quotient of AddMonoidHom.ker S.g by the image of the morphism S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

The definitions are made in the ShortComplex namespace so as to enable dot notation. The names contain the prefix ab in order to allow similar constructions for other categories like ModuleCat.

Main definitions #

@[simp]
theorem CategoryTheory.ShortComplex.ab_zero_apply (S : CategoryTheory.ShortComplex Ab) (x : S.X₁) :
S.g (S.f x) = 0
@[simp]
theorem CategoryTheory.ShortComplex.abToCycles_apply_coe (S : CategoryTheory.ShortComplex Ab) (x : S.X₁) :
(S.abToCycles x) = S.f x

The canonical additive morphism S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.ShortComplex.abLeftHomologyData_H (S : CategoryTheory.ShortComplex Ab) :
    S.abLeftHomologyData.H = AddCommGrp.of ((AddMonoidHom.ker S.g) S.abToCycles.range)
    @[simp]

    The explicit left homology data of a short complex of abelian group that is given by a kernel and a quotient given by the AddMonoidHom API.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.ShortComplex.abLeftHomologyData_f' (S : CategoryTheory.ShortComplex Ab) :
      S.abLeftHomologyData.f' = S.abToCycles

      Given a short complex S of abelian groups, this is the isomorphism between the abstract S.cycles of the homology API and the more concrete description as AddMonoidHom.ker S.g.

      Equations
      • S.abCyclesIso = S.abLeftHomologyData.cyclesIso
      Instances For
        noncomputable def CategoryTheory.ShortComplex.abHomologyIso (S : CategoryTheory.ShortComplex Ab) :
        S.homology AddCommGrp.of ((AddMonoidHom.ker S.g) S.abToCycles.range)

        Given a short complex S of abelian groups, this is the isomorphism between the abstract S.homology of the homology API and the more explicit quotient of AddMonoidHom.ker S.g by the image of S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g.

        Equations
        • S.abHomologyIso = S.abLeftHomologyData.homologyIso
        Instances For
          theorem CategoryTheory.ShortComplex.ab_exact_iff (S : CategoryTheory.ShortComplex Ab) :
          S.Exact ∀ (x₂ : S.X₂), S.g x₂ = 0∃ (x₁ : S.X₁), S.f x₁ = x₂