Theorems · Theorem · category theory

CategoryTheory.SubmonoidFunctor.map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (self : CategoryTheory.SubmonoidFunctor M) {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.

Defined in

Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Cited by

2 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category