Module

Herbrand.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.Herbrand

32 declarations indexed from sourceView source ↗

Module documentation

Herbrand cohomology of the relative idele class group

This file realizes the low-degree exact sequence on the actual relative idele group

1 → Lˣ → I_L → C_L → 1.

The Galois actions are the concrete conjugation actions from the tensor-product model of relative adeles. The class norm is descended from the determinant norm on relative ideles, and its relation with the Tate norm is proved from the Galois product formula.

Imports4

Imported by7

def

relativeIdeleMulDistribMulAction

L48 ↗

RelativeIdeleGroup.Cohomology.relativeIdeleMulDistribMulAction

Documentation

The natural Galois action on relative ideles, upgraded from the existing multiplicative action to an action by group automorphisms.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 relativeIdeleMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) where
  __ := RelativeIdeleGroup.relativeIdeleMulAction K L
  smul_one σ :=
    map_one (RelativeIdeleGroup.conjugationIdele K L σ)
  smul_mul σ a b :=
    map_mul
      (RelativeIdeleGroup.conjugationIdele K L σ) a b

theorem

principalRelativeIdele_smul_mem

L59 ↗

RelativeIdeleGroup.Cohomology.principalRelativeIdele_smul_mem

Source context 9 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 principalRelativeIdele_smul_mem
    (σ : L ≃ₐ[K] L)
    (a : RelativeIdeleGroup K L)
    (ha :
      a ∈ RelativeIdeleGroup.principalSubgroup K L) :
    σ • a ∈
      RelativeIdeleGroup.principalSubgroup K L

def

ideleClassMulDistribMulAction

L76 ↗

RelativeIdeleGroup.Cohomology.ideleClassMulDistribMulAction

Documentation

The actual quotient Galois action on the relative idele class group, upgraded to an action by group automorphisms.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 ideleClassMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L)

def

principalIdeleMulDistribMulAction

L88 ↗

RelativeIdeleGroup.Cohomology.principalIdeleMulDistribMulAction

Documentation

The restricted Galois action on the actual subgroup of principal relative ideles.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 principalIdeleMulDistribMulAction :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L)

def

ideleClassNorm

L99 ↗

RelativeIdeleGroup.Cohomology.ideleClassNorm

Documentation

The norm on relative ideles, descended through principal ideles to the actual idele class groups.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 ideleClassNorm :
    RelativeIdeleGroup.ClassGroup K L →*
      IdeleClassGroup K

theorem

ideleClassNorm_mk

L116 ↗

RelativeIdeleGroup.Cohomology.ideleClassNorm_mk

Source context 9 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
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 · statement

theorem ideleClassNorm_mk
    (a : RelativeIdeleGroup K L) :
    ideleClassNorm K L
        (QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) =
      QuotientGroup.mk'
        (IdeleGroup.principalSubgroup K)
        (RelativeIdeleGroup.norm K L a)

abbrev

IdeleClassNormQuotient

L127 ↗

RelativeIdeleGroup.Cohomology.IdeleClassNormQuotient

Documentation

The concrete norm quotient C_K / N_{L/K} C_L.

Source context 8 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev IdeleClassNormQuotient

instance

(anonymous instance)

L132 ↗

Source context 9 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions

Lean source · statement

instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L)

instance

(anonymous instance)

L137 ↗

Source context 10 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L)

instance

(anonymous instance)

L142 ↗

Source context 11 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L

Lean source · statement

instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L)

theorem

relativeIdele_smul_def

L149 ↗

RelativeIdeleGroup.Cohomology.relativeIdele_smul_def

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem relativeIdele_smul_def
    (σ : L ≃ₐ[K] L)
    (a : RelativeIdeleGroup K L) :
    σ • a =
      RelativeIdeleGroup.conjugationIdele K L σ a

theorem

ideleClass_smul_mk

L158 ↗

RelativeIdeleGroup.Cohomology.ideleClass_smul_mk

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem ideleClass_smul_mk
    (σ : L ≃ₐ[K] L)
    (a : RelativeIdeleGroup K L) :
    σ • QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K L) a =
      QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K L)
        (σ • a)

theorem

principalIdele_smul_coe

L170 ↗

RelativeIdeleGroup.Cohomology.principalIdele_smul_coe

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem principalIdele_smul_coe
    (σ : L ≃ₐ[K] L)
    (a :
      RelativeIdeleGroup.principalSubgroup K L) :
    ((σ • a :
        RelativeIdeleGroup.principalSubgroup K L) :
      RelativeIdeleGroup K L) =
        σ • (a : RelativeIdeleGroup K L)

theorem

principalIdeleSubtype_equivariant

L184 ↗

RelativeIdeleGroup.Cohomology.principalIdeleSubtype_equivariant

Documentation

Equivariance of the principal-idele inclusion.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem principalIdeleSubtype_equivariant :
    ∀ (σ : L ≃ₐ[K] L)
      (a : RelativeIdeleGroup.principalSubgroup K L),
      (RelativeIdeleGroup.principalSubgroup K L).subtype
          (σ • a) =
        σ •
          (RelativeIdeleGroup.principalSubgroup K L).subtype
            a

theorem

ideleClassQuotientMap_equivariant

L198 ↗

RelativeIdeleGroup.Cohomology.ideleClassQuotientMap_equivariant

Documentation

Equivariance of the actual quotient map I_L → C_L.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem ideleClassQuotientMap_equivariant :
    ∀ (σ : L ≃ₐ[K] L)
      (a : RelativeIdeleGroup K L),
      QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L)
          (σ • a) =
        σ • QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a

theorem

relativeIdele_tateNorm_eq_inclusion_norm

L214 ↗

RelativeIdeleGroup.Cohomology.relativeIdele_tateNorm_eq_inclusion_norm

Documentation

On relative ideles the Tate norm is the inclusion of the determinant norm. This is the Galois product formula, not a separate class-field hypothesis.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] in

Lean source · statement

theorem relativeIdele_tateNorm_eq_inclusion_norm
    (a : RelativeIdeleGroup K L) :
    tateNorm (L ≃ₐ[K] L)
        (RelativeIdeleGroup K L) a =
      RelativeIdeleGroup.inclusion K L
        (RelativeIdeleGroup.norm K L a)

theorem

classInclusion_ideleClassNorm_eq_tateNorm

L227 ↗

RelativeIdeleGroup.Cohomology.classInclusion_ideleClassNorm_eq_tateNorm

Documentation

The class norm agrees, after Galois descent, with the Tate norm on the actual relative idele class group.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] in

Lean source · statement

theorem classInclusion_ideleClassNorm_eq_tateNorm
    (c : RelativeIdeleGroup.ClassGroup K L) :
    RelativeIdeleGroup.classInclusion K L
        (ideleClassNorm K L c) =
      tateNorm (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) c

theorem

ideleClass_fixedSubgroup_eq_galoisFixed

L254 ↗

RelativeIdeleGroup.Cohomology.ideleClass_fixedSubgroup_eq_galoisFixed

Documentation

The fixed subgroup used by Tate cohomology is the concrete Galois-fixed subgroup from idele-class descent.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem ideleClass_fixedSubgroup_eq_galoisFixed :
    fixedSubgroup (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) =
      RelativeIdeleGroup.galoisFixedClassSubgroup K L

def

baseIdeleClassToFixed

L267 ↗

RelativeIdeleGroup.Cohomology.baseIdeleClassToFixed

Documentation

Galois descent as a homomorphism from the base idele class group to the Tate fixed subgroup.

Source context 12 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

def baseIdeleClassToFixed :
    IdeleClassGroup K →*
      fixedSubgroup (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L)

theorem

baseIdeleClassToFixed_coe

L283 ↗

RelativeIdeleGroup.Cohomology.baseIdeleClassToFixed_coe

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem baseIdeleClassToFixed_coe
    (c : IdeleClassGroup K) :
    ((baseIdeleClassToFixed K L c :
        fixedSubgroup (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)) :
      RelativeIdeleGroup.ClassGroup K L) =
        RelativeIdeleGroup.classInclusion K L c

def

baseIdeleClassEquivFixed

L294 ↗

RelativeIdeleGroup.Cohomology.baseIdeleClassEquivFixed

Documentation

Galois descent packaged as the multiplicative equivalence C_K ≃ C_L^G required by the H⁰ calculation.

Source context 12 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

def baseIdeleClassEquivFixed :
    IdeleClassGroup K ≃*
      fixedSubgroup (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L)

theorem

baseIdeleClassEquivFixed_coe

L319 ↗

RelativeIdeleGroup.Cohomology.baseIdeleClassEquivFixed_coe

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] in

Lean source · statement

theorem baseIdeleClassEquivFixed_coe
    (c : IdeleClassGroup K) :
    ((baseIdeleClassEquivFixed K L c :
        fixedSubgroup (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L)) :
      RelativeIdeleGroup.ClassGroup K L) =
        RelativeIdeleGroup.classInclusion K L c

theorem

ideleClassNorm_range_map_equivFixed

L331 ↗

RelativeIdeleGroup.Cohomology.ideleClassNorm_range_map_equivFixed

Documentation

Under Galois descent, the image of the class norm is exactly the Tate-norm subgroup of the fixed idele classes.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] in

Lean source · statement

theorem ideleClassNorm_range_map_equivFixed :
    (ideleClassNorm K L).range.map
        (baseIdeleClassEquivFixed K L).toMonoidHom =
      (tateNormSubgroup (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L)).subgroupOf
          (fixedSubgroup (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L))

theorem

ideleClass_normKernelSubgroup_eq_ker

L366 ↗

RelativeIdeleGroup.Cohomology.ideleClass_normKernelSubgroup_eq_ker

Documentation

The Tate norm kernel on idele classes is the kernel of the descended idele-class norm. Injectivity of C_K → C_L is the descent input.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] in

Lean source · statement

theorem ideleClass_normKernelSubgroup_eq_ker :
    normKernelSubgroup (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) =
      MonoidHom.ker (ideleClassNorm K L)

def

ideleClassHerbrandHMinusOneEquiv

L387 ↗

RelativeIdeleGroup.Cohomology.ideleClassHerbrandHMinusOneEquiv

Documentation

The negative-first Tate group for the actual idele class module, displayed as norm-one classes modulo augmentation classes.

Source context 12 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

def ideleClassHerbrandHMinusOneEquiv
    (σ : L ≃ₐ[K] L) :
    HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) σ ≃*
      normKernelSubgroup (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L) ⧸
        (augmentationSubgroup (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L) σ).subgroupOf
            (normKernelSubgroup (L ≃ₐ[K] L)
              (RelativeIdeleGroup.ClassGroup K L))

instance

ideleClassNormQuotient_baseIsMulCommutative

L403 ↗

RelativeIdeleGroup.Cohomology.ideleClassNormQuotient_baseIsMulCommutative

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
section NormQuotientIdentification

Lean source · statement

instance ideleClassNormQuotient_baseIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K)

def

ideleClassHerbrandH0EquivNormQuotient

L409 ↗

RelativeIdeleGroup.Cohomology.ideleClassHerbrandH0EquivNormQuotient

Documentation

The degree-zero Tate group of the actual idele class group is the class-norm quotient C_K / N_{L/K} C_L.

Source context 14 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
section NormQuotientIdentification
local instance ideleClassNormQuotient_baseIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

def ideleClassHerbrandH0EquivNormQuotient :
    HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) ≃*
      IdeleClassNormQuotient K L

theorem

ideleClassNorm_index_eq_herbrandH0_card

L429 ↗

RelativeIdeleGroup.Cohomology.ideleClassNorm_index_eq_herbrandH0_card

Documentation

The norm index is the cardinality of the actual degree-zero Tate cohomology group. This statement is valid without silently assigning a positive finite index to an infinite quotient.

Source context 15 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
section NormQuotientIdentification
local instance ideleClassNormQuotient_baseIsMulCommutative :
    IsMulCommutative (IdeleClassGroup K) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
omit [NumberField L] in

Lean source · statement

theorem ideleClassNorm_index_eq_herbrandH0_card :
    (ideleClassNorm K L).range.index =
      Nat.card
        (HerbrandH0 (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L))

theorem

principalIdele_ideleClass_exact

L444 ↗

RelativeIdeleGroup.Cohomology.principalIdele_ideleClass_exact

Documentation

Exactness at I_L of Lˣ → I_L → C_L.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem principalIdele_ideleClass_exact :
    ∀ a : RelativeIdeleGroup K L,
      QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a = 1 ↔
        ∃ p : RelativeIdeleGroup.principalSubgroup K L,
          (RelativeIdeleGroup.principalSubgroup K L).subtype p =
            a

theorem

principalIdele_ideleClass_shortExact

L457 ↗

RelativeIdeleGroup.Cohomology.principalIdele_ideleClass_shortExact

Documentation

The complete short-exactness data for the actual principal-idele inclusion and idele-class quotient.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem principalIdele_ideleClass_shortExact :
    (∀ (σ : L ≃ₐ[K] L)
      (p : RelativeIdeleGroup.principalSubgroup K L),
      (RelativeIdeleGroup.principalSubgroup K L).subtype
          (σ • p) =
        σ •
          (RelativeIdeleGroup.principalSubgroup K L).subtype p) ∧
    (∀ (σ : L ≃ₐ[K] L)
      (a : RelativeIdeleGroup K L),
      QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L)
          (σ • a) =
        σ • QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a) ∧
    (∀ a : RelativeIdeleGroup K L,
      QuotientGroup.mk'
          (RelativeIdeleGroup.principalSubgroup K L) a = 1 ↔
        ∃ p : RelativeIdeleGroup.principalSubgroup K L,
          (RelativeIdeleGroup.principalSubgroup K L).subtype p =
            a) ∧
    Function.Injective
      (RelativeIdeleGroup.principalSubgroup K L).subtype ∧
    Function.Surjective
      (QuotientGroup.mk'
        (RelativeIdeleGroup.principalSubgroup K L))

theorem

relativeIdele_herbrandQuotient_eq_principal_mul_class

L493 ↗

RelativeIdeleGroup.Cohomology.relativeIdele_herbrandQuotient_eq_principal_mul_class

Documentation

Herbrand-quotient multiplicativity for the actual exact sequence 1 → Lˣ → I_L → C_L → 1.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem relativeIdele_herbrandQuotient_eq_principal_mul_class
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ)
    [Finite
      (HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L))]
    [Finite
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) σ)]
    [Finite
      (HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup K L))]
    [Finite
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup K L) σ)]
    [Finite
      (HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L))]
    [Finite
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.ClassGroup K L) σ)] :
    herbrandQuotient
        (G := L ≃ₐ[K] L)
        (A := RelativeIdeleGroup K L) σ =
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A :=
            RelativeIdeleGroup.principalSubgroup K L) σ *
        herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := RelativeIdeleGroup.ClassGroup K L) σ

theorem

ideleClassHerbrandQuotientDefined_of_principal_relative

L569 ↗

RelativeIdeleGroup.Cohomology.ideleClassHerbrandQuotientDefined_of_principal_relative

Documentation

Once the Herbrand quotients of principal ideles and relative ideles have been computed, the actual idele-class quotient is automatically defined and satisfies the multiplicativity identity. This is the connection point for the unrestricted local-factor and S-unit calculations.

Source context 13 commands

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

open scoped BigOperators NumberField
open NumberField
noncomputable section
open CyclicCohomology.ProfiniteCohomology.Herbrand
open CyclicCohomology
namespace RelativeIdeleGroup
namespace Cohomology
variable
    (K L : Type) [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
section Actions
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L
local instance :
    MulDistribMulAction (L ≃ₐ[K] L)
      (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
omit [NumberField L] [IsGalois K L] in

Lean source · statement

theorem ideleClassHerbrandQuotientDefined_of_principal_relative
    (σ : L ≃ₐ[K] L)
    (hgen : ∀ τ : L ≃ₐ[K] L,
      τ ∈ Subgroup.zpowers σ)
    [Finite
      (HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L))]
    [Finite
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup.principalSubgroup K L) σ)]
    [Finite
      (HerbrandH0 (L ≃ₐ[K] L)
        (RelativeIdeleGroup K L))]
    [Finite
      (HerbrandHMinusOne (L ≃ₐ[K] L)
        (RelativeIdeleGroup K L) σ)] :
    ∃ hC :
        HerbrandQuotientDefined
          (L ≃ₐ[K] L)
          (RelativeIdeleGroup.ClassGroup K L) σ,
      herbrandQuotient
          (G := L ≃ₐ[K] L)
          (A := RelativeIdeleGroup K L) σ =
        herbrandQuotient
            (G := L ≃ₐ[K] L)
            (A :=
              RelativeIdeleGroup.principalSubgroup K L) σ *
          @herbrandQuotient
            (L ≃ₐ[K] L)
            (RelativeIdeleGroup.ClassGroup K L)
            inferInstance inferInstance inferInstance
            (ideleClassMulDistribMulAction K L)
            σ hC.1 hC.2

Module documentation

Herbrand cohomology of the relative idele class group

Declarations