English
Under NoZeroSMulDivisors and algebraicity of L over K, every K-algebra endomorphism of L is bijective.
Русский
При отсутствии нулевых делителей и алгебраичности L над K, вся K-алгебраическая эндоморфизм L в L биективен.
LaTeX
$$$[\mathrm{NoZeroSMulDivisors\ K\ L}] [\mathrm{Algebra.IsAlgebraic\ K\ L}] (f : L \to_{K} L) : \mathrm{Function.Bijective}\ f$$$
Lean4
theorem algHom_bijective [NoZeroSMulDivisors K L] [Algebra.IsAlgebraic K L] (f : L →ₐ[K] L) : Function.Bijective f :=
by
refine ⟨f.injective, fun b ↦ ?_⟩
obtain ⟨p, hp, he⟩ := Algebra.IsAlgebraic.isAlgebraic (R := K) b
let f' : p.rootSet L → p.rootSet L := (rootSet_maps_to' (fun x ↦ x) f).restrict f _ _
have : f'.Surjective := Finite.injective_iff_surjective.1 fun _ _ h ↦ Subtype.eq <| f.injective <| Subtype.ext_iff.1 h
obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩
exact ⟨a, Subtype.ext_iff.1 ha⟩
