Theorems · Theorem · category theory

CategoryTheory.IsPushout.IsVanKampen.exists_cube_filling

∀ {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}
  {H : CategoryTheory.IsPushout f g h i},
  H.IsVanKampen →
    ∀ {X' Y' Z' : C} {h' : X' ⟶ Z'} {i' : Y' ⟶ Z'} {αX : X' ⟶ X} {αY : Y' ⟶ Y} {αZ : Z' ⟶ Z}
      [CategoryTheory.Limits.HasPullback αX f],
      CategoryTheory.IsPullback h' αX αZ h →
        CategoryTheory.IsPullback i' αY αZ i →
          ∃ W' f' g' αW,
            CategoryTheory.IsPullback f' αW αX f ∧
              CategoryTheory.IsPullback g' αW αY g ∧ CategoryTheory.IsPushout f' g' h' i'

If a van Kampen pushout forms the bottom face of a commutative "half-cube" whose front faces are pullbacks, then there exist two back faces which are pullbacks and a top face which is a pushout.

Defined in

Mathlib.CategoryTheory.Adhesive.Basic

Cited by

2 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback