# Documentation

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

# Homology and exactness of short complexes of modules #

In this file, the homology of a short complex S of abelian groups is identified with the quotient of LinearMap.ker S.g by the image of the morphism S.moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g induced by S.f.

@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMk_X₂ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :
().X₂ = ModuleCat.of R X₂
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMk_f {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :
().f =
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMk_X₁ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :
().X₁ = ModuleCat.of R X₁
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMk_X₃ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :
().X₃ = ModuleCat.of R X₃
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMk_g {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :
().g =
def CategoryTheory.ShortComplex.moduleCatMk {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {X₃ : Type v} [] [] [] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : = 0) :

Constructor for short complexes in ModuleCat.{v} R taking as inputs linear maps f and g and the vanishing of their composition.

Equations
Instances For
@[simp]
theorem CategoryTheory.ShortComplex.moduleCat_zero_apply {R : Type u} [Ring R] (S : ) (x : S.X₁) :
S.g (S.f x) = 0
theorem CategoryTheory.ShortComplex.moduleCat_exact_iff {R : Type u} [Ring R] (S : ) :
∀ (x₂ : S.X₂), S.g x₂ = 0∃ (x₁ : S.X₁), S.f x₁ = x₂
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_g {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
= g
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₁ {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
.X₁ = X₁
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₂ {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
.X₂ = X₂
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₃ {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
.X₃ = X₃
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_f {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
= f
def CategoryTheory.ShortComplex.moduleCatMkOfKerLERange {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :

Constructor for short complexes in ModuleCat.{v} R taking as inputs morphisms f and g and the assumption LinearMap.range f ≤ LinearMap.ker g.

Equations
Instances For
theorem CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker {R : Type u} [Ring R] {X₁ : } {X₂ : } {X₃ : } (f : X₁ X₂) (g : X₂ X₃) (hfg : ) :
@[simp]
theorem CategoryTheory.ShortComplex.moduleCatToCycles_apply_coe {R : Type u} [Ring R] (S : ) (x : S.X₁) :
= S.f x
def CategoryTheory.ShortComplex.moduleCatToCycles {R : Type u} [Ring R] (S : ) :
S.X₁ →ₗ[R] ()

The canonical linear map S.X₁ →ₗ[R] LinearMap.ker S.g induced by S.f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

The explicit left homology data of a short complex of modules that is given by a kernel and a quotient given by the LinearMap API.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.ShortComplex.moduleCatCyclesIso {R : Type u} [Ring R] (S : ) :

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

Equations
Instances For
noncomputable def CategoryTheory.ShortComplex.moduleCatHomologyIso {R : Type u} [Ring R] (S : ) :

Given a short complex S of modules, this is the isomorphism between the abstract S.homology of the homology API and the more explicit quotient of LinearMap.ker S.g by the image of S.moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g.

Equations
Instances For