Theorems · Theorem · category theory

CategoryTheory.Arrow.w

∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) g.hom =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Arrow.Hom.right sq)

Defined in: Mathlib.CategoryTheory.Comma.Arrow
Cited by: 7 results in Mathlib
Foundations: Depth 15 from the axioms · uses no axioms
Assumes: CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

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.CategoryStruct.compstatement · cited by 17,999
CategoryTheory.Arrowstatement and proof · cited by 713
CategoryTheory.Arrow.leftstatement · cited by 426
CategoryTheory.Arrow.rightstatement · cited by 423
CategoryTheory.Arrow.homstatement · cited by 335
CategoryTheory.Arrow.Hom.rightstatement · cited by 176
CategoryTheory.Arrow.Hom.leftstatement · cited by 160
CategoryTheory.CommaMorphism.wproof · cited by 24

Cited by7

Results whose statement or proof uses this declaration.

CategoryTheory.Arrow.Hom.wproof · cited by 17
CategoryTheory.Arrow.w_assocproof · cited by 2
CategoryTheory.Limits.ImageMap.factor_mapproof · cited by 2
CategoryTheory.Arrow.inv_left_hom_rightproof · cited by 0
CategoryTheory.Arrow.isIso_of_isIso_left_of_isIso_rightproof · cited by 0
CategoryTheory.Arrow.left_hom_inv_rightproof · cited by 0
CategoryTheory.Arrow.square_from_iso_invertproof · cited by 0