English
If P and Q are maximal primes and A ⧸ P ⊆ B ⧸ Q is invariant under G, then the extension is normal.
Русский
Если P и Q — максимальные primes и A ⧸ P ⊆ B ⧸ Q инвариантны относительно G, то расширение нормальное.
LaTeX
$$$\\text{Normal} (A / P) (B / Q).$$$
Lean4
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`. -/
theorem normal [P.IsMaximal] [Q.IsMaximal] : Normal (A ⧸ P) (B ⧸ Q) :=
by
cases subsingleton_or_nontrivial B
· cases ‹Q.IsMaximal›.ne_top (Subsingleton.elim _ _)
have := Algebra.IsInvariant.isIntegral A B G
constructor
intro x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
cases nonempty_fintype G
obtain ⟨p, hp, h₁, h₂⟩ :=
Polynomial.lifts_and_degree_eq_and_monic (Algebra.IsInvariant.charpoly_mem_lifts A B G x)
(MulSemiringAction.monic_charpoly _ _)
have H : Polynomial.aeval x p = 0 := by
rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
have :=
minpoly.dvd _ (algebraMap _ (B ⧸ Q) x) (p := p.map (algebraMap _ (A ⧸ P)))
(by rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero])
refine Polynomial.splits_of_splits_of_dvd (algebraMap (A ⧸ P) (B ⧸ Q)) ?_ ?_ this
· exact (h₂.map (algebraMap A (A ⧸ P))).ne_zero
· rw [Polynomial.splits_map_iff, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B, ←
Polynomial.splits_map_iff, hp, MulSemiringAction.charpoly_eq]
exact Polynomial.splits_prod _ (fun _ _ ↦ Polynomial.splits_X_sub_C _)
