The absolute ideal norm under a ring isomorphism, and congruences of norms

Identifying two rings along an isomorphism identifies their ideals, and the absolute norm is insensitive to that identification.

In a Dedekind domain that is free of finite rank over ℤ, congruent elements whose norms have nonnegative product generate principal ideals with congruent absolute norms.

Main results

• Ideal.absNorm_comap_of_ringEquiv, Ideal.absNorm_map_of_ringEquiv: the absolute norm of an ideal is unchanged by transporting it along a ring isomorphism, in either direction.
• Ideal.natCast_absNorm_span_singleton_eq_of_sub_mem: congruent elements whose norms have nonnegative product generate ideals with absolute norms congruent modulo m.

@[simp]

theorem Ideal.absNorm_comap_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsDedekindDomain R] [IsDedekindDomain R'] [Infinite R] [Infinite R'] (e : R ≃+* R') (I : Ideal R') : absNorm (comap e I) = absNorm I

The absolute norm is invariant under transporting an ideal backwards along an isomorphism of Dedekind domains. Use this to move a norm computation to whichever of two identified rings it is easier to carry out in.

@[simp]

theorem Ideal.absNorm_map_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsDedekindDomain R] [IsDedekindDomain R'] [Infinite R] [Infinite R'] (e : R ≃+* R') (I : Ideal R) : absNorm (map e I) = absNorm I

The absolute norm is invariant under transporting an ideal forwards along an isomorphism of Dedekind domains. This is the form to use when the ideal is given on the source side.

theorem Ideal.natCast_absNorm_span_singleton_eq_of_sub_mem {S : Type u_1} [CommRing S] [Module.Free ℤ S] [Module.Finite ℤ S] [IsDedekindDomain S] [Infinite S] {m : ℕ} {a b : S} (hab : 0 ≤ (Algebra.norm ℤ) a * (Algebra.norm ℤ) b) (h : a - b ∈ span {↑m}) : ↑(absNorm (span {a})) = ↑(absNorm (span {b}))

Congruent elements with norms of nonnegative product generate ideals of congruent norms. If a ≡ b modulo the ideal (m) of a Dedekind domain S that is free of finite rank over ℤ, and N(a) N(b) ≥ 0, then the absolute norms of (a) and (b) are congruent modulo m.