Documentation

Mathlib.NumberTheory.NumberField.Norm

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 #

Main results #

source
theorem Algebra.coe_norm_int {K : Type u_1} [Field K] [NumberField K] (x : NumberField.RingOfIntegers K) :
↑((norm ℤ) x) = (norm ℚ) ↑x
source
theorem Algebra.coe_trace_int {K : Type u_1} [Field K] [NumberField K] (x : NumberField.RingOfIntegers K) :
↑((trace ℤ (NumberField.RingOfIntegers K)) x) = (trace ℚ K) ↑x
source
noncomputable def NumberField.RingOfIntegers.norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] :
RingOfIntegers L →* RingOfIntegers K

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

Equations
Instances For
    source
    @[simp]
    theorem NumberField.RingOfIntegers.coe_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : RingOfIntegers L) :
    ↑((norm K) x) = (Algebra.norm K) ↑x
    source
    theorem NumberField.RingOfIntegers.coe_algebraMap_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : RingOfIntegers L) :
    ↑((algebraMap (RingOfIntegers K) (RingOfIntegers L)) ((norm K) x)) = (algebraMap K L) ((Algebra.norm K) ↑x)
    source
    theorem NumberField.RingOfIntegers.algebraMap_norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : RingOfIntegers K) :
    (algebraMap (RingOfIntegers K) K) ((norm K) ((algebraMap (RingOfIntegers K) (RingOfIntegers L)) x)) = (Algebra.norm K) ((algebraMap K L) ((algebraMap (RingOfIntegers K) K) x))
    source
    theorem NumberField.RingOfIntegers.norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : RingOfIntegers K) :
    (norm K) ((algebraMap (RingOfIntegers K) (RingOfIntegers L)) x) = x ^ Module.finrank K L
    source
    theorem NumberField.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 : RingOfIntegers L) :
    x ∣ (algebraMap (RingOfIntegers K) (RingOfIntegers L)) ((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).

    source
    theorem NumberField.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 : RingOfIntegers L} :
    IsUnit ((norm K) x) ↔ IsUnit x
    source
    theorem NumberField.RingOfIntegers.norm_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (F : Type u_3) [Field F] [Algebra K F] [FiniteDimensional K F] [Algebra F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : RingOfIntegers L) :
    (norm K) ((norm F) x) = (norm K) x
    source
    theorem NumberField.RingOfIntegers.isUnit_norm (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra K F] [FiniteDimensional K F] [CharZero K] {x : RingOfIntegers F} :
    IsUnit ((norm K) x) ↔ IsUnit x
    source
    @[deprecated NumberField.RingOfIntegers.norm (since := "2026-11-08")]
    noncomputable def RingOfIntegers.norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] :
    NumberField.RingOfIntegers L →* NumberField.RingOfIntegers K

    Alias of NumberField.RingOfIntegers.norm.

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

    Equations
    Instances For
      source
      @[deprecated NumberField.RingOfIntegers.coe_norm (since := "2026-11-08")]
      theorem RingOfIntegers.coe_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : NumberField.RingOfIntegers L) :
      ↑((NumberField.RingOfIntegers.norm K) x) = (Algebra.norm K) ↑x

      Alias of NumberField.RingOfIntegers.coe_norm.

      source
      @[deprecated NumberField.RingOfIntegers.coe_algebraMap_norm (since := "2026-11-08")]
      theorem RingOfIntegers.coe_algebraMap_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : NumberField.RingOfIntegers L) :
      ↑((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ((NumberField.RingOfIntegers.norm K) x)) = (algebraMap K L) ((Algebra.norm K) ↑x)

      Alias of NumberField.RingOfIntegers.coe_algebraMap_norm.

      source
      @[deprecated NumberField.RingOfIntegers.algebraMap_norm_algebraMap (since := "2026-11-08")]
      theorem RingOfIntegers.algebraMap_norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : NumberField.RingOfIntegers K) :
      (algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x)) = (Algebra.norm K) ((algebraMap K L) ((algebraMap (NumberField.RingOfIntegers K) K) x))

      Alias of NumberField.RingOfIntegers.algebraMap_norm_algebraMap.

      source
      @[deprecated NumberField.RingOfIntegers.norm_algebraMap (since := "2026-11-08")]
      theorem RingOfIntegers.norm_algebraMap {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (x : NumberField.RingOfIntegers K) :
      (NumberField.RingOfIntegers.norm K) ((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) x) = x ^ Module.finrank K L

      Alias of NumberField.RingOfIntegers.norm_algebraMap.

      source
      @[deprecated NumberField.RingOfIntegers.dvd_norm (since := "2026-11-08")]
      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)) ((NumberField.RingOfIntegers.norm K) x)

      Alias of NumberField.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).

      source
      @[deprecated NumberField.RingOfIntegers.isUnit_norm_of_isGalois (since := "2026-11-08")]
      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 ((NumberField.RingOfIntegers.norm K) x) ↔ IsUnit x

      Alias of NumberField.RingOfIntegers.isUnit_norm_of_isGalois.

      source
      @[deprecated NumberField.RingOfIntegers.norm_norm (since := "2026-11-08")]
      theorem RingOfIntegers.norm_norm {L : Type u_1} (K : Type u_2) [Field K] [Field L] [Algebra K L] (F : Type u_3) [Field F] [Algebra K F] [FiniteDimensional K F] [Algebra F L] [FiniteDimensional F L] [IsScalarTower K F L] (x : NumberField.RingOfIntegers L) :
      (NumberField.RingOfIntegers.norm K) ((NumberField.RingOfIntegers.norm F) x) = (NumberField.RingOfIntegers.norm K) x

      Alias of NumberField.RingOfIntegers.norm_norm.

      source
      @[deprecated NumberField.RingOfIntegers.isUnit_norm (since := "2026-11-08")]
      theorem RingOfIntegers.isUnit_norm (K : Type u_2) [Field K] {F : Type u_3} [Field F] [Algebra K F] [FiniteDimensional K F] [CharZero K] {x : NumberField.RingOfIntegers F} :
      IsUnit ((NumberField.RingOfIntegers.norm K) x) ↔ IsUnit x

      Alias of NumberField.RingOfIntegers.isUnit_norm.