Documentation

Mathlib.CategoryTheory.Preadditive.Injective.Basic

Injective objects and categories with enough injectives #

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

  • factors {X Y : C} (g : X J) (f : X Y) [Mono f] : ∃ (h : Y J), CategoryStruct.comp f h = g

    An object J is injective iff every morphism into J can be obtained by extending a monomorphism.

Instances
    structure CategoryTheory.InjectivePresentation {C : Type u₁} [Category.{v₁, u₁} C] (X : C) :
    Type (max u₁ v₁)

    An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • J : C

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • injective : Injective self.J

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • f : X self.J

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    • mono : Mono self.f

      An injective presentation of an object X consists of a monomorphism f : X ⟶ J to some injective object J.

    A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

    • presentation (X : C) : Nonempty (InjectivePresentation X)

      A category "has enough injectives" if every object has an injective presentation, i.e. if for every object X there is an injective object J and a monomorphism X ↪ J.

    Instances
      def CategoryTheory.Injective.factorThru {C : Type u₁} [Category.{v₁, u₁} C] {J X Y : C} [Injective J] (g : X J) (f : X Y) [Mono f] :
      Y J

      Let J be injective and g a morphism into J, then g can be factored through any monomorphism.

      Equations
      @[simp]
      theorem CategoryTheory.Injective.comp_factorThru {C : Type u₁} [Category.{v₁, u₁} C] {J X Y : C} [Injective J] (g : X J) (f : X Y) [Mono f] :
      theorem CategoryTheory.Injective.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {P Q : C} (i : P Q) (hP : Injective P) :

      The axiom of choice says that every nonempty type is an injective object in Type.

      instance CategoryTheory.Injective.instPiObj {C : Type u₁} [Category.{v₁, u₁} C] {β : Type v} (c : βC) [Limits.HasProduct c] [∀ (b : β), Injective (c b)] :
      instance CategoryTheory.Injective.instBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {β : Type v} (c : βC) [Limits.HasZeroMorphisms C] [Limits.HasBiproduct c] [∀ (b : β), Injective (c b)] :

      Injective.under X provides an arbitrarily chosen injective object equipped with a monomorphism Injective.ι : X ⟶ Injective.under X.

      Equations

      The monomorphism Injective.ι : X ⟶ Injective.under X from the arbitrarily chosen injective object under X.

      Equations

      When C has enough injectives, the object Injective.syzygies f is an arbitrarily chosen injective object under cokernel f.

      Equations
      @[reducible, inline]

      When C has enough injective, Injective.d f : Y ⟶ syzygies f is the composition cokernel.π fι (cokernel f).

      (When C is abelian, we have exact f (injective.d f).)

      Equations
      theorem CategoryTheory.Adjunction.map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F G) [F.PreservesMonomorphisms] (I : D) (hI : Injective I) :
      theorem CategoryTheory.Adjunction.injective_of_map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {G : Functor D C} (adj : F G) [G.Full] [G.Faithful] (I : D) (hI : Injective (G.obj I)) :

      Given an adjunction F ⊣ G such that F preserves monos, G maps an injective presentation of X to an injective presentation of G(X).

      Equations

      Given an adjunction F ⊣ G such that F preserves monomorphisms and is faithful, then any injective presentation of F(X) can be pulled back to an injective presentation of X. This is similar to mapInjectivePresentation.

      Equations

      An equivalence of categories transfers enough injectives.

      Given an equivalence of categories F, an injective presentation of F(X) induces an injective presentation of X.

      Equations