Theorems · Definition · category theory

CategoryTheory.SubmonoidFunctor.lift

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

Defined in

Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category