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).

@[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 : { x // x ∈ 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] : { x // x ∈ NumberField.ringOfIntegers L } →* { x // x ∈ NumberField.ringOfIntegers K }

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

Equations

• One or more equations did not get rendered due to their size.

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 : { x // x ∈ NumberField.ringOfIntegers L }) : ↑(↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ 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 : { x // x ∈ NumberField.ringOfIntegers K }) : ↑(↑(RingOfIntegers.norm K) (↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ 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 : { x // x ∈ NumberField.ringOfIntegers K }) : ↑(RingOfIntegers.norm K) (↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ 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 : { x // 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 : { x // x ∈ NumberField.ringOfIntegers L }) : x ∣ ↑(algebraMap { x // x ∈ NumberField.ringOfIntegers K } { x // x ∈ 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 : { x // 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 : { x // x ∈ NumberField.ringOfIntegers F }} : IsUnit (↑(RingOfIntegers.norm K) x) ↔ IsUnit x