NYLL
Module

FinitePlaceFieldUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceFieldUnitsH2
11 declarations indexed from sourceView source ↗

Module documentation

H² of finite-place field-unit blocks

The actual tensor block is an induced representation. Shapiro and the chosen decomposition-group equivalence identify its cohomology with the local field-unit cohomology. Finite Galois p-extensions therefore have cyclic H² on every finite tensor block, with at most n elements of n-torsion.

Imports4
Imported by2

Declarations

instance

fieldH2DecompositionAction

L36 ↗
ClassFieldTower.Martinet.Shafarevich.fieldH2DecompositionAction
Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v)
instance

fieldH2InducedCommGroup

L41 ↗
ClassFieldTower.Martinet.Shafarevich.fieldH2InducedCommGroup
Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
Lean source · statement
instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v)
instance

fieldH2InducedAction

L45 ↗
ClassFieldTower.Martinet.Shafarevich.fieldH2InducedAction
Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
Lean source · statement
instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v)
instance

fieldH2TensorAction

L49 ↗
ClassFieldTower.Martinet.Shafarevich.fieldH2TensorAction
Source context 13 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
Lean source · statement
instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ
def

finiteTensorRepIsoInduced

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finiteTensorRepIsoInduced
Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
def finiteTensorRepIsoInduced
    (v : HeightOneSpectrum (𝓞 K)) :
    Rep.ofMulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ ≅
      Rep.ofMulDistribMulAction Gal(L / K)
        (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v)
def

chosenFieldCohomologyIso

L71 ↗
ClassFieldTower.Martinet.Shafarevich.chosenFieldCohomologyIso
Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
def chosenFieldCohomologyIso
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    groupCohomology (Rep.ofMulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v)) n ≅
    groupCohomology (Rep.ofAlgebraAutOnUnits
      (ChosenFinitePlaceBaseCompletion (K := K) v)
      (ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v)) n
def

tensorCohomologyIsoInduced

L96 ↗
ClassFieldTower.Martinet.Shafarevich.tensorCohomologyIsoInduced
Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
def tensorCohomologyIsoInduced
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (v.adicCompletion K ⊗[K] L)ˣ) n ≅
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v)) n
def

chosenInducedCohomologyIso

L104 ↗
ClassFieldTower.Martinet.Shafarevich.chosenInducedCohomologyIso
Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
def chosenInducedCohomologyIso
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v)) n ≅
    groupCohomology (Rep.ofMulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v)) n
def

finitePlaceFieldUnitsCohomologyIso

L117 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceFieldUnitsCohomologyIso
Documentation

The actual finite tensor block has the cohomology of the chosen local Galois field-unit representation, in every degree.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
Lean source · statement
def finitePlaceFieldUnitsCohomologyIso
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (v.adicCompletion K ⊗[K] L)ˣ) n ≅
    groupCohomology (Rep.ofAlgebraAutOnUnits
      (ChosenFinitePlaceBaseCompletion (K := K) v)
      (ChosenFinitePlaceLocalizedCompletion (K := K) (L := L) v)) n
theorem

finitePGroupFinitePlaceFieldUnitsH2_finite_isAddCyclic

L129 ↗
ClassFieldTower.Martinet.Shafarevich.finitePGroupFinitePlaceFieldUnitsH2_finite_isAddCyclic
Documentation

Finite-place tensor H² is finite and cyclic for any finite Galois p-extension.

Source context 15 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
omit [NumberField L] in
Lean source · statement
theorem finitePGroupFinitePlaceFieldUnitsH2_finite_isAddCyclic
    (p : ℕ) [Fact p.Prime] (hP : IsPGroup p Gal(L/K))
    (v : HeightOneSpectrum (𝓞 K)) :
    Finite (groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (v.adicCompletion K ⊗[K] L)ˣ) 2) ∧
    IsAddCyclic (groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (v.adicCompletion K ⊗[K] L)ˣ) 2)
theorem

finitePGroupFinitePlaceFieldUnitsH2_torsion_natCard_le

L153 ↗
ClassFieldTower.Martinet.Shafarevich.finitePGroupFinitePlaceFieldUnitsH2_torsion_natCard_le
Documentation

Positive n-torsion in each actual finite-place tensor H² has at most n elements.

Source context 15 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField TensorProduct ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification
open LocalClassFieldTheory LocalFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
local instance fieldH2DecompositionAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedFieldUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupLocalUnitsAction (K := K) (L := L) v
local instance fieldH2InducedCommGroup (v : HeightOneSpectrum (𝓞 K)) :
    CommGroup (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  Subgroup.toCommGroup _
local instance fieldH2InducedAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (ChosenFinitePlaceLocalPlaceBlock (K := K) (L := L) v) :=
  chosenFinitePlaceLocalPlaceBlockAction (K := K) (L := L) v
local instance fieldH2TensorAction (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K) (v.adicCompletion K ⊗[K] L)ˣ :=
  scalarTensorUnitsAction (K := K) (L := L) (A := v.adicCompletion K)
omit [NumberField L] in
Lean source · statement
theorem finitePGroupFinitePlaceFieldUnitsH2_torsion_natCard_le
    (p : ℕ) [Fact p.Prime] (hP : IsPGroup p Gal(L/K))
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) (hn : 0 < n) :
    Nat.card {x : groupCohomology (Rep.ofMulDistribMulAction Gal(L / K)
      (v.adicCompletion K ⊗[K] L)ˣ) 2 // n • x = 0} ≤ n

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