NYLL
Module

Principal.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Principal
7 declarations indexed from sourceView source ↗

Module documentation

Principal ideles and their Galois module structure

This module exposes the diagonal embedding and idele class group, identifies field units with principal relative ideles, and transports low-degree Tate cohomology across that identification.

Imports4
Imported by8

Declarations

def

fieldUnitsEquivPrincipalIdeles

L38 ↗
Documentation

The field-unit group is multiplicatively equivalent to the actual subgroup of principal relative ideles.

Source context 6 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def fieldUnitsEquivPrincipalIdeles :
    Lˣ ≃*
      RelativeIdeleGroup.principalSubgroup K L
theorem

fieldUnitsEquivPrincipalIdeles_coe

L50 ↗
Source context 7 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem fieldUnitsEquivPrincipalIdeles_coe
    (x : Lˣ) :
    ((fieldUnitsEquivPrincipalIdeles K L x :
        RelativeIdeleGroup.principalSubgroup K L) :
      RelativeIdeleGroup K L) =
        RelativeIdeleGroup.principalIdele K L x
theorem

fieldUnitsEquivPrincipalIdeles_smul

L61 ↗
Documentation

The identification of field units with principal ideles is equivariant for the genuine Galois actions.

Source context 7 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in
Lean source · full declaration
theorem fieldUnitsEquivPrincipalIdeles_smul
    (σ : L ≃ₐ[K] L) (x : Lˣ) :
    letI :=
      galoisGroupFieldUnitsMulDistribMulAction K L
    letI :=
      relativeIdeleMulDistribMulAction K L
    letI :=
      principalIdeleMulDistribMulAction K L
    fieldUnitsEquivPrincipalIdeles K L (σ • x) =
      σ • fieldUnitsEquivPrincipalIdeles K L x := by
  let _ :=
    galoisGroupFieldUnitsMulDistribMulAction K L
  let _ :=
    relativeIdeleMulDistribMulAction K L
  let _ :=
    principalIdeleMulDistribMulAction K L
  apply Subtype.ext
  change
    RelativeIdeleGroup.principalIdele K L
        (Units.mapEquiv σ.toMulEquiv x) =
      σ • RelativeIdeleGroup.principalIdele K L x
  exact
    (RelativeIdeleGroup.smul_principalIdele
      K L σ x).symm
def

fieldUnitsHerbrandH0EquivPrincipalIdeles

L88 ↗
Documentation

Degree-zero Tate cohomology of principal ideles is the actual degree-zero cohomology of Lˣ.

Source context 6 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def fieldUnitsHerbrandH0EquivPrincipalIdeles :
    letI :=
      galoisGroupFieldUnitsMulDistribMulAction K L
    letI :=
      relativeIdeleMulDistribMulAction K L
    letI :=
      principalIdeleMulDistribMulAction K L
    HerbrandH0 (L ≃ₐ[K] L) Lˣ ≃*
      HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) := by
  letI :=
    galoisGroupFieldUnitsMulDistribMulAction K L
  letI :=
    relativeIdeleMulDistribMulAction K L
  letI :=
    principalIdeleMulDistribMulAction K L
  exact
    herbrandH0EquivariantMulEquiv
      (fieldUnitsEquivPrincipalIdeles K L)
      (fieldUnitsEquivPrincipalIdeles_smul K L)
def

fieldUnitsHerbrandHMinusOneEquivPrincipalIdeles

L111 ↗
Documentation

Degree-minus-one Tate cohomology of principal ideles is the actual degree-minus-one cohomology of Lˣ.

Source context 6 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · full declaration
def fieldUnitsHerbrandHMinusOneEquivPrincipalIdeles
    (σ : L ≃ₐ[K] L) :
    letI :=
      galoisGroupFieldUnitsMulDistribMulAction K L
    letI :=
      relativeIdeleMulDistribMulAction K L
    letI :=
      principalIdeleMulDistribMulAction K L
    HerbrandHMinusOne (L ≃ₐ[K] L) Lˣ σ ≃*
      HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) σ := by
  letI :=
    galoisGroupFieldUnitsMulDistribMulAction K L
  letI :=
    relativeIdeleMulDistribMulAction K L
  letI :=
    principalIdeleMulDistribMulAction K L
  exact
    herbrandHMinusOneEquivariantMulEquiv
      (fieldUnitsEquivPrincipalIdeles K L)
      (fieldUnitsEquivPrincipalIdeles_smul K L) σ
theorem

principalIdelesHerbrandQuotientDefined

L135 ↗
Documentation

A defined Herbrand quotient for field units supplies the corresponding defined quotient for the actual principal-idele subgroup.

Source context 7 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · full declaration
theorem principalIdelesHerbrandQuotientDefined
    (σ : L ≃ₐ[K] L)
    (h :
      letI :=
        galoisGroupFieldUnitsMulDistribMulAction K L
      HerbrandQuotientDefined
        (L ≃ₐ[K] L) Lˣ σ) :
    letI :=
      relativeIdeleMulDistribMulAction K L
    letI :=
      principalIdeleMulDistribMulAction K L
    HerbrandQuotientDefined
      (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) σ := by
  let _ :=
    galoisGroupFieldUnitsMulDistribMulAction K L
  let _ :=
    relativeIdeleMulDistribMulAction K L
  let _ :=
    principalIdeleMulDistribMulAction K L
  let _ : Finite
      (HerbrandH0 (L ≃ₐ[K] L) Lˣ) :=
    h.1
  let _ : Finite
      (HerbrandHMinusOne
        (L ≃ₐ[K] L) Lˣ σ) :=
    h.2
  exact
    ⟨herbrandH0Finite_of_equivariantMulEquiv
        (fieldUnitsEquivPrincipalIdeles K L)
        (fieldUnitsEquivPrincipalIdeles_smul K L),
      herbrandHMinusOneFinite_of_equivariantMulEquiv
        (fieldUnitsEquivPrincipalIdeles K L)
        (fieldUnitsEquivPrincipalIdeles_smul K L) σ⟩
theorem

fieldUnits_herbrandQuotient_eq_principalIdeles

L172 ↗
Documentation

The field-unit and principal-idele Herbrand quotients agree.

Source context 7 commands

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

noncomputable section
open RelativeIdeleGroup.Cohomology
open LocalClassFieldTheory
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · full declaration
theorem fieldUnits_herbrandQuotient_eq_principalIdeles
    (σ : L ≃ₐ[K] L)
    (h :
      letI :=
        galoisGroupFieldUnitsMulDistribMulAction K L
      HerbrandQuotientDefined
        (L ≃ₐ[K] L) Lˣ σ) :
    letI _fieldAction :=
      galoisGroupFieldUnitsMulDistribMulAction K L
    letI _relativeAction :=
      relativeIdeleMulDistribMulAction K L
    letI _principalAction :=
      principalIdeleMulDistribMulAction K L
    let hP :=
      principalIdelesHerbrandQuotientDefined
        K L σ h
    @herbrandQuotient
        (L ≃ₐ[K] L) Lˣ _ _ _
        (galoisGroupFieldUnitsMulDistribMulAction K L)
        σ h.1 h.2 =
      @herbrandQuotient
        (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L)
        _ _ _
        (principalIdeleMulDistribMulAction K L)
        σ hP.1 hP.2 := by
  let _ :=
    galoisGroupFieldUnitsMulDistribMulAction K L
  let _ :=
    relativeIdeleMulDistribMulAction K L
  let _ :=
    principalIdeleMulDistribMulAction K L
  let _ : Finite
      (HerbrandH0 (L ≃ₐ[K] L) Lˣ) :=
    h.1
  let _ : Finite
      (HerbrandHMinusOne
        (L ≃ₐ[K] L) Lˣ σ) :=
    h.2
  exact
    herbrandQuotient_eq_of_equivariantMulEquiv
      (fieldUnitsEquivPrincipalIdeles K L)
      (fieldUnitsEquivPrincipalIdeles_smul K L) σ

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