Subpresheaves that are generated by finitely many sections

Given F : Cᵒᵖ ⥤ Type w, G : Subpresheaf F, objects X : ι → Cᵒᵖ and sections x : (i : ι) → F.obj (X i), we define a predicate G.IsGeneratedBy x saying that G is the subpresheaf generated by the sections x i. If this holds for a finite index type ι, we say that G is "finite", and this gives a type class G.IsFinite.

def CategoryTheory.Subpresheaf.IsGeneratedBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {ι : Type w'} {X : ι → Cᵒᵖ} (x : (i : ι) → F.obj (X i)) : Prop

A subpresheaf G : Subpresheaf F is generated by sections x i : F.obj (X i) if ⨆ (i : ι), ofSection (x i) = G.

Equations

• G.IsGeneratedBy x = (⨆ (i : ι), CategoryTheory.Subpresheaf.ofSection (x i) = G)

theorem CategoryTheory.Subpresheaf.isGeneratedBy_iff {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {ι : Type w'} {X : ι → Cᵒᵖ} (x : (i : ι) → F.obj (X i)) : G.IsGeneratedBy x ↔ ⨆ (i : ι), ofSection (x i) = G

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.iSup_eq {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) : ⨆ (i : ι), ofSection (x i) = G

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.ofSection_le {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) (i : ι) : ofSection (x i) ≤ G

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.mem {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) (i : ι) : x i ∈ G.obj (X i)

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.of_equiv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) {ι' : Type w''} (e : ι' ≃ ι) : G.IsGeneratedBy fun (i' : ι') => x (e i')

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.image {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') : (G.image f).IsGeneratedBy fun (i : ι) => f.app (X i) (x i)

class CategoryTheory.Subpresheaf.IsFinite {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) : Prop

A subpresheaf of types is "finite" if it is generated by finitely many sections.

• exists_isGeneratedBy : ∃ (ι : Type) (_ : Finite ι) (X : ι → Cᵒᵖ) (x : (i : ι) → F.obj (X i)), Nonempty (G.IsGeneratedBy x)

def CategoryTheory.Subpresheaf.IsFinite.Index {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) [hG : G.IsFinite] : Type

A choice of index type for the generating sections of a finitely generated subpresheaf.

Equations

• CategoryTheory.Subpresheaf.IsFinite.Index G = ⋯.choose

instance CategoryTheory.Subpresheaf.IsFinite.instFiniteIndex {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) [hG : G.IsFinite] : Finite (Index G)

noncomputable def CategoryTheory.Subpresheaf.IsFinite.X {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} [hG : G.IsFinite] : Index G → Cᵒᵖ

Objects on which a choice of generating sections of a finitely generated subpresheaf are defined.

Equations

• CategoryTheory.Subpresheaf.IsFinite.X = ⋯.choose

noncomputable def CategoryTheory.Subpresheaf.IsFinite.x {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subpresheaf F} [hG : G.IsFinite] (i : Index G) : F.obj (X i)

A choice of generating sections of a finitely generated subpresheaf.

Equations

• CategoryTheory.Subpresheaf.IsFinite.x = ⋯.choose

theorem CategoryTheory.Subpresheaf.isGeneratedBy_of_isFinite {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) [hG : G.IsFinite] : G.IsGeneratedBy IsFinite.x

theorem CategoryTheory.Subpresheaf.IsGeneratedBy.isFinite {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {ι : Type w'} [Finite ι] {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : G.IsGeneratedBy x) : G.IsFinite

theorem CategoryTheory.Subpresheaf.image_isFinite {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) [G.IsFinite] {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') : (G.image f).IsFinite

@[reducible, inline]

abbrev CategoryTheory.PresheafIsGeneratedBy {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) {ι : Type w'} {X : ι → Cᵒᵖ} (x : (i : ι) → F.obj (X i)) : Prop

The condition that a presheaf of types F : Cᵒᵖ ⥤ Type w is generated by a family of sections.

Equations

• CategoryTheory.PresheafIsGeneratedBy F x = ⊤.IsGeneratedBy x

theorem CategoryTheory.PresheafIsGeneratedBy.range {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : PresheafIsGeneratedBy F x) {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') : (Subpresheaf.range f).IsGeneratedBy fun (i : ι) => f.app (X i) (x i)

theorem CategoryTheory.PresheafIsGeneratedBy.of_epi {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)} (h : PresheafIsGeneratedBy F x) {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [Epi f] : PresheafIsGeneratedBy F' fun (i : ι) => f.app (X i) (x i)

@[reducible, inline]

abbrev CategoryTheory.PresheafIsFinite {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) : Prop

A presheaf is "finite" if it is generated by finitely many sections.

Equations

• CategoryTheory.PresheafIsFinite F = ⊤.IsFinite

theorem CategoryTheory.presheafIsGeneratedBy_of_isFinite {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) [PresheafIsFinite F] : PresheafIsGeneratedBy F Subpresheaf.IsFinite.x

theorem CategoryTheory.Subpresheaf.range_isFinite {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) [PresheafIsFinite F] {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') : (range f).IsFinite

theorem CategoryTheory.presheafIsFinite_of_epi {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) [PresheafIsFinite F] {F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [Epi f] : PresheafIsFinite F'

theorem CategoryTheory.yoneda_obj_isGeneratedBy {C : Type u} [Category.{v, u} C] (X : C) : PresheafIsGeneratedBy (yoneda.obj X) fun (x : Unit) => CategoryStruct.id X

instance CategoryTheory.instPresheafIsFiniteObjFunctorOppositeTypeYoneda {C : Type u} [Category.{v, u} C] (X : C) : PresheafIsFinite (yoneda.obj X)