Subfunctor of types #

We define subfunctors of a type-valued functors.

Main definition #

CategoryTheory.Subfunctor : A subfunctor of a type-valued functor.

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

Type (max u w)

A subfunctor of a functor 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 subfunctor 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 subfunctor 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.Subfunctor.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C (Type w)} {x y : Subfunctor F} :

x = y ↔ x.obj = y.obj

source

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

x = y

source

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

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

Type (max u w)

Alias of CategoryTheory.Subfunctor.

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

Equations

@CategoryTheory.Subpresheaf = @CategoryTheory.Subfunctor

Instances For

source

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

PartialOrder (Subfunctor F)

Equations

CategoryTheory.instPartialOrderSubfunctor = PartialOrder.lift CategoryTheory.Subfunctor.obj ⋯

source

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

CompleteLattice (Subfunctor F)

Equations

One or more equations did not get rendered due to their size.

source

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

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

source

@[simp]

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

⊤.obj i = ⊤

source

@[simp]

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

⊥.obj i = ⊥

source

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

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

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

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

source

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

Nonempty (Subfunctor F)

source

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

Functor C (Type w)

The subfunctor as a functor.

Equations

G.toFunctor = { 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 := ⋯ }