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.

Equations
  • CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂ = { preservesKernels := inferInstance, preservesCokernels := inferInstance }
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :

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.moduleCat_zero_apply {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : S.X₁) :
    S.g (S.f x) = 0
    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₂
    @[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) :
    @[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) :
    @[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) :
    @[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) :
    @[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) :
    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) :

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

      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
        @[reducible, inline]

        The homology of S, defined as the quotient of the kernel of S.g by the image of S.moduleCatToCycles

        Equations
        Instances For
          @[reducible, inline]

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

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :
            S.moduleCatLeftHomologyData = S.moduleCatHomologyπ
            @[simp]
            theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :
            S.moduleCatLeftHomologyData.i = (LinearMap.ker S.g).subtype
            @[simp]
            theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :
            S.moduleCatLeftHomologyData.H = S.moduleCatHomology

            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
              @[simp]
              theorem CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f' {R : Type u} [Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) :
              S.moduleCatLeftHomologyData.f' = S.moduleCatToCycles

              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
                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
                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)
                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)
                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
                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)
                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
                @[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
                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
                  @[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)
                  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))
                  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)
                  @[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π
                  @[simp]
                  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)
                  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))
                  @[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