Hensel's lemma for the norm

Let R be a ring Henselian at an ideal I, and S a finite free R-algebra containing a unit w whose trace is a unit of R. Then every unit v of R that is a norm modulo I is a norm: if N_{S/R}(a) ≡ v (mod I) then N_{S/R}(y) = v for some y ≡ a (mod IS).

So a norm equation over R with a unit right-hand side is solvable as soon as it is solvable modulo I, with a solution as close to the approximate one as the approximation was good. At the maximal ideal of a Henselian local ring this makes the norm surjective on units in an unramified extension of local fields, where the residue norm is surjective and the residue trace is nonzero. At a power 𝔪 ^ i of the maximal ideal of a complete local ring, applied to the approximate solution a = 1, it makes the norm surjective on the depth-i step of the unit filtration.

Main results

• TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem: a unit that is a norm modulo I is the norm of an element congruent to the approximate solution modulo IS.

References

• J.-P. Serre, Local Fields, Chapter V, §2.

theorem TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {I : Ideal R} [HenselianRing R I] {w : S} (hw : IsUnit w) (htr : IsUnit ((Algebra.trace R S) w)) {a : S} {v : R} (hv : IsUnit v) (hav : (Algebra.norm R) a - v ∈ I) : ∃ (y : S), (Algebra.norm R) y = v ∧ y - a ∈ Ideal.map (algebraMap R S) I

Hensel's lemma for the norm. Let S be a finite free algebra over a ring R Henselian at an ideal I, containing a unit w whose trace is a unit. If a unit v of R is congruent to the norm of a modulo I, then v is the norm of some y congruent to a modulo IS.