con — Mathlib

English

The pushout construction glues together multiple monoids using a family of homomorphisms to form a universal pushout in the category of monoids (equivalently, in groups).

Русский

Конструкция пушаут объединяет множество монойдов по заданной системе гомоморфизмов, образуя универсальный пушаут в категории монойдов (а значит и в группах).

LaTeX

$$con : (φ i) → Con (Coprod (CoprodI G) H)$$

Lean4

/-- The relation we quotient by to form the pushout -/
def con [∀ i, Monoid (G i)] [Monoid H] (φ : ∀ i, H →* G i) : Con (Coprod (CoprodI G) H) :=
  conGen (fun x y : Coprod (CoprodI G) H => ∃ i x', x = inl (of (φ i x')) ∧ y = inr x')

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