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.
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)
:
Constructor for short complexes in ModuleCat.{v} R taking as inputs
linear maps f and g and the vanishing of their composition.
Equations
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCat_zero_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.X₁)
:
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₂
theorem
CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
theorem
CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
theorem
CategoryTheory.ShortComplex.Exact.moduleCat_range_eq_ker
{R : Type u}
[Ring R]
{S : ShortComplex (ModuleCat R)}
(hS : S.Exact)
:
theorem
CategoryTheory.ShortComplex.ShortExact.moduleCat_injective_f
{R : Type u}
[Ring R]
{S : ShortComplex (ModuleCat R)}
(hS : S.ShortExact)
:
theorem
CategoryTheory.ShortComplex.ShortExact.moduleCat_surjective_g
{R : Type u}
[Ring R]
{S : ShortComplex (ModuleCat R)}
(hS : S.ShortExact)
:
theorem
CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
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)
:
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
Instances For
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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
@[reducible, inline]
abbrev
CategoryTheory.ShortComplex.moduleCatToCycles
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
The canonical linear map S.X₁ →ₗ[R] LinearMap.ker S.g induced by S.f.
Equations
Instances For
def
CategoryTheory.ShortComplex.moduleCatLeftHomologyData
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
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
Instances For
@[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)
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[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)
:
@[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)
:
noncomputable def
CategoryTheory.ShortComplex.moduleCatCyclesIso
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
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
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
{Z : ModuleCat R}
(h : S.X₂ ⟶ Z)
:
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) ↑((ConcreteCategory.hom S.moduleCatCyclesIso.hom) x) = (ConcreteCategory.hom h) ((ConcreteCategory.hom S.iCycles) x)
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.cycles)
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
{Z : ModuleCat R}
(h : S.X₂ ⟶ Z)
:
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.moduleCatLeftHomologyData.K)
:
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) ↑x
@[simp]
theorem
CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[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)
:
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)
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
noncomputable def
CategoryTheory.ShortComplex.moduleCatOpcyclesIso
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
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
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[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)
:
@[simp]
theorem
CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.X₂)
:
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
theorem
CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.X₂)
:
noncomputable def
CategoryTheory.ShortComplex.moduleCatHomologyIso
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
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
Instances For
@[simp]
theorem
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
{Z : ModuleCat R}
(h : S.moduleCatLeftHomologyData.H ⟶ Z)
:
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)
:
theorem
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.cycles)
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[simp]
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
{Z : ModuleCat R}
(h : S.homology ⟶ Z)
:
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)
:
theorem
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
(x : ↑S.moduleCatLeftHomologyData.K)
:
theorem
CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles
{R : Type u}
[Ring R]
(S : ShortComplex (ModuleCat R))
:
@[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)
:
Given a linear map f : M → N, we can obtain a short complex 0 → ker(f) → M → N.
Equations
Instances For
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)
: