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₂LinearMapIdCarrierAddMonoidHomCarrier {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₃_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_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.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₂_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.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 ↔ (ModuleCat.Hom.hom S.g).ker ≤ (ModuleCat.Hom.hom S.f).range

source

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

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

source

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

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

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 : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker) :

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_g {R : Type u} [Ring R] {X₁ X₂ X₃ : ModuleCat R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker) :

(moduleCatMkOfKerLERange f g hfg).g = g

source

@[simp]

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

(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 : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker) :

(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 : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker) :

(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 : (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker) :

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

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 : (ModuleCat.Hom.hom f).range = (ModuleCat.Hom.hom g).ker) :

(moduleCatMkOfKerLERange f g ⋯).Exact

source

@[reducible, inline]

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

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

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

Equations

S.moduleCatToCycles = LinearMap.codRestrict (ModuleCat.Hom.hom S.g).ker (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_K {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

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

source

@[simp]

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

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

source

@[simp]

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

ModuleCat.Hom.hom S.moduleCatLeftHomologyData.π = S.moduleCatToCycles.range.mkQ

source

@[simp]

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

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

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

@[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) = (ModuleCat.Hom.hom S.moduleCatLeftHomologyData.f').range.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 (ModuleCat.Hom.hom S.g).ker (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_assoc_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z) (x : ↑S.cycles) :

(ConcreteCategory.hom h) ((ModuleCat.Hom.hom S.g).ker.subtype ((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x)) = (ConcreteCategory.hom h) ((ConcreteCategory.hom S.iCycles) x)

source

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

(ModuleCat.Hom.hom S.g).ker.subtype ((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x) = (ConcreteCategory.hom S.iCycles) x

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 : ↑S.moduleCatLeftHomologyData.K) :

(ConcreteCategory.hom h) ((ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x)) = (ConcreteCategory.hom h) ((ModuleCat.Hom.hom S.g).ker.subtype x)

source

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

(ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x) = (ModuleCat.Hom.hom S.g).ker.subtype 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 : ↑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 : ↑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.moduleCatOpcyclesIso {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) :

S.opcycles ≅ ModuleCat.of R (↑S.X₂ ⧸ (ModuleCat.Hom.hom S.f).range)

Given a short complex S of modules, this is the isomorphism between the abstract S.opcycles of the homology API and the more concrete description as S.X₂ ⧸ LinearMap.range S.f.hom.

Equations

S.moduleCatOpcyclesIso = S.opcyclesIsoCokernel ≪≫ ModuleCat.cokernelIsoRangeQuotient S.f

Instances For

source

@[simp]

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

CategoryStruct.comp S.pOpcycles S.moduleCatOpcyclesIso.hom = ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ

source

@[simp]

theorem CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : ModuleCat.of R (↑S.X₂ ⧸ (ModuleCat.Hom.hom S.f).range) ⟶ Z) :

CategoryStruct.comp S.pOpcycles (CategoryStruct.comp S.moduleCatOpcyclesIso.hom h) = CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom S.f).range.mkQ) h

source

@[simp]

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

(ConcreteCategory.hom S.moduleCatOpcyclesIso.hom) ((ConcreteCategory.hom S.pOpcycles) x) = Submodule.Quotient.mk x

source

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

(ConcreteCategory.hom S.pOpcycles) x = (ConcreteCategory.hom S.pOpcycles) y ↔ x - y ∈ (ModuleCat.Hom.hom S.f).range

source

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

(ConcreteCategory.hom S.pOpcycles) x = 0 ↔ x ∈ (ModuleCat.Hom.hom S.f).range

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

S.moduleCatHomologyIso = S.moduleCatLeftHomologyData.homologyIso

Instances For

source

@[simp]

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

CategoryStruct.comp S.homologyπ S.moduleCatHomologyIso.hom = CategoryStruct.comp S.moduleCatCyclesIso.hom S.moduleCatLeftHomologyData.π

source

@[simp]

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

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

source

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

(ConcreteCategory.hom h) ((ConcreteCategory.hom S.moduleCatHomologyIso.hom) ((ConcreteCategory.hom S.homologyπ) x)) = (ConcreteCategory.hom h) (S.moduleCatToCycles.range.mkQ ((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x))

source

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

(ConcreteCategory.hom S.moduleCatHomologyIso.hom) ((ConcreteCategory.hom S.homologyπ) x) = S.moduleCatToCycles.range.mkQ ((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x)

source

@[simp]

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

CategoryStruct.comp S.moduleCatCyclesIso.inv S.homologyπ = CategoryStruct.comp S.moduleCatLeftHomologyData.π S.moduleCatHomologyIso.inv

source

@[simp]

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

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

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) (x : ↑S.moduleCatLeftHomologyData.K) :

(ConcreteCategory.hom S.homologyπ) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x) = (ConcreteCategory.hom S.moduleCatHomologyIso.inv) (S.moduleCatToCycles.range.mkQ x)

source

theorem CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply {R : Type u} [Ring R] (S : ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.homology ⟶ Z) (x : ↑S.moduleCatLeftHomologyData.K) :

(ConcreteCategory.hom h) ((ConcreteCategory.hom S.homologyπ) ((ConcreteCategory.hom S.moduleCatCyclesIso.inv) x)) = (ConcreteCategory.hom h) ((ConcreteCategory.hom S.moduleCatHomologyIso.inv) (S.moduleCatToCycles.range.mkQ x))

source

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

S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles

source

@[reducible, inline]

abbrev LinearMap.shortComplexKer {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) :

CategoryTheory.ShortComplex (ModuleCat R)

Given a linear map f : M → N, we can obtain a short complex 0 → ker(f) → M → N.

Equations

f.shortComplexKer = { X₁ := ModuleCat.of R ↥f.ker, X₂ := ModuleCat.of R M, X₃ := ModuleCat.of R N, f := ModuleCat.ofHom f.ker.subtype, g := ModuleCat.ofHom f, zero := ⋯ }

Instances For

source

theorem LinearMap.shortExact_shortComplexKer {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (h : Function.Surjective ⇑f) :

f.shortComplexKer.ShortExact

source

@[reducible, inline]

abbrev ModuleCat.shortComplexOfCompEqZero {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] {L : Type v} [AddCommGroup L] [Module R L] (f : M →ₗ[R] N) (g : N →ₗ[R] L) (eq0 : g ∘ₗ f = 0) :

CategoryTheory.ShortComplex (ModuleCat R)

The short complex in ModuleCat obtained from two linear map with composition equal to zero.

Equations

ModuleCat.shortComplexOfCompEqZero f g eq0 = { X₁ := ModuleCat.of R M, X₂ := ModuleCat.of R N, X₃ := ModuleCat.of R L, f := ModuleCat.ofHom f, g := ModuleCat.ofHom g, zero := ⋯ }

Instances For

source

theorem ModuleCat.shortComplex_exact {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (exac : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)) :

S.Exact

source

theorem ModuleCat.shortComplex_shortExact {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (exac : Function.Exact ⇑(CategoryTheory.ConcreteCategory.hom S.f) ⇑(CategoryTheory.ConcreteCategory.hom S.g)) (inj : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom S.f)) (surj : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom S.g)) :

S.ShortExact

source

@[reducible, inline]

abbrev ModuleCat.shortComplexOfConj {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] {L : Type v} [AddCommGroup L] [Module R L] {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup L'] [Module R M'] [Module R N'] [Module R L'] (eM : M ≃ₗ[R] M') (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (eq0 : g ∘ₗ f = 0) :

CategoryTheory.ShortComplex (ModuleCat R)

Suppose that f and g are linear maps that compose to zero, and that eM, eN, and eL indicated in the diagram below are linear equivalences to modules that all belong to the same universe. Then this is the short complex in ModuleCat given by the bottom row in the diagram. M --f--> N --g--> L | | | eM eN eL | | | v v v M'-----> N'-----> L' This complex is exact when we have Function.Exact f g, see ModuleCat.shortComplexOfConj_exact.

Equations

ModuleCat.shortComplexOfConj eM eN eL f g eq0 = ModuleCat.shortComplexOfCompEqZero ((↑eN.symm ∘ₗ f) ∘ₗ ↑eM) (↑eL.symm ∘ₗ g ∘ₗ ↑eN) ⋯

Instances For

source

theorem ModuleCat.shortComplexOfConj_exact {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] {L : Type v} [AddCommGroup L] [Module R L] {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup L'] [Module R M'] [Module R N'] [Module R L'] (eM : M ≃ₗ[R] M') (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (exact : Function.Exact ⇑f ⇑g) :

(shortComplexOfConj eM eN eL f g ⋯).Exact

source

theorem ModuleCat.shortComplexOfConj_shortExact {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] {L : Type v} [AddCommGroup L] [Module R L] {M' : Type u_1} {N' : Type u_2} {L' : Type u_3} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup L'] [Module R M'] [Module R N'] [Module R L'] (eM : M ≃ₗ[R] M') (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (exact : Function.Exact ⇑f ⇑g) (inj : Function.Injective ⇑f) (surj : Function.Surjective ⇑g) :

(shortComplexOfConj eM eN eL f g ⋯).ShortExact

Documentation

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Homology and exactness of short complexes of modules #