Norm in number fields

Given a finite extension of number fields, we define the norm morphism as a function between the rings of integers.

Main definitions

• RingOfIntegers.norm K : Algebra.norm as a morphism (𝓞 L) →* (𝓞 K).

Main results

• RingOfIntegers.dvd_norm : if L/K is a finite Galois extension of fields, then, for all (x : 𝓞 L) we have that x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x).

theorem Algebra.coe_norm_int {K : Type u_1} [Field K] [NumberField K] (x : ↥(NumberField.ringOfIntegers K)) : ↑((Algebra.norm ℤ) x) = (Algebra.norm ℚ) ↑x

theorem Algebra.coe_trace_int {K : Type u_1} [Field K] [NumberField K] (x : ↥(NumberField.ringOfIntegers K)) : ↑((Algebra.trace ℤ ↥(NumberField.ringOfIntegers K)) x) = (Algebra.trace ℚ K) ↑x

@[simp]

theorem RingOfIntegers.norm_apply_coe {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] (n : ↥(NumberField.ringOfIntegers L)) : ↑((RingOfIntegers.norm K) n) = (Algebra.norm K) ↑n

noncomputable def RingOfIntegers.norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] : ↥(NumberField.ringOfIntegers L) →* ↥(NumberField.ringOfIntegers K)

Algebra.norm as a morphism betwen the rings of integers.

Equations

• RingOfIntegers.norm K = MonoidHom.codRestrict (MonoidHom.restrict (Algebra.norm K) (NumberField.ringOfIntegers L)) (NumberField.ringOfIntegers K) ⋯

theorem RingOfIntegers.coe_algebraMap_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] (x : ↥(NumberField.ringOfIntegers L)) : ↑((algebraMap ↥(NumberField.ringOfIntegers K) ↥(NumberField.ringOfIntegers L)) ((RingOfIntegers.norm K) x)) = (algebraMap K L) ((Algebra.norm K) ↑x)

theorem RingOfIntegers.coe_norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] (x : ↥(NumberField.ringOfIntegers K)) : ↑((RingOfIntegers.norm K) ((algebraMap ↥(NumberField.ringOfIntegers K) ↥(NumberField.ringOfIntegers L)) x)) = (Algebra.norm K) ((algebraMap K L) ↑x)

theorem RingOfIntegers.norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsSeparable K L] (x : ↥(NumberField.ringOfIntegers K)) : (RingOfIntegers.norm K) ((algebraMap ↥(NumberField.ringOfIntegers K) ↥(NumberField.ringOfIntegers L)) x) = x ^ FiniteDimensional.finrank K L

theorem RingOfIntegers.isUnit_norm_of_isGalois {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] {x : ↥(NumberField.ringOfIntegers L)} : IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x

theorem RingOfIntegers.dvd_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (x : ↥(NumberField.ringOfIntegers L)) : x ∣ (algebraMap ↥(NumberField.ringOfIntegers K) ↥(NumberField.ringOfIntegers L)) ((RingOfIntegers.norm K) x)

If L/K is a finite Galois extension of fields, then, for all (x : 𝓞 L) we have that x ∣ algebraMap (𝓞 K) (𝓞 L) (norm K x).

theorem RingOfIntegers.norm_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (F : Type u_3) [Field F] [Algebra K F] [IsSeparable K F] [FiniteDimensional K F] [IsSeparable K L] [Algebra F L] [IsSeparable F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : ↥(NumberField.ringOfIntegers L)) : (RingOfIntegers.norm K) ((RingOfIntegers.norm F) x) = (RingOfIntegers.norm K) x

theorem RingOfIntegers.isUnit_norm (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra K F] [IsSeparable K F] [FiniteDimensional K F] [CharZero K] {x : ↥(NumberField.ringOfIntegers F)} : IsUnit ((RingOfIntegers.norm K) x) ↔ IsUnit x