Theorems · Definition · category theory
CategoryTheory.Square.IsPushout
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → PropThe condition that a commutative square is a pushout square.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- CategoryTheory.IsPushoutproof · cited by 219
- CategoryTheory.Squarestatement and proof · cited by 193
- CategoryTheory.Square.f₁₃proof · cited by 56
- CategoryTheory.Square.f₂₄proof · cited by 52
- CategoryTheory.Square.f₁₂proof · cited by 51
- CategoryTheory.Square.f₃₄proof · cited by 51
Cited by28
Results whose statement or proof uses this declaration.
- CategoryTheory.Square.IsPushout.mapstatement and proof · cited by 2
- CategoryTheory.Square.IsPushout.mkstatement · cited by 2
- CategoryTheory.Square.IsPushout.of_isostatement and proof · cited by 2
- CategoryTheory.Square.IsPushout.opstatement and proof · cited by 2
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutstatement · cited by 2
- CategoryTheory.Square.IsPushout.epi_f₂₄statement and proof · cited by 1
- CategoryTheory.Square.IsPushout.flipstatement and proof · cited by 1
- CategoryTheory.Square.IsPushout.isColimitstatement and proof · cited by 1
- CategoryTheory.Square.IsPushout.isColimitCokernelCoforkstatement and proof · cited by 1
- CategoryTheory.Square.IsPushout.of_mapstatement and proof · cited by 1
- CategoryTheory.Square.isPushout_iffstatement and proof · cited by 1
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk.injstatement and proof · cited by 1