Theorems · Theorem · category theory

CategoryTheory.IsPushout.isVanKampen_isPullback_isPullback_hom_ext

∀ {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} [CategoryTheory.Limits.HasPullback αX f] {αY : Y' ⟶ Y}
      {αZ : Z' ⟶ Z} {W : C} {f₁ f₂ : Z' ⟶ W},
      CategoryTheory.IsPullback h' αX αZ h →
        CategoryTheory.IsPullback i' αY αZ i →
          CategoryTheory.CategoryStruct.comp h' f₁ = CategoryTheory.CategoryStruct.comp h' f₂ →
            CategoryTheory.CategoryStruct.comp i' f₁ = CategoryTheory.CategoryStruct.comp i' f₂ → f₁ = f₂

Defined in

Mathlib.CategoryTheory.Adhesive.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback