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.

source

instance CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂ {R : Type u} [Ring R] :

(forget₂ (ModuleCat R) Ab).PreservesHomology

source

def CategoryTheory.ShortComplex.moduleCatMk {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

ShortComplex (ModuleCat R)

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

Equations

CategoryTheory.ShortComplex.moduleCatMk f g hfg = { X₁ := ModuleCat.of R X₁, X₂ := ModuleCat.of R X₂, X₃ := ModuleCat.of R X₃, f := ModuleCat.ofHom f, g := ModuleCat.ofHom g, zero := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₂_carrier {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

↑(moduleCatMk f g hfg).X₂ = X₂

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₂_isModule {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₂.isModule = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₁_isModule {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₁.isModule = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₃_isModule {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₃.isModule = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₁_isAddCommGroup {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₁.isAddCommGroup = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₁_carrier {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

↑(moduleCatMk f g hfg).X₁ = X₁

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₃_carrier {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

↑(moduleCatMk f g hfg).X₃ = X₃

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_f {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).f = ModuleCat.ofHom f

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₂_isAddCommGroup {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₂.isAddCommGroup = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₃_isAddCommGroup {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).X₃.isAddCommGroup = inst✝

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_g {R : Type u} [Ring R] {X₁ X₂ X₃ : Type v} [AddCommGroup X₁] [AddCommGroup X₂] [AddCommGroup X₃] [Module R X₁] [Module R X₂] [Module R X₃] (f : X₁ →ₗ[R] X₂) (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0) :

(moduleCatMk f g hfg).g = ModuleCat.ofHom g

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCat_zero_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) (x : ↑S.X₁) :

(ConcreteCategory.hom S.g) ((ConcreteCategory.hom S.f) x) = 0

source

theorem CategoryTheory.ShortComplex.moduleCat_exact_iff {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.Exact ↔ ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ (x₁ : ↑S.X₁), (ConcreteCategory.hom S.f) x₁ = x₂

source

theorem CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.Exact ↔ LinearMap.ker (ModuleCat.Hom.hom S.g) ≤ LinearMap.range (ModuleCat.Hom.hom S.f)

source

theorem CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.Exact ↔ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

source

theorem CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker {R : Type u} [Ring R] {S : ShortComplex (ModuleCat R)} (hS : S.Exact) :

LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

source

theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_injective_f {R : Type u} [Ring R] {S : ShortComplex (ModuleCat R)} (hS : S.ShortExact) :

Function.Injective ⇑(ConcreteCategory.hom S.f)

source

theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_surjective_g {R : Type u} [Ring R] {S : ShortComplex (ModuleCat R)} (hS : S.ShortExact) :

Function.Surjective ⇑(ConcreteCategory.hom S.g)

source

theorem CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

source

def CategoryTheory.ShortComplex.moduleCatMkOfKerLERange {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

ShortComplex (ModuleCat R)

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

CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg = { X₁ := X₁, X₂ := X₂, X₃ := X₃, f := f, g := g, zero := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_f {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g hfg).f = f

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₃ {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g hfg).X₃ = X₃

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₁ {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g hfg).X₁ = X₁

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₂ {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g hfg).X₂ = X₂

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_g {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) ≤ LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g hfg).g = g

source

theorem CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range (ModuleCat.Hom.hom f) = LinearMap.ker (ModuleCat.Hom.hom g)) :

(moduleCatMkOfKerLERange f g ⋯).Exact

source

@[reducible, inline]

abbrev CategoryTheory.ShortComplex.moduleCatToCycles {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

↑S.X₁ →ₗ[R] ↥(LinearMap.ker (ModuleCat.Hom.hom S.g))

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

Equations

S.moduleCatToCycles = LinearMap.codRestrict (LinearMap.ker (ModuleCat.Hom.hom S.g)) (ModuleCat.Hom.hom S.f) ⋯

Instances For

source

def CategoryTheory.ShortComplex.moduleCatLeftHomologyData {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.LeftHomologyData

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. The projections to K and H are not simp lemmas because the generic lemmas about LeftHomologyData are more useful here.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.moduleCatLeftHomologyData.H = ModuleCat.of R (↥(LinearMap.ker (ModuleCat.Hom.hom S.g)) ⧸ LinearMap.range S.moduleCatToCycles)

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.i = (LinearMap.ker (ModuleCat.Hom.hom S.g)).subtype

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.moduleCatLeftHomologyData.K = ModuleCat.of R ↥(LinearMap.ker (ModuleCat.Hom.hom S.g))

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.π = (LinearMap.range S.moduleCatToCycles).mkQ

source

@[reducible, inline, deprecated "This abbreviation is now inlined" (since := "2025-05-14")]

abbrev CategoryTheory.ShortComplex.moduleCatHomology {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat R

The homology of a short complex of modules as a concrete quotient.

Equations

S.moduleCatHomology = S.moduleCatLeftHomologyData.H

Instances For

source

@[reducible, inline, deprecated "This abbreviation is now inlined" (since := "2025-05-14")]

abbrev CategoryTheory.ShortComplex.moduleCatHomologyπ {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.moduleCatLeftHomologyData.K ⟶ S.moduleCatLeftHomologyData.H

The natural projection map to the homology of a short complex of modules as a concrete quotient.

Equations

S.moduleCatHomologyπ = S.moduleCatLeftHomologyData.π

Instances For

source

@[deprecated CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom (since := "2025-05-09")]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.i = (LinearMap.ker (ModuleCat.Hom.hom S.g)).subtype

Alias of CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom.

source

@[deprecated CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom (since := "2025-05-09")]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.π = (LinearMap.range S.moduleCatToCycles).mkQ

Alias of CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom.

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles

source

@[deprecated CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom (since := "2025-05-09")]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f' {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles

Alias of CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom.

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {M : ModuleCat R} (φ : S.moduleCatLeftHomologyData.K ⟶ M) (h : CategoryStruct.comp S.moduleCatLeftHomologyData.f' φ = 0) :

ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.descH φ h) = (LinearMap.range (ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f')).liftQ (ModuleCat.Hom.hom φ) ⋯

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {M : ModuleCat R} (φ : M ⟶ S.X₂) (h : CategoryStruct.comp φ S.g = 0) :

ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.liftK φ h) = LinearMap.codRestrict (LinearMap.ker (ModuleCat.Hom.hom S.g)) (ModuleCat.Hom.hom φ) ⋯

source

noncomputable def CategoryTheory.ShortComplex.moduleCatCyclesIso {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.cycles ≅ S.moduleCatLeftHomologyData.K

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

S.moduleCatCyclesIso = S.moduleCatLeftHomologyData.cyclesIso

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatLeftHomologyData.i = S.iCycles

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp S.moduleCatCyclesIso.hom (CategoryStruct.comp S.moduleCatLeftHomologyData.i h) = CategoryStruct.comp S.iCycles h

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) (x : ToType S.cycles) :

↑((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x) = (ConcreteCategory.hom S.iCycles) x

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) (x : ToType S.cycles) :

(ConcreteCategory.hom h) ↑((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x) = (ConcreteCategory.hom h) ((ConcreteCategory.hom S.iCycles) x)

source

@[deprecated CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i (since := "2025-05-09")]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_subtype {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatLeftHomologyData.i = S.iCycles

Alias of CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i.

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

CategoryStruct.comp S.moduleCatCyclesIso.inv S.iCycles = S.moduleCatLeftHomologyData.i

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp S.moduleCatCyclesIso.inv (CategoryStruct.comp S.iCycles h) = CategoryStruct.comp S.moduleCatLeftHomologyData.i h

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) (x : ToType S.moduleCatLeftHomologyData.K) :

(ConcreteCategory.hom h) ((ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x)) = (ConcreteCategory.hom h) ↑x

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) (x : ToType S.moduleCatLeftHomologyData.K) :

(ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x) = ↑x

source

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

CategoryStruct.comp S.toCycles S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f'

source

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.moduleCatLeftHomologyData.K ⟶ Z) :

CategoryStruct.comp S.toCycles (CategoryStruct.comp S.moduleCatCyclesIso.hom h) = CategoryStruct.comp S.moduleCatLeftHomologyData.f' h

source

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) (x : ToType S.X₁) :

(ConcreteCategory.hom S.moduleCatCyclesIso.hom) ((ConcreteCategory.hom S.toCycles) x) = S.moduleCatToCycles x

source

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.moduleCatLeftHomologyData.K ⟶ Z) (x : ToType S.X₁) :

(ConcreteCategory.hom h) ((ConcreteCategory.hom S.moduleCatCyclesIso.hom) ((ConcreteCategory.hom S.toCycles) x)) = (ConcreteCategory.hom h) (S.moduleCatToCycles x)

source

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

S.homology ≅ S.moduleCatLeftHomologyData.H

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