English
Over a commutative base ring with smooth multiplication, units Equiv Aut enumerates Rˣ as CL equivalences R ≃L[R] R.
Русский
При основе кольца R с непрерывным умножением единицы Rˣ эквивалентны непрерывно-линейные эквивалентности R ≃L[R] R.
LaTeX
$$$R^{\\times} \\simeq Aut_{CL}(R)$$$
Lean4
/-- Continuous linear equivalences `R ≃L[R] R` are enumerated by `Rˣ`. -/
def unitsEquivAut : Rˣ ≃ R ≃L[R] R
where
toFun
u :=
equivOfInverse (ContinuousLinearMap.smulRight (1 : R →L[R] R) ↑u)
(ContinuousLinearMap.smulRight (1 : R →L[R] R) ↑u⁻¹) (fun x => by simp) fun x => by simp
invFun
e :=
⟨e 1, e.symm 1, by rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, symm_apply_apply], by
rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]⟩
left_inv u := Units.ext <| by simp
right_inv e := ext₁ <| by simp
