Theorems · Definition · category theory
CategoryTheory.MorphismProperty.Arrow.homMk
{T : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} T] →
{P Q W : CategoryTheory.MorphismProperty T} →
[inst_1 : Q.IsMultiplicative] →
[inst_2 : W.IsMultiplicative] →
{A B : P.Arrow Q W} →
(f : A.left ⟶ B.left) →
(g : A.right ⟶ B.right) →
autoParam (CategoryTheory.CategoryStruct.comp f B.hom = CategoryTheory.CategoryStruct.comp A.hom g)
CategoryTheory.MorphismProperty.Arrow.homMk._auto_1 →
autoParam (Q f) CategoryTheory.MorphismProperty.Arrow.homMk._auto_3 →
autoParam (W g) CategoryTheory.MorphismProperty.Arrow.homMk._auto_5 → (A ⟶ B)Make a morphism in P.Arrow Q X from morphisms in T with compatibilities.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
- CategoryTheory.Functor.idstatement · cited by 3,333
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.Comma.leftstatement and proof · cited by 886
- CategoryTheory.Comma.rightstatement and proof · cited by 727
- CategoryTheory.Comma.homstatement and proof · cited by 490
- CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
- CategoryTheory.MorphismProperty.Comma.toCommastatement and proof · cited by 260
- CategoryTheory.Arrow.homMkproof · cited by 35
Cited by2
Results whose statement or proof uses this declaration.
- TopPair.ofHomproof · cited by 4
- CategoryTheory.MorphismProperty.Arrow.homMk_homstatement and proof · cited by 0