Documentation

TauCeti.CategoryTheory.Exact.Stable.Injective

Injective stable Hom spaces #

For an exact structure E, the injective stable category is the additive quotient by maps factoring through relatively injective objects. This is the costable category used on the Hom side of Auslander–Reiten duality; the algebra need not be self-injective.

An inflation i : X ⟶ I with relatively injective target computes its Hom spaces: HomCokernel R i Y is canonically the space of maps X ⟶ Y in the injective stable category. Indeed, a map factors through a relative injective exactly when it extends across i. The comparison works for any such inflation, so it does not depend on a choice of injective envelope or a minimal presentation. It is natural in the target.

The quotient category and its additive and linear structures use ObjectProperty.factorIdeal and MorphismIdeal.quotientFunctor.

References #

source
def TauCeti.ExactStructure.injectiveStableIdeal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
MorphismIdeal C

The ideal of morphisms factoring through objects injective relative to E.

Instances For
    source
    @[reducible, inline]
    abbrev TauCeti.ExactStructure.InjectiveStableCategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
    Type u

    The additive category obtained by killing morphisms through relative injectives.

    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.ExactStructure.injectiveStableFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
      CategoryTheory.Functor C E.InjectiveStableCategory

      The quotient functor to the injective stable category.

      Instances For
        source
        @[simp]
        theorem TauCeti.ExactStructure.mem_injectiveStableIdeal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : C} {f : X ⟶ Y} :
        f ∈ E.injectiveStableIdeal.hom X Y ↔ E.isInjective.FactorsThrough f

        Membership in the injective stable ideal is equivalent to a single factorization through a relative injective object.

        source
        @[simp]
        theorem TauCeti.ExactStructure.injectiveStableFunctor_map_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : C} {f : X ⟶ Y} :
        E.injectiveStableFunctor.map f = 0 ↔ E.isInjective.FactorsThrough f

        A morphism vanishes in the injective stable category exactly when it factors through a relative injective.

        source
        @[simp]
        theorem TauCeti.ExactStructure.isZero_injectiveStableFunctor_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (X : C) :
        CategoryTheory.Limits.IsZero (E.injectiveStableFunctor.obj X) ↔ E.isInjective X

        Precisely the relative injective objects become zero in the injective stable category.

        source
        theorem TauCeti.ExactStructure.injectiveStableFunctor_map_eq_zero_iff_mem_range {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (R : Type t) [Ring R] [CategoryTheory.Linear R C] {X I Y : C} (i : X ⟶ I) (hi : E.IsInflation i) (hI : E.isInjective I) (f : X ⟶ Y) :
        E.injectiveStableFunctor.map f = 0 ↔ f ∈ (CategoryTheory.Linear.leftComp R Y i).range

        An injective stable morphism is zero exactly when its representative belongs to the image of restriction from a fixed inflation into a relative injective.

        source
        noncomputable def TauCeti.ExactStructure.homCokernelEquivInjectiveStableHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (R : Type t) [Ring R] [CategoryTheory.Linear R C] {X I : C} (i : X ⟶ I) (hi : E.IsInflation i) (hI : E.isInjective I) (Y : C) :
        HomCokernel R i Y ≃ₗ[R] E.injectiveStableFunctor.obj X ⟶ E.injectiveStableFunctor.obj Y

        The Hom cokernel of an inflation into a relative injective is the Hom space in the injective stable category. The equivalence sends the class of a map to its stable image.

        Instances For
          source
          @[simp]
          theorem TauCeti.ExactStructure.homCokernelEquivInjectiveStableHom_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (R : Type t) [Ring R] [CategoryTheory.Linear R C] {X I Y : C} (i : X ⟶ I) (hi : E.IsInflation i) (hI : E.isInjective I) (f : X ⟶ Y) :
          (E.homCokernelEquivInjectiveStableHom R i hi hI Y) (Submodule.Quotient.mk f) = E.injectiveStableFunctor.map f

          The Hom-cokernel comparison sends a representative to its injective stable image.

          source
          @[simp]
          theorem TauCeti.ExactStructure.homCokernelEquivInjectiveStableHom_symm_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (R : Type t) [Ring R] [CategoryTheory.Linear R C] {X I Y : C} (i : X ⟶ I) (hi : E.IsInflation i) (hI : E.isInjective I) (f : X ⟶ Y) :
          (E.homCokernelEquivInjectiveStableHom R i hi hI Y).symm (E.injectiveStableFunctor.map f) = Submodule.Quotient.mk f

          The inverse comparison gives the class of any representative of a stable morphism.

          source
          theorem TauCeti.ExactStructure.homCokernelEquivInjectiveStableHom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (R : Type t) [Ring R] [CategoryTheory.Linear R C] {X I Y Z : C} (i : X ⟶ I) (hi : E.IsInflation i) (hI : E.isInjective I) (g : Y ⟶ Z) (x : HomCokernel R i Y) :
          (E.homCokernelEquivInjectiveStableHom R i hi hI Z) ((HomCokernel.map R i g) x) = CategoryTheory.CategoryStruct.comp ((E.homCokernelEquivInjectiveStableHom R i hi hI Y) x) (E.injectiveStableFunctor.map g)

          The comparison with injective stable Hom commutes with postcomposition.