Injective objects and categories with enough injectives #
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, CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : C)
:
Type (max u₁ v₁)
- J : C
- injective : CategoryTheory.Injective s.J
- f : X ⟶ s.J
- mono : CategoryTheory.Mono s.f
An injective presentation of an object X consists of a monomorphism f : X ⟶ J
to some injective object J.
Instances For
- presentation : ∀ (X : C), Nonempty (CategoryTheory.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₁}
[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.
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]
:
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.
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)
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)]
:
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)
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)]
:
instance
CategoryTheory.Injective.instInjectiveUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : Cᵒᵖ}
[CategoryTheory.Projective P]
:
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
instance
CategoryTheory.Injective.instProjectiveOppositeOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : C}
[CategoryTheory.Injective J]
:
instance
CategoryTheory.Injective.instInjectiveOppositeOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{P : C}
[CategoryTheory.Projective 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.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.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.
Instances For
instance
CategoryTheory.Injective.injective_under
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
(X : C)
:
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.
Instances For
instance
CategoryTheory.Injective.ι_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.EnoughInjectives C]
(X : C)
:
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.
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]
:
@[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).)
Instances For
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
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.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.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.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).
Instances For
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.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.obj X))
:
Given an equivalence of categories F, an injective presentation of F(X) induces an
injective presentation of X.
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)
: