English
In the quotient setting, the stabilizer of Q surjects onto the automorphism group of the fraction field extension (Frac(B/Q))/(Frac(A/P)).
Русский
В фактор-сценарии стабилизатор Q сюрьективно проецируется на группу автоморфизмов расширения полей Frac(B/Q) над Frac(A/P).
LaTeX
$$$\\operatorname{Function.Surjective} (\\operatorname{Ideal.Quotient.stabilizerHom Q P G)$$$
Lean4
/-- The stabilizer subgroup of `Q` surjects onto `Aut((B/Q)/(A/P))`. -/
theorem stabilizerHom_surjective : Function.Surjective (Ideal.Quotient.stabilizerHom Q P G) :=
by
have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q
let _ := FractionRing.liftAlgebra (A ⧸ P) (FractionRing (B ⧸ Q))
have key := IsFractionRing.stabilizerHom_surjective G P Q (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q))
rw [IsFractionRing.stabilizerHom, MonoidHom.coe_comp] at key
exact
key.of_comp_left
(IsFractionRing.fieldEquivOfAlgEquivHom_injective (A ⧸ P) (B ⧸ Q) (FractionRing (A ⧸ P)) (FractionRing (B ⧸ Q)))
