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))
:
A subpresheaf G : Subpresheaf F is generated by sections x i : F.obj (X i)
if ⨆ (i : ι), ofSection (x i) = G.
Equations
Instances For
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))
:
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)
:
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 : ι)
:
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 : ι)
:
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)
:
A subpresheaf of types is "finite" if it is generated by finitely many sections.
Instances
def
CategoryTheory.Subpresheaf.IsFinite.Index
{C : Type u}
[Category.{v, u} C]
{F : Functor Cᵒᵖ (Type w)}
(G : Subpresheaf F)
[hG : G.IsFinite]
:
A choice of index type for the generating sections of a finitely generated subpresheaf.
Equations
Instances For
instance
CategoryTheory.Subpresheaf.IsFinite.instFiniteIndex
{C : Type u}
[Category.{v, u} C]
{F : Functor Cᵒᵖ (Type w)}
(G : Subpresheaf F)
[hG : G.IsFinite]
:
noncomputable def
CategoryTheory.Subpresheaf.IsFinite.X
{C : Type u}
[Category.{v, u} C]
{F : Functor Cᵒᵖ (Type w)}
{G : Subpresheaf F}
[hG : G.IsFinite]
:
Objects on which a choice of generating sections of a finitely generated subpresheaf are defined.
Equations
Instances For
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)
:
A choice of generating sections of a finitely generated subpresheaf.
Equations
Instances For
theorem
CategoryTheory.Subpresheaf.isGeneratedBy_of_isFinite
{C : Type u}
[Category.{v, u} C]
{F : Functor Cᵒᵖ (Type w)}
(G : Subpresheaf F)
[hG : G.IsFinite]
:
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')
:
@[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
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')
:
(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))
:
A presheaf is "finite" if it is generated by finitely many sections.
Equations
Instances For
theorem
CategoryTheory.presheafIsGeneratedBy_of_isFinite
{C : Type u}
[Category.{v, u} C]
(F : Functor Cᵒᵖ (Type w))
[PresheafIsFinite F]
:
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')
:
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]
:
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)
: