Injective objects and categories with enough injectives #
An object J is injective iff every morphism into J can be obtained by extending a monomorphism.
theorem
CategoryTheory.Limits.IsZero.injective
{C : Type u₁}
[Category.{v₁, u₁} C]
{X : C}
(h : IsZero X)
:
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
Instances For
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)
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]
:
Let J be injective and g a morphism into J, then g can be factored through any monomorphism.
Equations
Instances For
@[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]
:
@[simp]
theorem
CategoryTheory.Injective.comp_factorThru_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J X Y : C}
[Injective J]
(g : X ⟶ J)
(f : X ⟶ Y)
[Mono f]
{Z : C}
(h : J ⟶ Z)
:
instance
CategoryTheory.Injective.zero_injective
{C : Type u₁}
[Category.{v₁, u₁} C]
[Limits.HasZeroObject C]
:
theorem
CategoryTheory.Injective.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : C}
(i : P ≅ Q)
(hP : Injective P)
:
theorem
CategoryTheory.Injective.iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : C}
(i : P ≅ Q)
:
The axiom of choice says that every nonempty type is an injective object in Type.
instance
CategoryTheory.Injective.instProd
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : C}
[Limits.HasBinaryProduct P Q]
[Injective P]
[Injective Q]
:
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.instBiprod
{C : Type u₁}
[Category.{v₁, u₁} C]
{P Q : C}
[Limits.HasZeroMorphisms C]
[Limits.HasBinaryBiproduct P Q]
[Injective P]
[Injective Q]
:
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)]
:
instance
CategoryTheory.Injective.instUnopOfProjectiveOpposite
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : Cᵒᵖ}
[Projective P]
:
instance
CategoryTheory.Injective.instProjectiveUnopOfOpposite
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Cᵒᵖ}
[Injective J]
:
instance
CategoryTheory.Injective.instProjectiveOppositeOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : C}
[Injective J]
:
instance
CategoryTheory.Injective.instOppositeOpOfProjective
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
[Projective P]
:
Injective (Opposite.op P)
theorem
CategoryTheory.Injective.injective_iff_projective_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : C}
:
theorem
CategoryTheory.Injective.projective_iff_injective_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
:
theorem
CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj
{C : Type u₁}
[Category.{v₁, u₁} C]
(J : C)
:
theorem
CategoryTheory.Injective.injective_of_adjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
[L.PreservesMonomorphisms]
(adj : L ⊣ R)
(J : D)
[Injective J]
:
def
CategoryTheory.Injective.under
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
(X : C)
:
C
Injective.under X provides an arbitrarily chosen injective object equipped with
a monomorphism Injective.ι : X ⟶ Injective.under X.
Equations
Instances For
instance
CategoryTheory.Injective.injective_under
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
(X : C)
:
The monomorphism Injective.ι : X ⟶ Injective.under X
from the arbitrarily chosen injective object under X.
Equations
Instances For
instance
CategoryTheory.Injective.ι_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
(X : C)
:
def
CategoryTheory.Injective.syzygies
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
[Limits.HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[Limits.HasCokernel f]
:
C
When C has enough injectives, the object Injective.syzygies f is
an arbitrarily chosen injective object under cokernel f.
Equations
Instances For
instance
CategoryTheory.Injective.instSyzygies
{C : Type u_2}
[Category.{u_1, u_2} C]
[EnoughInjectives C]
[Limits.HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[Limits.HasCokernel f]
:
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.Injective.d
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
[Limits.HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[Limits.HasCokernel f]
:
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
Instances For
theorem
CategoryTheory.Injective.enoughProjectives_of_enoughInjectives_op
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughInjectives Cᵒᵖ]
:
theorem
CategoryTheory.Injective.enoughInjectives_of_enoughProjectives_op
{C : Type u₁}
[Category.{v₁, u₁} C]
[EnoughProjectives Cᵒᵖ]
:
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))
:
def
CategoryTheory.Adjunction.mapInjectivePresentation
{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]
(X : D)
(I : InjectivePresentation X)
:
InjectivePresentation (G.obj X)
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
Instances For
def
CategoryTheory.Adjunction.injectivePresentationOfMap
{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]
[F.ReflectsMonomorphisms]
(X : C)
(I : InjectivePresentation (F.obj X))
:
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
Instances For
theorem
CategoryTheory.Functor.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)
[F.Full]
[F.Faithful]
[F.PreservesMonomorphisms]
{I : C}
(hI : Injective (F.obj I))
:
theorem
CategoryTheory.EnoughInjectives.of_adjunction
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
[L.PreservesMonomorphisms]
[L.ReflectsMonomorphisms]
[EnoughInjectives D]
:
theorem
CategoryTheory.EnoughInjectives.of_equivalence
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
(e : Functor C D)
[e.IsEquivalence]
[EnoughInjectives D]
:
An equivalence of categories transfers enough injectives.
theorem
CategoryTheory.Equivalence.map_injective_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
(F : C ≌ D)
(P : C)
:
def
CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
(F : C ≌ D)
(X : C)
(I : InjectivePresentation (F.functor.obj X))
:
Given an equivalence of categories F, an injective presentation of F(X) induces an
injective presentation of X.
Equations
Instances For
theorem
CategoryTheory.Equivalence.enoughInjectives_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u_1}
[Category.{u_2, u_1} D]
(F : C ≌ D)
: