equivToUnitHom — Mathlib

English

There is a natural equivalence between MulChar R R' and MonoidHom(Units R, Units R').

Русский

Существует естественное эквивалентность между MulChar R R' и MonoidHom(Units R, Units R').

LaTeX

$$$\text{MulChar}(R,R') \simeq (R^{\times} \to* (R')^{\times}).$$$

Lean4

/-- The equivalence between multiplicative characters and homomorphisms of unit groups. -/
noncomputable def equivToUnitHom : MulChar R R' ≃ (Rˣ →* R'ˣ)
    where
  toFun := toUnitHom
  invFun := ofUnitHom
  left_inv := by
    intro χ
    ext x
    rw [ofUnitHom_coe, coe_toUnitHom]
  right_inv := by
    intro f
    ext x
    simp only [coe_toUnitHom, ofUnitHom_coe]

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