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 ⊆ ⇑(ConcreteCategory.hom (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

@[instance_reducible]

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 ⋯

@[instance_reducible]

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.

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 = Set.univ

@[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)} {ι : Sort 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)} {ι : Sort 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)} {ι : Sort 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)

@[implicit_reducible]

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

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

@[simp]

theorem CategoryTheory.Subfunctor.toFunctor_map {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) {X✝ Y✝ : C} (i : X✝ ⟶ Y✝) : G.toFunctor.map i = TypeCat.ofHom fun (x : ↑(G.obj X✝)) => ⟨(ConcreteCategory.hom (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_reducible]

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)

Equations

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

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.

Equations

• G.ι = { app := fun (x : C) => TypeCat.ofHom fun (x_1 : G.toFunctor.obj x) => ↑x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subfunctor.ι_app {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} (G : Subfunctor F) (x✝ : C) : G.ι.app x✝ = TypeCat.ofHom fun (x : G.toFunctor.obj 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

Equations

• CategoryTheory.Subfunctor.homOfLe h = { app := fun (U : C) => TypeCat.ofHom fun (x : G.toFunctor.obj U) => ⟨↑x, ⋯⟩, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Subfunctor.homOfLe_app {C : Type u} [Category.{v, u} C] {F : Functor C (Type w)} {G G' : Subfunctor F} (h : G ≤ G') (U : C) : (homOfLe h).app U = TypeCat.ofHom fun (x : G.toFunctor.obj U) => ⟨↑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) : ↑((ConcreteCategory.hom (f.app V)) ((ConcreteCategory.hom (F'.map i)) x)) = (ConcreteCategory.hom (F.map i)) ↑((ConcreteCategory.hom (f.app U)) x)