English
There is a monoid homomorphism from the set of all functions α → M into Germ_l M, sending a function to its germ, i.e., a canonical lifting of functions to germs that preserves multiplication and identity.
Русский
Существует моноид-гомоморфизм от множества функций α → M в Germ_l M, отправляющий функцию в её жерм, т.е. каноническое цилиндровое поднятие функций до жермов, сохраняющее умножение и единицу.
LaTeX
$$$[Monoid\\ M] \\to (\\alpha \\to M) \\to* \\mathrm{Germ}_l M$, with $toFun$ being the embedding and $map\\_1$, $map\\_mul$ preserving 1 and multiplication.$$
Lean4
/-- Coercion from functions to germs as a monoid homomorphism. -/
@[to_additive /-- Coercion from functions to germs as an additive monoid homomorphism. -/
]
def coeMulHom [Monoid M] (l : Filter α) : (α → M) →* Germ l M where toFun := ofFun; map_one' := rfl; map_mul' _ _ := rfl
