functorObj_comm — Mathlib

English

The canonical square formed by functorObjTop, functorObjLeft, ιFunctorObj, and ρFunctorObj is a pushout.

Русский

Канонический квадрат, образованный functorObjTop, functorObjLeft, ιFunctorObj и ρFunctorObj, является пушаутом.

LaTeX

$$$ IsPushout(\text{functorObjTop } f \piX, \text{functorObjLeft } f \piX, \iotaFunctorObj f \piX, \rhoFunctorObj f \piX) $$$

Lean4

@[reassoc]
theorem functorObj_comm : functorObjTop f πX ≫ ιFunctorObj f πX = functorObjLeft f πX ≫ ρFunctorObj f πX :=
  pushout.condition

Похожие утверждения