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.instPreservesHomologyModuleCatAbModuleCategoryInstAddCommGroupCatLargeCategoryPreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategoryPreadditiveHasZeroMorphismsInstPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategoryForget₂ModuleConcreteCategoryConcreteCategoryHasForgetToAddCommGroupPreservesZeroMorphisms_of_additiveForget₂_addCommGroupCat_additive {R : Type u} [Ring R] :

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

Equations

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

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.ofHom 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_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.ofHom f

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

Instances For

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

CategoryTheory.ShortComplex.Exact S ↔ ∀ (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)) :

CategoryTheory.ShortComplex.Exact S ↔ 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)) :

CategoryTheory.ShortComplex.Exact S ↔ 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 : CategoryTheory.ShortComplex.Exact S) :

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

Function.Injective ⇑S.f

source

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

Function.Surjective ⇑S.g

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

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 (_ : CategoryTheory.CategoryStruct.comp f g = 0)

Instances For

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.Exact (CategoryTheory.ShortComplex.moduleCatMkOfKerLERange f g (_ : LinearMap.range f ≤ LinearMap.ker g))

source

@[simp]

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

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

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

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

Instances For

source

@[inline, reducible]

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

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

Instances For

source

@[inline, reducible]

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

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

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

Equations

CategoryTheory.ShortComplex.moduleCatHomologyπ S = Submodule.mkQ (LinearMap.range (CategoryTheory.ShortComplex.moduleCatToCycles S))

Instances For

source

@[simp]

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

(CategoryTheory.ShortComplex.moduleCatLeftHomologyData S).i = Submodule.subtype (LinearMap.ker S.g)

source

@[simp]

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

(CategoryTheory.ShortComplex.moduleCatLeftHomologyData S).H = CategoryTheory.ShortComplex.moduleCatHomology S

source

@[simp]

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

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

source

@[simp]

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

(CategoryTheory.ShortComplex.moduleCatLeftHomologyData S).π = CategoryTheory.ShortComplex.moduleCatHomologyπ S

source

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

CategoryTheory.ShortComplex.LeftHomologyData S

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

CategoryTheory.ShortComplex.LeftHomologyData.f' (CategoryTheory.ShortComplex.moduleCatLeftHomologyData S) = CategoryTheory.ShortComplex.moduleCatToCycles S

source

instance CategoryTheory.ShortComplex.instEpiModuleCatModuleCategoryOfSubtypeCarrierX₂PreadditiveHasZeroMorphismsInstPreadditiveModuleCatModuleCategoryMemSubmoduleToSemiringToAddCommMonoidIsAddCommGroupIsModuleInstMembershipSetLikeKerX₃IdToNonAssocSemiringHomToQuiverToCategoryStructInstFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierInstLinearMapClassHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierToSemiringToAddCommMonoidIsAddCommGroupIsModuleInstFunLikeHomModuleCatToQuiverToCategoryStructModuleCategoryCarrierGAddCommGroupModuleModuleCatHomologyModuleCatHomologyπ {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :

CategoryTheory.Epi (CategoryTheory.ShortComplex.moduleCatHomologyπ S)

Equations

(_ : CategoryTheory.Epi (CategoryTheory.ShortComplex.moduleCatHomologyπ S)) = (_ : CategoryTheory.Epi (CategoryTheory.ShortComplex.moduleCatLeftHomologyData S).π)

source

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

CategoryTheory.ShortComplex.cycles S ≅ 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

CategoryTheory.ShortComplex.moduleCatCyclesIso S = CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso (CategoryTheory.ShortComplex.moduleCatLeftHomologyData S)

Instances For

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 (CategoryTheory.ShortComplex.moduleCatCyclesIso S).hom (CategoryTheory.CategoryStruct.comp (Submodule.subtype (LinearMap.ker S.g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.iCycles S) h

source

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

(Submodule.subtype (LinearMap.ker S.g)) ((CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso (CategoryTheory.ShortComplex.moduleCatLeftHomologyData S)).hom x) = (CategoryTheory.ShortComplex.iCycles S) 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)).toPrefunctor.obj (CategoryTheory.ShortComplex.cycles S)) :

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

source

@[simp]

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

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

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

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)).toPrefunctor.obj (ModuleCat.of R ↥(LinearMap.ker S.g))) :

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

source

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

(CategoryTheory.ShortComplex.iCycles S) ((CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso (CategoryTheory.ShortComplex.moduleCatLeftHomologyData S)).inv x) = (Submodule.subtype (LinearMap.ker S.g)) x

source

@[simp]

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

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

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 (CategoryTheory.ShortComplex.toCycles S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.moduleCatCyclesIso S).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.moduleCatToCycles S) h

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)).toPrefunctor.obj S.X₁) :

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

source

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

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

source

@[simp]

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

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

source

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

CategoryTheory.ShortComplex.homology S ≅ CategoryTheory.ShortComplex.moduleCatHomology 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