Theorems · Inductive type · category theory

CategoryTheory.IsPullback

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {P X Y Z : C} → (P ⟶ X) → (P ⟶ Y) → (X ⟶ Z) → (Y ⟶ Z) → Prop

The proposition that a square `` P --fst--> X | | snd f | | v v Y g > Z `` is a pullback square. (Also known as a fibered product or Cartesian square.)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Cited by

320 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 7 definitions · uses no axioms

Assumes

CategoryTheory.Category