Theorems · Theorem · category theory

CategoryTheory.SubmonoidFunctor.lift_app

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

Defined in

Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category