Theorems · Theorem · category theory

CategoryTheory.Adhesive.isPushout_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}
  [CategoryTheory.Adhesive C] [CategoryTheory.Mono f],
  CategoryTheory.IsPushout f g h i →
    ∀ {X' Y' Z' : C} {h' : X' ⟶ Z'} {i' : Y' ⟶ Z'} {αX : X' ⟶ X} {α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

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AdhesiveCategoryTheory.Mono