pullback_symmetry_hom_of_epi_eq

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

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

English

The same symmetry result: the hom component of pushout symmetry equals identity when epi f.

Русский

Та же симметрия: гом-часть симметрии пушпоута равна тождественному отображению при epi f.

LaTeX

$$$(\\text{pushoutSymmetry } f f).hom = \\mathrm{id}$$$

Lean4

@[simp]
theorem pullback_symmetry_hom_of_epi_eq : (pushoutSymmetry f f).hom = 𝟙 _ := by ext <;> simp [inl_eq_inr_of_epi_eq]

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

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

Разделы

Аффилиация

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