inr_iso_hom

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

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

English

If F preserves the pushout of f,g, it also preserves the pushout of g,f.

Русский

Если F сохраняет пуш-аут для f,g, тогда она сохраняет пуш-аут для g,f.

LaTeX

$$$PreservesColimit( span g f) G)$$$

Lean4

@[reassoc]
theorem inr_iso_hom : pushout.inr _ _ ≫ (PreservesPushout.iso G f g).hom = G.map (pushout.inr _ _) := by simp

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

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

Разделы

Аффилиация

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