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

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

(CategoryTheory.forget₂ (ModuleCat R) Ab).PreservesHomology

Equations

CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂ = { preservesKernels := inferInstance, preservesCokernels := inferInstance }

source

def CategoryTheory.ShortComplex.moduleCatMk {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

CategoryTheory.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 = CategoryTheory.ShortComplex.mk (ModuleCat.asHom f) (ModuleCat.asHom g) hfg

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₂ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₂ = ModuleCat.of R X₂

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_g {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).g = ModuleCat.asHom g

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₃ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₃ = ModuleCat.of R X₃

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_f {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).f = ModuleCat.asHom f

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_X₁ {R : Type u} [Ring R] {X₁ : Type v} {X₂ : Type v} {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₁ = ModuleCat.of R X₁

source

@[simp]

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

S.g (S.f x) = 0

source

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

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

source

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

S.Exact ↔ LinearMap.ker S.g ≤ LinearMap.range S.f

source

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

S.Exact ↔ LinearMap.range S.f = LinearMap.ker S.g

source

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

LinearMap.range S.f = LinearMap.ker S.g

source

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

Function.Injective ⇑S.f

source

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

Function.Surjective ⇑S.g

source

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

S.Exact ↔ Function.Exact ⇑S.f ⇑S.g

source

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

CategoryTheory.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 = CategoryTheory.ShortComplex.mk f g ⋯

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).f = f

source

@[simp]

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

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

source

@[simp]

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

(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g hfg).g = g

source

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

(CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g ⋯).Exact

source

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

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

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

Equations

S.moduleCatToCycles = { toFun := fun (x : ↑S.X₁) => ⟨S.f x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

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

↑(S.moduleCatToCycles x) = S.f x

source

@[reducible, inline]

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

ModuleCat R

The homology of S, defined as the quotient of the kernel of S.g by the image of S.moduleCatToCycles

Equations

S.moduleCatHomology = ModuleCat.of R (↥(LinearMap.ker S.g) ⧸ LinearMap.range S.moduleCatToCycles)

Instances For

source

@[reducible, inline]

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

ModuleCat.of R ↥(LinearMap.ker S.g) ⟶ S.moduleCatHomology

The canonical map ModuleCat.of R (LinearMap.ker S.g) ⟶ S.moduleCatHomology.

Equations

S.moduleCatHomologyπ = (LinearMap.range S.moduleCatToCycles).mkQ

Instances For

source

def CategoryTheory.ShortComplex.moduleCatLeftHomologyData {R : Type u} [Ring R] (S : CategoryTheory.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.

Equations

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

Instances For

source

@[simp]

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

S.moduleCatLeftHomologyData.π = S.moduleCatHomologyπ

source

@[simp]

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

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

source

@[simp]

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

S.moduleCatLeftHomologyData.i = (LinearMap.ker S.g).subtype

source

@[simp]

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

S.moduleCatLeftHomologyData.H = S.moduleCatHomology

source

@[simp]

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

S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles

source

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

CategoryTheory.Epi S.moduleCatHomologyπ

Equations

⋯ = ⋯

source

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

S.cycles ≅ ModuleCat.of R ↥(LinearMap.ker S.g)

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_subtype {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom (LinearMap.ker S.g).subtype = S.iCycles

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom (CategoryTheory.CategoryStruct.comp (LinearMap.ker S.g).subtype h) = CategoryTheory.CategoryStruct.comp S.iCycles h

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_subtype_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : (CategoryTheory.forget (ModuleCat R)).obj S.cycles) :

(LinearMap.ker S.g).subtype (S.moduleCatCyclesIso.hom x) = S.iCycles x

source

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

h ((LinearMap.ker S.g).subtype (S.moduleCatCyclesIso.hom x)) = h (S.iCycles x)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.iCycles = (LinearMap.ker S.g).subtype

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv (CategoryTheory.CategoryStruct.comp S.iCycles h) = CategoryTheory.CategoryStruct.comp (LinearMap.ker S.g).subtype h

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R ↥(LinearMap.ker S.g))) :

S.iCycles (S.moduleCatCyclesIso.inv x) = (LinearMap.ker S.g).subtype x

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R ↥(LinearMap.ker S.g))) :

h (S.iCycles (S.moduleCatCyclesIso.inv x)) = h ((LinearMap.ker S.g).subtype x)

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.toCycles S.moduleCatCyclesIso.hom = S.moduleCatToCycles

source

@[simp]

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : ModuleCat.of R ↥(LinearMap.ker S.g) ⟶ Z) :

CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom h) = CategoryTheory.CategoryStruct.comp S.moduleCatToCycles h

source

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

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

source

theorem CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : ModuleCat.of R ↥(LinearMap.ker S.g) ⟶ Z) (x : (CategoryTheory.forget (ModuleCat R)).obj S.X₁) :

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

source

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

S.homology ≅ S.moduleCatHomology

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

S.moduleCatHomologyIso = S.moduleCatLeftHomologyData.homologyIso

Instances For

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.homologyπ S.moduleCatHomologyIso.hom = CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatHomologyπ

source

@[simp]

theorem CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.moduleCatHomology ⟶ Z) :

CategoryTheory.CategoryStruct.comp S.homologyπ (CategoryTheory.CategoryStruct.comp S.moduleCatHomologyIso.hom h) = CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom (CategoryTheory.CategoryStruct.comp S.moduleCatHomologyπ h)

source

theorem CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : (CategoryTheory.forget (ModuleCat R)).obj S.cycles) :

S.moduleCatHomologyIso.hom (S.homologyπ x) = S.moduleCatHomologyπ (S.moduleCatCyclesIso.hom x)

source

theorem CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.moduleCatHomology ⟶ Z) (x : (CategoryTheory.forget (ModuleCat R)).obj S.cycles) :

h (S.moduleCatHomologyIso.hom (S.homologyπ x)) = h (S.moduleCatHomologyπ (S.moduleCatCyclesIso.hom x))

source

@[simp]

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

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv S.homologyπ = CategoryTheory.CategoryStruct.comp S.moduleCatHomologyπ S.moduleCatHomologyIso.inv

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.homology ⟶ Z) :

CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.inv (CategoryTheory.CategoryStruct.comp S.homologyπ h) = CategoryTheory.CategoryStruct.comp S.moduleCatHomologyπ (CategoryTheory.CategoryStruct.comp S.moduleCatHomologyIso.inv h)

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R ↥(LinearMap.ker S.g))) :

S.homologyπ (S.moduleCatCyclesIso.inv x) = S.moduleCatHomologyIso.inv (S.moduleCatHomologyπ x)

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.homology ⟶ Z) (x : (CategoryTheory.forget (ModuleCat R)).obj (ModuleCat.of R ↥(LinearMap.ker S.g))) :

h (S.homologyπ (S.moduleCatCyclesIso.inv x)) = h (S.moduleCatHomologyIso.inv (S.moduleCatHomologyπ x))

source

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

S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles

Documentation

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Homology and exactness of short complexes of modules #