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) [inst : CategoryTheory.Mono f], ∃ (h : Y ⟶ J), CategoryTheory.CategoryStruct.comp f h = g
Instances
theorem
CategoryTheory.Limits.IsZero.injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(h : CategoryTheory.Limits.IsZero X)
:
structure
CategoryTheory.InjectivePresentation
{C : Type u₁}
[CategoryTheory.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
- injective : CategoryTheory.Injective self.J
- f : X ⟶ self.J
- mono : CategoryTheory.Mono self.f
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 (CategoryTheory.InjectivePresentation X)
Instances
def
CategoryTheory.Injective.factorThru
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : C}
{X : C}
{Y : C}
[CategoryTheory.Injective J]
(g : X ⟶ J)
(f : X ⟶ Y)
[CategoryTheory.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 = Exists.choose (_ : ∃ (h : Y ⟶ J), CategoryTheory.CategoryStruct.comp f h = g)
Instances For
@[simp]
theorem
CategoryTheory.Injective.comp_factorThru
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : C}
{X : C}
{Y : C}
[CategoryTheory.Injective J]
(g : X ⟶ J)
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
instance
CategoryTheory.Injective.zero_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroObject C]
:
Equations
- (_ : CategoryTheory.Injective 0) = (_ : CategoryTheory.Injective 0)
theorem
CategoryTheory.Injective.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
{Q : C}
(i : P ≅ Q)
(hP : CategoryTheory.Injective P)
:
theorem
CategoryTheory.Injective.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
{Q : C}
(i : P ≅ Q)
:
The axiom of choice says that every nonempty type is an injective object in Type.
Equations
- (_ : CategoryTheory.Injective X) = (_ : CategoryTheory.Injective X)
instance
CategoryTheory.Injective.instInjectiveProd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
{Q : C}
[CategoryTheory.Limits.HasBinaryProduct P Q]
[CategoryTheory.Injective P]
[CategoryTheory.Injective Q]
:
CategoryTheory.Injective (P ⨯ Q)
Equations
- (_ : CategoryTheory.Injective (P ⨯ Q)) = (_ : CategoryTheory.Injective (P ⨯ Q))
instance
CategoryTheory.Injective.instInjectivePiObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Type v}
(c : β → C)
[CategoryTheory.Limits.HasProduct c]
[∀ (b : β), CategoryTheory.Injective (c b)]
:
Equations
- (_ : CategoryTheory.Injective (∏ c)) = (_ : CategoryTheory.Injective (∏ c))
instance
CategoryTheory.Injective.instInjectiveBiprod
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
{Q : C}
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasBinaryBiproduct P Q]
[CategoryTheory.Injective P]
[CategoryTheory.Injective Q]
:
CategoryTheory.Injective (P ⊞ Q)
Equations
- (_ : CategoryTheory.Injective (P ⊞ Q)) = (_ : CategoryTheory.Injective (P ⊞ Q))
instance
CategoryTheory.Injective.instInjectiveBiproduct
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{β : Type v}
(c : β → C)
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasBiproduct c]
[∀ (b : β), CategoryTheory.Injective (c b)]
:
Equations
- (_ : CategoryTheory.Injective (⨁ c)) = (_ : CategoryTheory.Injective (⨁ c))
instance
CategoryTheory.Injective.instInjectiveUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : Cᵒᵖ}
[CategoryTheory.Projective P]
:
CategoryTheory.Injective P.unop
Equations
- (_ : CategoryTheory.Injective P.unop) = (_ : CategoryTheory.Injective P.unop)
instance
CategoryTheory.Injective.instProjectiveUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Cᵒᵖ}
[CategoryTheory.Injective J]
:
CategoryTheory.Projective J.unop
Equations
- (_ : CategoryTheory.Projective J.unop) = (_ : CategoryTheory.Projective J.unop)
instance
CategoryTheory.Injective.instProjectiveOppositeOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : C}
[CategoryTheory.Injective J]
:
Equations
- (_ : CategoryTheory.Projective (Opposite.op J)) = (_ : CategoryTheory.Projective (Opposite.op J))
instance
CategoryTheory.Injective.instInjectiveOppositeOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
[CategoryTheory.Projective P]
:
Equations
- (_ : CategoryTheory.Injective (Opposite.op P)) = (_ : CategoryTheory.Injective (Opposite.op P))
theorem
CategoryTheory.Injective.injective_iff_projective_op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : C}
:
theorem
CategoryTheory.Injective.projective_iff_injective_op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
:
theorem
CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(J : C)
:
CategoryTheory.Injective J ↔ CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.yoneda.toPrefunctor.obj J)
theorem
CategoryTheory.Injective.injective_of_adjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
[CategoryTheory.Functor.PreservesMonomorphisms L]
(adj : L ⊣ R)
(J : D)
[CategoryTheory.Injective J]
:
CategoryTheory.Injective (R.toPrefunctor.obj J)
def
CategoryTheory.Injective.under
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
(X : C)
:
Equations
- (_ : CategoryTheory.Injective (CategoryTheory.Injective.under X)) = (_ : CategoryTheory.Injective (Nonempty.some (_ : Nonempty (CategoryTheory.InjectivePresentation X))).J)
def
CategoryTheory.Injective.ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
(X : C)
:
Equations
- (_ : CategoryTheory.Mono (CategoryTheory.Injective.ι X)) = (_ : CategoryTheory.Mono (Nonempty.some (_ : Nonempty (CategoryTheory.InjectivePresentation X))).f)
def
CategoryTheory.Injective.syzygies
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.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.instInjectiveSyzygies
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
Equations
@[inline, reducible]
abbrev
CategoryTheory.Injective.d
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.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
instance
CategoryTheory.Injective.instEnoughProjectivesOppositeOpposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
:
Equations
- (_ : CategoryTheory.EnoughProjectives Cᵒᵖ) = (_ : CategoryTheory.EnoughProjectives Cᵒᵖ)
instance
CategoryTheory.Injective.instEnoughInjectivesOppositeOpposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughProjectives C]
:
Equations
- (_ : CategoryTheory.EnoughInjectives Cᵒᵖ) = (_ : CategoryTheory.EnoughInjectives Cᵒᵖ)
def
CategoryTheory.Injective.Exact.desc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasImages Cᵒᵖ]
[CategoryTheory.Limits.HasEqualizers Cᵒᵖ]
{J : C}
{Q : C}
{R : C}
{S : C}
[CategoryTheory.Injective J]
(h : R ⟶ J)
(f : Q ⟶ R)
(g : R ⟶ S)
(hgf : CategoryTheory.Exact g.op f.op)
(w : CategoryTheory.CategoryStruct.comp f h = 0)
:
S ⟶ J
Given a pair of exact morphism f : Q ⟶ R and g : R ⟶ S and a map h : R ⟶ J to an injective
object J such that f ≫ h = 0, then g descents to a map S ⟶ J. See below:
Q --- f --> R --- g --> S
|
| h
v
J
Equations
- CategoryTheory.Injective.Exact.desc h f g hgf w = (CategoryTheory.Exact.lift h.op g.op f.op hgf (_ : (CategoryTheory.CategoryStruct.comp f.op.unop h.op.unop).op = 0.op)).unop
Instances For
@[simp]
theorem
CategoryTheory.Injective.Exact.comp_desc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasImages Cᵒᵖ]
[CategoryTheory.Limits.HasEqualizers Cᵒᵖ]
{J : C}
{Q : C}
{R : C}
{S : C}
[CategoryTheory.Injective J]
(h : R ⟶ J)
(f : Q ⟶ R)
(g : R ⟶ S)
(hgf : CategoryTheory.Exact g.op f.op)
(w : CategoryTheory.CategoryStruct.comp f h = 0)
:
CategoryTheory.CategoryStruct.comp g (CategoryTheory.Injective.Exact.desc h f g hgf w) = h
theorem
CategoryTheory.Adjunction.map_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[CategoryTheory.Functor.PreservesMonomorphisms F]
(I : D)
(hI : CategoryTheory.Injective I)
:
CategoryTheory.Injective (G.toPrefunctor.obj I)
theorem
CategoryTheory.Adjunction.injective_of_map_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[CategoryTheory.Full G]
[CategoryTheory.Faithful G]
(I : D)
(hI : CategoryTheory.Injective (G.toPrefunctor.obj I))
:
def
CategoryTheory.Adjunction.mapInjectivePresentation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[CategoryTheory.Functor.PreservesMonomorphisms F]
(X : D)
(I : CategoryTheory.InjectivePresentation X)
:
CategoryTheory.InjectivePresentation (G.toPrefunctor.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
- CategoryTheory.Adjunction.mapInjectivePresentation adj X I = CategoryTheory.InjectivePresentation.mk (G.toPrefunctor.obj I.J) (G.toPrefunctor.map I.f)
Instances For
def
CategoryTheory.Adjunction.injectivePresentationOfMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[CategoryTheory.Functor.PreservesMonomorphisms F]
[CategoryTheory.Functor.ReflectsMonomorphisms F]
(X : C)
(I : CategoryTheory.InjectivePresentation (F.toPrefunctor.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
- CategoryTheory.Adjunction.injectivePresentationOfMap adj X I = CategoryTheory.InjectivePresentation.mk (G.toPrefunctor.obj I.J) ((adj.homEquiv X I.J) I.f)
Instances For
theorem
CategoryTheory.EnoughInjectives.of_adjunction
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.Functor D C}
(adj : L ⊣ R)
[CategoryTheory.Functor.PreservesMonomorphisms L]
[CategoryTheory.Functor.ReflectsMonomorphisms L]
[CategoryTheory.EnoughInjectives D]
:
theorem
CategoryTheory.EnoughInjectives.of_equivalence
{C : Type u₁}
{D : Type u₂}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Category.{v₂, u₂} D]
(e : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence e]
[CategoryTheory.EnoughInjectives D]
:
An equivalence of categories transfers enough injectives.
theorem
CategoryTheory.Equivalence.map_injective_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
(F : C ≌ D)
(P : C)
:
CategoryTheory.Injective (F.functor.toPrefunctor.obj P) ↔ CategoryTheory.Injective P
def
CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
(F : C ≌ D)
(X : C)
(I : CategoryTheory.InjectivePresentation (F.functor.toPrefunctor.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
(F : C ≌ D)
: