Theorems · Definition · category theory
CategoryTheory.MorphismProperty.Arrow.Hom.mk
{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 :
(CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj A ⟶
(CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj B) →
Q (CategoryTheory.Arrow.Hom.left f) → W (CategoryTheory.Arrow.Hom.right f) → (A ⟶ B)Construct a morphism in P.Arrow Q W from a morphism in Arrow T.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 19 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 and proof · cited by 19,642
- CategoryTheory.Functor.idstatement · cited by 3,333
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.Arrowstatement · cited by 713
- CategoryTheory.Arrow.leftstatement and proof · cited by 426
- CategoryTheory.Arrow.rightstatement and proof · cited by 423
- CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
- CategoryTheory.Arrow.Hom.rightstatement and proof · cited by 176
- CategoryTheory.Arrow.Hom.leftstatement and proof · cited by 160
- CategoryTheory.MorphismProperty.Arrowstatement and proof · cited by 17
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.Arrow.Hom.mk_homstatement and proof · cited by 0