Theorems · Inductive type · category theory
CategoryTheory.CommSq
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] → {W X Y Z : C} → (W ⟶ X) → (W ⟶ Y) → (X ⟶ Z) → (Y ⟶ Z) → PropThe proposition that a square
``
W f > X
| |
g h
| |
v v
Y i > Z
``
is a commuting square.
- Defined in
- Mathlib.CategoryTheory.CommSq
- Cited by
- 158 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 7 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- Quiver.Homstatement · cited by 32,603
Cited by214
Results whose statement or proof uses this declaration.
- CategoryTheory.CommSq.wstatement and proof · cited by 122
- CategoryTheory.IsPullback.toCommSqstatement · cited by 52
- CategoryTheory.IsPushout.toCommSqstatement · cited by 35
- CategoryTheory.CommSq.liftstatement and proof · cited by 34
- CategoryTheory.CommSq.LiftStructstatement · cited by 33
- CategoryTheory.CommSq.fac_leftstatement and proof · cited by 22
- CategoryTheory.IsPullback.of_vert_isIsostatement and proof · cited by 21
- CategoryTheory.CommSq.HasLiftstatement · cited by 20
- CategoryTheory.CommSq.fac_rightstatement and proof · cited by 19
- CategoryTheory.IsPushout.IsVanKampenproof · cited by 13
- CategoryTheory.CommSq.flipstatement and proof · cited by 11
- CategoryTheory.CommSq.vert_invstatement and proof · cited by 11
Showing the 200 most cited of 214.