English
There is a natural action of L ≃ₐ[K] L on the set of primes lying over p in B, given by the rule σ • Q = primesOver.mk p (map (galRestrict A K L B) σ) Q.1. This defines a group action of AlgEquiv K L L on (p.primesOver B).Elem.
Русский
Существует естественное действие Aut(K,L) на множество primesOver, задаваемое σ • Q = primesOver.mk p (map (galRestrict A K L B) σ) Q.1.
LaTeX
$$$\\sigma \\cdot Q = \\text{primesOver.mk } p (\\mathrm{map}(\\mathrm{galRestrict}\\ A K L B \\sigma)\\; Q.1)$$$
Lean4
/-- If `p` is a maximal ideal of `A`, `P` and `Q` are prime ideals
lying over `p`, then there exists `σ ∈ Aut (B / A)` such that `σ P = Q`. In other words,
the Galois group `Gal(L / K)` acts transitively on the set of all prime ideals lying over `p`. -/
theorem exists_map_eq_of_isGalois [IsGalois K L] : ∃ σ : B ≃ₐ[A] B, map σ P = Q :=
by
have : FaithfulSMul A B := FaithfulSMul.of_field_isFractionRing A B K L
have : IsInvariant A B (B ≃ₐ[A] B) := isInvariant_of_isGalois' A K L B
rcases IsInvariant.exists_smul_of_under_eq A B (B ≃ₐ[A] B) P Q <| (over_def P p).symm.trans (over_def Q p) with
⟨σ, hs⟩
exact ⟨σ, hs.symm⟩
