NYLL
Module

FinitePlaceUnramifiedH1Family.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceUnramifiedH1Family
7 declarations indexed from sourceView source ↗

Module documentation

The family of finite-place unramified H¹ spaces

The unramified continuous degree-one subspaces at every finite place are assembled into a dependent product module. Coordinatewise subtype inclusion embeds it in the corresponding product of local decomposition-group H¹ spaces.

Imports2
Imported by1

Declarations

instance

finitePlaceUnramifiedH1FamilyModule

L29 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1FamilyModule
Source context 6 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
Lean source · statement
instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
abbrev

FinitePlaceUnramifiedH1Family

L35 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceUnramifiedH1Family
Documentation

The dependent product of the unramified H¹ subspaces over all finite places.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev FinitePlaceUnramifiedH1Family : ModuleCat (ZMod p)
abbrev

FinitePlaceDecompositionH1Family

L41 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceDecompositionH1Family
Documentation

The dependent product of decomposition-group H¹ spaces over all finite places.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev FinitePlaceDecompositionH1Family : ModuleCat (ZMod p)
def

finitePlaceUnramifiedH1FamilyInclusion

L48 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1FamilyInclusion
Documentation

Coordinatewise subtype inclusion of every unramified local class into local H¹.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceUnramifiedH1FamilyInclusion :
    FinitePlaceUnramifiedH1Family F p →ₗ[ZMod p]
      FinitePlaceDecompositionH1Family F p
theorem

finitePlaceUnramifiedH1FamilyInclusion_apply

L55 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1FamilyInclusion_apply
Documentation

A component of the family inclusion is the ordinary submodule subtype inclusion.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceUnramifiedH1FamilyInclusion_apply
    (x : FinitePlaceUnramifiedH1Family F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceUnramifiedH1FamilyInclusion F p x v = (x v).1
theorem

finitePlaceUnramifiedH1FamilyInclusion_apply_apply

L63 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1FamilyInclusion_apply_apply
Documentation

Evaluation after family inclusion does not change an unramified character.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceUnramifiedH1FamilyInclusion_apply_apply
    (x : FinitePlaceUnramifiedH1Family F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceUnramifiedH1FamilyInclusion F p x v (Additive.ofMul sigma) =
      (x v).1 (Additive.ofMul sigma)
theorem

finitePlaceUnramifiedH1FamilyInclusion_injective

L72 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1FamilyInclusion_injective
Documentation

Coordinatewise inclusion of the unramified family is injective.

Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1FamilyModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceUnramifiedH1FamilyInclusion_injective :
    Function.Injective (finitePlaceUnramifiedH1FamilyInclusion F p)

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