algEquivEquivAlgHom — Mathlib

English

There is a natural multiplicative equivalence between the group of algebra equivalences L ≃ₐ[K] L and the monoid of algebra homomorphisms L →ₐ[K] L, when L is finite-dimensional over K.

Русский

Существуют естественные биекция между группой алгебраических эквивалентностей L ≃ₐ[K] L и моноидом алгебраических гомоморфизмов L →ₐ[K] L, когда L конечномерно над K.

LaTeX

$$$(L \simeqₐ[K] L) \;\simeq_*\; (L \toₐ[K] L)$$$

Lean4

/-- Bijection between algebra equivalences and algebra homomorphisms -/
noncomputable abbrev algEquivEquivAlgHom [FiniteDimensional K L] : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) :=
  Algebra.IsAlgebraic.algEquivEquivAlgHom K L

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