NYLL
Module

RestrictedAction.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.RestrictedAction
15 declarations indexed from sourceView source β†—

Module documentation

Galois action on the restricted local product

The Galois action on 𝔸_K βŠ—[K] L commutes with evaluation at every place. Consequently the exact restricted-product equivalence for relative ideles is equivariant, and the transported action is the coordinatewise tensor-conjugation action.

Imports1
Imported by6

Declarations

def

relativeIdeleRestrictedMulDistribMulAction

L37 β†—
Documentation

The natural action on relative ideles, upgraded to an action by group automorphisms for the restricted-product comparison.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· full declaration
def relativeIdeleRestrictedMulDistribMulAction :
    MulDistribMulAction
      (L ≃ₐ[K] L) (RelativeIdeleGroup K L) where
  __ := RelativeIdeleGroup.relativeIdeleMulAction K L
  smul_one Οƒ :=
    map_one
      (RelativeIdeleGroup.conjugationIdele K L Οƒ)
  smul_mul Οƒ a b :=
    map_mul
      (RelativeIdeleGroup.conjugationIdele K L Οƒ) a b
def

scalarTensorConjugation

L55 β†—
Documentation

Conjugation on the second factor of an arbitrary scalar extension A βŠ—[K] L.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
Lean source Β· statement
def scalarTensorConjugation
    (Οƒ : L ≃ₐ[K] L) :
    A βŠ—[K] L ≃ₐ[A] A βŠ—[K] L
theorem

scalarTensorConjugation_tmul

L71 β†—
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
omit [NumberField K] [NumberField L]
    [FiniteDimensional K L] in
Lean source Β· statement
theorem scalarTensorConjugation_tmul
    (Οƒ : L ≃ₐ[K] L) (a : A) (x : L) :
    scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ
        (a βŠ—β‚œ[K] x) =
      a βŠ—β‚œ[K] Οƒ x
theorem

scalarTensorConjugation_one

L81 β†—
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
omit [NumberField K] [NumberField L]
    [FiniteDimensional K L] in
Lean source Β· statement
theorem scalarTensorConjugation_one
    (z : A βŠ—[K] L) :
    scalarTensorConjugation
        (K := K) (L := L) (A := A)
        (1 : L ≃ₐ[K] L) z = z
theorem

scalarTensorConjugation_mul

L92 β†—
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
omit [NumberField K] [NumberField L]
    [FiniteDimensional K L] in
Lean source Β· statement
theorem scalarTensorConjugation_mul
    (Οƒ Ο„ : L ≃ₐ[K] L)
    (z : A βŠ—[K] L) :
    scalarTensorConjugation
        (K := K) (L := L) (A := A) (Οƒ * Ο„) z =
      scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ
        (scalarTensorConjugation
          (K := K) (L := L) (A := A) Ο„ z)
def

scalarTensorUnitsAction

L107 β†—
Documentation

The action by tensor conjugation on local tensor units.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
Lean source Β· full declaration
def scalarTensorUnitsAction :
    MulDistribMulAction
      (L ≃ₐ[K] L) (A βŠ—[K] L)Λ£ where
  smul Οƒ z :=
    Units.mapEquiv
      (scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ).toMulEquiv z
  one_smul z := by
    apply Units.ext
    exact scalarTensorConjugation_one
      (K := K) (L := L) (A := A)
      (z : A βŠ—[K] L)
  mul_smul Οƒ Ο„ z := by
    apply Units.ext
    exact scalarTensorConjugation_mul
      (K := K) (L := L) (A := A)
      Οƒ Ο„ (z : A βŠ—[K] L)
  smul_one Οƒ := by
    apply Units.ext
    exact
      (scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ).map_one
  smul_mul Οƒ x y := by
    apply Units.ext
    exact
      (scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ).map_mul
        (x : A βŠ—[K] L) (y : A βŠ—[K] L)
theorem

scalarTensorUnitsAction_coe

L139 β†—
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
section ScalarTensor
variable
    {A : Type w} [CommRing A] [Algebra K A]
omit [NumberField K] [NumberField L]
    [FiniteDimensional K L] in
Lean source Β· full declaration
theorem scalarTensorUnitsAction_coe
    (Οƒ : L ≃ₐ[K] L)
    (z : (A βŠ—[K] L)Λ£) :
    letI := scalarTensorUnitsAction
      (K := K) (L := L) (A := A)
    ((Οƒ β€’ z : (A βŠ—[K] L)Λ£) :
        A βŠ—[K] L) =
      scalarTensorConjugation
        (K := K) (L := L) (A := A) Οƒ
        (z : A βŠ—[K] L) :=
  rfl
theorem

relativeAdeleInfiniteComponent_conjugation

L155 β†—
Documentation

Infinite-place evaluation commutes with Galois conjugation.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem relativeAdeleInfiniteComponent_conjugation
    (w : InfinitePlace K)
    (Οƒ : L ≃ₐ[K] L)
    (z : RelativeAdeleRing K L) :
    relativeAdeleInfiniteComponent
        (K := K) (L := L) w
        (RelativeIdeleGroup.conjugation K L Οƒ z) =
      scalarTensorConjugation
        (K := K) (L := L)
        (A := w.Completion) Οƒ
        (relativeAdeleInfiniteComponent
          (K := K) (L := L) w z)
theorem

relativeAdeleFiniteComponent_conjugation

L173 β†—
Documentation

Finite-place evaluation commutes with Galois conjugation.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· statement
theorem relativeAdeleFiniteComponent_conjugation
    (w : HeightOneSpectrum (π“ž K))
    (Οƒ : L ≃ₐ[K] L)
    (z : RelativeAdeleRing K L) :
    relativeAdeleFiniteComponent
        (K := K) (L := L) w
        (RelativeIdeleGroup.conjugation K L Οƒ z) =
      scalarTensorConjugation
        (K := K) (L := L)
        (A := w.adicCompletion K) Οƒ
        (relativeAdeleFiniteComponent
          (K := K) (L := L) w z)
theorem

infiniteComponent_smul

L191 β†—
RelativeIdeleGroup.infiniteComponent_smul
Documentation

The infinite local unit component map is equivariant.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· full declaration
theorem RelativeIdeleGroup.infiniteComponent_smul
    (w : InfinitePlace K)
    (Οƒ : L ≃ₐ[K] L)
    (z : RelativeIdeleGroup K L) :
    letI := scalarTensorUnitsAction
      (K := K) (L := L) (A := w.Completion)
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w (Οƒ β€’ z) =
      Οƒ β€’ RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w z := by
  let _ := scalarTensorUnitsAction
    (K := K) (L := L) (A := w.Completion)
  apply Units.ext
  exact relativeAdeleInfiniteComponent_conjugation
    (K := K) (L := L) w Οƒ
      (z : RelativeAdeleRing K L)
theorem

finiteComponent_smul

L210 β†—
RelativeIdeleGroup.finiteComponent_smul
Documentation

The finite local unit component map is equivariant.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source Β· full declaration
theorem RelativeIdeleGroup.finiteComponent_smul
    (w : HeightOneSpectrum (π“ž K))
    (Οƒ : L ≃ₐ[K] L)
    (z : RelativeIdeleGroup K L) :
    letI := scalarTensorUnitsAction
      (K := K) (L := L)
      (A := w.adicCompletion K)
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w (Οƒ β€’ z) =
      Οƒ β€’ RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w z := by
  let _ := scalarTensorUnitsAction
    (K := K) (L := L)
    (A := w.adicCompletion K)
  apply Units.ext
  exact relativeAdeleFiniteComponent_conjugation
    (K := K) (L := L) w Οƒ
      (z : RelativeAdeleRing K L)
def

relativeLocalIdeleDataMulDistribMulAction

L232 β†—
Documentation

The Galois action on the restricted local product transported through the exact relative-idele equivalence.

Source context 5 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source Β· statement
def relativeLocalIdeleDataMulDistribMulAction :
    MulDistribMulAction
      (L ≃ₐ[K] L)
      (RelativeLocalIdeleData
        (K := K) (L := L))
theorem

relativeIdeleMulEquivLocalData_smul

L271 β†—
Documentation

Equivariance of the exact restricted-product equivalence.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· full declaration
theorem relativeIdeleMulEquivLocalData_smul
    (Οƒ : L ≃ₐ[K] L)
    (z : RelativeIdeleGroup K L) :
    letI :=
      relativeIdeleRestrictedMulDistribMulAction
        (K := K) (L := L)
    letI :=
      relativeLocalIdeleDataMulDistribMulAction
        (K := K) (L := L)
    relativeIdeleMulEquivLocalData
        (K := K) (L := L) (Οƒ β€’ z) =
      Οƒ β€’ relativeIdeleMulEquivLocalData
        (K := K) (L := L) z := by
  let _ :=
    relativeIdeleRestrictedMulDistribMulAction
      (K := K) (L := L)
  let _ :=
    relativeLocalIdeleDataMulDistribMulAction
      (K := K) (L := L)
  change
    relativeIdeleMulEquivLocalData
        (K := K) (L := L) (Οƒ β€’ z) =
      relativeIdeleMulEquivLocalData
        (K := K) (L := L)
        (Οƒ β€’
          (relativeIdeleMulEquivLocalData
            (K := K) (L := L)).symm
            (relativeIdeleMulEquivLocalData
              (K := K) (L := L) z))
  rw [(relativeIdeleMulEquivLocalData
    (K := K) (L := L)).symm_apply_apply]
theorem

infinite_smul

L306 β†—
RelativeLocalIdeleData.infinite_smul
Documentation

The transported action is coordinatewise tensor conjugation at infinite places.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· full declaration
theorem RelativeLocalIdeleData.infinite_smul
    (Οƒ : L ≃ₐ[K] L)
    (a : RelativeLocalIdeleData (K := K) (L := L))
    (w : InfinitePlace K) :
    letI :=
      relativeIdeleRestrictedMulDistribMulAction
        (K := K) (L := L)
    letI :=
      relativeLocalIdeleDataMulDistribMulAction
        (K := K) (L := L)
    letI := scalarTensorUnitsAction
      (K := K) (L := L) (A := w.Completion)
    (Οƒ β€’ a).infinite w =
      Οƒ β€’ a.infinite w := by
  let _ :=
    relativeIdeleRestrictedMulDistribMulAction
      (K := K) (L := L)
  let _ :=
    relativeLocalIdeleDataMulDistribMulAction
      (K := K) (L := L)
  let _ := scalarTensorUnitsAction
    (K := K) (L := L) (A := w.Completion)
  change
    RelativeIdeleGroup.infiniteComponent
        (K := K) (L := L) w
        (Οƒ β€’ relativeIdeleOfLocalData
          (K := K) (L := L) a) =
      Οƒ β€’ a.infinite w
  rw [RelativeIdeleGroup.infiniteComponent_smul,
    relativeIdeleOfLocalData_infiniteComponent]
theorem

finite_smul

L340 β†—
RelativeLocalIdeleData.finite_smul
Documentation

The transported action is coordinatewise tensor conjugation at finite places.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [NumberField L] in
Lean source Β· full declaration
theorem RelativeLocalIdeleData.finite_smul
    (Οƒ : L ≃ₐ[K] L)
    (a : RelativeLocalIdeleData (K := K) (L := L))
    (w : HeightOneSpectrum (π“ž K)) :
    letI :=
      relativeIdeleRestrictedMulDistribMulAction
        (K := K) (L := L)
    letI :=
      relativeLocalIdeleDataMulDistribMulAction
        (K := K) (L := L)
    letI := scalarTensorUnitsAction
      (K := K) (L := L)
      (A := w.adicCompletion K)
    (Οƒ β€’ a).finite w =
      Οƒ β€’ a.finite w := by
  let _ :=
    relativeIdeleRestrictedMulDistribMulAction
      (K := K) (L := L)
  let _ :=
    relativeLocalIdeleDataMulDistribMulAction
      (K := K) (L := L)
  let _ := scalarTensorUnitsAction
    (K := K) (L := L)
    (A := w.adicCompletion K)
  change
    RelativeIdeleGroup.finiteComponent
        (K := K) (L := L) w
        (Οƒ β€’ relativeIdeleOfLocalData
          (K := K) (L := L) a) =
      Οƒ β€’ a.finite w
  rw [RelativeIdeleGroup.finiteComponent_smul,
    relativeIdeleOfLocalData_finiteComponent]

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