English
The units of the algebra endomorphism monoid of S over R are in natural bijection with the algebra automorphisms of S over R.
Русский
Единицы моноида алгебраических эндоморфизмов S над R естественно эквивалентны алгебраическим автоморфизмам S над R.
LaTeX
$$$ (\\mathrm{Units}(\\mathrm{AlgHom}\\, R\\, S\\, S)) \\ \\cong\\ \\mathrm{AlgEquiv}(R\\, S\\, S). $$$
Lean4
/-- The units group of `S →ₐ[R] S` is `S ≃ₐ[R] S`.
See `LinearMap.GeneralLinearGroup.generalLinearEquiv` for the linear map version. -/
@[simps]
def algHomUnitsEquiv (R S : Type*) [CommSemiring R] [Semiring S] [Algebra R S] : (S →ₐ[R] S)ˣ ≃* (S ≃ₐ[R] S)
where
toFun := fun f ↦
{ (f : S →ₐ[R] S) with
invFun := ↑(f⁻¹)
left_inv := (fun x ↦ show (↑(f⁻¹ * f) : S →ₐ[R] S) x = x by rw [inv_mul_cancel]; rfl)
right_inv := (fun x ↦ show (↑(f * f⁻¹) : S →ₐ[R] S) x = x by rw [mul_inv_cancel]; rfl) }
invFun := fun f ↦ ⟨f, f.symm, f.comp_symm, f.symm_comp⟩
map_mul' := fun _ _ ↦ rfl
