Theorems · Theorem · category theory

CategoryTheory.Limits.Types.isPullback_of_isPushout

∀ {X₁ X₂ X₃ X₄ : Type u} {t : X₁ ⟶ X₂} {r : X₂ ⟶ X₄} {l : X₁ ⟶ X₃} {b : X₃ ⟶ X₄},
  CategoryTheory.IsPushout t l r b →
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom t) → CategoryTheory.IsPullback t l r b

A pushout square in Type where the top map is injective is a pullback square. This is also essentially the lemma isPullback_of_isPushout_of_mono_left from the file CategoryTheory.Adhesive.Basic in the case of the adhesive category of types.

Defined in

Mathlib.CategoryTheory.Limits.Types.Pushouts

Cited by

0 results in Mathlib

Foundations

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