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

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 = NumberField.RingOfIntegers.restrict_monoidHom ((Algebra.norm K).comp ↑(algebraMap (NumberField.RingOfIntegers L) L)) ⋯

@[simp]

theorem RingOfIntegers.coe_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) : ↑((RingOfIntegers.norm K) x) = (Algebra.norm K) ↑x

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.algebraMap_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) : (algebraMap (NumberField.RingOfIntegers K) K) ((RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x)) = (Algebra.norm K) ((algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) 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