Theorems · Theorem · category theory

CategoryTheory.Limits.Types.isPullback_iff

∀ {X₁ X₂ X₃ X₄ : Type u} (t : X₁ ⟶ X₂) (r : X₂ ⟶ X₄) (l : X₁ ⟶ X₃) (b : X₃ ⟶ X₄),
  CategoryTheory.IsPullback t l r b ↔
    CategoryTheory.CategoryStruct.comp t r = CategoryTheory.CategoryStruct.comp l b ∧
      (∀ (x₁ y₁ : (fun X => X) X₁),
          (CategoryTheory.ConcreteCategory.hom t) x₁ = (CategoryTheory.ConcreteCategory.hom t) y₁ ∧
              (CategoryTheory.ConcreteCategory.hom l) x₁ = (CategoryTheory.ConcreteCategory.hom l) y₁ →
            x₁ = y₁) ∧
        ∀ (x₂ : (fun X => X) X₂) (x₃ : (fun X => X) X₃),
          (CategoryTheory.ConcreteCategory.hom r) x₂ = (CategoryTheory.ConcreteCategory.hom b) x₃ →
            ∃ x₁, (CategoryTheory.ConcreteCategory.hom t) x₁ = x₂ ∧ (CategoryTheory.ConcreteCategory.hom l) x₁ = x₃

Defined in

Mathlib.CategoryTheory.Limits.Types.Pullbacks

Cited by

4 results in Mathlib

Foundations

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