Theorems · Definition · category theory

CategoryTheory.IsPushout.IsVanKampen

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} → {f : W ⟶ X} → {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → CategoryTheory.IsPushout f g h i → Prop

A convenient formulation for a pushout being a van Kampen colimit. For any commutative cube of which a van Kampen pushout forms the bottom face and the back faces are pullbacks, the front faces are pullbacks if and only if the top face is a pushout. See IsPushout.isVanKampen_iff below.

Defined in

Mathlib.CategoryTheory.Adhesive.Basic

Cited by

13 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category