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.
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]
:
Y ⟶ J
Let J be injective and g a morphism into J, then g can be factored through any monomorphism.
Equations
- CategoryTheory.Injective.factorThru g f = ⋯.choose
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]
:
CategoryStruct.comp f (factorThru g f) = g
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}
:
Injective J ↔ Projective (Opposite.op J)
theorem
CategoryTheory.Injective.projective_iff_injective_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{P : C}
:
Projective P ↔ Injective (Opposite.op P)
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]
:
Injective (R.obj 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
- CategoryTheory.Injective.under X = ⋯.some.J
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
- CategoryTheory.Injective.ι X = ⋯.some.f
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₁}
[Category.{v₁, u₁} C]
[EnoughInjectives C]
[Limits.HasZeroMorphisms C]
{X Y : C}
(f : X ⟶ Y)
[Limits.HasCokernel f]
:
@[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)
:
Injective (G.obj 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
- adj.mapInjectivePresentation X I = { J := G.obj I.J, injective := ⋯, f := G.map I.f, mono := ⋯ }
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
- adj.injectivePresentationOfMap X I = { J := G.obj I.J, injective := ⋯, f := (adj.homEquiv X I.J) I.f, mono := ⋯ }
Instances For
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
- F.injectivePresentationOfMapInjectivePresentation X I = F.toAdjunction.injectivePresentationOfMap X I
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)
: