Module

ArithmeticStageSupportedIdeleH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageSupportedIdeleH2

3 declarations indexed from sourceView source ↗

Module documentation

Integral idele primitives at the actual arithmetic stage

The open-normal arithmetic stage supplies both finite- and infinite-place unramifiedness. Thus its everywhere-integral relative idele subgroup has zero H², and every supported two-cocycle has an actual idele primitive. There are no new local vanishing, Shapiro, or glue hypotheses.

Imports2

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

instance

arithmeticStageSupportedH2IdeleAction

L36 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageSupportedH2IdeleAction

Source context 9 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.Cohomology ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "J" => relativeIdeleLocalTensorDecompositionSupportedSubgroup
  (K := F) (L := StageField) ∅

Lean source · statement

instance arithmeticStageSupportedH2IdeleAction : MulDistribMulAction Gal(StageField / F) J

theorem

openNormalArithmeticStage_supportedIdeleH2_subsingleton

L41 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_supportedIdeleH2_subsingleton

Documentation

The actual arithmetic stage has zero H² on everywhere-integral relative ideles.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.Cohomology ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "J" => relativeIdeleLocalTensorDecompositionSupportedSubgroup
  (K := F) (L := StageField) ∅
local instance arithmeticStageSupportedH2IdeleAction : MulDistribMulAction Gal(StageField / F) J :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := F) (L := StageField) ∅

Lean source · statement

theorem openNormalArithmeticStage_supportedIdeleH2_subsingleton :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction Gal(StageField / F) J) 2)

theorem

openNormalArithmeticStage_supportedIdeleTwoCocycle_isCoboundary

L50 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_supportedIdeleTwoCocycle_isCoboundary

Documentation

Every two-cocycle in the arithmetic stage's everywhere-integral relative ideles admits an actual one-cochain primitive in that subgroup.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ClassFieldTower.Cohomology ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "StageField" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "J" => relativeIdeleLocalTensorDecompositionSupportedSubgroup
  (K := F) (L := StageField) ∅
local instance arithmeticStageSupportedH2IdeleAction : MulDistribMulAction Gal(StageField / F) J :=
  relativeIdeleLocalTensorDecompositionSupportedSubgroupAction (K := F) (L := StageField) ∅

Lean source · statement

theorem openNormalArithmeticStage_supportedIdeleTwoCocycle_isCoboundary
    (f : Gal(StageField/F) × Gal(StageField/F) → J)
    (hf : groupCohomology.IsMulCocycle₂ f) : groupCohomology.IsMulCoboundary₂ f

Module documentation

Integral idele primitives at the actual arithmetic stage

Declarations

arithmeticStageSupportedH2IdeleAction

openNormalArithmeticStage_supportedIdeleH2_subsingleton

openNormalArithmeticStage_supportedIdeleTwoCocycle_isCoboundary