Theorems · Theorem · category theory
CategoryTheory.MorphismProperty.Arrow.forget_comp_leftFunc_map
∀ {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 ⟶ B),
((CategoryTheory.MorphismProperty.Arrow.forget P Q W).comp CategoryTheory.Arrow.leftFunc).map f = f.leftOccasionally useful for rewriting in the backwards direction.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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.Functor.mapstatement · cited by 8,698
- CategoryTheory.Functor.compstatement · cited by 6,529
- CategoryTheory.Functor.idstatement · cited by 3,333
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.Arrowstatement · cited by 713
- CategoryTheory.CommaMorphism.leftstatement · cited by 526
- CategoryTheory.MorphismProperty.IsMultiplicativestatement and proof · cited by 332
- CategoryTheory.MorphismProperty.Comma.toCommastatement · cited by 260
- CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphismstatement · cited by 142
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.