English
If L/K is a finite Galois extension and x ∈ 𝓞 L, then norm_K x is a unit in 𝓞 K if and only if x is a unit in 𝓞 L.
Русский
Если L/K — конечное Галоевское расширение и x ∈ 𝓞 L, то norm_K x единичный элемент в 𝓞 K тогда и только тогда, когда x единичный в 𝓞 L.
LaTeX
$$$[\text{FiniteDimensional } K L] \land [\text{IsGalois } K L] \Rightarrow (\operatorname{IsUnit}(\operatorname{norm}_K x) \iff \operatorname{IsUnit}(x))$$$
Lean4
theorem isUnit_norm_of_isGalois [FiniteDimensional K L] [IsGalois K L] {x : 𝓞 L} : IsUnit (norm K x) ↔ IsUnit x := by
classical
refine ⟨fun hx => ?_, IsUnit.map _⟩
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
refine
@isUnit_of_mul_isUnit_right (𝓞 L) _
⟨(univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x, prod_mem fun σ _ => x.2.map (σ : L →+* L).toIntAlgHom⟩
_ ?_
convert hx using 1
ext
convert_to ((univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x) * ∏ σ ∈ {(AlgEquiv.refl : L ≃ₐ[K] L)}, σ x = _
· rw [prod_singleton, AlgEquiv.coe_refl, _root_.id, RingOfIntegers.coe_eq_algebraMap, map_mul, RingOfIntegers.map_mk]
· rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
