Strong generators

If P : ObjectProperty C, we say that P is a strong generator if it is a generator (in the sense that IsSeparating P holds) such that for any proper subobject A ⊂ X, there exists a morphism G ⟶ X which does not factor through A from an object satisfying P.

The main result is the lemma isStrongGenerator_iff_exists_extremalEpi which says that if P is w-small, C is locally w-small and has coproducts of size w, then P is a strong generator iff any object of C is the target of an extremal epimorphism from a coproduct of objects satisfying P.

References

• [Adámek, J. and Rosický, J., Locally presentable and accessible categories][Adamek_Rosicky_1994]

def CategoryTheory.ObjectProperty.IsStrongGenerator {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

A property P : ObjectProperty C is a strong generator if it is separating and for any proper subobject A ⊂ X, there exists a morphism G ⟶ X which does not factor through A from an object such that P G holds.

Equations

• P.IsStrongGenerator = (P.IsSeparating ∧ ∀ ⦃X : C⦄ (A : CategoryTheory.Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤)

theorem CategoryTheory.ObjectProperty.isStrongGenerator_iff {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} : P.IsStrongGenerator ↔ P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun (f : G ⟶ X) => CategoryStruct.comp f i) → IsIso i

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.isSeparating {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) : P.IsSeparating

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) {X : C} {A : Subobject X} (hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) : A = ⊤

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.isIso_of_mono {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i] (hi : ∀ (G : C), P G → Function.Surjective fun (f : G ⟶ X) => CategoryStruct.comp f i) : IsIso i

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_subobject_ne_top {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) {X : C} {A : Subobject X} (hA : A ≠ ⊤) : ∃ (G : C) (_ : P G) (f : G ⟶ X), ¬A.Factors f

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_mono_not_isIso {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) {X Y : C} (i : X ⟶ Y) [Mono i] (hi : ¬IsIso i) : ∃ (G : C) (_ : P G) (g : G ⟶ Y), ∀ (f : G ⟶ X), CategoryStruct.comp f i ≠ g

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_extremalEpi {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hS : ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Limits.Cofan s) (x : Limits.IsColimit c) (p : c.pt ⟶ X), ExtremalEpi p) : P.IsStrongGenerator

theorem CategoryTheory.ObjectProperty.IsStrongGenerator.extremalEpi_coproductFrom {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} (hP : P.IsStrongGenerator) (X : C) [Limits.HasCoproduct (P.coproductFromFamily X)] : ExtremalEpi (P.coproductFrom X)

theorem CategoryTheory.ObjectProperty.isStrongGenerator_iff_exists_extremalEpi {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} [Limits.HasCoproducts C] [LocallySmall.{w, v, u} C] [ObjectProperty.Small.{w, v, u} P] : P.IsStrongGenerator ↔ ∀ (X : C), ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Limits.Cofan s) (x : Limits.IsColimit c) (p : c.pt ⟶ X), ExtremalEpi p