Theorems · Definition · category theory

CategoryTheory.MonoOver.mapComp

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Mono f] →
            [inst_2 : CategoryTheory.Mono g] →
              CategoryTheory.MonoOver.map (CategoryTheory.CategoryStruct.comp f g) ≅
                (CategoryTheory.MonoOver.map f).comp (CategoryTheory.MonoOver.map g)

MonoOver.map commutes with composition (up to a natural isomorphism).

Defined in

Mathlib.CategoryTheory.Subobject.MonoOver

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoCategoryTheory.Mono