English
The map toAlgAut G (FixedPoints.subfield G F) F is bijective when G is finite and acts faithfully on F.
Русский
Отображение toAlgAut для G и FixedPoints.subfield G F биективно, если G конечно и действовать на F верно.
LaTeX
$$$\\text{toAlgAut}_\\text{Mul} G (\\operatorname{FixedPoints.subfield } G F) F\\ \\text{ is bijective}$$$
Lean4
/-- `MulSemiringAction.toAlgAut` is bijective. -/
theorem toAlgAut_bijective [Finite G] [FaithfulSMul G F] :
Function.Bijective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F) := by
refine
⟨fun _ _ h ↦ (FixedPoints.toAlgHom_bijective G F).injective ?_, fun f ↦
((FixedPoints.toAlgHom_bijective G F).surjective f).imp (fun _ h ↦ ?_)⟩ <;>
rwa [DFunLike.ext_iff] at h ⊢
