NYLL
Module

GaloisAction.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.GaloisAction
57 declarations indexed from sourceView source ↗

Module documentation

Galois actions on S-units and their logarithmic lattice

This file supplies the equivariant input for the S-unit calculation. A Galois automorphism acts on finite places through its restriction to the ring of integers, on infinite places by precomposition, and on field units in the usual way. For a stable finite set of finite places these actions restrict to the actual S-unit group.

Imports3
Imported by5

Declarations

def

finitePlaceEquiv

L35 ↗
Documentation

The permutation of finite places induced by a Galois automorphism.

Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
def finitePlaceEquiv
    (σ : L ≃ₐ[K] L) :
    HeightOneSpectrum (𝓞 L) ≃
      HeightOneSpectrum (𝓞 L)
def

idealMapMulEquiv

L44 ↗
Documentation

Transport of ideals along a ring automorphism, as a multiplicative equivalence.

Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · full declaration
def idealMapMulEquiv
    {R : Type*} [CommRing R]
    (e : R ≃+* R) : Ideal R ≃* Ideal R where
  toFun I := I.map e
  invFun I := I.map e.symm
  left_inv _ := Ideal.map_of_equiv e
  right_inv _ := Ideal.map_of_equiv e.symm
  map_mul' I J := Ideal.map_mul e I J
theorem

idealMapMulEquiv_apply

L54 ↗
Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem idealMapMulEquiv_apply
    {R : Type*} [CommRing R]
    (e : R ≃+* R) (I : Ideal R) :
    idealMapMulEquiv e I = I.map e
theorem

finitePlaceEquiv_asIdeal

L62 ↗
Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem finitePlaceEquiv_asIdeal
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L)) :
    (finitePlaceEquiv K L σ v).asIdeal =
      v.asIdeal.map
        (NumberField.RingOfIntegers.mapAlgEquiv σ).toRingEquiv
theorem

finitePlaceEquiv_one

L73 ↗
Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem finitePlaceEquiv_one
    (v : HeightOneSpectrum (𝓞 L)) :
    finitePlaceEquiv K L (1 : L ≃ₐ[K] L) v = v
theorem

finitePlaceEquiv_mul

L91 ↗
Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem finitePlaceEquiv_mul
    (σ τ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L)) :
    finitePlaceEquiv K L (σ * τ) v =
      finitePlaceEquiv K L σ
        (finitePlaceEquiv K L τ v)
theorem

finitePlaceEquiv_inv_apply

L115 ↗
Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem finitePlaceEquiv_inv_apply
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L)) :
    finitePlaceEquiv K L σ
        (finitePlaceEquiv K L σ⁻¹ v) = v
def

finitePlaceMulAction

L125 ↗
Documentation

The actual Galois action on finite places of L.

Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · full declaration
def finitePlaceMulAction :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) where
  smul σ v := finitePlaceEquiv K L σ v
  one_smul := finitePlaceEquiv_one K L
  mul_smul := finitePlaceEquiv_mul K L
theorem

intValuation_finitePlaceEquiv

L135 ↗
Documentation

The integral adic valuation is invariant under simultaneous transport of the finite place and the integer.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] in
Lean source · statement
theorem intValuation_finitePlaceEquiv
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L))
    (r : 𝓞 L) :
    (finitePlaceEquiv K L σ v).intValuation
        (NumberField.RingOfIntegers.mapAlgEquiv σ r) =
      v.intValuation r
theorem

valuation_finitePlaceEquiv

L167 ↗
Documentation

The field-valued adic valuation is invariant under simultaneous transport of the finite place and the field element.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] in
Lean source · statement
theorem valuation_finitePlaceEquiv
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L))
    (x : L) :
    (finitePlaceEquiv K L σ v).valuation L (σ x) =
      v.valuation L x
theorem

absNorm_map_ringEquiv

L192 ↗
Documentation

Absolute ideal norms are invariant under a ring automorphism.

Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem absNorm_map_ringEquiv
    {R : Type*} [CommRing R] [IsDedekindDomain R]
    [Module.Free ℤ R] [Infinite R]
    (e : R ≃+* R) (I : Ideal R) :
    Ideal.absNorm (I.map e) = Ideal.absNorm I
theorem

toNNReal_apply_congr

L202 ↗
Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem toNNReal_apply_congr
    {e f : NNReal} (he : e ≠ 0) (hf : f ≠ 0)
    (hef : e = f) (q : WithZero (Multiplicative ℤ)) :
    ((WithZeroMulInt.toNNReal he q : NNReal) : ℝ) =
      ((WithZeroMulInt.toNNReal hf q : NNReal) : ℝ)
theorem

adicAbv_finitePlaceEquiv

L213 ↗
Documentation

The normalized finite absolute value is invariant under simultaneous transport of its finite place and its field element.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] in
Lean source · statement
theorem adicAbv_finitePlaceEquiv
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L))
    (x : L) :
    NumberField.HeightOneSpectrum.adicAbv L
        (finitePlaceEquiv K L σ v) (σ x) =
      NumberField.HeightOneSpectrum.adicAbv L v x
theorem

infinitePlace_mult_smul

L241 ↗
Documentation

Archimedean multiplicities are constant on Galois orbits.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem infinitePlace_mult_smul
    (σ : L ≃ₐ[K] L)
    (w : NumberField.InfinitePlace L) :
    (σ • w).mult = w.mult
def

fieldUnitsMulDistribMulAction

L250 ↗
Documentation

The usual action of the relative Galois group on field units.

Source context 6 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · full declaration
def fieldUnitsMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ where
  smul σ x := Units.mapEquiv σ.toMulEquiv x
  one_smul x := by
    ext
    rfl
  mul_smul σ τ x := by
    ext
    rfl
  smul_one σ := map_one (Units.mapEquiv σ.toMulEquiv)
  smul_mul σ x y := map_mul (Units.mapEquiv σ.toMulEquiv) x y
instance

(anonymous instance)

L264 ↗
Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
Lean source · statement
instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L))
instance

(anonymous instance)

L269 ↗
Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
Lean source · statement
instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ
theorem

finitePlace_smul_def

L275 ↗
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem finitePlace_smul_def
    (σ : L ≃ₐ[K] L)
    (v : HeightOneSpectrum (𝓞 L)) :
    σ • v = finitePlaceEquiv K L σ v
def

IsGaloisStableFinitePlaces

L283 ↗
Documentation

A finite set of finite places is Galois-stable when it is invariant under the concrete place permutation.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def IsGaloisStableFinitePlaces
    (S : Finset (HeightOneSpectrum (𝓞 L))) : Prop
theorem

smul_mem

L290 ↗
IsGaloisStableFinitePlaces.smul_mem
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem IsGaloisStableFinitePlaces.smul_mem
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L) {v : HeightOneSpectrum (𝓞 L)}
    (hv : v ∈ S) :
    σ • v ∈ S
theorem

smul_not_mem

L299 ↗
IsGaloisStableFinitePlaces.smul_not_mem
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · statement
theorem IsGaloisStableFinitePlaces.smul_not_mem
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L) {v : HeightOneSpectrum (𝓞 L)}
    (hv : v ∉ S) :
    σ • v ∉ S
theorem

sUnit_smul_mem

L311 ↗
Documentation

Galois automorphisms preserve the concrete S-unit subgroup when the finite-place set is stable.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · statement
theorem sUnit_smul_mem
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L) (x : Lˣ)
    (hx : x ∈ SUnitGroup (K := L) S) :
    σ • x ∈ SUnitGroup (K := L) S
def

sUnitMulDistribMulAction

L338 ↗
Documentation

The actual Galois action on the S-unit group.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def sUnitMulDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    MulDistribMulAction (L ≃ₐ[K] L)
      (SUnitGroup (K := L) S)
theorem

sUnit_smul_coe

L349 ↗
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem sUnit_smul_coe
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (x : SUnitGroup (K := L) S) :
    letI := sUnitMulDistribMulAction K L S hS
    ((σ • x : SUnitGroup (K := L) S) : Lˣ) =
      Units.mapEquiv σ.toMulEquiv (x : Lˣ) :=
  rfl
def

stableFinitePlaceMulAction

L362 ↗
Documentation

The action on the finite set S obtained by restricting the finite-place permutation.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · full declaration
def stableFinitePlaceMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    MulAction (L ≃ₐ[K] L) S where
  smul σ v :=
    ⟨σ • (v : HeightOneSpectrum (𝓞 L)),
      IsGaloisStableFinitePlaces.smul_mem K L hS σ
        v.property⟩
  one_smul v := by
    apply Subtype.ext
    exact one_smul _ (v : HeightOneSpectrum (𝓞 L))
  mul_smul σ τ v := by
    apply Subtype.ext
    exact mul_smul σ τ (v : HeightOneSpectrum (𝓞 L))
def

logPlaceMulAction

L380 ↗
Documentation

The permutation action on all logarithmic places InfinitePlace L ⊕ S.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def logPlaceMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    MulAction (L ≃ₐ[K] L)
      (SUnitGroup.LogPlace (K := L) S)
def

additiveSUnitDistribMulAction

L417 ↗
Documentation

The additive action on the additive form of the S-unit group.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def additiveSUnitDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    DistribMulAction (L ≃ₐ[K] L)
      (Additive (SUnitGroup (K := L) S))
def

fullLogSpaceDistribMulAction

L453 ↗
Documentation

The contragredient coordinate-permutation action on the full logarithmic coordinate space.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogSpaceDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    DistribMulAction (L ≃ₐ[K] L)
      (SUnitGroup.FullLogSpace (K := L) S)
theorem

fullLogSpace_smul_apply

L481 ↗
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem fullLogSpace_smul_apply
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.FullLogSpace (K := L) S)
    (p : SUnitGroup.LogPlace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    (σ • z) p = z (σ⁻¹ • p) :=
  rfl
def

logPlacePermutationHom

L493 ↗
Documentation

The permutation representation on the set of logarithmic places.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def logPlacePermutationHom
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    (L ≃ₐ[K] L) →*
      Equiv.Perm (SUnitGroup.LogPlace (K := L) S)
theorem

logPlacePermutationHom_apply

L504 ↗
Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem logPlacePermutationHom_apply
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (p : SUnitGroup.LogPlace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    logPlacePermutationHom K L S hS σ p = σ • p :=
  rfl
theorem

permutationRepresentation_logPlace

L516 ↗
Documentation

The concrete contragredient action is the coordinate permutation representation associated to the action on logarithmic places.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem permutationRepresentation_logPlace
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.FullLogSpace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    permutationRepresentation
        (logPlacePermutationHom K L S hS) σ z =
      σ • z := by
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  ext p
  rfl
theorem

coordinateSum_smul

L533 ↗
Documentation

Coordinate sum is invariant under the place permutation.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem coordinateSum_smul
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.FullLogSpace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    SUnitGroup.coordinateSum (K := L) S (σ • z) =
      SUnitGroup.coordinateSum (K := L) S z := by
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  change
    (∑ p : SUnitGroup.LogPlace (K := L) S,
      z (σ⁻¹ • p)) = ∑ p, z p
  exact
    Fintype.sum_equiv (MulAction.toPerm σ⁻¹)
      (fun p : SUnitGroup.LogPlace (K := L) S =>
        z (σ⁻¹ • p))
      z (fun _ => rfl)
def

normalizedLogDiagonal

L554 ↗
Documentation

The constant vector whose coordinate sum is one.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def normalizedLogDiagonal
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup.FullLogSpace (K := L) S
theorem

coordinateSum_normalizedLogDiagonal

L562 ↗
Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
theorem coordinateSum_normalizedLogDiagonal
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup.coordinateSum (K := L) S
        (normalizedLogDiagonal L S) = 1
def

fullLogSpaceSplit

L578 ↗
Documentation

Splitting of the full coordinate space into the sum-zero hyperplane and its coordinate sum.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · full declaration
def fullLogSpaceSplit
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup.FullLogSpace (K := L) S →ₗ[ℝ]
      (SUnitGroup.LogHyperplane (K := L) S × ℝ) where
  toFun z :=
    (⟨z -
        SUnitGroup.coordinateSum (K := L) S z •
          normalizedLogDiagonal L S, by
      apply LinearMap.mem_ker.mpr
      rw [map_sub, map_smul,
        coordinateSum_normalizedLogDiagonal]
      simp⟩,
      SUnitGroup.coordinateSum (K := L) S z)
  map_add' z z' := by
    apply Prod.ext
    · ext p
      simp only [Pi.add_apply, Pi.sub_apply, Pi.smul_apply, map_add,
        Prod.fst_add, Submodule.coe_add]
      module
    · exact map_add
        (SUnitGroup.coordinateSum (K := L) S) z z'
  map_smul' c z := by
    apply Prod.ext
    · ext p
      simp only [Pi.smul_apply, Pi.sub_apply, map_smul,
        Prod.smul_fst, RingHom.id_apply, Submodule.coe_smul]
      module
    · exact map_smul
        (SUnitGroup.coordinateSum (K := L) S) c z
theorem

fullLogSpaceSplit_injective

L608 ↗
Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
theorem fullLogSpaceSplit_injective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Injective (fullLogSpaceSplit L S)
theorem

fullLogSpaceSplit_surjective

L646 ↗
Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
theorem fullLogSpaceSplit_surjective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Surjective (fullLogSpaceSplit L S)
def

fullLogSpaceEquivHyperplaneProd

L676 ↗
Documentation

Linear coordinate splitting used to adjoin one invariant diagonal direction to the logarithmic lattice.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogSpaceEquivHyperplaneProd
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup.FullLogSpace (K := L) S ≃ₗ[ℝ]
      (SUnitGroup.LogHyperplane (K := L) S × ℝ)
def

fullLogSpaceContinuousEquivHyperplaneProd

L686 ↗
Documentation

The coordinate splitting as a continuous linear equivalence.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogSpaceContinuousEquivHyperplaneProd
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup.FullLogSpace (K := L) S ≃L[ℝ]
      (SUnitGroup.LogHyperplane (K := L) S × ℝ)
def

fullLogLatticeRealBasis

L694 ↗
Documentation

A real basis of the logarithmic hyperplane obtained from an integral basis of the complete logarithmic lattice.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogLatticeRealBasis
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Basis
      (Module.Free.ChooseBasisIndex ℤ
        (SUnitGroup.fullLogLattice (K := L) S))
      ℝ (SUnitGroup.LogHyperplane (K := L) S)
def

fullLogHyperplaneDiagonalBasis

L706 ↗
Documentation

A basis of the product of the logarithmic hyperplane with the one-dimensional diagonal direction.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogHyperplaneDiagonalBasis
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Basis
      (Module.Free.ChooseBasisIndex ℤ
          (SUnitGroup.fullLogLattice (K := L) S) ⊕ Unit)
      ℝ (SUnitGroup.LogHyperplane (K := L) S × ℝ)
def

fullLogHyperplaneDiagonalLattice

L716 ↗
Documentation

The product lattice formed from the logarithmic lattice and one integral diagonal direction.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def fullLogHyperplaneDiagonalLattice
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Submodule ℤ
      (SUnitGroup.LogHyperplane (K := L) S × ℝ)
def

extendedFullLogLattice

L725 ↗
Documentation

The complete lattice in the full logarithmic coordinate space obtained by adjoining an integral invariant diagonal direction.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def extendedFullLogLattice
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Submodule ℤ (SUnitGroup.FullLogSpace (K := L) S)
instance

instDiscreteTopology_extendedFullLogLattice

L732 ↗
Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
instance instDiscreteTopology_extendedFullLogLattice
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    DiscreteTopology (extendedFullLogLattice L S)
instance

instIsZLattice_extendedFullLogLattice

L759 ↗
Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
instance instIsZLattice_extendedFullLogLattice
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    IsZLattice ℝ (extendedFullLogLattice L S)
theorem

fullLogAmbient_smul

L791 ↗
Documentation

The normalized all-place logarithm is equivariant for the actual S-unit and place-permutation actions.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem fullLogAmbient_smul
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (x : Additive (SUnitGroup (K := L) S)) :
    letI := sUnitMulDistribMulAction K L S hS
    letI := additiveSUnitDistribMulAction K L S hS
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    SUnitGroup.fullLogAmbient (K := L) S (σ • x) =
      σ • SUnitGroup.fullLogAmbient (K := L) S x := by
  let := sUnitMulDistribMulAction K L S hS
  let := additiveSUnitDistribMulAction K L S hS
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  let y : L :=
    (((Additive.toMul x :
      SUnitGroup (K := L) S) : Lˣ) : L)
  funext p
  cases p with
  | inl w =>
      change
        w.mult *
            Real.log (w (σ y)) =
          (σ⁻¹ • w).mult *
            Real.log ((σ⁻¹ • w) y)
      rw [infinitePlace_mult_smul]
      rfl
  | inr v =>
      change
        Real.log
            (NumberField.HeightOneSpectrum.adicAbv L
              (v : HeightOneSpectrum (𝓞 L))
              (σ y)) =
          Real.log
            (NumberField.HeightOneSpectrum.adicAbv L
              (finitePlaceEquiv K L σ⁻¹
                (v : HeightOneSpectrum (𝓞 L)))
              y)
      congr 1
      have h :=
        adicAbv_finitePlaceEquiv K L σ
          (finitePlaceEquiv K L σ⁻¹
            (v : HeightOneSpectrum (𝓞 L)))
          y
      simpa using h
def

logHyperplaneDistribMulAction

L841 ↗
Documentation

The coordinate-permutation action restricted to the coordinate-sum-zero hyperplane.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def logHyperplaneDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    DistribMulAction (L ≃ₐ[K] L)
      (SUnitGroup.LogHyperplane (K := L) S)
theorem

fullLog_smul

L879 ↗
Documentation

Equivariance of the logarithmic map after restricting its codomain to the coordinate-sum-zero hyperplane.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem fullLog_smul
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (x : Additive (SUnitGroup (K := L) S)) :
    letI := sUnitMulDistribMulAction K L S hS
    letI := additiveSUnitDistribMulAction K L S hS
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    letI := logHyperplaneDistribMulAction K L S hS
    SUnitGroup.fullLog (K := L) S (σ • x) =
      σ • SUnitGroup.fullLog (K := L) S x := by
  let := sUnitMulDistribMulAction K L S hS
  let := additiveSUnitDistribMulAction K L S hS
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  let := logHyperplaneDistribMulAction K L S hS
  apply Subtype.ext
  exact fullLogAmbient_smul K L hS σ x
theorem

fullLog_ker_eq_torsion

L901 ↗
Documentation

The kernel of fullLog, stated as an equality of additive subgroups.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
theorem fullLog_ker_eq_torsion
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    (SUnitGroup.fullLog (K := L) S).ker =
      AddCommGroup.torsion
        (Additive (SUnitGroup (K := L) S))
def

additiveSUnitQuotientTorsionEquivFullLogLattice

L915 ↗
Documentation

The first-isomorphism identification of S-units modulo torsion with the actual logarithmic lattice.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · statement
def
    additiveSUnitQuotientTorsionEquivFullLogLattice
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    (Additive (SUnitGroup (K := L) S) ⧸
        AddCommGroup.torsion
          (Additive (SUnitGroup (K := L) S))) ≃+
      SUnitGroup.fullLogLattice (K := L) S
theorem

fullLogLattice_smul_mem

L948 ↗
Documentation

The complete logarithmic lattice is stable under the concrete Galois action.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem fullLogLattice_smul_mem
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.LogHyperplane (K := L) S)
    (hz : z ∈ SUnitGroup.fullLogLattice (K := L) S) :
    letI := sUnitMulDistribMulAction K L S hS
    letI := additiveSUnitDistribMulAction K L S hS
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    letI := logHyperplaneDistribMulAction K L S hS
    σ • z ∈ SUnitGroup.fullLogLattice (K := L) S := by
  let := sUnitMulDistribMulAction K L S hS
  let := additiveSUnitDistribMulAction K L S hS
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  let := logHyperplaneDistribMulAction K L S hS
  rw [SUnitGroup.fullLogLattice_eq_range] at hz ⊢
  obtain ⟨x, hx⟩ := hz
  change SUnitGroup.fullLog (K := L) S x = z at hx
  refine ⟨σ • x, ?_⟩
  change
    SUnitGroup.fullLog (K := L) S (σ • x) = σ • z
  rw [fullLog_smul K L hS, hx]
theorem

fullLogSpaceSplit_fst_smul

L976 ↗
Documentation

Under the coordinate splitting, the hyperplane component transforms by the restricted Galois action.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem fullLogSpaceSplit_fst_smul
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.FullLogSpace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    letI := logHyperplaneDistribMulAction K L S hS
    (fullLogSpaceSplit L S (σ • z)).1 =
      σ • (fullLogSpaceSplit L S z).1 := by
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  let := logHyperplaneDistribMulAction K L S hS
  apply Subtype.ext
  change
    σ • z -
        SUnitGroup.coordinateSum (K := L) S (σ • z) •
          normalizedLogDiagonal L S =
      σ •
        (z -
          SUnitGroup.coordinateSum (K := L) S z •
            normalizedLogDiagonal L S)
  rw [coordinateSum_smul K L hS]
  ext p
  rfl
theorem

fullLogSpaceSplit_snd_smul

L1005 ↗
Documentation

Under the coordinate splitting, the diagonal coordinate is Galois-invariant.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · full declaration
theorem fullLogSpaceSplit_snd_smul
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (z : SUnitGroup.FullLogSpace (K := L) S) :
    letI := logPlaceMulAction K L S hS
    letI := fullLogSpaceDistribMulAction K L S hS
    (fullLogSpaceSplit L S (σ • z)).2 =
      (fullLogSpaceSplit L S z).2 := by
  let := logPlaceMulAction K L S hS
  let := fullLogSpaceDistribMulAction K L S hS
  exact coordinateSum_smul K L hS σ z
theorem

extendedFullLogLattice_permutation_stable

L1021 ↗
Documentation

The full logarithmic lattice with its adjoined diagonal direction is stable under the place-permutation representation.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
omit [NumberField K] in
Lean source · statement
theorem extendedFullLogLattice_permutation_stable
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    ∀ (σ : L ≃ₐ[K] L)
      (z : SUnitGroup.FullLogSpace (K := L) S),
      z ∈ extendedFullLogLattice L S →
        permutationRepresentation
            (logPlacePermutationHom K L S hS) σ z ∈
          extendedFullLogLattice L S
theorem

extendedFullLogPermutationSublattice_finite_quotient

L1093 ↗
Documentation

The canonical complete permutation sublattice of the extended logarithmic lattice has finite index.

Source context 10 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
open scoped Classical in
Lean source · statement
theorem extendedFullLogPermutationSublattice_finite_quotient
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    Finite
      (extendedFullLogLattice L S ⧸
        (permutationSublattice
          (logPlacePermutationHom K L S hS)
          (extendedFullLogLattice L S)
          (extendedFullLogLattice_permutation_stable K L hS)).comap
            (extendedFullLogLattice L S).subtype)
theorem

extendedFullLogLattice_herbrandQuotient_eq_stabilizerProduct

L1111 ↗
Documentation

For the actual full logarithmic S-unit lattice. The Herbrand quotient is the product of the orders of the stabilizers of the Galois orbits of logarithmic places.

Source context 9 commands

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

open scoped BigOperators NumberField nonZeroDivisors
open IsDedekindDomain Module
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
noncomputable section
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section FinitePlaceAction
local instance :
    MulAction (L ≃ₐ[K] L)
      (HeightOneSpectrum (𝓞 L)) :=
  finitePlaceMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L) Lˣ :=
  fieldUnitsMulDistribMulAction K L
Lean source · full declaration
theorem
    extendedFullLogLattice_herbrandQuotient_eq_stabilizerProduct
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ) :
    let ρ :=
      logPlacePermutationHom K L S hS
    letI _indexAction :
        MulAction (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S) :=
      permutationMulAction ρ
    letI _ambientAction :
        DistribMulAction (L ≃ₐ[K] L)
          (extendedFullLogLattice L S) :=
      completePermutationLatticeDistribMulAction
        ρ (extendedFullLogLattice L S)
        (extendedFullLogLattice_permutation_stable
          K L hS)
    letI _ambientMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S)) :=
      multiplicativeDistribMulAction
    letI _orbitFintype :
        Fintype
          (MulAction.orbitRel.Quotient
            (L ≃ₐ[K] L)
            (SUnitGroup.LogPlace (K := L) S)) :=
      Fintype.ofFinite _
    letI _stabilizerFintype :
        ∀ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          Fintype (permutationOrbitStabilizer ω) :=
      fun _ => Fintype.ofFinite _
    ∃ h :
        HerbrandQuotientDefined
          (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S)) σ,
      @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S))
          _ _ _ _ σ h.1 h.2 =
        ∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ) := by
  let ρ :=
    logPlacePermutationHom K L S hS
  exact
    completePermutationLattice_herbrandQuotient_eq_stabilizerProduct
      (G := L ≃ₐ[K] L)
      (ι := SUnitGroup.LogPlace (K := L) S)
      ρ (extendedFullLogLattice L S)
      (extendedFullLogLattice_permutation_stable
        K L hS) σ hgen

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