English
There is a canonical bijection between algebra equivalences of L over K and K-algebra endomorphisms of L, given L is algebraic over K.
Русский
Существует каноническое биективное соответствие между алгебраическими экваленциями L над K и K-алгебраическими гомоморфизмами L в L, когда L алгебраичен над K.
LaTeX
$$$(L \equiv_{K} L) \to (L \to_{K} L)$ является биекцией (MulEquiv) через алгебраические алгебры, с toFun = функции AlgHom и invFun = AlgEquiv.ofBijective$$$
Lean4
/-- Bijection between algebra equivalences and algebra homomorphisms -/
@[simps]
noncomputable def algEquivEquivAlgHom [NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L)
where
toFun ϕ := ϕ.toAlgHom
invFun ϕ := AlgEquiv.ofBijective ϕ (algHom_bijective ϕ)
map_mul' _ _ := rfl
