Module

UnramifiedFinitePlaceIntegralBlockH2.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.UnramifiedFinitePlaceIntegralBlockH2

7 declarations indexed from sourceView source ↗

Module documentation

H² of the actual unramified finite-place integral block

At an unramified finite place, integer-unit H² vanishes on the chosen localized extension. The actual decomposition-group action, the proved multiplicative Shapiro isomorphism, and the equivariant integral tensor decomposition transport this vanishing to the full global Galois group. No cyclicity of the global Galois group is assumed.

Imports15

Imported by3

instance

(anonymous instance)

L50 ↗

Source context 10 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.

Lean source · statement

instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v)

instance

(anonymous instance)

L56 ↗

Source context 11 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v

Lean source · statement

instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v)

instance

(anonymous instance)

L61 ↗

Source context 12 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceInducedIntegerUnitsAction (K := K) (L := L) v

Lean source · statement

instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v)

theorem

chosenFinitePlaceIntegerUnitsH2_subsingleton

L69 ↗

ClassFieldTower.Martinet.Shafarevich.chosenFinitePlaceIntegerUnitsH2_subsingleton

Documentation

The actual chosen decomposition-group representation on integer units has zero H² at an unramified finite place.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceInducedIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v
omit [NumberField L] in

Lean source · statement

theorem chosenFinitePlaceIntegerUnitsH2_subsingleton
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : ChosenFinitePlaceIsUnramified (K := K) (L := L) v) :
    Subsingleton (groupCohomology
      (Rep.ofMulDistribMulAction
        (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
        (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v)) 2)

theorem

chosenFinitePlaceInducedIntegerUnitsH2_subsingleton

L102 ↗

ClassFieldTower.Martinet.Shafarevich.chosenFinitePlaceInducedIntegerUnitsH2_subsingleton

Documentation

Shapiro transfers the actual unramified integer-unit vanishing to the full global Galois action on its induced local block.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceInducedIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v
omit [NumberField L] in

Lean source · statement

theorem chosenFinitePlaceInducedIntegerUnitsH2_subsingleton
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : ChosenFinitePlaceIsUnramified (K := K) (L := L) v) :
    Subsingleton (groupCohomology
      (Rep.ofMulDistribMulAction Gal(L / K)
        (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v)) 2)

theorem

unramifiedFinitePlaceIntegralBlockH2_subsingleton

L116 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedFinitePlaceIntegralBlockH2_subsingleton

Documentation

The actual integral tensor block at an unramified finite place has zero H² for the full, not necessarily cyclic, global Galois group.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceInducedIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v
omit [NumberField L] in

Lean source · statement

theorem unramifiedFinitePlaceIntegralBlockH2_subsingleton
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : ChosenFinitePlaceIsUnramified (K := K) (L := L) v) :
    Subsingleton (groupCohomology
      (Rep.ofMulDistribMulAction Gal(L / K)
        (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v)) 2)

theorem

unramifiedFinitePlaceIntegralBlockTwoCocycle_isCoboundary

L148 ↗

ClassFieldTower.Martinet.Shafarevich.unramifiedFinitePlaceIntegralBlockTwoCocycle_isCoboundary

Documentation

Every two-cocycle in the actual integral finite-place tensor block admits a primitive which stays inside that integral block.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField ValuativeRel NNReal
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]

-- Each of the three canonical representations is fixed once; their
-- coefficient types are distinct, so no competing action is introduced.
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction
      (ChosenFinitePlaceDecompositionGroup (K := K) (L := L) v)
      (ChosenFinitePlaceLocalizedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceDecompositionGroupIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (ChosenFinitePlaceInducedIntegerUnits (K := K) (L := L) v) :=
  chosenFinitePlaceInducedIntegerUnitsAction (K := K) (L := L) v
local instance (v : HeightOneSpectrum (𝓞 K)) :
    MulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v) :=
  relativeLocalTensorDecompositionIntegralUnitSubgroupAction (K := K) (L := L) v
omit [NumberField L] in

Lean source · statement

theorem unramifiedFinitePlaceIntegralBlockTwoCocycle_isCoboundary
    (v : HeightOneSpectrum (𝓞 K))
    (hunram : ChosenFinitePlaceIsUnramified (K := K) (L := L) v) :
    ∀ c : groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction Gal(L / K)
      (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v)),
      ∃ b : Gal(L / K) → Additive
          (relativeLocalTensorDecompositionIntegralUnitSubgroup (K := K) (L := L) v),
        (groupCohomology.d₁₂ (Rep.ofMulDistribMulAction Gal(L / K)
          (relativeLocalTensorDecompositionIntegralUnitSubgroup
            (K := K) (L := L) v))).hom b = c.1

Module documentation

H² of the actual unramified finite-place integral block

Declarations

(anonymous instance)

(anonymous instance)

(anonymous instance)

chosenFinitePlaceIntegerUnitsH2_subsingleton

chosenFinitePlaceInducedIntegerUnitsH2_subsingleton

unramifiedFinitePlaceIntegralBlockH2_subsingleton

unramifiedFinitePlaceIntegralBlockTwoCocycle_isCoboundary