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] :

(CategoryTheory.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) :

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.ofHom f) (ModuleCat.ofHom g) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_f_hom {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).f.hom = f

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) :

↑(CategoryTheory.ShortComplex.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) :

(CategoryTheory.ShortComplex.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) :

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

source

@[simp]

theorem CategoryTheory.ShortComplex.moduleCatMk_g_hom {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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).g.hom = g

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) :

↑(CategoryTheory.ShortComplex.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) :

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

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) :

(CategoryTheory.ShortComplex.moduleCatMk f g hfg).X₃.isAddCommGroup = 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) :

(CategoryTheory.ShortComplex.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) :

(CategoryTheory.ShortComplex.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) :

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

source

@[simp]

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

S.g.hom (S.f.hom 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.hom x₂ = 0 → ∃ (x₁ : ↑S.X₁), S.f.hom 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.hom ≤ LinearMap.range S.f.hom

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.hom = LinearMap.ker S.g.hom

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.hom = LinearMap.ker S.g.hom

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.hom

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.hom

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.hom ⇑S.g.hom

source

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

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₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range f.hom ≤ LinearMap.ker g.hom) :

(CategoryTheory.ShortComplex.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 f.hom ≤ LinearMap.ker g.hom) :

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

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 f.hom ≤ LinearMap.ker g.hom) :

(CategoryTheory.ShortComplex.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 f.hom ≤ LinearMap.ker g.hom) :

(CategoryTheory.ShortComplex.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 f.hom ≤ LinearMap.ker g.hom) :

(CategoryTheory.ShortComplex.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 f.hom = LinearMap.ker g.hom) :

(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.hom)

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.hom 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.hom 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.hom) ⧸ 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.hom) ⟶ S.moduleCatHomology

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

Equations

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

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

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

S.moduleCatLeftHomologyData.π = S.moduleCatHomologyπ

source

@[simp]

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

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

source

@[simp]

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

S.moduleCatLeftHomologyData.f' = ModuleCat.ofHom S.moduleCatToCycles

source

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

CategoryTheory.Epi S.moduleCatHomologyπ

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.hom)

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 (ModuleCat.ofHom (LinearMap.ker S.g.hom).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 : ModuleCat.of R ↑S.X₂ ⟶ Z) :

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

source

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

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

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) :

(ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype) (S.moduleCatCyclesIso.hom x) = 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 = ModuleCat.ofHom (LinearMap.ker S.g.hom).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 (ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype) h

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.hom))) :

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

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.hom))) :

S.iCycles (S.moduleCatCyclesIso.inv x) = (ModuleCat.ofHom (LinearMap.ker S.g.hom).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 = ModuleCat.ofHom 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.hom) ⟶ Z) :

CategoryTheory.CategoryStruct.comp S.toCycles (CategoryTheory.CategoryStruct.comp S.moduleCatCyclesIso.hom h) = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom 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) = (ModuleCat.ofHom 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.hom) ⟶ Z) (x : (CategoryTheory.forget (ModuleCat R)).obj S.X₁) :

h (S.moduleCatCyclesIso.hom (S.toCycles x)) = h ((ModuleCat.ofHom 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_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

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

@[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_π_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.hom))) :

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

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.hom))) :

S.homologyπ (S.moduleCatCyclesIso.inv x) = 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 #