English
In a Galois situation, the product over all L/K-automorphisms of galRestrict applied to x equals the image in A→B of a canonical integral-normal form built from the norm of x.
Русский
В гауссовой ситуации произведение по всем автоматическим отображениям L над K от galRestrict применяемому к x равняется образу в A→B от канонической интеграл-нормальной формы, построенной из нормы x.
LaTeX
$$$\\prod_{\\sigma \\in \\mathrm{Aut}_K(L)} \\mathrm{galRestrict}\\,A K L B\\ \\sigma(x) = \\mathrm{algebraMap}_{A B}\\bigl(\\mathrm{IsIntegralClosure.mk'}(A, A)\\bigl(\\mathrm{Algebra.norm}_K(\\mathrm{algebraMap}_{B L}(x))\\bigr)\\bigr)$$$
Lean4
theorem prod_galRestrict_eq_norm [IsGalois K L] [IsIntegrallyClosed A] (x : B) :
(∏ σ : L ≃ₐ[K] L, galRestrict A K L B σ x) =
algebraMap A B
(IsIntegralClosure.mk' (R := A) A (Algebra.norm K <| algebraMap B L x)
(Algebra.isIntegral_norm K (IsIntegralClosure.isIntegral A L x).algebraMap)) :=
by
apply IsIntegralClosure.algebraMap_injective B A L
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq A K L]
simp only [map_prod, algebraMap_galRestrict_apply, IsIntegralClosure.algebraMap_mk',
Algebra.norm_eq_prod_automorphisms, RingHom.coe_comp, Function.comp_apply]
