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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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)

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)

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

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

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

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

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

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

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

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.

@[simp]

theorem CategoryTheory.Subfunctor.toFunctor_map_coe {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) (x✝ x✝¹ : C) (i : x✝ ⟶ x✝¹) (x : ↑(G.obj x✝)) : ↑(G.toFunctor.map i x) = F.map i ↑x

@[simp]

theorem CategoryTheory.Subfunctor.toFunctor_obj {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) (U : C) : G.toFunctor.obj U = ↑(G.obj U)

instance CategoryTheory.Subfunctor.instCoeHeadObjToFunctor {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) {U : C} : CoeHead (G.toFunctor.obj U) (F.obj U)

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

The inclusion of a subfunctor to the original functor.

@[simp]

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

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

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

The inclusion of a subfunctor to a larger subfunctor

@[simp]

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Subfunctor.homOfLe_ι_assoc {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {G G' : Subfunctor 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.Subfunctor.instIsIsoFunctorTypeιTop {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} : IsIso ⊤.ι

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

theorem CategoryTheory.Subfunctor.nat_trans_naturality {C : Type u} [Category.{v, u} C] {F F' : Functor C (Type w)} (G : Subfunctor F) (f : F' ⟶ G.toFunctor) {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.Subfunctor.le_def (since := "2025-12-11")]

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.le_def.

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

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

Alias of CategoryTheory.Subfunctor.top_obj.

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

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

Alias of CategoryTheory.Subfunctor.bot_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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)

Alias of CategoryTheory.Subfunctor.sSup_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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)

Alias of CategoryTheory.Subfunctor.sInf_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.iSup_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.iInf_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.max_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.min_obj.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.max_min.

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

theorem CategoryTheory.Subfunctor.Subpresheaf.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

Alias of CategoryTheory.Subfunctor.iSup_min.

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

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

Alias of CategoryTheory.Subfunctor.toFunctor.

---

The subfunctor as a functor.

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

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

Alias of CategoryTheory.Subfunctor.ι.

---

The inclusion of a subfunctor to the original functor.

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

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

Alias of CategoryTheory.Subfunctor.homOfLe.

---

The inclusion of a subfunctor to a larger subfunctor

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

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

Alias of CategoryTheory.Subfunctor.homOfLe_ι.

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

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

Alias of CategoryTheory.Subfunctor.eq_top_iff_isIso.

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

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

Alias of CategoryTheory.Subfunctor.nat_trans_naturality.

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

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

Alias of CategoryTheory.Subfunctor.toFunctor.

---

The subfunctor as a functor.

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

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

Alias of CategoryTheory.Subfunctor.toFunctor_obj.

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

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

Alias of CategoryTheory.Subfunctor.toFunctor_map_coe.