base

Mathlib.GroupTheory.PushoutI

URI: https://scilib.ai/kg/mathlib#Monoid.PushoutI.base

English

There is a canonical monoid homomorphism base φ: H → PushoutI φ, giving the pushout its base from the base monoid.

Русский

Существует канонический моноид-гомоморфизм base φ: H → PushoutI φ, задающий базу пушота.

LaTeX

$$$base\;\varphi : H \to^* PushoutI(\varphi)$$$

Lean4

/-- The map from the base monoid into the pushout -/
def base : H →* PushoutI φ :=
  (Con.mk' _).comp inr

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

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

Разделы

Аффилиация

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