Functors of submonoids

Given a functor M : C ⥤ MonCat, we define a functor of submonoids S to be a family Submonoid (M.obj U) for all U : C that are compatible with the maps induced by M.

We provide the complete lattice structure and the basic functoriality properties.

TODO

• Show the Galois connection between SubmonoidFunctor.image and SubmonoidFunctor.comap and provide the related API.

structure CategoryTheory.SubmonoidFunctor {C : Type u} [Category.{v, u} C] (M : Functor C MonCat) : Type (max u w)

A submonoid functor consists of a submonoid of M.obj U for every U, compatible with the restriction maps M.map i.

• obj (U : C) : Submonoid ↑(M.obj U)

  A submonoid of M.obj U for all U : C.

• map {U V : C} (i : U ⟶ V) : self.obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (self.obj V)

  For any i : U ⟶ V, M.map i maps the submonoid obj U into the submonoid obj V.

theorem CategoryTheory.SubmonoidFunctor.ext {C : Type u} {inst✝ : Category.{v, u} C} {M : Functor C MonCat} {x y : SubmonoidFunctor M} (obj : x.obj = y.obj) : x = y

theorem CategoryTheory.SubmonoidFunctor.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {M : Functor C MonCat} {x y : SubmonoidFunctor M} : x = y ↔ x.obj = y.obj

theorem CategoryTheory.SubmonoidFunctor.map_le {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) {U V : C} (f : U ⟶ V) : Submonoid.map (MonCat.Hom.hom (M.map f)) (S.obj U) ≤ S.obj V

def CategoryTheory.SubmonoidFunctor.toFunctor {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) : Functor C MonCat

The functor of monoids associated to a functor of submonoids.

Equations

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

@[simp]

theorem CategoryTheory.SubmonoidFunctor.toFunctor_map {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) {X✝ Y✝ : C} (i : X✝ ⟶ Y✝) : S.toFunctor.map i = MonCat.ofHom (((MonCat.Hom.hom (M.map i)).submonoidComap (S.obj Y✝)).comp (Submonoid.inclusion ⋯))

@[simp]

theorem CategoryTheory.SubmonoidFunctor.toFunctor_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) (x✝ : C) : S.toFunctor.obj x✝ = MonCat.of ↥(S.obj x✝)

def CategoryTheory.SubmonoidFunctor.toSubfunctor {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) : Subfunctor (M.comp (forget MonCat))

The subfunctor associated to a functor of submonoids.

Equations

• S.toSubfunctor = { obj := fun (x : C) => (S.obj x).carrier, map := ⋯ }

@[simp]

theorem CategoryTheory.SubmonoidFunctor.toSubfunctor_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) (x✝ : C) : S.toSubfunctor.obj x✝ = (S.obj x✝).carrier

@[implicit_reducible]

instance CategoryTheory.SubmonoidFunctor.instCoeHeadCarrierObjMonCatToFunctor {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) {U : C} : CoeHead ↑(S.toFunctor.obj U) ↑(M.obj U)

Equations

• S.instCoeHeadCarrierObjMonCatToFunctor = { coe := Subtype.val }

@[implicit_reducible]

instance CategoryTheory.SubmonoidFunctor.instPartialOrder {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} : PartialOrder (SubmonoidFunctor M)

Equations

• CategoryTheory.SubmonoidFunctor.instPartialOrder = PartialOrder.lift CategoryTheory.SubmonoidFunctor.obj ⋯

@[implicit_reducible]

instance CategoryTheory.SubmonoidFunctor.instCompleteLattice {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} : CompleteLattice (SubmonoidFunctor M)

Equations

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

@[simp]

theorem CategoryTheory.SubmonoidFunctor.sSup_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : Set (SubmonoidFunctor M)) (x✝ : C) : (sSup S).obj x✝ = ⨆ F ∈ S, F.obj x✝

@[simp]

theorem CategoryTheory.SubmonoidFunctor.sup_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (F G : SubmonoidFunctor M) (x✝ : C) : (SemilatticeSup.sup F G).obj x✝ = F.obj x✝ ⊔ G.obj x✝

@[simp]

theorem CategoryTheory.SubmonoidFunctor.top_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (x✝ : C) : ⊤.obj x✝ = ⊤

@[simp]

theorem CategoryTheory.SubmonoidFunctor.inf_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S T : SubmonoidFunctor M) (x✝ : C) : (Lattice.inf S T).obj x✝ = S.obj x✝ ⊓ T.obj x✝

@[simp]

theorem CategoryTheory.SubmonoidFunctor.sInf_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : Set (SubmonoidFunctor M)) (x✝ : C) : (sInf S).obj x✝ = ⨅ F ∈ S, F.obj x✝

@[simp]

theorem CategoryTheory.SubmonoidFunctor.bot_obj {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (x✝ : C) : ⊥.obj x✝ = ⊥

def CategoryTheory.SubmonoidFunctor.ι {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) : S.toFunctor ⟶ M

The inclusion of a submonoid functor S to the original functor of monoids M.

Equations

• S.ι = { app := fun (x : C) => MonCat.ofHom (S.obj x).subtype, naturality := ⋯ }

@[simp]

theorem CategoryTheory.SubmonoidFunctor.ι_app {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) (x✝ : C) : S.ι.app x✝ = MonCat.ofHom (S.obj x✝).subtype

instance CategoryTheory.SubmonoidFunctor.instMonoFunctorMonCatι {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) : Mono S.ι

def CategoryTheory.SubmonoidFunctor.image {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S : SubmonoidFunctor M) : SubmonoidFunctor M'

The submonoid functor defined by the image along a morphism of functors of monoids.

Equations

• CategoryTheory.SubmonoidFunctor.image p S = { obj := fun (x : C) => Submonoid.map (MonCat.Hom.hom (p.app x)) (S.obj x), map := ⋯ }

@[simp]

theorem CategoryTheory.SubmonoidFunctor.image_obj {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S : SubmonoidFunctor M) (x✝ : C) : (image p S).obj x✝ = Submonoid.map (MonCat.Hom.hom (p.app x✝)) (S.obj x✝)

@[simp]

theorem CategoryTheory.SubmonoidFunctor.image_id {C : Type u} [Category.{v, u} C] (M : Functor C MonCat) : image (CategoryStruct.id M) ⊤ = ⊤

@[simp]

theorem CategoryTheory.SubmonoidFunctor.image_comp {C : Type u} [Category.{v, u} C] {M M' M'' : Functor C MonCat} (S : SubmonoidFunctor M) (p : M ⟶ M') (p' : M' ⟶ M'') : image (CategoryStruct.comp p p') S = image p' (image p S)

def CategoryTheory.SubmonoidFunctor.comap {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') : SubmonoidFunctor M

The submonoid functor defined by the preimage along a morphism of functors of monoids.

Equations

• CategoryTheory.SubmonoidFunctor.comap p S' = { obj := fun (x : C) => Submonoid.comap (MonCat.Hom.hom (p.app x)) (S'.obj x), map := ⋯ }

@[simp]

theorem CategoryTheory.SubmonoidFunctor.comap_obj {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') (x✝ : C) : (comap p S').obj x✝ = Submonoid.comap (MonCat.Hom.hom (p.app x✝)) (S'.obj x✝)

@[simp]

theorem CategoryTheory.SubmonoidFunctor.comap_id {C : Type u} [Category.{v, u} C] (M : Functor C MonCat) : comap (CategoryStruct.id M) ⊤ = ⊤

@[simp]

theorem CategoryTheory.SubmonoidFunctor.comap_comp {C : Type u} [Category.{v, u} C] {M M' M'' : Functor C MonCat} (p : M ⟶ M') (S'' : SubmonoidFunctor M'') (p' : M' ⟶ M'') : comap (CategoryStruct.comp p p') S'' = comap p (comap p' S'')

@[simp]

theorem CategoryTheory.SubmonoidFunctor.image_comap_ι {C : Type u} [Category.{v, u} C] {M : Functor C MonCat} (S : SubmonoidFunctor M) : image S.ι (comap S.ι S) = S

def CategoryTheory.SubmonoidFunctor.lift {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') (hp : image p ⊤ ≤ S') : M ⟶ S'.toFunctor

If the image of morphism M' ⟶ M lands in a submonoid functor S, then the morphism factors through it.

Equations

• CategoryTheory.SubmonoidFunctor.lift p S' hp = { app := fun (U : C) => MonCat.ofHom ((MonCat.Hom.hom (p.app U)).codRestrict (S'.obj U) ⋯), naturality := ⋯ }

@[simp]

theorem CategoryTheory.SubmonoidFunctor.lift_app {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') (hp : image p ⊤ ≤ S') (U : C) : (lift p S' hp).app U = MonCat.ofHom ((MonCat.Hom.hom (p.app U)).codRestrict (S'.obj U) ⋯)

@[simp]

theorem CategoryTheory.SubmonoidFunctor.lift_ι {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') (hp : image p ⊤ ≤ S') : CategoryStruct.comp (lift p S' hp) S'.ι = p

@[simp]

theorem CategoryTheory.SubmonoidFunctor.lift_ι_assoc {C : Type u} [Category.{v, u} C] {M M' : Functor C MonCat} (p : M ⟶ M') (S' : SubmonoidFunctor M') (hp : image p ⊤ ≤ S') {Z : Functor C MonCat} (h : M' ⟶ Z) : CategoryStruct.comp (lift p S' hp) (CategoryStruct.comp S'.ι h) = CategoryStruct.comp p h