Documentation

Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject

The full subcategory of injective objects #

source
@[reducible, inline]
abbrev CategoryTheory.InjectiveObject (C : Type u) [Category.{v, u} C] :
Type u

The full subcategory of injective objects in a category C.

Equations
Instances For
    source
    instance CategoryTheory.InjectiveObject.instIsClosedUnderLimitsOfShapeIsInjectiveDiscrete (C : Type u) [Category.{v, u} C] (J : Type u_1) :
    (isInjective C).IsClosedUnderLimitsOfShape (Discrete J)
    source
    instance CategoryTheory.InjectiveObject.instHasFiniteProducts (C : Type u) [Category.{v, u} C] [Limits.HasFiniteProducts C] :
    Limits.HasFiniteProducts (InjectiveObject C)
    source
    instance CategoryTheory.InjectiveObject.instHasFiniteBiproductsOfHasFiniteProducts (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasFiniteProducts C] :
    Limits.HasFiniteBiproducts (InjectiveObject C)
    source
    instance CategoryTheory.InjectiveObject.instHasBinaryBiproducts (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasBinaryBiproducts C] :
    Limits.HasBinaryBiproducts (InjectiveObject C)
    source
    instance CategoryTheory.InjectiveObject.instContainsZeroIsInjectiveOfHasZeroMorphismsOfHasZeroObject (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasZeroObject C] :
    (isInjective C).ContainsZero
    source
    @[reducible, inline]
    abbrev CategoryTheory.InjectiveObject.ι (C : Type u) [Category.{v, u} C] :
    Functor (InjectiveObject C) C

    The inclusion InjectiveObject C ⥤ C of the full subcategory of injective objects in C.

    Equations
    Instances For
      source
      instance CategoryTheory.InjectiveObject.instInjectiveObjι (C : Type u) [Category.{v, u} C] (X : InjectiveObject C) :
      Injective ((ι C).obj X)
      source
      instance CategoryTheory.InjectiveObject.instInjectiveObjIsInjective (C : Type u) [Category.{v, u} C] (X : InjectiveObject C) :
      Injective X.obj