hasPushout_of_right_factors_epi

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasPushout_of_right_factors_epi

English

If h: W → X is epi and HasPushout f g holds, then HasPushout (h ≫ f) (h ≫ g).

Русский

Если h: W → X эпиморфизм и существует Pushout f g, то HasPushout (h ∘ f) (h ∘ g).

LaTeX

$$$\\text{HasPushout }(h\\circ f)(h\\circ g)$$$

Lean4

instance hasPushout_of_right_factors_epi : HasPushout h (h ≫ f) := by
  simpa only [Category.comp_id] using hasPushout_of_epi_comp (𝟙 X) f h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru