English
Let pb be a PowerBasis K L and assume the minimal polynomial of pb.gen splits over an algebraically closed E, pb.gen is separable over K, and L is finite-dimensional over K. Then the product over all embeddings σ: F → E of σ(algebraMap L F pb.gen) equals the [L:F]-th power of the product over embeddings σ: L → E of σ(pb.gen).
Русский
Пусть pb задаёт базис мощности K в L, предположим что minpoly_K(pb.gen) распадается в E, pb.gen разделим над K, и [L:K] конечно. Тогда произведение по всем вложениям σ: F→E от σ(algebraMap_L^F(pb.gen)) равно {[L:F]}-й степени произведения σ(pb.gen) по всем σ: L→E.
LaTeX
$$$ \\prod_{\\sigma : F \\to_{K} E} \\sigma(\\mathrm{algebraMap}_{L F}(pb.gen)) = \\left( \\prod_{\\sigma : L \\to_{K} E} \\sigma(pb.gen) \\right)^{\\mathrm{finrank} \\, L \\, F} $$$
Lean4
theorem prod_embeddings_eq_finrank_pow [Algebra L F] [IsScalarTower K L F] [IsAlgClosed E] [Algebra.IsSeparable K F]
[FiniteDimensional K F] (pb : PowerBasis K L) :
∏ σ : F →ₐ[K] E, σ (algebraMap L F pb.gen) =
((@Finset.univ _ (PowerBasis.AlgHom.fintype pb)).prod fun σ : L →ₐ[K] E => σ pb.gen) ^ finrank L F :=
by
haveI : FiniteDimensional L F := FiniteDimensional.right K L F
haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
letI : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen, ← Finset.univ_sigma_univ,
Finset.prod_sigma, ← Finset.prod_pow]
· refine Finset.prod_congr rfl fun σ _ => ?_
letI : Algebra L E := σ.toRingHom.toAlgebra
simp_rw [Finset.prod_const]
congr
exact AlgHom.card L F E
· intro σ
simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply, IsScalarTower.coe_toAlgHom']
