NYLL
Module

BaseChange.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Extension.BaseChange
31 declarations indexed from sourceView source β†—

Module documentation

Ideles in finite extensions: the tensor-product model

This file uses the canonical presentation 𝔸_L = 𝔸_K βŠ—_K L. This makes extension, Galois conjugation, and the idele norm formal linear-algebra operations.

Imports7
Imported by4

Declarations

abbrev

RelativeAdeleRing

L36 β†—
Documentation

The adele algebra of L, written in base-change form 𝔸_K βŠ—_K L.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
abbrev RelativeAdeleRing
abbrev

RelativeIdeleGroup

L40 β†—
Documentation

The idele group of the base-changed adele algebra.

Source context 4 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
abbrev RelativeIdeleGroup
instance

baseAdeleRingNontrivial

L45 β†—
RelativeIdeleGroup.baseAdeleRingNontrivial
Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
instance baseAdeleRingNontrivial :
    Nontrivial (NumberField.AdeleRing (π“ž K) K)
def

adeleInclusion

L52 β†—
RelativeIdeleGroup.adeleInclusion
Documentation

The base-adele algebra map into its scalar extension.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def adeleInclusion :
    NumberField.AdeleRing (π“ž K) K β†’+*
      RelativeAdeleRing K L
def

fieldInclusion

L60 β†—
RelativeIdeleGroup.fieldInclusion
Documentation

The extension field embedded in the scalar-extended adele algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def fieldInclusion :
    L β†’+* RelativeAdeleRing K L
def

inclusion

L67 β†—
RelativeIdeleGroup.inclusion
Documentation

The canonical inclusion I_K β†’ I_L in the tensor-product model.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def inclusion :
    IdeleGroup K β†’* RelativeIdeleGroup K L
theorem

inclusion_injective

L73 β†—
RelativeIdeleGroup.inclusion_injective
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem inclusion_injective :
    Function.Injective (inclusion K L)
def

principalIdele

L84 β†—
RelativeIdeleGroup.principalIdele
Documentation

The diagonal copy of LΛ£ inside the relative idele group.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def principalIdele :
    LΛ£ β†’* RelativeIdeleGroup K L
theorem

inclusion_principalIdele

L90 β†—
RelativeIdeleGroup.inclusion_principalIdele
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem inclusion_principalIdele
    (x : KΛ£) :
    inclusion K L (IdeleGroup.principalIdele K x) =
      principalIdele K L
        (Units.map (algebraMap K L) x)
def

norm

L110 β†—
RelativeIdeleGroup.norm
Documentation

The norm of relative ideles, obtained as the determinant over the base adele ring.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def norm :
    RelativeIdeleGroup K L β†’* IdeleGroup K
theorem

norm_inclusion

L119 β†—
RelativeIdeleGroup.norm_inclusion
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem norm_inclusion (a : IdeleGroup K) :
    norm K L (inclusion K L a) =
      a ^ Module.finrank K L
theorem

norm_fieldInclusion

L143 β†—
RelativeIdeleGroup.norm_fieldInclusion
Documentation

Norm commutes with scalar extension from K to the base adele ring.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem norm_fieldInclusion (x : L) :
    Algebra.norm (NumberField.AdeleRing (π“ž K) K)
        (fieldInclusion K L x) =
      algebraMap K (NumberField.AdeleRing (π“ž K) K)
        (Algebra.norm K x)
theorem

norm_principalIdele

L167 β†—
RelativeIdeleGroup.norm_principalIdele
Documentation

The relative idele norm carries a principal idele to the principal idele of the field norm.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem norm_principalIdele (x : LΛ£) :
    norm K L (principalIdele K L x) =
      IdeleGroup.principalIdele K
        (Units.map (Algebra.norm K) x)
def

conjugation

L181 β†—
RelativeIdeleGroup.conjugation
Documentation

Galois conjugation on the scalar-extended adele algebra.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def conjugation
    (Οƒ : L ≃ₐ[K] L) :
    RelativeAdeleRing K L ≃ₐ[
      NumberField.AdeleRing (π“ž K) K]
      RelativeAdeleRing K L
theorem

conjugation_tmul

L190 β†—
RelativeIdeleGroup.conjugation_tmul
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem conjugation_tmul
    (Οƒ : L ≃ₐ[K] L)
    (a : NumberField.AdeleRing (π“ž K) K) (x : L) :
    conjugation K L Οƒ (a βŠ—β‚œ[K] x) =
      a βŠ—β‚œ[K] Οƒ x
def

conjugationIdele

L198 β†—
RelativeIdeleGroup.conjugationIdele
Documentation

Galois conjugation on relative ideles.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def conjugationIdele
    (Οƒ : L ≃ₐ[K] L) :
    RelativeIdeleGroup K L ≃*
      RelativeIdeleGroup K L
theorem

conjugationIdele_coe

L206 β†—
RelativeIdeleGroup.conjugationIdele_coe
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem conjugationIdele_coe
    (Οƒ : L ≃ₐ[K] L) (a : RelativeIdeleGroup K L) :
    ((conjugationIdele K L Οƒ a :
      RelativeIdeleGroup K L) : RelativeAdeleRing K L) =
      conjugation K L Οƒ (a : RelativeAdeleRing K L)
theorem

conjugation_one

L214 β†—
RelativeIdeleGroup.conjugation_one
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem conjugation_one
    (a : RelativeAdeleRing K L) :
    conjugation K L (1 : L ≃ₐ[K] L) a = a
theorem

conjugation_mul

L229 β†—
RelativeIdeleGroup.conjugation_mul
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem conjugation_mul
    (Οƒ Ο„ : L ≃ₐ[K] L)
    (a : RelativeAdeleRing K L) :
    conjugation K L (Οƒ * Ο„) a =
      conjugation K L Οƒ (conjugation K L Ο„ a)
instance

relativeIdeleMulAction

L256 β†—
RelativeIdeleGroup.relativeIdeleMulAction
Documentation

The natural Galois action on relative ideles.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· full declaration
instance relativeIdeleMulAction :
    MulAction (L ≃ₐ[K] L) (RelativeIdeleGroup K L) where
  smul Οƒ a := conjugationIdele K L Οƒ a
  one_smul a := by
    apply Units.ext
    exact conjugation_one K L (a : RelativeAdeleRing K L)
  mul_smul Οƒ Ο„ a := by
    apply Units.ext
    change conjugation K L (Οƒ * Ο„)
        (a : RelativeAdeleRing K L) =
      conjugation K L Οƒ
        (conjugation K L Ο„ (a : RelativeAdeleRing K L))
    exact conjugation_mul K L Οƒ Ο„ _
def

relativeIdeleMulDistribMulAction

L273 β†—
RelativeIdeleGroup.relativeIdeleMulDistribMulAction
Documentation

The natural Galois action on relative ideles, viewed as an action by group automorphisms.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· full declaration
def relativeIdeleMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L) (RelativeIdeleGroup K L) where
  __ := relativeIdeleMulAction K L
  smul_one Οƒ := map_one (conjugationIdele K L Οƒ)
  smul_mul Οƒ a b := map_mul (conjugationIdele K L Οƒ) a b
theorem

smul_def

L281 β†—
RelativeIdeleGroup.smul_def
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem smul_def
    (Οƒ : L ≃ₐ[K] L) (a : RelativeIdeleGroup K L) :
    Οƒ β€’ a = conjugationIdele K L Οƒ a
theorem

smul_inclusion

L288 β†—
RelativeIdeleGroup.smul_inclusion
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem smul_inclusion
    (Οƒ : L ≃ₐ[K] L) (a : IdeleGroup K) :
    Οƒ β€’ inclusion K L a = inclusion K L a
theorem

smul_principalIdele

L309 β†—
RelativeIdeleGroup.smul_principalIdele
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem smul_principalIdele
    (Οƒ : L ≃ₐ[K] L) (x : LΛ£) :
    Οƒ β€’ principalIdele K L x =
      principalIdele K L (Units.map Οƒ.toRingEquiv.toMonoidHom x)
def

galoisAverage

L322 β†—
RelativeIdeleGroup.galoisAverage
Documentation

Reynolds averaging for the finite Galois action.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def galoisAverage
    (z : RelativeAdeleRing K L) :
    RelativeAdeleRing K L
theorem

galoisAverage_eq_of_fixed

L329 β†—
RelativeIdeleGroup.galoisAverage_eq_of_fixed
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem galoisAverage_eq_of_fixed
    [IsGalois K L]
    (z : RelativeAdeleRing K L)
    (hz : βˆ€ Οƒ : L ≃ₐ[K] L,
      conjugation K L Οƒ z = z) :
    galoisAverage K L z = z
theorem

galoisAverage_tmul

L344 β†—
RelativeIdeleGroup.galoisAverage_tmul
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem galoisAverage_tmul
    [IsGalois K L]
    (a : NumberField.AdeleRing (π“ž K) K) (x : L) :
    galoisAverage K L (a βŠ—β‚œ[K] x) =
      adeleInclusion K L
        (a * algebraMap K
          (NumberField.AdeleRing (π“ž K) K)
          ((Fintype.card (L ≃ₐ[K] L) : K)⁻¹ *
            Algebra.trace K L x))
theorem

galoisAverage_mem_adeleInclusion_range

L372 β†—
RelativeIdeleGroup.galoisAverage_mem_adeleInclusion_range
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem galoisAverage_mem_adeleInclusion_range
    [IsGalois K L]
    (z : RelativeAdeleRing K L) :
    βˆƒ a : NumberField.AdeleRing (π“ž K) K,
      adeleInclusion K L a = galoisAverage K L z
theorem

exists_adele_eq_of_galois_fixed

L393 β†—
RelativeIdeleGroup.exists_adele_eq_of_galois_fixed
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem exists_adele_eq_of_galois_fixed
    [IsGalois K L]
    (z : RelativeAdeleRing K L)
    (hz : βˆ€ Οƒ : L ≃ₐ[K] L,
      conjugation K L Οƒ z = z) :
    βˆƒ a : NumberField.AdeleRing (π“ž K) K,
      adeleInclusion K L a = z
def

galoisFixedSubgroup

L405 β†—
RelativeIdeleGroup.galoisFixedSubgroup
Documentation

The subgroup of relative ideles fixed by every Galois automorphism.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
Lean source Β· statement
def galoisFixedSubgroup :
    Subgroup (RelativeIdeleGroup K L)
theorem

inclusion_range_eq_galoisFixedSubgroup

L413 β†—
RelativeIdeleGroup.inclusion_range_eq_galoisFixedSubgroup
Documentation

In the canonical tensor-product presentation, the fixed relative ideles are exactly the ideles of the base field.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
namespace RelativeIdeleGroup
omit [NumberField L] in
Lean source Β· statement
theorem inclusion_range_eq_galoisFixedSubgroup
    [IsGalois K L] :
    (inclusion K L).range =
      galoisFixedSubgroup K L

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