3.2. Weakly contractible categories
From now on, we assume that pullbacks in \mathcal{C} preserve epimorphisms.
For example this holds in abelian categories and (pre)topoi.
-
CategoryTheory.WeaklyContractible[complete]
An object F of \mathcal{C} is called weakly contractible if every
epimorphism G \to F has a section. We say \mathcal{C} has enough weakly
contractible objects, if every object admits an epimorphism from a weakly
contractible one. (Bhatt–Scholze, Definition 3.2.1)
Lean code for Definition3.2.1●1 definition
Associated Lean declarations
-
CategoryTheory.WeaklyContractible[complete]
-
CategoryTheory.WeaklyContractible[complete]
-
classdefined in Proetale/Replete/WeaklyContractible.leancomplete
class CategoryTheory.WeaklyContractible.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : C) : Prop
class CategoryTheory.WeaklyContractible.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : C) : Prop
An object `P` is weakly contractible if it is projective.
Extends
-
CategoryTheory.Projective P
Methods
factors : ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e], ∃ f', CategoryTheory.CategoryStruct.comp f' e = f
Inherited from-
CategoryTheory.Projective
-
Under our assumptions on \mathcal{C}, an object F is weakly contractible
if and only if it is projective.
Lean code for Lemma3.2.2●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Replete/WeaklyContractible.leancomplete
theorem CategoryTheory.Projective.iff_forall_isSplitEpi_of_hasPullbacks.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (H : ∀ {X E S : C} (f : X ⟶ S) (e : E ⟶ S), CategoryTheory.Epi e → CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst f e)) (P : C) : CategoryTheory.Projective P ↔ ∀ {X : C} (f : X ⟶ P), CategoryTheory.Epi f → CategoryTheory.IsSplitEpi f
theorem CategoryTheory.Projective.iff_forall_isSplitEpi_of_hasPullbacks.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (H : ∀ {X E S : C} (f : X ⟶ S) (e : E ⟶ S), CategoryTheory.Epi e → CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst f e)) (P : C) : CategoryTheory.Projective P ↔ ∀ {X : C} (f : X ⟶ P), CategoryTheory.Epi f → CategoryTheory.IsSplitEpi f
If `C` has pullbacks and epimorphisms are stable under pullbacks, `P` is projective if and only if every epimorphism to `P` splits. The conditions hold for example in abelian categories and pretopoi.
- No associated Lean code or declarations.
We say \mathcal{C} is locally weakly contractible, if each X in
\mathcal{C} admits an epimorphism from the coproduct of Y_i, where
Y_i is coherent and weakly contractible.
(Bhatt–Scholze, Definition 3.2.1)
If \mathcal{C} is locally weakly contractible, it has
enough weakly contractible objects: the coproduct of projective objects is
projective. For example, the category of sets is locally weakly contractible.
Let \mathcal{C} have enough weakly contractible objects and F \to G be a
morphism. Then F \to G is an epimorphism if and only if for every weakly
contractible Y in \mathcal{C}, the induced map
F(Y) = \mathrm{Hom}(Y, F) \to \mathrm{Hom}(Y, G) = G(Y) is surjective.
Lean code for Lemma3.2.4●1 theorem
Associated Lean declarations
-
theoremdefined in Proetale/Replete/WeaklyContractible.leancomplete
theorem CategoryTheory.EnoughProjectives.epi_iff_forall_projective.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.EnoughProjectives C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (P : C), CategoryTheory.Projective P → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyoneda.obj (Opposite.op P)).map f))
theorem CategoryTheory.EnoughProjectives.epi_iff_forall_projective.{u_1, u_2} {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.EnoughProjectives C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Epi f ↔ ∀ (P : C), CategoryTheory.Projective P → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyoneda.obj (Opposite.op P)).map f))
If `C` has enough projectives, being an epimorphism can be detected on sections over projective objects.
Choose an epimorphism e \colon P \to G where P is weakly contractible
and lift that to P \to F.
- No associated Lean code or declarations.
If \mathcal{C} has enough weakly contractible objects, it is replete.
This follows from Lemma 3.2.4, the fact that
\mathrm{Hom}(Y, -) commutes with limits and the corresponding statement in
the category of sets.