Documentation

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

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
  • ⋯ = ⋯
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
Instances For
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.moduleCatMk_X₂ {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₂ = ModuleCat.of R 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) :
    (CategoryTheory.ShortComplex.moduleCatMk f g hfg).g = ModuleCat.asHom g
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.moduleCatMk_X₃ {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₃ = ModuleCat.of R X₃
    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) :
    (CategoryTheory.ShortComplex.moduleCatMk f g hfg).f = ModuleCat.asHom f
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.moduleCatMk_X₁ {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₁ = 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₁ X₂ 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
    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 ≤ LinearMap.ker g) :
      (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 ≤ LinearMap.ker g) :
      (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 ≤ LinearMap.ker g) :
      (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 ≤ LinearMap.ker g) :
      (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 ≤ 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₁ X₂ 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
        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
          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