The norm modulo an ideal #
Let S be a finite free R-algebra and I an ideal of R. The norm of S ⧸ IS over R ⧸ I
of the class of x is the class of the norm of x. This is the norm counterpart of Mathlib's
Algebra.trace_quotient_mk. It lets a norm equation over R be solved first over the quotient:
taking I to be the maximal ideal of a local ring, it supplies the residual norm input for lifting
norm equations with Hensel's lemma (TauCeti.Algebra.exists_norm_eq_of_norm_sub_mem).
Main results #
TauCeti.Algebra.norm_quotient_mk: the norm ofS ⧸ ISoverR ⧸ Iof the class ofxis the class of the norm ofx.
@[simp]
theorem
TauCeti.Algebra.norm_quotient_mk
{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)
(x : S)
:
(Algebra.norm (R ⧸ I)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) x) = (Ideal.Quotient.mk I) ((Algebra.norm R) x)
The norm commutes with reduction modulo an ideal. For a finite free algebra S over R
and an ideal I of R, the norm of S ⧸ IS over R ⧸ I of the class of x is the class of the
norm of x.