English
For a domain k containing B/Q, any A ⧸ P-algebra endomorphism σ of k arises as the restriction of an endomorphism τ of B/Q over A ⧸ P, compatible with the k-structure via the natural maps.
Русский
Для области k, содержащей B/Q, любое концевое отображение σ над A ⧸ P в k ограничивается конечным отображением τ над A ⧸ P в B/Q, совместимым со структурой k через естественные отображения.
LaTeX
$$$\\exists \\tau : (B/Q) \\to_{A/P} B/Q,\\ \\forall x:\\ B/Q,\\ algebraMap_{A/P}(\\tau x) = \\sigma( algebraMap_{(B/Q)\\to k}(x)).$$$
Lean4
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`.
This is basically the fact that `L/K` normal implies `κ(Q)/κ(P)` normal in the Galois setting.
-/
theorem exists_algHom_fixedPoint_quotient_under (σ : k →ₐ[A ⧸ P] k) :
∃ τ : (B ⧸ Q) →ₐ[A ⧸ P] B ⧸ Q, ∀ x : B ⧸ Q, algebraMap _ _ (τ x) = σ (algebraMap (B ⧸ Q) k x) :=
by
let f : (B ⧸ Q) →ₐ[A ⧸ P] k := IsScalarTower.toAlgHom _ _ _
have hf : Function.Injective f := FaithfulSMul.algebraMap_injective _ _
suffices (σ.comp f).range ≤ f.range by
let e := (AlgEquiv.ofInjective f hf)
exact
⟨(e.symm.toAlgHom.comp (Subalgebra.inclusion this)).comp (σ.comp f).rangeRestrict, fun x ↦
congr_arg Subtype.val (e.apply_symm_apply ⟨_, _⟩)⟩
rintro _ ⟨x, rfl⟩
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
cases nonempty_fintype G
algebraize [(algebraMap (A ⧸ P) k).comp (algebraMap A (A ⧸ P)), (algebraMap (B ⧸ Q) k).comp (algebraMap B (B ⧸ Q))]
haveI : IsScalarTower A (B ⧸ Q) k :=
.of_algebraMap_eq fun x ↦ (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
haveI : IsScalarTower A B k := .of_algebraMap_eq fun x ↦ (IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) k (mk P x))
obtain ⟨P, hp⟩ := Algebra.IsInvariant.charpoly_mem_lifts A B G x
have : Polynomial.aeval x P = 0 := by
rw [Polynomial.aeval_def, ← Polynomial.eval_map, ← Polynomial.coe_mapRingHom (R := A), hp,
MulSemiringAction.eval_charpoly]
have : Polynomial.aeval (σ (algebraMap (B ⧸ Q) k (mk _ x))) P = 0 :=
by
refine
(DFunLike.congr_fun (Polynomial.aeval_algHom ((σ.restrictScalars A).comp (IsScalarTower.toAlgHom A (B ⧸ Q) k)) _)
P).trans
?_
rw [AlgHom.comp_apply, ← algebraMap_eq, Polynomial.aeval_algebraMap_apply, this, map_zero, map_zero]
rw [← Polynomial.aeval_map_algebraMap B, ← Polynomial.coe_mapRingHom, hp] at this
obtain ⟨τ, hτ⟩ : ∃ τ : G, σ (algebraMap _ _ x) = algebraMap _ _ (τ • x) := by
simpa [MulSemiringAction.charpoly, sub_eq_zero, Finset.prod_eq_zero_iff] using this
exact ⟨Ideal.Quotient.mk _ (τ • x), hτ.symm⟩
