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).

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

@[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

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 ⋯

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

Equations

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

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

@[simp]

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

@[simp]

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

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)

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)

@[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

@[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

@[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

@[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

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

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

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

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 := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.toPresheaf_obj {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (U : Cᵒᵖ) : G.toPresheaf.obj U = ↑(G.obj U)

@[simp]

theorem CategoryTheory.Subpresheaf.toPresheaf_map_coe {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (x✝ x✝¹ : Cᵒᵖ) (i : x✝ ⟶ x✝¹) (x : ↑(G.obj x✝)) : ↑(G.toPresheaf.map i x) = F.map i ↑x

instance CategoryTheory.Subpresheaf.instCoeHeadObjOppositeToPresheaf {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} : CoeHead (G.toPresheaf.obj U) (F.obj U)

Equations

• G.instCoeHeadObjOppositeToPresheaf = { coe := Subtype.val }

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

The inclusion of a subpresheaf to the original presheaf.

Equations

• G.ι = { app := fun (x : Cᵒᵖ) (x_1 : G.toPresheaf.obj x) => ↑x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.ι_app {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (x✝ : Cᵒᵖ) (x : G.toPresheaf.obj x✝) : G.ι.app x✝ x = ↑x

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

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

The inclusion of a subpresheaf to a larger subpresheaf

Equations

• CategoryTheory.Subpresheaf.homOfLe h = { app := fun (U : Cᵒᵖ) (x : G.toPresheaf.obj U) => ⟨↑x, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.homOfLe_app_coe {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G G' : Subpresheaf F} (h : G ≤ G') (U : Cᵒᵖ) (x : G.toPresheaf.obj U) : ↑((homOfLe h).app U x) = ↑x

instance CategoryTheory.Subpresheaf.instMonoFunctorOppositeTypeHomOfLe {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G G' : Subpresheaf F} (h : G ≤ G') : Mono (homOfLe h)

@[simp]

theorem CategoryTheory.Subpresheaf.homOfLe_ι {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G G' : Subpresheaf F} (h : G ≤ G') : CategoryStruct.comp (homOfLe h) G'.ι = G.ι

@[simp]

theorem CategoryTheory.Subpresheaf.homOfLe_ι_assoc {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G G' : Subpresheaf F} (h : G ≤ G') {Z : Functor Cᵒᵖ (Type w)} (h✝ : F ⟶ Z) : CategoryStruct.comp (homOfLe h) (CategoryStruct.comp G'.ι h✝) = CategoryStruct.comp G.ι h✝

instance CategoryTheory.Subpresheaf.instIsIsoFunctorOppositeTypeιTop {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} : IsIso ⊤.ι

theorem CategoryTheory.Subpresheaf.eq_top_iff_isIso {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) : G = ⊤ ↔ IsIso G.ι

theorem CategoryTheory.Subpresheaf.nat_trans_naturality {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F' ⟶ G.toPresheaf) {U V : Cᵒᵖ} (i : U ⟶ V) (x : F'.obj U) : ↑(f.app V (F'.map i x)) = F.map i ↑(f.app U x)

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

theorem CategoryTheory.top_subpresheaf_obj {C : Type u} [Category.{v, u} C] (F : Functor Cᵒᵖ (Type w)) (i : Cᵒᵖ) : ⊤.obj i = ⊤

Alias of CategoryTheory.Subpresheaf.top_obj.