Documentation

Mathlib.CategoryTheory.Subfunctor.Finite

Subpresheaves that are generated by finitely many sections #

Given F : Cᵒᵖ ⥤ Type w, G : Subfunctor 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.Subfunctor.IsGeneratedBy {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) {ι : Type w'} {X : ι → Cᵒᵖ} (x : (i : ι) → F.obj (X i)) :

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

Equations

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

Instances For

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

G.IsGeneratedBy x ↔ ⨆ (i : ι), ofSection (x i) = G

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

⨆ (i : ι), ofSection (x i) = G

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

ofSection (x i) ≤ G

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

x i ∈ G.obj (X i)

theorem CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subfunctor 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.Subfunctor.IsGeneratedBy.image {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subfunctor 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.Subfunctor.IsFinite {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subfunctor F) :

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)

Instances

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

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

Equations

CategoryTheory.Subfunctor.IsFinite.Index G = ⋯.choose

Instances For

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

Finite (Index G)

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

Index G → Cᵒᵖ

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

Equations

CategoryTheory.Subfunctor.IsFinite.X = ⋯.choose

Instances For

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

F.obj (X i)

A choice of generating sections of a finitely generated subpresheaf.

Equations

CategoryTheory.Subfunctor.IsFinite.x = ⋯.choose

Instances For

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

G.IsGeneratedBy IsFinite.x

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

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

(G.image f).IsFinite

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.

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

Equations

@CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy = @CategoryTheory.Subfunctor.IsGeneratedBy

Instances For

@[deprecated CategoryTheory.Subfunctor.isGeneratedBy_iff (since := "2025-12-11")]

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

G.IsGeneratedBy x ↔ ⨆ (i : ι), Subfunctor.ofSection (x i) = G

Alias of CategoryTheory.Subfunctor.isGeneratedBy_iff.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq (since := "2025-12-11")]

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

⨆ (i : ι), Subfunctor.ofSection (x i) = G

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le (since := "2025-12-11")]

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

Subfunctor.ofSection (x i) ≤ G

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.mem (since := "2025-12-11")]

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

x i ∈ G.obj (X i)

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.mem.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy.of_equiv {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subfunctor 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')

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.of_equiv.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.image (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy.image {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G : Subfunctor 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)

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.image.

@[deprecated CategoryTheory.Subfunctor.IsFinite (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.IsFinite.

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

Equations

@CategoryTheory.Subfunctor.Subpresheaf.IsFinite = @CategoryTheory.Subfunctor.IsFinite

Instances For

@[deprecated CategoryTheory.Subfunctor.IsFinite.Index (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.IsFinite.Index.

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

Equations

@CategoryTheory.Subfunctor.Subpresheaf.IsFinite.Index = @CategoryTheory.Subfunctor.IsFinite.Index

Instances For

@[deprecated CategoryTheory.Subfunctor.IsFinite.X (since := "2025-12-11")]

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

Subfunctor.IsFinite.Index G → Cᵒᵖ

Alias of CategoryTheory.Subfunctor.IsFinite.X.

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

Equations

@CategoryTheory.Subfunctor.Subpresheaf.IsFinite.X = @CategoryTheory.Subfunctor.IsFinite.X

Instances For

@[deprecated CategoryTheory.Subfunctor.IsFinite.x (since := "2025-12-11")]

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

F.obj (Subfunctor.IsFinite.X i)

Alias of CategoryTheory.Subfunctor.IsFinite.x.

A choice of generating sections of a finitely generated subpresheaf.

Equations

@CategoryTheory.Subfunctor.Subpresheaf.IsFinite.x = @CategoryTheory.Subfunctor.IsFinite.x

Instances For

@[deprecated CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite (since := "2025-12-11")]

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

G.IsGeneratedBy Subfunctor.IsFinite.x

Alias of CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite.

@[deprecated CategoryTheory.Subfunctor.IsGeneratedBy.isFinite (since := "2025-12-11")]

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

Alias of CategoryTheory.Subfunctor.IsGeneratedBy.isFinite.

@[deprecated CategoryTheory.Subfunctor.image_isFinite (since := "2025-12-11")]

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

(G.image f).IsFinite

Alias of CategoryTheory.Subfunctor.image_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)) :

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

Instances For

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') :

(Subfunctor.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)) :

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

Equations

CategoryTheory.PresheafIsFinite F = ⊤.IsFinite

Instances For

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

PresheafIsGeneratedBy F Subfunctor.IsFinite.x

theorem CategoryTheory.Subfunctor.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)