ModuleUnramifiedInfinitePlaceBlockH2.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.UnramifiedInfinitePlaceBlockH2
3 declarations indexed from sourceView source ↗ Module documentation
H² of an unramified infinite-place idele block
The stabilizer of an unramified infinite place has order one. Its higher cohomology therefore vanishes, and the proved Shapiro and tensor-block comparisons transfer this to the actual archimedean idele factor. No cyclicity of the global Galois group is assumed.
Declarations
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory NumberField
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable (v : InfinitePlace K)
local notation "w" => chosenInfinitePlaceAbove (L := L) v
local notation "u" => infinitePlaceAbsoluteValueExtension v w
(chosenInfinitePlaceAbove_comap (L := L) v)
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory NumberField
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable (v : InfinitePlace K)
local notation "w" => chosenInfinitePlaceAbove (L := L) v
local notation "u" => infinitePlaceAbsoluteValueExtension v w
(chosenInfinitePlaceAbove_comap (L := L) v)
local instance : MulDistribMulAction Gal(L / K) (v.Completion ⊗[K] L)ˣ :=
scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
ClassFieldTower.Martinet.Shafarevich.unramifiedInfinitePlaceBlockH2_subsingleton
DocumentationThe actual infinite tensor-unit factor has zero degree-two cohomology when the chosen place above it is unramified.
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory NumberField
open scoped NumberField TensorProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology CyclicCohomology
open AlgebraicNumberTheory.Valuations HilbertRamification LocalClassFieldTheory
variable (K L : Type) [Field K] [NumberField K]
variable [Field L] [NumberField L] [Algebra K L]
variable [FiniteDimensional K L] [IsGalois K L]
variable (v : InfinitePlace K)
local notation "w" => chosenInfinitePlaceAbove (L := L) v
local notation "u" => infinitePlaceAbsoluteValueExtension v w
(chosenInfinitePlaceAbove_comap (L := L) v)
local instance : MulDistribMulAction Gal(L / K) (v.Completion ⊗[K] L)ˣ :=
scalarTensorUnitsAction (K := K) (L := L) (A := v.Completion)
local instance : MulDistribMulAction (absoluteValueDecompositionGroup K u.1)
(LocalizedCompletion v.1 u)ˣ :=
decompositionGroupLocalUnitsAction v.1 v.isNontrivial u
omit [NumberField K] [NumberField L] in