mathlib3 documentation

category_theory.preadditive.projective

Projective objects and categories with enough projectives #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An object P is called projective if every morphism out of P factors through every epimorphism.

A category C has enough projectives if every object admits an epimorphism from some projective object.

projective.over X picks an arbitrary such projective object, and projective.π X : projective.over X ⟶ X is the corresponding epimorphism.

Given a morphism f : X ⟶ Y, projective.left f is a projective object over kernel f, and projective.d f : projective.left f ⟶ X is the morphism π (kernel f) ≫ kernel.ι f.

source
@[class]
structure category_theory.projective {C : Type u} [category_theory.category C] (P : C) :
Prop

An object P is called projective if every morphism out of P factors through every epimorphism.

Instances of this typeclass
source
@[nolint]
structure category_theory.projective_presentation {C : Type u} [category_theory.category C] (X : C) :
Type (max u v)

A projective presentation of an object X consists of an epimorphism f : P ⟶ X from some projective object P.

Instances for category_theory.projective_presentation
  • category_theory.projective_presentation.has_sizeof_inst
source
@[class]
structure category_theory.enough_projectives (C : Type u) [category_theory.category C] :
Prop

A category "has enough projectives" if for every object X there is a projective object P and an epimorphism P ↠ X.

Instances of this typeclass
source
noncomputable def category_theory.projective.factor_thru {C : Type u} [category_theory.category C] {P X E : C} [category_theory.projective P] (f : P ⟶ X) (e : E ⟶ X) [category_theory.epi e] :
P ⟶ E

An arbitrarily chosen factorisation of a morphism out of a projective object through an epimorphism.

Equations
source
@[simp]
theorem category_theory.projective.factor_thru_comp {C : Type u} [category_theory.category C] {P X E : C} [category_theory.projective P] (f : P ⟶ X) (e : E ⟶ X) [category_theory.epi e] :
category_theory.projective.factor_thru f e ≫ e = f
source
@[protected, instance]
def category_theory.projective.zero_projective {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_morphisms C] :
category_theory.projective 0
source
theorem category_theory.projective.of_iso {C : Type u} [category_theory.category C] {P Q : C} (i : P ≅ Q) (hP : category_theory.projective P) :
category_theory.projective Q
source
theorem category_theory.projective.iso_iff {C : Type u} [category_theory.category C] {P Q : C} (i : P ≅ Q) :
category_theory.projective P ↔ category_theory.projective Q
source
@[protected, instance]
def category_theory.projective.projective (X : Type u) :
category_theory.projective X

The axiom of choice says that every type is a projective object in Type.

source
@[protected, instance]
def category_theory.projective.Type.enough_projectives  :
category_theory.enough_projectives (Type u)
source
@[protected, instance]
def category_theory.projective.category_theory.limits.coprod.projective {C : Type u} [category_theory.category C] {P Q : C} [category_theory.limits.has_binary_coproduct P Q] [category_theory.projective P] [category_theory.projective Q] :
category_theory.projective (P ⨿ Q)
source
@[protected, instance]
def category_theory.projective.category_theory.limits.sigma_obj.projective {C : Type u} [category_theory.category C] {β : Type v} (g : β → C) [category_theory.limits.has_coproduct g] [∀ (b : β), category_theory.projective (g b)] :
category_theory.projective (∐ g)
source
@[protected, instance]
def category_theory.projective.category_theory.limits.biprod.projective {C : Type u} [category_theory.category C] {P Q : C} [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_binary_biproduct P Q] [category_theory.projective P] [category_theory.projective Q] :
category_theory.projective (P ⊞ Q)
source
@[protected, instance]
def category_theory.projective.category_theory.limits.biproduct.projective {C : Type u} [category_theory.category C] {β : Type v} (g : β → C) [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_biproduct g] [∀ (b : β), category_theory.projective (g b)] :
category_theory.projective (⨁ g)
source
theorem category_theory.projective.projective_iff_preserves_epimorphisms_coyoneda_obj {C : Type u} [category_theory.category C] (P : C) :
category_theory.projective P ↔ (category_theory.coyoneda.obj (opposite.op P)).preserves_epimorphisms
source
noncomputable def category_theory.projective.over {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] (X : C) :
C

projective.over X provides an arbitrarily chosen projective object equipped with an epimorphism projective.π : projective.over X ⟶ X.

Equations
Instances for category_theory.projective.over
source
@[protected, instance]
def category_theory.projective.projective_over {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] (X : C) :
category_theory.projective (category_theory.projective.over X)
source
noncomputable def category_theory.projective.π {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] (X : C) :
category_theory.projective.over X ⟶ X

The epimorphism projective.π : projective.over X ⟶ X from the arbitrarily chosen projective object over X.

Equations
Instances for category_theory.projective.π
source
@[protected, instance]
def category_theory.projective.π_epi {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] (X : C) :
category_theory.epi (category_theory.projective.π X)
source
@[protected, instance]
def category_theory.projective.syzygies.projective {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_kernel f] :
category_theory.projective (category_theory.projective.syzygies f)
source
noncomputable def category_theory.projective.syzygies {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_kernel f] :
C

When C has enough projectives, the object projective.syzygies f is an arbitrarily chosen projective object over kernel f.

Equations
Instances for category_theory.projective.syzygies
source
@[reducible]
noncomputable def category_theory.projective.d {C : Type u} [category_theory.category C] [category_theory.enough_projectives C] [category_theory.limits.has_zero_morphisms C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_kernel f] :
category_theory.projective.syzygies f ⟶ X

When C has enough projectives, projective.d f : projective.syzygies f ⟶ X is the composition π (kernel f) ≫ kernel.ι f.

(When C is abelian, we have exact (projective.d f) f.)

source
theorem category_theory.adjunction.map_projective {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [G.preserves_epimorphisms] (P : C) (hP : category_theory.projective P) :
category_theory.projective (F.obj P)
source
theorem category_theory.adjunction.projective_of_map_projective {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [category_theory.full F] [category_theory.faithful F] (P : C) (hP : category_theory.projective (F.obj P)) :
category_theory.projective P
source
def category_theory.adjunction.map_projective_presentation {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [G.preserves_epimorphisms] (X : C) (Y : category_theory.projective_presentation X) :
category_theory.projective_presentation (F.obj X)

Given an adjunction F ⊣ G such that G preserves epis, F maps a projective presentation of X to a projective presentation of F(X).

Equations
source
def category_theory.equivalence.projective_presentation_of_map_projective_presentation {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ≌ D) (X : C) (Y : category_theory.projective_presentation (F.functor.obj X)) :
category_theory.projective_presentation X

Given an equivalence of categories F, a projective presentation of F(X) induces a projective presentation of X.

Equations
source
theorem category_theory.equivalence.enough_projectives_iff {C : Type u} [category_theory.category C] {D : Type u_1} [category_theory.category D] (F : C ≌ D) :
category_theory.enough_projectives C ↔ category_theory.enough_projectives D
source
noncomputable def category_theory.exact.lift {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {P Q R S : C} [category_theory.projective P] (h : P ⟶ R) (f : Q ⟶ R) (g : R ⟶ S) (hfg : category_theory.exact f g) (w : h ≫ g = 0) :
P ⟶ Q

Given a projective object P mapping via h into the middle object R of a pair of exact morphisms f : Q ⟶ R and g : R ⟶ S, such that h ≫ g = 0, there is a lift of h to Q.

Equations
source
@[simp]
theorem category_theory.exact.lift_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_images C] {P Q R S : C} [category_theory.projective P] (h : P ⟶ R) (f : Q ⟶ R) (g : R ⟶ S) (hfg : category_theory.exact f g) (w : h ≫ g = 0) :
category_theory.exact.lift h f g hfg w ≫ f = h