The zero extension of an inverse unit character #
MulChar.ofUnitHom extends a unit homomorphism χ : Rˣ →* R'ˣ by zero to a multiplicative
character. It carries the inverse of χ to the inverse character, and for complex values, where
the inverse of a character of finite order is its complex conjugate (MulChar.star_eq_inv), to
the conjugate character.
Main results #
MulChar.ofUnitHom_inv:ofUnitHom χ⁻¹ = (ofUnitHom χ)⁻¹.MulChar.ofUnitHom_inv_eq_star: for complex values,ofUnitHom χ⁻¹ = star (ofUnitHom χ).
theorem
MulChar.ofUnitHom_inv
{R : Type u_1}
{R' : Type u_2}
[CommMonoid R]
[CommMonoidWithZero R']
(χ : Rˣ →* R'ˣ)
:
The zero extension of the inverse of a unit homomorphism is the inverse character.