Theorems · Theorem · category theory

CategoryTheory.IsPullback.of_bot

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
  CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
      (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ →
    CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
      CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ → CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁

Given a pullback square assembled from a commuting square on the top and a pullback square on the bottom, the top square is a pullback square. The objects in the statement fit into the following diagram: `` X₁₁ - h₁₁ -> X₁₂ | | v₁₁ v₁₂ ↓ ↓ X₂₁ - h₂₁ -> X₂₂ | | v₂₁ v₂₂ ↓ ↓ X₃₁ - h₃₁ -> X₃₂ ``

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category