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.instTopSubpresheaf {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} : Top (Subpresheaf F)

Equations

• CategoryTheory.instTopSubpresheaf = { top := { obj := fun (x : Cᵒᵖ) => ⊤, map := ⋯ } }

instance CategoryTheory.instNonemptySubpresheaf {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.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

• CategoryTheory.instCoeHeadObjOppositeToPresheaf G = { 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.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.instMonoFunctorOppositeTypeHomOfLe {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} {G G' : Subpresheaf F} (h : G ≤ G') : Mono (Subpresheaf.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.instIsIsoFunctorOppositeTypeιTopSubpresheaf {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.ι

def CategoryTheory.Subpresheaf.lift {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F' ⟶ F) (hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U) : F' ⟶ G.toPresheaf

If the image of a morphism falls in a subpresheaf, then the morphism factors through it.

Equations

• G.lift f hf = { app := fun (U : Cᵒᵖ) (x : F'.obj U) => ⟨f.app U x, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.lift_app_coe {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F' ⟶ F) (hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U) (U : Cᵒᵖ) (x : F'.obj U) : ↑((G.lift f hf).app U x) = f.app U x

@[simp]

theorem CategoryTheory.Subpresheaf.lift_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F' ⟶ F) (hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U) : CategoryStruct.comp (G.lift f hf) G.ι = f

@[simp]

theorem CategoryTheory.Subpresheaf.lift_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) (f : F' ⟶ F) (hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) : CategoryStruct.comp (G.lift f hf) (CategoryStruct.comp G.ι h) = CategoryStruct.comp f h

def CategoryTheory.Subpresheaf.sieveOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) : Sieve (Opposite.unop U)

Given a subpresheaf G of F, an F-section s on U, we may define a sieve of U consisting of all f : V ⟶ U such that the restriction of s along f is in G.

Equations

• G.sieveOfSection s = { arrows := fun (V : C) (f : V ⟶ Opposite.unop U) => F.map f.op s ∈ G.obj (Opposite.op V), downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Subpresheaf.sieveOfSection_apply {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) (V : C) (f : V ⟶ Opposite.unop U) : (G.sieveOfSection s).arrows f = (F.map f.op s ∈ G.obj (Opposite.op V))

def CategoryTheory.Subpresheaf.familyOfElementsOfSection {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) : Presieve.FamilyOfElements G.toPresheaf (G.sieveOfSection s).arrows

Given an F-section s on U and a subpresheaf G, we may define a family of elements in G consisting of the restrictions of s

Equations

• G.familyOfElementsOfSection s i hi = ⟨F.map i.op s, hi⟩

theorem CategoryTheory.Subpresheaf.family_of_elements_compatible {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} (G : Subpresheaf F) {U : Cᵒᵖ} (s : F.obj U) : (G.familyOfElementsOfSection s).Compatible

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)

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

The image presheaf of a morphism, whose components are the set-theoretic images.

Equations

• CategoryTheory.imagePresheaf f = { obj := fun (U : Cᵒᵖ) => Set.range (f.app U), map := ⋯ }

@[simp]

theorem CategoryTheory.imagePresheaf_obj {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (U : Cᵒᵖ) : (imagePresheaf f).obj U = Set.range (f.app U)

@[simp]

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

@[simp]

theorem CategoryTheory.imagePresheaf_id {C : Type u} [Category.{v, u} C] {F : Functor Cᵒᵖ (Type w)} : imagePresheaf (CategoryStruct.id F) = ⊤

def CategoryTheory.toImagePresheaf {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : F' ⟶ (imagePresheaf f).toPresheaf

A morphism factors through the image presheaf.

Equations

• CategoryTheory.toImagePresheaf f = (CategoryTheory.imagePresheaf f).lift f ⋯

@[simp]

theorem CategoryTheory.toImagePresheaf_app_coe {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) (U : Cᵒᵖ) (x : F'.obj U) : ↑((toImagePresheaf f).app U x) = f.app U x

@[simp]

theorem CategoryTheory.toImagePresheaf_ι {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) : CategoryStruct.comp (toImagePresheaf f) (imagePresheaf f).ι = f

@[simp]

theorem CategoryTheory.toImagePresheaf_ι_assoc {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F' ⟶ F) {Z : Functor Cᵒᵖ (Type w)} (h : F ⟶ Z) : CategoryStruct.comp (toImagePresheaf f) (CategoryStruct.comp (imagePresheaf f).ι h) = CategoryStruct.comp f h

theorem CategoryTheory.imagePresheaf_comp_le {C : Type u} [Category.{v, u} C] {F F' F'' : Functor Cᵒᵖ (Type w)} (f₁ : F ⟶ F') (f₂ : F' ⟶ F'') : imagePresheaf (CategoryStruct.comp f₁ f₂) ≤ imagePresheaf f₂

instance CategoryTheory.isIso_toImagePresheaf {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [hf : Mono f] : IsIso (toImagePresheaf f)