English
Let A and B be commutative rings with A ⊆ B via an algebra structure, and P ⊆ A, Q ⊆ B primes with Q lying over P. Suppose a finite group G acts on B compatibly with A. Then the natural stabilizer homomorphism from the stabilizer of Q to the automorphism group of the fraction field extension Frac(B/Q) over Frac(A/P) is surjective.
Русский
Пусть A и B - коммутативные кольца, t.ч. A ⊆ B через алгебраический отображение; P ⊆ A и Q ⊆ B - простые идеалы с Q лежит над P. Пусть конечная группа G действует на B так, чтобы это действие совместимо с A. Тогда естественный гомоморф стабилизатора из стабилизатора Q на группу автоморфизмов расширения Frac(B/Q) над Frac(A/P) является сюрьективным.
LaTeX
$$$\\operatorname{Function.Surjective} (\\operatorname{stabilizerHom} G P Q K L)$$$
Lean4
/-- The stabilizer subgroup of `Q` surjects onto `Aut(Frac(B/Q)/Frac(A/P))`. -/
theorem stabilizerHom_surjective : Function.Surjective (stabilizerHom G P Q K L) :=
by
let _ := MulSemiringAction.compHom L (stabilizerHom G P Q K L)
intro f
obtain ⟨g, hg⟩ :=
FixedPoints.toAlgAut_surjective (MulAction.stabilizer G Q) L
(AlgEquiv.ofRingEquiv (f := f) (fun x ↦ fixed_of_fixed2 G P Q K L f x x.2))
exact ⟨g, by rwa [AlgEquiv.ext_iff] at hg ⊢⟩
