Subpresheaf of types #

We define the subpresheaf of a type valued presheaf.

Main results #

CategoryTheory.Subpresheaf : A subpresheaf of a presheaf of types.

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

Type (max u w)

A subpresheaf of a presheaf consists of a subset of F.obj U for every U, compatible with the restriction maps F.map i.

obj (U : Cᵒᵖ) : Set (F.obj U)
If G is a sub-presheaf of F, then the sections of G on U forms a subset of sections of F on U.
map {U V : Cᵒᵖ} (i : U ⟶ V) : self.obj U ⊆ F.map i ⁻¹' self.obj V
If G is a sub-presheaf of F and i : U ⟶ V, then for each G-sections on U x, F i x is in F(V).

Instances For

source

theorem CategoryTheory.Subpresheaf.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor Cᵒᵖ (Type w)} {x y : Subpresheaf F} (obj : x.obj = y.obj) :

x = y

source

@[deprecated CategoryTheory.Subpresheaf (since := "2025-01-08")]

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

Type (max u w)

Alias of CategoryTheory.Subpresheaf.

A subpresheaf of a presheaf consists of a subset of F.obj U for every U, compatible with the restriction maps F.map i.

Equations

@CategoryTheory.GrothendieckTopology.Subpresheaf = @CategoryTheory.Subpresheaf

source

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

PartialOrder (Subpresheaf F)

Equations

CategoryTheory.instPartialOrderSubpresheaf = PartialOrder.lift CategoryTheory.Subpresheaf.obj ⋯

source

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

CompleteLattice (Subpresheaf F)

Equations

CategoryTheory.instCompleteLatticeSubpresheaf = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

theorem CategoryTheory.Subpresheaf.le_def {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S T : Subpresheaf F) :

S ≤ T ↔ ∀ (U : Cᵒᵖ), S.obj U ≤ T.obj U

source

@[simp]

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

⊤.obj i = ⊤

source

@[simp]

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

⊥.obj i = ⊥

source

theorem CategoryTheory.Subpresheaf.sSup_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S : Set (Subpresheaf F)) (U : Cᵒᵖ) :

(sSup S).obj U = sSup ((fun (T : Subpresheaf F) => T.obj U) '' S)

source

theorem CategoryTheory.Subpresheaf.sInf_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S : Set (Subpresheaf F)) (U : Cᵒᵖ) :

(sInf S).obj U = sInf ((fun (T : Subpresheaf F) => T.obj U) '' S)

source

@[simp]

theorem CategoryTheory.Subpresheaf.iSup_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {ι : Type u_1} (S : ι → Subpresheaf F) (U : Cᵒᵖ) :

(⨆ (i : ι), S i).obj U = ⋃ (i : ι), (S i).obj U

source

@[simp]

theorem CategoryTheory.Subpresheaf.iInf_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {ι : Type u_1} (S : ι → Subpresheaf F) (U : Cᵒᵖ) :

(⨅ (i : ι), S i).obj U = ⋂ (i : ι), (S i).obj U

source

@[simp]

theorem CategoryTheory.Subpresheaf.max_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S T : Subpresheaf F) (i : Cᵒᵖ) :

(S ⊔ T).obj i = S.obj i ∪ T.obj i

source

@[simp]

theorem CategoryTheory.Subpresheaf.min_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S T : Subpresheaf F) (i : Cᵒᵖ) :

(S ⊓ T).obj i = S.obj i ∩ T.obj i

source

theorem CategoryTheory.Subpresheaf.max_min {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (S₁ S₂ T : Subpresheaf F) :

(S₁ ⊔ S₂) ⊓ T = S₁ ⊓ T ⊔ S₂ ⊓ T

source

theorem CategoryTheory.Subpresheaf.iSup_min {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {ι : Type u_1} (S : ι → Subpresheaf F) (T : Subpresheaf F) :

(⨆ (i : ι), S i) ⊓ T = ⨆ (i : ι), S i ⊓ T

source

instance CategoryTheory.Subpresheaf.instNonempty {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} :

Nonempty (Subpresheaf F)

source

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

Functor Cᵒᵖ (Type w)

The subpresheaf as a presheaf.

Equations

G.toPresheaf = { obj := fun (U : Cᵒᵖ) => ↑(G.obj U), map := fun (x x_1 : Cᵒᵖ) (i : x ⟶ x_1) (x_2 : ↑(G.obj x)) => ⟨F.map i ↑x_2, ⋯⟩, map_id := ⋯, map_comp := ⋯ }