English
The action of G on the primes of B above a prime of A is transitive when G is finite.
Русский
Действие G на простые идеалы B над простым A транзитивно при конечности G.
LaTeX
$$$\exists g: G, Q=g\cdot P$ whenever $P$ and $Q$ lie over the same prime of A.$$
Lean4
/-- `G` acts transitively on the prime ideals of `B` above a given prime ideal of `A`. -/
theorem exists_smul_of_under_eq [Finite G] [SMulCommClass G A B] (P Q : Ideal B) [hP : P.IsPrime] [hQ : Q.IsPrime]
(hPQ : P.under A = Q.under A) : ∃ g : G, Q = g • P :=
by
cases nonempty_fintype G
have : ∀ (P Q : Ideal B) [P.IsPrime] [Q.IsPrime], P.under A = Q.under A → ∃ g ∈ (⊤ : Finset G), Q ≤ g • P :=
by
intro P Q hP hQ hPQ
rw [← Ideal.subset_union_prime 1 1 (fun _ _ _ _ ↦ hP.smul _)]
intro b hb
suffices h : ∃ g ∈ Finset.univ, g • b ∈ P by
obtain ⟨g, -, hg⟩ := h
apply Set.mem_biUnion (Finset.mem_univ g⁻¹) (Ideal.mem_inv_pointwise_smul_iff.mpr hg)
obtain ⟨a, ha⟩ := isInvariant (A := A) (∏ g : G, g • b) (Finset.smul_prod_perm b)
rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A, hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]
exact ⟨1, Finset.mem_univ 1, (one_smul G b).symm ▸ hb⟩
obtain ⟨g, -, hg⟩ := this P Q hPQ
obtain ⟨g', -, hg'⟩ := this Q (g • P) ((P.under_smul A g).trans hPQ).symm
exact ⟨g, le_antisymm hg (smul_eq_of_le_smul (hg.trans hg') ▸ hg')⟩
