Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.Under.Hom.mk_hom

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X}
  (f :
    (CategoryTheory.MorphismProperty.Under.forget P Q X).obj A ⟶
      (CategoryTheory.MorphismProperty.Under.forget P Q X).obj B)
  (hf : Q (CategoryTheory.Under.Hom.right f)),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.Hom.mk f hf) = f

Defined in

Mathlib.CategoryTheory.MorphismProperty.Comma

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicative