Theorems · Inductive type · category theory

CategoryTheory.IsPushout

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

The proposition that a square `` Z f > X | | g inl | | v v Y --inr--> P `` is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)

Defined in

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

Cited by

219 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category