Module

UnramifiedLocalIntegerUnitsH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.UnramifiedLocalIntegerUnitsH2

3 declarations indexed from sourceView source ↗

Module documentation

Integer-unit H² in an actual unramified local extension

The canonical unramified Frobenius and the existing unit-norm theorem identify degree-two cohomology of the actual integer-unit representation with a zero Tate norm quotient. In particular every two-cocycle has an integer-unit primitive, including in residue characteristic dividing the extension degree.

Imports2

Imported by2

instance

(anonymous instance)

L41 ↗

Source context 15 commands

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

open CategoryTheory
open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open LocalClassFieldTheory LocalFieldTheory LocalFieldTheory.IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
variable [IsNonarchimedeanLocalField L]
variable [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
variable [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
variable [IsUnramifiedValuedExtension K L]

-- Fix the canonical integer-unit action once for both endpoints.

Lean source · statement

instance : MulDistribMulAction Gal(L / K) 𝒪[L]ˣ

theorem

unramifiedLocalIntegerUnitsH2_subsingleton

L46 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedLocalIntegerUnitsH2_subsingleton

Documentation

The actual integer-unit representation of a finite unramified local extension has zero degree-two cohomology.

Source context 16 commands

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

open CategoryTheory
open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open LocalClassFieldTheory LocalFieldTheory LocalFieldTheory.IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
variable [IsNonarchimedeanLocalField L]
variable [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
variable [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
variable [IsUnramifiedValuedExtension K L]

-- Fix the canonical integer-unit action once for both endpoints.
local instance : MulDistribMulAction Gal(L / K) 𝒪[L]ˣ :=
  galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L

Lean source · statement

theorem unramifiedLocalIntegerUnitsH2_subsingleton :
    Subsingleton (groupCohomology (Rep.ofMulDistribMulAction Gal(L / K) 𝒪[L]ˣ) 2)

theorem

unramifiedLocalIntegerUnitsTwoCocycle_isCoboundary

L60 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedLocalIntegerUnitsTwoCocycle_isCoboundary

Documentation

Every actual integer-unit two-cocycle in an unramified local extension has an integer-unit one-cochain primitive.

Source context 16 commands

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

open CategoryTheory
open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open LocalClassFieldTheory LocalFieldTheory LocalFieldTheory.IsNonarchimedeanLocalField
open CyclicCohomology.ProfiniteCohomology.Herbrand
variable (K L : Type) [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
variable [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
variable [IsNonarchimedeanLocalField L]
variable [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
variable [IsIntegralClosure 𝒪[L] 𝒪[K] L] [Module.Finite 𝒪[K] 𝒪[L]]
variable [IsUnramifiedValuedExtension K L]

-- Fix the canonical integer-unit action once for both endpoints.
local instance : MulDistribMulAction Gal(L / K) 𝒪[L]ˣ :=
  galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L

Lean source · statement

theorem unramifiedLocalIntegerUnitsTwoCocycle_isCoboundary :
    ∀ c : groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L / K) 𝒪[L]ˣ),
      ∃ b : Gal(L / K) → Additive 𝒪[L]ˣ,
        (groupCohomology.d₁₂ (Rep.ofMulDistribMulAction Gal(L / K) 𝒪[L]ˣ)).hom b = c.1

Module documentation

Integer-unit H² in an actual unramified local extension

Declarations

(anonymous instance)

unramifiedLocalIntegerUnitsH2_subsingleton

unramifiedLocalIntegerUnitsTwoCocycle_isCoboundary