mapValueGroupWithZero — Mathlib

English

The map on value groups with zero associated to a structure morphism is a monoid-with-zero homomorphism.

Русский

Отображение значений с нулём, связанное с морфизмом структуры, является гомоморфизмом моноида с нулём.

LaTeX

$$$\\text{mapValueGroupWithZero} : \\mathrm{ValueGroupWithZero} A \\to \\mathrm{ValueGroupWithZero} B \\\\text{is a } (\\text{MonoidWithZeroHom})$$$

Lean4

/-- The map on value groups-with-zero associated to the structure morphism of an algebra. -/
def mapValueGroupWithZero : ValueGroupWithZero A →*₀ ValueGroupWithZero B :=
  have := compatible_comap A (valuation B)
  ValueGroupWithZero.embed ((valuation B).comap (algebraMap A B))

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