Module

FiniteIdeleH2Injection.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.FiniteIdeleH2Injection

7 declarations indexed from sourceView source ↗

Module documentation

The principal-idele sequence in degree two

The actual principal ideles, relative ideles, and relative idele classes form a short exact sequence of Galois representations. Its long exact sequence is the source of the global degree-two diagonal injection.

Imports4

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Cohomology.Herbrand
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.IdeleClassPGroupH1
Nyll.GaloisCohomology.Cyclic.Herbrand.HerbrandLowDegree.TateComparison
Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Imported by3

instance

(anonymous instance)

L32 ↗

Source context 7 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]

Lean source · statement

instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L)

instance

(anonymous instance)

L35 ↗

Source context 8 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L

Lean source · statement

instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L)

instance

(anonymous instance)

L39 ↗

Source context 9 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L

Lean source · statement

instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup.ClassGroup K L)

def

finiteIdeleShortComplex

L43 ↗

ClassFieldTower.Martinet.Shafarevich.finiteIdeleShortComplex

Documentation

The concrete principal-idele sequence, regarded as Galois representations.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L

Lean source · statement

def finiteIdeleShortComplex : ShortComplex (Rep ℤ (Gal(L/K)))

theorem

finiteIdeleShortComplex_shortExact

L54 ↗

ClassFieldTower.Martinet.Shafarevich.finiteIdeleShortComplex_shortExact

Documentation

Short exactness is supplied by the actual principal subgroup and quotient.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L

Lean source · statement

theorem finiteIdeleShortComplex_shortExact : (finiteIdeleShortComplex K L).ShortExact

def

finitePrincipalIdeleH2Map

L65 ↗

ClassFieldTower.Martinet.Shafarevich.finitePrincipalIdeleH2Map

Documentation

The degree-two map induced by the actual inclusion of principal ideles.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L

Lean source · statement

def finitePrincipalIdeleH2Map :
    groupCohomology (finiteIdeleShortComplex K L).X₁ 2 →ₗ[ℤ]
      groupCohomology (finiteIdeleShortComplex K L).X₂ 2

theorem

finitePrincipalIdeleH2Map_injective_of_isPGroup

L73 ↗

ClassFieldTower.Martinet.Shafarevich.finitePrincipalIdeleH2Map_injective_of_isPGroup

Documentation

For a finite Galois p-extension, the actual inclusion of principal ideles is injective on H². Vanishing of idele-class H¹ is supplied by the class-field axiom, rather than assumed as an additional exactness input.

Source context 10 commands

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

open CategoryTheory NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open RelativeIdeleGroup.Cohomology
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [Algebra K L]
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup K L) :=
  relativeIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K))
    (RelativeIdeleGroup.principalSubgroup K L) :=
  principalIdeleMulDistribMulAction K L
local instance : MulDistribMulAction (Gal(L/K)) (RelativeIdeleGroup.ClassGroup K L) :=
  ideleClassMulDistribMulAction K L

Lean source · statement

theorem finitePrincipalIdeleH2Map_injective_of_isPGroup
    [NumberField L] [FiniteDimensional K L] [IsGalois K L]
    {p : ℕ} [Fact p.Prime] (hP : IsPGroup p (Gal(L/K))) :
    Function.Injective (finitePrincipalIdeleH2Map K L)

Module documentation

The principal-idele sequence in degree two

Declarations

(anonymous instance)

(anonymous instance)

(anonymous instance)

finiteIdeleShortComplex

finiteIdeleShortComplex_shortExact

finitePrincipalIdeleH2Map

finitePrincipalIdeleH2Map_injective_of_isPGroup