Theorems · Definition · category theory

CategoryTheory.MorphismProperty.Over.mapComp

{T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          {X Y Z : T} →
            [inst_2 : P.IsStableUnderComposition] →
              {f : X ⟶ Y} →
                (hf : P f) →
                  {g : Y ⟶ Z} →
                    (hg : P g) →
                      [Q.RespectsIso] →
                        (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                          (hfg :
                              autoParam (fg = CategoryTheory.CategoryStruct.comp f g)
                                CategoryTheory.MorphismProperty.Over.mapComp._auto_1) →
                            CategoryTheory.MorphismProperty.Over.map Q ⋯ ≅
                              (CategoryTheory.MorphismProperty.Over.map Q hf).comp
                                (CategoryTheory.MorphismProperty.Over.map Q hg)

Over.map commutes with composition.

Defined in

Mathlib.CategoryTheory.MorphismProperty.OverAdjunction

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.RespectsIso