NYLL
Module

GaloisNorm.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.GaloisNorm
16 declarations indexed from sourceView source ↗

Module documentation

The Galois product formula for the relative idele norm

This file proves that, in the tensor-product presentation 𝔸_L = 𝔸_K ⊗_K L, extension of the determinant norm back to 𝔸_L is the product of all Galois conjugates.

Imports4
Imported by4

Declarations

def

normPolynomial

L38 ↗
RelativeIdeleGroup.normPolynomial
Documentation

The determinant norm as a homogeneous polynomial in the coordinates of a basis. Keeping this polynomial over the ground field is what makes the Galois product formula stable under arbitrary scalar extension.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def normPolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) : MvPolynomial ι K
theorem

eval_normPolynomial

L45 ↗
RelativeIdeleGroup.eval_normPolynomial
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem eval_normPolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (x : L) :
    MvPolynomial.eval (b.repr x) (normPolynomial b) =
      Algebra.norm K x
def

conjugatePolynomial

L58 ↗
RelativeIdeleGroup.conjugatePolynomial
Documentation

The linear polynomial whose value at the coordinates of x is the σ-conjugate of x.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def conjugatePolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (σ : L ≃ₐ[K] L) :
    MvPolynomial ι L
theorem

eval_conjugatePolynomial

L66 ↗
RelativeIdeleGroup.eval_conjugatePolynomial
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem eval_conjugatePolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (σ : L ≃ₐ[K] L) (x : L) :
    MvPolynomial.eval
        (fun i ↦ algebraMap K L (b.repr x i))
        (conjugatePolynomial b σ) =
      σ x := by
  rw [conjugatePolynomial, map_sum]
  simp only [map_mul, MvPolynomial.eval_X, MvPolynomial.eval_C]
  calc
    ∑ i, algebraMap K L (b.repr x i) * σ (b i) =
        ∑ i, σ ((b.repr x i) • b i) := by
      apply Finset.sum_congr rfl
      intro i hi
      simp [Algebra.smul_def]
    _ = σ (∑ i, (b.repr x i) • b i) := by
      rw [map_sum]
    _ = σ x := by rw [b.sum_repr]
def

galoisProductPolynomial

L87 ↗
RelativeIdeleGroup.galoisProductPolynomial
Documentation

The product of the universal conjugates, written as a polynomial over the splitting field.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def galoisProductPolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) :
    MvPolynomial ι L
theorem

eval_galoisProductPolynomial

L94 ↗
RelativeIdeleGroup.eval_galoisProductPolynomial
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · full declaration
theorem eval_galoisProductPolynomial
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (x : L) :
    MvPolynomial.eval
        (fun i ↦ algebraMap K L (b.repr x i))
        (galoisProductPolynomial b) =
      ∏ σ : L ≃ₐ[K] L, σ x := by
  simp [galoisProductPolynomial]
theorem

map_normPolynomial_eq_galoisProductPolynomial

L105 ↗
RelativeIdeleGroup.map_normPolynomial_eq_galoisProductPolynomial
Documentation

The universal determinant norm polynomial becomes the product of the universal Galois conjugates after extending its coefficients to L.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem map_normPolynomial_eq_galoisProductPolynomial
    [IsGalois K L] [Infinite K]
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) :
    MvPolynomial.map (algebraMap K L) (normPolynomial b) =
      galoisProductPolynomial b
theorem

baseChangedLmul_eq

L139 ↗
RelativeIdeleGroup.baseChangedLmul_eq
Documentation

Base change carries the regular representation of L/K to the regular representation of A ⊗[K] L over A.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem baseChangedLmul_eq
    (A : Type w) [CommRing A] [Algebra K A] :
    LinearMap.tensorProduct K A L L ∘ₗ
        (Algebra.lmul K L).toLinearMap.baseChange A =
      (Algebra.lmul A (A ⊗[K] L)).toLinearMap
theorem

eval₂_normPolynomial_baseChange

L162 ↗
RelativeIdeleGroup.eval₂_normPolynomial_baseChange
Documentation

Evaluation of the universal norm polynomial after arbitrary scalar extension is the determinant norm on the scalar-extended algebra.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem eval₂_normPolynomial_baseChange
    (A : Type*) [CommRing A] [Algebra K A] [Nontrivial A]
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (z : A ⊗[K] L) :
    MvPolynomial.eval₂ (algebraMap K A)
        ((Algebra.TensorProduct.basis A b).repr z)
        (normPolynomial b) =
      Algebra.norm A z
def

scalarConjugation

L193 ↗
RelativeIdeleGroup.scalarConjugation
Documentation

Galois conjugation after scalar extension to an arbitrary commutative K-algebra.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
def scalarConjugation
    (A : Type*) [CommRing A] [Algebra K A]
    (σ : L ≃ₐ[K] L) :
    A ⊗[K] L →ₐ[A] A ⊗[K] L
theorem

scalarConjugation_tmul

L201 ↗
RelativeIdeleGroup.scalarConjugation_tmul
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem scalarConjugation_tmul
    (A : Type*) [CommRing A] [Algebra K A]
    (σ : L ≃ₐ[K] L) (a : A) (x : L) :
    scalarConjugation (K := K) (L := L) A σ (a ⊗ₜ[K] x) =
      a ⊗ₜ[K] σ x
theorem

eval₂_conjugatePolynomial_baseChange

L211 ↗
RelativeIdeleGroup.eval₂_conjugatePolynomial_baseChange
Documentation

Evaluating a universal conjugate polynomial at the coordinates of a base-changed element gives its actual scalar-extended conjugate.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem eval₂_conjugatePolynomial_baseChange
    (A : Type*) [CommRing A] [Algebra K A]
    {ι : Type w} [Fintype ι] [DecidableEq ι]
    (b : Module.Basis ι K L) (σ : L ≃ₐ[K] L)
    (z : A ⊗[K] L) :
    MvPolynomial.eval₂
        ((Algebra.TensorProduct.includeRight
          (R := K) (A := A) (B := L)).toRingHom)
        (fun i ↦ (Algebra.TensorProduct.includeLeft
          (R := K) (S := K) (A := A) (B := L))
          ((Algebra.TensorProduct.basis A b).repr z i))
        (conjugatePolynomial b σ) =
      scalarConjugation (K := K) (L := L) A σ z := by
  simp only [conjugatePolynomial, MvPolynomial.eval₂_sum,
    MvPolynomial.eval₂_mul, MvPolynomial.eval₂_X,
    MvPolynomial.eval₂_C]
  calc
    ∑ i, (Algebra.TensorProduct.includeLeft
          (R := K) (S := K) (A := A) (B := L))
          ((Algebra.TensorProduct.basis A b).repr z i) *
        (Algebra.TensorProduct.includeRight
          (R := K) (A := A) (B := L)) (σ (b i)) =
        ∑ i, scalarConjugation (K := K) (L := L) A σ
          (((Algebra.TensorProduct.basis A b).repr z i) •
            Algebra.TensorProduct.basis A b i) := by
      apply Finset.sum_congr rfl
      intro i hi
      simp [scalarConjugation, Algebra.TensorProduct.basis_apply,
        Algebra.TensorProduct.tmul_mul_tmul,
        Algebra.smul_def]
    _ = scalarConjugation (K := K) (L := L) A σ
          (∑ i, ((Algebra.TensorProduct.basis A b).repr z i) •
            Algebra.TensorProduct.basis A b i) := by
      rw [map_sum]
    _ = scalarConjugation (K := K) (L := L) A σ z := by
      rw [(Algebra.TensorProduct.basis A b).sum_repr]
theorem

includeLeft_norm_eq_prod_scalarConjugations

L251 ↗
RelativeIdeleGroup.includeLeft_norm_eq_prod_scalarConjugations
Documentation

The full scalar-extension formula: extending the determinant norm back to a Galois algebra is the product of all Galois conjugates. The coefficient algebra A is arbitrary.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem includeLeft_norm_eq_prod_scalarConjugations
    [IsGalois K L] [Infinite K]
    (A : Type*) [CommRing A] [Algebra K A] [Nontrivial A]
    (z : A ⊗[K] L) :
    (Algebra.TensorProduct.includeLeft
      (R := K) (S := K) (A := A) (B := L))
        (Algebra.norm A z) =
      ∏ σ : L ≃ₐ[K] L,
        scalarConjugation (K := K) (L := L) A σ z
theorem

scalarConjugation_baseAdele_apply

L303 ↗
RelativeIdeleGroup.scalarConjugation_baseAdele_apply
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem scalarConjugation_baseAdele_apply
    [NumberField K]
    (σ : L ≃ₐ[K] L) (z : RelativeAdeleRing K L) :
    scalarConjugation
        (NumberField.AdeleRing (𝓞 K) K) σ z =
      conjugation K L σ z
theorem

adeleInclusion_norm_eq_prod_conjugates

L314 ↗
RelativeIdeleGroup.adeleInclusion_norm_eq_prod_conjugates
Documentation

In full adèle form, the base extension of the determinant norm of an arbitrary relative adèle is the product of all of its Galois conjugates.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem adeleInclusion_norm_eq_prod_conjugates
    [NumberField K] [IsGalois K L]
    (z : RelativeAdeleRing K L) :
    adeleInclusion K L
        (Algebra.norm
          (NumberField.AdeleRing (𝓞 K) K) z) =
      ∏ σ : L ≃ₐ[K] L, conjugation K L σ z
theorem

inclusion_norm_eq_prod_conjugates

L336 ↗
RelativeIdeleGroup.inclusion_norm_eq_prod_conjugates
Documentation

In full idèle form, i_{L/K}(N_{L/K}(a)) = ∏_{σ ∈ Gal(L/K)} σ(a) for every relative idèle a.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped BigOperators TensorProduct
open NumberField
noncomputable section
namespace RelativeIdeleGroup
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem inclusion_norm_eq_prod_conjugates
    [NumberField K] [IsGalois K L]
    (a : RelativeIdeleGroup K L) :
    inclusion K L (norm K L a) =
      ∏ σ : L ≃ₐ[K] L, σ • a

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.