llp_isStableUnderCobaseChange — Mathlib

English

LLP is stable under cobase change: if i is left map with LLP and g' is a pushout along i, then the pushout map has LLP.

Русский

LLP сохраняется при cobase change: если стрелка слева имеет LLP и проводится пуш-аута по этой стрелке, то правая стрелка после пуш-аута имеет LLP.

LaTeX

$$$T.llp.IsStableUnderCobaseChange$$$

Lean4

instance llp_isStableUnderCobaseChange : T.llp.IsStableUnderCobaseChange where
  of_isPushout h hf _ _ g'
    hg' :=
    letI := hf _ hg'
    h.hasLiftingProperty g'

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