NYLL
Module

Herbrand.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.SUnit.Herbrand
35 declarations indexed from sourceView source ↗

Module documentation

The Herbrand quotient of the global S-unit group

This file computes the Herbrand quotient of the global S-unit group. It connects the actual S-unit group to its logarithmic lattice, adds the invariant diagonal integer direction, and combines the resulting exact sequences with the permutation-lattice calculation.

Imports4
Imported by3

Declarations

def

fullLogLatticeDistribMulAction

L40 ↗
Documentation

The additive Galois action restricted to the actual full logarithmic lattice.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
def fullLogLatticeDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    DistribMulAction (L ≃ₐ[K] L)
      (SUnitGroup.fullLogLattice (K := L) S)
def

sUnitFullLogMulHom

L79 ↗
Documentation

The full logarithm as a surjective multiplicative homomorphism from S-units onto the multiplicative logarithmic lattice.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · full declaration
def sUnitFullLogMulHom
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    SUnitGroup (K := L) S →*
      Multiplicative
        (SUnitGroup.fullLogLattice (K := L) S) where
  toFun x :=
    Multiplicative.ofAdd
      ⟨SUnitGroup.fullLog (K := L) S
          (Additive.ofMul x), by
        rw [SUnitGroup.fullLogLattice_eq_range]
        exact ⟨Additive.ofMul x, rfl⟩⟩
  map_one' := by
    apply Multiplicative.toAdd.injective
    apply Subtype.ext
    exact map_zero
      (SUnitGroup.fullLog (K := L) S)
  map_mul' x y := by
    apply Multiplicative.toAdd.injective
    apply Subtype.ext
    exact map_add
      (SUnitGroup.fullLog (K := L) S)
      (Additive.ofMul x) (Additive.ofMul y)
theorem

sUnitFullLogMulHom_surjective

L103 ↗
Documentation

The multiplicative full logarithm is onto its defining lattice.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
theorem sUnitFullLogMulHom_surjective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Surjective
      (sUnitFullLogMulHom L S)
theorem

sUnitFullLogMulHom_ker

L129 ↗
Documentation

The kernel of the multiplicative full logarithm is exactly the torsion subgroup of the S-unit group.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
theorem sUnitFullLogMulHom_ker
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    (sUnitFullLogMulHom L S).ker =
      CommGroup.torsion
        (SUnitGroup (K := L) S)
theorem

sUnitFullLogMulHom_equivariant

L170 ↗
Documentation

The multiplicative full logarithm is equivariant for the actual Galois actions.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
omit [NumberField K] in
Lean source · full declaration
theorem sUnitFullLogMulHom_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    letI _sUnitAction :=
      sUnitMulDistribMulAction K L S hS
    letI _latticeAction :=
      fullLogLatticeDistribMulAction K L S hS
    letI _multiplicativeLatticeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S)) :=
      multiplicativeDistribMulAction
    ∀ (σ : L ≃ₐ[K] L)
      (x : SUnitGroup (K := L) S),
      sUnitFullLogMulHom L S (σ • x) =
        σ • sUnitFullLogMulHom L S x := by
  let sUnitAction :=
    sUnitMulDistribMulAction K L S hS
  let additiveSUnitAction :=
    additiveSUnitDistribMulAction K L S hS
  let logPlaceAction :=
    logPlaceMulAction K L S hS
  let fullLogSpaceAction :=
    fullLogSpaceDistribMulAction K L S hS
  let logHyperplaneAction :=
    logHyperplaneDistribMulAction K L S hS
  let latticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let multiplicativeLatticeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S)) :=
    multiplicativeDistribMulAction
  intro σ x
  apply Multiplicative.toAdd.injective
  apply Subtype.ext
  exact fullLog_smul K L hS σ (Additive.ofMul x)
def

rootsOfUnityEquivSUnitTorsion

L210 ↗
Documentation

Ordinary roots of unity identify with the torsion subgroup of the S-unit group.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
def rootsOfUnityEquivSUnitTorsion
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    NumberField.Units.torsion L ≃*
      CommGroup.torsion
        (SUnitGroup (K := L) S)
theorem

sUnitTorsionFinite

L224 ↗
Documentation

Torsion in an S-unit group over a number field is finite.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
theorem sUnitTorsionFinite
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Finite
      (CommGroup.torsion
        (SUnitGroup (K := L) S))
theorem

sUnitTorsion_stable

L235 ↗
Documentation

The torsion subgroup is stable under Galois automorphisms.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
omit [NumberField K] in
Lean source · full declaration
theorem sUnitTorsion_stable
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    letI _sUnitAction :=
      sUnitMulDistribMulAction K L S hS
    ∀ (σ : L ≃ₐ[K] L)
      (x : SUnitGroup (K := L) S),
      x ∈ CommGroup.torsion
          (SUnitGroup (K := L) S) →
        σ • x ∈ CommGroup.torsion
          (SUnitGroup (K := L) S) := by
  let sUnitAction :=
    sUnitMulDistribMulAction K L S hS
  intro σ x hx
  exact
    CommGroup.le_comap_torsion
      (MulDistribMulAction.toMonoidHom
        (SUnitGroup (K := L) S) σ) hx
theorem

sUnitTorsion_fullLog_exact

L255 ↗
Documentation

Exactness of torsion inclusion followed by the full logarithm.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogarithmicQuotient
Lean source · statement
theorem sUnitTorsion_fullLog_exact
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    ∀ x : SUnitGroup (K := L) S,
      sUnitFullLogMulHom L S x = 1 ↔
        ∃ t :
            CommGroup.torsion
              (SUnitGroup (K := L) S),
          (CommGroup.torsion
            (SUnitGroup (K := L) S)).subtype t = x
theorem

mem_fullLogHyperplaneDiagonalLattice_iff

L290 ↗
Documentation

Membership in the product lattice is exactly integrality in the logarithmic lattice and in the diagonal coordinate.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
Lean source · statement
theorem mem_fullLogHyperplaneDiagonalLattice_iff
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (z :
      SUnitGroup.LogHyperplane (K := L) S × ℝ) :
    z ∈ fullLogHyperplaneDiagonalLattice L S ↔
      z.1 ∈ SUnitGroup.fullLogLattice (K := L) S ∧
        ∃ n : ℤ, (n : ℝ) = z.2
def

fullLogLatticeProdIntToExtended

L351 ↗
Documentation

The natural integral-linear map from the logarithmic lattice and one diagonal integer coordinate to the extended full logarithmic lattice.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
Lean source · statement
def fullLogLatticeProdIntToExtended
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    (SUnitGroup.fullLogLattice (K := L) S × ℤ) →ₗ[ℤ]
      extendedFullLogLattice L S
theorem

fullLogLatticeProdIntToExtended_bijective

L438 ↗
Documentation

The preceding map is bijective.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
Lean source · statement
theorem fullLogLatticeProdIntToExtended_bijective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Bijective
      (fullLogLatticeProdIntToExtended L S)
def

extendedFullLogLatticeEquivProdInt

L525 ↗
Documentation

Integral-linear decomposition of the extended lattice into the logarithmic lattice and one integer diagonal direction.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
Lean source · statement
def extendedFullLogLatticeEquivProdInt
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    extendedFullLogLattice L S ≃ₗ[ℤ]
      (SUnitGroup.fullLogLattice (K := L) S × ℤ)
def

fullLogLatticeProdIntDistribMulAction

L536 ↗
Documentation

The componentwise action on the logarithmic lattice paired with the invariant integer diagonal.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
Lean source · statement
def fullLogLatticeProdIntDistribMulAction
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (hS : IsGaloisStableFinitePlaces K L S) :
    DistribMulAction (L ≃ₐ[K] L)
      (SUnitGroup.fullLogLattice (K := L) S × ℤ)
theorem

fullLogLatticeProdIntToExtended_equivariant

L569 ↗
Documentation

The map from logarithmic-plus-diagonal coordinates into the extended lattice is equivariant.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
omit [NumberField K] in
Lean source · full declaration
theorem fullLogLatticeProdIntToExtended_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    let ρ :=
      logPlacePermutationHom K L S hS
    letI _indexAction :
        MulAction (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S) :=
      permutationMulAction ρ
    letI _extendedAction :
        DistribMulAction (L ≃ₐ[K] L)
          (extendedFullLogLattice L S) :=
      completePermutationLatticeDistribMulAction
        ρ (extendedFullLogLattice L S)
        (extendedFullLogLattice_permutation_stable
          K L hS)
    letI _productAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
      fullLogLatticeProdIntDistribMulAction K L S hS
    ∀ (σ : L ≃ₐ[K] L)
      (z :
        SUnitGroup.fullLogLattice (K := L) S × ℤ),
      fullLogLatticeProdIntToExtended L S
          (_productAction.toMulAction.toSemigroupAction.toSMul.smul
            σ z) =
        _extendedAction.toMulAction.toSemigroupAction.toSMul.smul
          σ (fullLogLatticeProdIntToExtended L S z) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let sUnitAction :=
    sUnitMulDistribMulAction K L S hS
  let additiveSUnitAction :=
    additiveSUnitDistribMulAction K L S hS
  let logPlaceAction :=
    logPlaceMulAction K L S hS
  let fullLogSpaceAction :=
    fullLogSpaceDistribMulAction K L S hS
  let logHyperplaneAction :=
    logHyperplaneDistribMulAction K L S hS
  let fullLogLatticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let extendedAction :
      DistribMulAction (L ≃ₐ[K] L)
        (extendedFullLogLattice L S) :=
    completePermutationLatticeDistribMulAction
      ρ (extendedFullLogLattice L S)
      (extendedFullLogLattice_permutation_stable
        K L hS)
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  intro σ z
  apply Subtype.ext
  apply fullLogSpaceSplit_injective L S
  apply Prod.ext
  · change
      (fullLogSpaceSplit L S
        ((fullLogSpaceEquivHyperplaneProd L S).symm
          (((σ • z.1 :
                SUnitGroup.fullLogLattice
                  (K := L) S) :
              SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ)))).1 =
        (fullLogSpaceSplit L S
          (permutationRepresentation ρ σ
            ((fullLogSpaceEquivHyperplaneProd L S).symm
              (((z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
                (z.2 : ℝ))))).1
    rw [permutationRepresentation_logPlace K L hS,
      fullLogSpaceSplit_fst_smul K L hS]
    rw [show
      fullLogSpaceSplit L S
          ((fullLogSpaceEquivHyperplaneProd L S).symm
            (((σ • z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ))) =
        (((σ • z.1 :
              SUnitGroup.fullLogLattice
                (K := L) S) :
            SUnitGroup.LogHyperplane (K := L) S),
          (z.2 : ℝ)) by
      exact
        (fullLogSpaceEquivHyperplaneProd L S).apply_symm_apply _]
    rw [show
      fullLogSpaceSplit L S
          ((fullLogSpaceEquivHyperplaneProd L S).symm
            (((z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ))) =
        (((z.1 :
              SUnitGroup.fullLogLattice
                (K := L) S) :
            SUnitGroup.LogHyperplane (K := L) S),
          (z.2 : ℝ)) by
      exact
        (fullLogSpaceEquivHyperplaneProd L S).apply_symm_apply _]
    change
      σ • (z.1 :
          SUnitGroup.LogHyperplane (K := L) S) =
        σ • (z.1 :
          SUnitGroup.LogHyperplane (K := L) S)
    rfl
  · change
      (fullLogSpaceSplit L S
        ((fullLogSpaceEquivHyperplaneProd L S).symm
          (((σ • z.1 :
                SUnitGroup.fullLogLattice
                  (K := L) S) :
              SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ)))).2 =
        (fullLogSpaceSplit L S
          (permutationRepresentation ρ σ
            ((fullLogSpaceEquivHyperplaneProd L S).symm
              (((z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
                (z.2 : ℝ))))).2
    rw [permutationRepresentation_logPlace K L hS,
      fullLogSpaceSplit_snd_smul K L hS]
    rw [show
      fullLogSpaceSplit L S
          ((fullLogSpaceEquivHyperplaneProd L S).symm
            (((σ • z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ))) =
        (((σ • z.1 :
              SUnitGroup.fullLogLattice
                (K := L) S) :
            SUnitGroup.LogHyperplane (K := L) S),
          (z.2 : ℝ)) by
      exact
        (fullLogSpaceEquivHyperplaneProd L S).apply_symm_apply _]
    rw [show
      fullLogSpaceSplit L S
          ((fullLogSpaceEquivHyperplaneProd L S).symm
            (((z.1 :
                  SUnitGroup.fullLogLattice
                    (K := L) S) :
                SUnitGroup.LogHyperplane (K := L) S),
              (z.2 : ℝ))) =
        (((z.1 :
              SUnitGroup.fullLogLattice
                (K := L) S) :
            SUnitGroup.LogHyperplane (K := L) S),
          (z.2 : ℝ)) by
      exact
        (fullLogSpaceEquivHyperplaneProd L S).apply_symm_apply _]
theorem

extendedFullLogLatticeEquivProdInt_equivariant

L736 ↗
Documentation

The integral decomposition of the extended lattice is equivariant.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section DiagonalExtension
omit [NumberField K] in
Lean source · full declaration
theorem extendedFullLogLatticeEquivProdInt_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    let ρ :=
      logPlacePermutationHom K L S hS
    letI _indexAction :
        MulAction (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S) :=
      permutationMulAction ρ
    letI _extendedAction :
        DistribMulAction (L ≃ₐ[K] L)
          (extendedFullLogLattice L S) :=
      completePermutationLatticeDistribMulAction
        ρ (extendedFullLogLattice L S)
        (extendedFullLogLattice_permutation_stable
          K L hS)
    letI _productAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
      fullLogLatticeProdIntDistribMulAction K L S hS
    ∀ (σ : L ≃ₐ[K] L)
      (x : extendedFullLogLattice L S),
      extendedFullLogLatticeEquivProdInt L S
          (_extendedAction.toMulAction.toSemigroupAction.toSMul.smul
            σ x) =
        _productAction.toMulAction.toSemigroupAction.toSMul.smul
          σ (extendedFullLogLatticeEquivProdInt L S x) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let sUnitAction :=
    sUnitMulDistribMulAction K L S hS
  let additiveSUnitAction :=
    additiveSUnitDistribMulAction K L S hS
  let logPlaceAction :=
    logPlaceMulAction K L S hS
  let fullLogSpaceAction :=
    fullLogSpaceDistribMulAction K L S hS
  let logHyperplaneAction :=
    logHyperplaneDistribMulAction K L S hS
  let fullLogLatticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let extendedAction :
      DistribMulAction (L ≃ₐ[K] L)
        (extendedFullLogLattice L S) :=
    completePermutationLatticeDistribMulAction
      ρ (extendedFullLogLattice L S)
      (extendedFullLogLattice_permutation_stable
        K L hS)
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  intro σ x
  let e :=
    extendedFullLogLatticeEquivProdInt L S
  apply e.symm.injective
  have hmap :=
    fullLogLatticeProdIntToExtended_equivariant
      K L hS σ (e x)
  change
    e.symm
        (productAction.toMulAction.toSemigroupAction.toSMul.smul
          σ (e x)) =
      extendedAction.toMulAction.toSemigroupAction.toSMul.smul
        σ (e.symm (e x)) at hmap
  rw [e.symm_apply_apply, hmap,
    e.symm_apply_apply]
def

fullLogLatticeProdIntIncl

L815 ↗
Documentation

Inclusion of the logarithmic lattice as the first factor of the logarithmic-plus-diagonal lattice, in multiplicative notation.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · full declaration
def fullLogLatticeProdIntIncl
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Multiplicative
        (SUnitGroup.fullLogLattice (K := L) S) →*
      Multiplicative
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) where
  toFun z :=
    Multiplicative.ofAdd
      (Multiplicative.toAdd z, 0)
  map_one' := rfl
  map_mul' _ _ := rfl
def

fullLogLatticeProdIntProj

L829 ↗
Documentation

Projection from the logarithmic-plus-diagonal lattice to its integer diagonal coordinate, in multiplicative notation.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · full declaration
def fullLogLatticeProdIntProj
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Multiplicative
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) →*
      Multiplicative ℤ where
  toFun z :=
    Multiplicative.ofAdd
      (Multiplicative.toAdd z).2
  map_one' := rfl
  map_mul' _ _ := rfl
def

extendedFullLogLatticeMulEquivProdInt

L842 ↗
Documentation

The multiplicative equivalence induced by the integral decomposition of the extended lattice.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · statement
def extendedFullLogLatticeMulEquivProdInt
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Multiplicative (extendedFullLogLattice L S) ≃*
      Multiplicative
        (SUnitGroup.fullLogLattice (K := L) S × ℤ)
theorem

extendedFullLogLatticeMulEquivProdInt_equivariant

L852 ↗
Documentation

The multiplicative form of the integral decomposition is Galois-equivariant.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
omit [NumberField K] in
Lean source · full declaration
theorem extendedFullLogLatticeMulEquivProdInt_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    let ρ :=
      logPlacePermutationHom K L S hS
    letI _indexAction :
        MulAction (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S) :=
      permutationMulAction ρ
    letI _extendedAction :
        DistribMulAction (L ≃ₐ[K] L)
          (extendedFullLogLattice L S) :=
      completePermutationLatticeDistribMulAction
        ρ (extendedFullLogLattice L S)
        (extendedFullLogLattice_permutation_stable
          K L hS)
    letI _extendedMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S)) :=
      multiplicativeDistribMulAction
    letI _productAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
      fullLogLatticeProdIntDistribMulAction K L S hS
    letI _productMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
      multiplicativeDistribMulAction
    ∀ (σ : L ≃ₐ[K] L)
      (x : Multiplicative (extendedFullLogLattice L S)),
      extendedFullLogLatticeMulEquivProdInt L S
          (_extendedMultiplicativeAction.toMulAction.toSemigroupAction.toSMul.smul
            σ x) =
        _productMultiplicativeAction.toMulAction.toSemigroupAction.toSMul.smul
          σ (extendedFullLogLatticeMulEquivProdInt L S x) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let sUnitAction :=
    sUnitMulDistribMulAction K L S hS
  let additiveSUnitAction :=
    additiveSUnitDistribMulAction K L S hS
  let logPlaceAction :=
    logPlaceMulAction K L S hS
  let fullLogSpaceAction :=
    fullLogSpaceDistribMulAction K L S hS
  let logHyperplaneAction :=
    logHyperplaneDistribMulAction K L S hS
  let fullLogLatticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let extendedAction :
      DistribMulAction (L ≃ₐ[K] L)
        (extendedFullLogLattice L S) :=
    completePermutationLatticeDistribMulAction
      ρ (extendedFullLogLattice L S)
      (extendedFullLogLattice_permutation_stable
        K L hS)
  let extendedMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (extendedFullLogLattice L S)) :=
    multiplicativeDistribMulAction
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  let productMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
    multiplicativeDistribMulAction
  intro σ x
  apply Multiplicative.toAdd.injective
  change
    extendedFullLogLatticeEquivProdInt L S
        (extendedAction.toMulAction.toSemigroupAction.toSMul.smul
          σ (Multiplicative.toAdd x)) =
      productAction.toMulAction.toSemigroupAction.toSMul.smul
        σ
        (extendedFullLogLatticeEquivProdInt L S
          (Multiplicative.toAdd x))
  exact
    extendedFullLogLatticeEquivProdInt_equivariant
      K L hS σ (Multiplicative.toAdd x)
theorem

fullLogLatticeProdIntIncl_equivariant

L945 ↗
Documentation

The first-factor inclusion is Galois-equivariant.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
omit [NumberField K] in
Lean source · full declaration
theorem fullLogLatticeProdIntIncl_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    letI _latticeAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S) :=
      fullLogLatticeDistribMulAction K L S hS
    letI _latticeMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S)) :=
      multiplicativeDistribMulAction
    letI _productAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
      fullLogLatticeProdIntDistribMulAction K L S hS
    letI _productMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
      multiplicativeDistribMulAction
    ∀ (σ : L ≃ₐ[K] L)
      (z :
        Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S)),
      fullLogLatticeProdIntIncl L S (σ • z) =
        σ • fullLogLatticeProdIntIncl L S z := by
  let latticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let latticeMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S)) :=
    multiplicativeDistribMulAction
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  let productMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
    multiplicativeDistribMulAction
  intro σ z
  rfl
theorem

fullLogLatticeProdIntProj_equivariant

L994 ↗
Documentation

The diagonal projection is Galois-equivariant for the trivial action on its integer target.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
omit [NumberField K] in
Lean source · full declaration
theorem fullLogLatticeProdIntProj_equivariant
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    letI _latticeAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S) :=
      fullLogLatticeDistribMulAction K L S hS
    letI _productAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
      fullLogLatticeProdIntDistribMulAction K L S hS
    letI _productMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
      multiplicativeDistribMulAction
    letI _integerAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative ℤ) :=
      trivialIntMulDistribMulAction (L ≃ₐ[K] L)
    ∀ (σ : L ≃ₐ[K] L)
      (z :
        Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)),
      fullLogLatticeProdIntProj L S (σ • z) =
        σ • fullLogLatticeProdIntProj L S z := by
  let latticeAction :=
    fullLogLatticeDistribMulAction K L S hS
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  let productMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
    multiplicativeDistribMulAction
  let integerAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative ℤ) :=
    trivialIntMulDistribMulAction (L ≃ₐ[K] L)
  intro σ z
  rfl
theorem

fullLogLatticeProdInt_exact

L1040 ↗
Documentation

Exactness of the first-factor inclusion followed by the diagonal projection.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · statement
theorem fullLogLatticeProdInt_exact
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    ∀ z :
        Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ),
      fullLogLatticeProdIntProj L S z = 1 ↔
        ∃ x :
            Multiplicative
              (SUnitGroup.fullLogLattice (K := L) S),
          fullLogLatticeProdIntIncl L S x = z
theorem

fullLogLatticeProdIntIncl_injective

L1064 ↗
Documentation

The first-factor inclusion is injective.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · statement
theorem fullLogLatticeProdIntIncl_injective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Injective
      (fullLogLatticeProdIntIncl L S)
theorem

fullLogLatticeProdIntProj_surjective

L1078 ↗
Documentation

The diagonal projection is surjective.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · statement
theorem fullLogLatticeProdIntProj_surjective
    (S : Finset (HeightOneSpectrum (𝓞 L))) :
    Function.Surjective
      (fullLogLatticeProdIntProj L S)
theorem

fullLogLattice_herbrandQuotient_eq_stabilizerProduct_div_card

L1089 ↗
Documentation

For the genuine sum-zero logarithmic lattice, adjoining the invariant diagonal multiplies the Herbrand quotient by |G|.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LogLatticeHerbrand
Lean source · full declaration
theorem fullLogLattice_herbrandQuotient_eq_stabilizerProduct_div_card
    (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 _latticeAction :
        DistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup.fullLogLattice (K := L) S) :=
      fullLogLatticeDistribMulAction K L S hS
    letI _latticeMultiplicativeAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := 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
            (SUnitGroup.fullLogLattice (K := L) S)) σ,
      @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S))
          _ _ _ _ σ h.1 h.2 =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let latticeAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S) :=
    fullLogLatticeDistribMulAction K L S hS
  let latticeMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S)) :=
    multiplicativeDistribMulAction
  let productAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S × ℤ) :=
    fullLogLatticeProdIntDistribMulAction K L S hS
  let productMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)) :=
    multiplicativeDistribMulAction
  let integerAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative ℤ) :=
    trivialIntMulDistribMulAction (L ≃ₐ[K] L)
  let extendedAction :
      DistribMulAction (L ≃ₐ[K] L)
        (extendedFullLogLattice L S) :=
    completePermutationLatticeDistribMulAction
      ρ (extendedFullLogLattice L S)
      (extendedFullLogLattice_permutation_stable
        K L hS)
  let extendedMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (extendedFullLogLattice L S)) :=
    multiplicativeDistribMulAction
  let orbitFintype :
      Fintype
        (MulAction.orbitRel.Quotient
          (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S)) :=
    Fintype.ofFinite _
  let stabilizerFintype :
      ∀ ω :
          MulAction.orbitRel.Quotient
            (L ≃ₐ[K] L)
            (SUnitGroup.LogPlace (K := L) S),
        Fintype (permutationOrbitStabilizer ω) :=
    fun _ => Fintype.ofFinite _
  obtain ⟨hExtended, hExtendedValue⟩ :=
    extendedFullLogLattice_herbrandQuotient_eq_stabilizerProduct
      K L hS σ hgen
  let extendedH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S))) :=
    hExtended.1
  let extendedHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S)) σ) :=
    hExtended.2
  let e :=
    extendedFullLogLatticeMulEquivProdInt L S
  have he :
      ∀ (τ : L ≃ₐ[K] L)
        (x : Multiplicative (extendedFullLogLattice L S)),
        e (τ • x) = τ • e x :=
    extendedFullLogLatticeMulEquivProdInt_equivariant
      K L hS
  let hProduct :
      HerbrandQuotientDefined
        (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S × ℤ)) σ :=
    ⟨herbrandH0Finite_of_equivariantMulEquiv e he,
      herbrandHMinusOneFinite_of_equivariantMulEquiv
        e he σ⟩
  let productH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ))) :=
    hProduct.1
  let productHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) σ) :=
    hProduct.2
  let hInteger :
      HerbrandQuotientDefined
        (L ≃ₐ[K] L) (Multiplicative ℤ) σ :=
    ⟨trivialIntHerbrandH0Finite,
      trivialIntHerbrandHMinusOneFinite σ⟩
  let integerH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L) (Multiplicative ℤ)) :=
    hInteger.1
  let integerHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L) (Multiplicative ℤ) σ) :=
    hInteger.2
  let hLattice :=
    herbrandQuotientDefined_left_of_middle_right
      (fullLogLatticeProdIntIncl L S)
      (fullLogLatticeProdIntProj L S)
      (fullLogLatticeProdIntIncl_equivariant K L hS)
      (fullLogLatticeProdIntProj_equivariant K L hS)
      (fullLogLatticeProdInt_exact L S)
      (fullLogLatticeProdIntIncl_injective L S)
      (fullLogLatticeProdIntProj_surjective L S)
      σ hgen hProduct hInteger
  let latticeH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S))) :=
    hLattice.1
  let latticeHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S)) σ) :=
    hLattice.2
  have hMultiplicative :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) σ =
        herbrandQuotient
            (G := L ≃ₐ[K] L)
            (A := Multiplicative
              (SUnitGroup.fullLogLattice (K := L) S)) σ *
          herbrandQuotient
            (G := L ≃ₐ[K] L)
            (A := Multiplicative ℤ) σ :=
    herbrandQuotient_multiplicative_of_shortExact
      (fullLogLatticeProdIntIncl L S)
      (fullLogLatticeProdIntProj L S)
      (fullLogLatticeProdIntIncl_equivariant K L hS)
      (fullLogLatticeProdIntProj_equivariant K L hS)
      (fullLogLatticeProdInt_exact L S)
      (fullLogLatticeProdIntIncl_injective L S)
      (fullLogLatticeProdIntProj_surjective L S)
      σ hgen
  have hIntegerValue :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := Multiplicative ℤ) σ =
        (Fintype.card (L ≃ₐ[K] L) : ℚ) :=
    trivialInt_herbrandQuotient_eq_card σ
  have hExtendedProduct :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := Multiplicative
            (extendedFullLogLattice L S)) σ =
        herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ)) σ := by
    exact
      herbrandQuotient_eq_of_equivariantMulEquiv
        e he σ
  refine ⟨hLattice, ?_⟩
  have hcard :
      (Fintype.card (L ≃ₐ[K] L) : ℚ) ≠ 0 := by
    exact_mod_cast
      (Fintype.card_ne_zero :
        Fintype.card (L ≃ₐ[K] L) ≠ 0)
  rw [eq_div_iff hcard]
  calc
    @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S))
          _ _ _ _ σ hLattice.1 hLattice.2 *
        (Fintype.card (L ≃ₐ[K] L) : ℚ) =
        @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S × ℤ))
          _ _ _ _ σ hProduct.1 hProduct.2 := by
      rw [← hIntegerValue]
      exact hMultiplicative.symm
    _ =
        @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (extendedFullLogLattice L S))
          _ _ _ _ σ hExtended.1 hExtended.2 :=
      hExtendedProduct.symm
    _ =
        ∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ) :=
      hExtendedValue
theorem

sUnit_herbrandQuotient_eq_stabilizerProduct_div_card

L1366 ↗
Documentation

For the actual S-unit group, the finite roots-of-unity kernel has Herbrand quotient one, so the logarithmic lattice formula transfers unchanged.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section ActualSUnitHerbrand
Lean source · full declaration
theorem sUnit_herbrandQuotient_eq_stabilizerProduct_div_card
    (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 _sUnitAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S) :=
      sUnitMulDistribMulAction K L S hS
    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)
          (SUnitGroup (K := L) S) σ,
      @herbrandQuotient
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S)
          _ _ _ _ σ h.1 h.2 =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let sUnitAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup (K := L) S) :=
    sUnitMulDistribMulAction K L S hS
  let latticeAction :
      DistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup.fullLogLattice (K := L) S) :=
    fullLogLatticeDistribMulAction K L S hS
  let latticeMultiplicativeAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (Multiplicative
          (SUnitGroup.fullLogLattice (K := L) S)) :=
    multiplicativeDistribMulAction
  let orbitFintype :
      Fintype
        (MulAction.orbitRel.Quotient
          (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S)) :=
    Fintype.ofFinite _
  let stabilizerFintype :
      ∀ ω :
          MulAction.orbitRel.Quotient
            (L ≃ₐ[K] L)
            (SUnitGroup.LogPlace (K := L) S),
        Fintype (permutationOrbitStabilizer ω) :=
    fun _ => Fintype.ofFinite _
  let torsionAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (CommGroup.torsion
          (SUnitGroup (K := L) S)) :=
    stableSubgroupMulDistribMulAction
      (CommGroup.torsion
        (SUnitGroup (K := L) S))
      (sUnitTorsion_stable K L hS)
  let torsionFinite :
      Finite
        (CommGroup.torsion
          (SUnitGroup (K := L) S)) :=
    sUnitTorsionFinite L S
  obtain ⟨hLattice, hLatticeValue⟩ :=
    fullLogLattice_herbrandQuotient_eq_stabilizerProduct_div_card
      K L hS σ hgen
  let latticeH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S))) :=
    hLattice.1
  let latticeHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S)) σ) :=
    hLattice.2
  let hTorsion :
      HerbrandQuotientDefined
        (L ≃ₐ[K] L)
        (CommGroup.torsion
          (SUnitGroup (K := L) S)) σ :=
    ⟨inferInstance, inferInstance⟩
  let torsionH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (CommGroup.torsion
            (SUnitGroup (K := L) S))) :=
    hTorsion.1
  let torsionHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (CommGroup.torsion
            (SUnitGroup (K := L) S)) σ) :=
    hTorsion.2
  let hSUnit :=
    herbrandQuotientDefined_middle_of_left_right
      (CommGroup.torsion
        (SUnitGroup (K := L) S)).subtype
      (sUnitFullLogMulHom L S)
      (stableSubgroup_subtype_equivariant
        (CommGroup.torsion
          (SUnitGroup (K := L) S))
        (sUnitTorsion_stable K L hS))
      (sUnitFullLogMulHom_equivariant K L hS)
      (sUnitTorsion_fullLog_exact L S)
      (CommGroup.torsion
        (SUnitGroup (K := L) S)).subtype_injective
      (sUnitFullLogMulHom_surjective L S)
      σ hgen hTorsion hLattice
  let sUnitH0Finite :
      Finite
        (HerbrandH0
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S)) :=
    hSUnit.1
  let sUnitHMinusOneFinite :
      Finite
        (HerbrandHMinusOne
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S) σ) :=
    hSUnit.2
  have hMultiplicative :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := SUnitGroup (K := L) S) σ =
        herbrandQuotient
            (G := L ≃ₐ[K] L)
            (A := CommGroup.torsion
              (SUnitGroup (K := L) S)) σ *
          herbrandQuotient
            (G := L ≃ₐ[K] L)
            (A := Multiplicative
              (SUnitGroup.fullLogLattice (K := L) S)) σ :=
    herbrandQuotient_multiplicative_of_shortExact
      (CommGroup.torsion
        (SUnitGroup (K := L) S)).subtype
      (sUnitFullLogMulHom L S)
      (stableSubgroup_subtype_equivariant
        (CommGroup.torsion
          (SUnitGroup (K := L) S))
        (sUnitTorsion_stable K L hS))
      (sUnitFullLogMulHom_equivariant K L hS)
      (sUnitTorsion_fullLog_exact L S)
      (CommGroup.torsion
        (SUnitGroup (K := L) S)).subtype_injective
      (sUnitFullLogMulHom_surjective L S)
      σ hgen
  have hTorsionValue :
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := CommGroup.torsion
            (SUnitGroup (K := L) S)) σ = 1 :=
    herbrandQuotient_eq_one_of_finite_module
      σ hgen
  refine ⟨hSUnit, ?_⟩
  calc
    @herbrandQuotient
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S)
          _ _ _ _ σ hSUnit.1 hSUnit.2 =
        @herbrandQuotient
            (L ≃ₐ[K] L)
            (CommGroup.torsion
              (SUnitGroup (K := L) S))
            _ _ _ _ σ hTorsion.1 hTorsion.2 *
          @herbrandQuotient
            (L ≃ₐ[K] L)
            (Multiplicative
              (SUnitGroup.fullLogLattice (K := L) S))
            _ _ _ _ σ hLattice.1 hLattice.2 :=
      hMultiplicative
    _ =
        @herbrandQuotient
          (L ≃ₐ[K] L)
          (Multiplicative
            (SUnitGroup.fullLogLattice (K := L) S))
          _ _ _ _ σ hLattice.1 hLattice.2 := by
      rw [hTorsionValue, one_mul]
    _ =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) :=
      hLatticeValue
theorem

finitePlace_stabilizer_eq_idealStabilizer

L1597 ↗
Documentation

Stabilizing a finite place is equivalent to stabilizing its underlying prime ideal.

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem finitePlace_stabilizer_eq_idealStabilizer
    (P : HeightOneSpectrum (𝓞 L)) :
    letI _finitePlaceAction :=
      finitePlaceMulAction K L
    MulAction.stabilizer (L ≃ₐ[K] L) P =
      MulAction.stabilizer (L ≃ₐ[K] L) P.asIdeal := by
  let finitePlaceAction :=
    finitePlaceMulAction K L
  ext σ
  simp only [MulAction.mem_stabilizer_iff]
  change
    finitePlaceEquiv K L σ P = P ↔
      σ • P.asIdeal = P.asIdeal
  rw [HeightOneSpectrum.ext_iff,
    finitePlaceEquiv_asIdeal,
    Ideal.pointwise_smul_def]
  change
    Ideal.map
          (NumberField.RingOfIntegers.mapAlgEquiv
            σ).toRingEquiv.toRingHom P.asIdeal =
        P.asIdeal ↔
      Ideal.map
          (MulSemiringAction.toRingHom
            (L ≃ₐ[K] L) (𝓞 L) σ) P.asIdeal =
        P.asIdeal
  have hhom :
      (NumberField.RingOfIntegers.mapAlgEquiv
          σ).toRingEquiv.toRingHom =
        MulSemiringAction.toRingHom
          (L ≃ₐ[K] L) (𝓞 L) σ := by
    ext x
    rfl
  rw [hhom]
def

finiteLogPlaceLocalDegree

L1634 ↗
Documentation

The finite local degree at the place P, in the standard ramification-index times inertia-degree form [L_P : K_p] = e(P/p) f(P/p).

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · statement
def finiteLogPlaceLocalDegree
    (P : HeightOneSpectrum (𝓞 L)) : ℕ
theorem

finitePlace_stabilizer_card_eq_localDegree

L1642 ↗
Documentation

The stabilizer of a finite place has order equal to its local degree.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · full declaration
theorem finitePlace_stabilizer_card_eq_localDegree
    [IsGalois K L]
    (P : HeightOneSpectrum (𝓞 L)) :
    letI _finitePlaceAction :=
      finitePlaceMulAction K L
    Nat.card
        (MulAction.stabilizer (L ≃ₐ[K] L) P) =
      finiteLogPlaceLocalDegree K L P := by
  let finitePlaceAction :=
    finitePlaceMulAction K L
  rw [finitePlace_stabilizer_eq_idealStabilizer K L P]
  unfold finiteLogPlaceLocalDegree
  let p := P.asIdeal.under (𝓞 K)
  have hp : p ≠ ⊥ :=
    Ideal.under_ne_bot (𝓞 K) P.ne_bot
  let quotientFinite : Finite ((𝓞 K) ⧸ p) :=
    Ring.HasFiniteQuotients.finiteQuotient hp
  let residueFinite : Finite p.ResidueField :=
    inferInstance
  let residuePerfect : PerfectField p.ResidueField :=
    inferInstance
  exact
    Ideal.card_stabilizer_eq p P.asIdeal
theorem

stableFinitePlace_stabilizer_card_eq_localDegree

L1668 ↗
Documentation

Passing to a stable finite set does not change the stabilizer or the finite local degree of one of its places.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · full declaration
theorem stableFinitePlace_stabilizer_card_eq_localDegree
    [IsGalois K L]
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (v : S) :
    letI _stableAction :=
      stableFinitePlaceMulAction K L S hS
    Nat.card
        (MulAction.stabilizer (L ≃ₐ[K] L) v) =
      finiteLogPlaceLocalDegree K L v := by
  let stableAction :=
    stableFinitePlaceMulAction K L S hS
  let finitePlaceAction :=
    finitePlaceMulAction K L
  rw [show
    MulAction.stabilizer (L ≃ₐ[K] L) v =
        MulAction.stabilizer
          (L ≃ₐ[K] L)
          (v : HeightOneSpectrum (𝓞 L)) by
      ext σ
      simp only [MulAction.mem_stabilizer_iff]
      change
        (⟨finitePlaceEquiv K L σ v, _⟩ : S) = v ↔
          finitePlaceEquiv K L σ v = v
      exact Subtype.ext_iff]
  exact
    finitePlace_stabilizer_card_eq_localDegree
      K L v
def

logPlaceLocalDegree

L1701 ↗
Documentation

The local degree attached to a logarithmic place. At an archimedean place it is 1 or 2; at a finite place it is e(P/p) f(P/p).

Source context 8 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
open scoped Classical in
Lean source · statement
def logPlaceLocalDegree
    (S : Finset (HeightOneSpectrum (𝓞 L)))
    (q : SUnitGroup.LogPlace (K := L) S) : ℕ
theorem

logPlace_stabilizer_card_eq_localDegree

L1713 ↗
Documentation

For every actual logarithmic place, the order of its Galois stabilizer is its local degree.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · full declaration
theorem logPlace_stabilizer_card_eq_localDegree
    [IsGalois K L]
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S)
    (q : SUnitGroup.LogPlace (K := L) S) :
    letI _logPlaceAction :=
      logPlaceMulAction K L S hS
    Nat.card
        (MulAction.stabilizer (L ≃ₐ[K] L) q) =
      logPlaceLocalDegree K L S q := by
  let stableAction :=
    stableFinitePlaceMulAction K L S hS
  let logPlaceAction :=
    logPlaceMulAction K L S hS
  cases q with
  | inl w =>
      unfold logPlaceLocalDegree
      rw [show
        MulAction.stabilizer
              (L ≃ₐ[K] L)
              (Sum.inl w :
                SUnitGroup.LogPlace (K := L) S) =
            MulAction.stabilizer (L ≃ₐ[K] L) w by
          ext σ
          simp only [MulAction.mem_stabilizer_iff]
          change Sum.inl (σ • w) = Sum.inl w ↔
            σ • w = w
          simp]
      exact
        NumberField.InfinitePlace.card_stabilizer
  | inr v =>
      unfold logPlaceLocalDegree
      rw [show
        MulAction.stabilizer
              (L ≃ₐ[K] L)
              (Sum.inr v :
                SUnitGroup.LogPlace (K := L) S) =
            MulAction.stabilizer (L ≃ₐ[K] L) v by
          ext σ
          simp only [MulAction.mem_stabilizer_iff]
          change Sum.inr (σ • v) = Sum.inr v ↔
            σ • v = v
          simp]
      exact
        stableFinitePlace_stabilizer_card_eq_localDegree
          K L hS v
theorem

permutationOrbitStabilizer_card_eq_logPlaceLocalDegree

L1762 ↗
Documentation

The canonical representative of every logarithmic-place orbit has stabilizer order equal to its local degree.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · full declaration
theorem permutationOrbitStabilizer_card_eq_logPlaceLocalDegree
    [IsGalois K L]
    {S : Finset (HeightOneSpectrum (𝓞 L))}
    (hS : IsGaloisStableFinitePlaces K L S) :
    let ρ :=
      logPlacePermutationHom K L S hS
    letI _indexAction :
        MulAction (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S) :=
      permutationMulAction ρ
    ∀ ω :
        MulAction.orbitRel.Quotient
          (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S),
      Nat.card (permutationOrbitStabilizer ω) =
        logPlaceLocalDegree K L S ω.out := by
  dsimp only
  intro ω
  exact
    logPlace_stabilizer_card_eq_localDegree
      K L hS ω.out
theorem

sUnit_herbrandQuotient_eq_localDegreeProduct_div_card

L1787 ↗
Documentation

The Herbrand quotient in local-degree form: h(G, L^S) = |G|⁻¹ ∏_{p ∈ S} [L_P : K_p], with the archimedean places included in the logarithmic place set.

Source context 7 commands

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

open scoped BigOperators NumberField nonZeroDivisors Pointwise
open IsDedekindDomain Module
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type*) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
section LocalDegreeInterpretation
Lean source · full declaration
theorem sUnit_herbrandQuotient_eq_localDegreeProduct_div_card
    (K L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [IsGalois 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 _sUnitAction :
        MulDistribMulAction (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S) :=
      sUnitMulDistribMulAction K L S hS
    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)
          (SUnitGroup (K := L) S) σ,
      @herbrandQuotient
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S)
          _ _ _ _ σ h.1 h.2 =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (logPlaceLocalDegree K L S ω.out : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) := by
  dsimp only
  let ρ :=
    logPlacePermutationHom K L S hS
  let indexAction :
      MulAction (L ≃ₐ[K] L)
        (SUnitGroup.LogPlace (K := L) S) :=
    permutationMulAction ρ
  let sUnitAction :
      MulDistribMulAction (L ≃ₐ[K] L)
        (SUnitGroup (K := L) S) :=
    sUnitMulDistribMulAction K L S hS
  let orbitFintype :
      Fintype
        (MulAction.orbitRel.Quotient
          (L ≃ₐ[K] L)
          (SUnitGroup.LogPlace (K := L) S)) :=
    Fintype.ofFinite _
  let stabilizerFintype :
      ∀ ω :
          MulAction.orbitRel.Quotient
            (L ≃ₐ[K] L)
            (SUnitGroup.LogPlace (K := L) S),
        Fintype (permutationOrbitStabilizer ω) :=
    fun _ => Fintype.ofFinite _
  obtain ⟨hSUnit, hSUnitValue⟩ :=
    sUnit_herbrandQuotient_eq_stabilizerProduct_div_card
      K L hS σ hgen
  refine ⟨hSUnit, ?_⟩
  calc
    @herbrandQuotient
          (L ≃ₐ[K] L)
          (SUnitGroup (K := L) S)
          _ _ _ _ σ hSUnit.1 hSUnit.2 =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (Fintype.card
            (permutationOrbitStabilizer ω) : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) :=
      hSUnitValue
    _ =
        (∏ ω :
            MulAction.orbitRel.Quotient
              (L ≃ₐ[K] L)
              (SUnitGroup.LogPlace (K := L) S),
          (logPlaceLocalDegree K L S ω.out : ℚ)) /
          (Fintype.card (L ≃ₐ[K] L) : ℚ) := by
      congr 1
      apply Finset.prod_congr rfl
      intro ω _
      norm_cast
      rw [← Nat.card_eq_fintype_card]
      exact
        permutationOrbitStabilizer_card_eq_logPlaceLocalDegree
          K L hS ω

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