NYLL
Module

LocalIntrinsicUnramifiedH1Line.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.LocalIntrinsicUnramifiedH1Line
19 declarations indexed from sourceView source ↗

Module documentation

The intrinsic unramified local first-cohomology line

Restriction to intrinsic inertia defines the unramified submodule of continuous first-cohomology characters. The residue-degree character modulo p spans this submodule, and its scalar parametrization is injective.

Imports5
Imported by3

Declarations

instance

localUnramifiedH1LineTopology

L35 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedH1LineTopology
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p)
instance

localUnramifiedH1LineDiscreteTopology

L37 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedH1LineDiscreteTopology
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p)
instance

localUnramifiedH1LineZModAddCommGroup

L40 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedH1LineZModAddCommGroup
Source context 10 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p)
instance

localUnramifiedH1LineAddCommGroup

L43 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedH1LineAddCommGroup
Source context 11 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
Lean source · statement
instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G))
instance

localUnramifiedH1LineModule

L48 ↗
ClassFieldTower.Martinet.Shafarevich.localUnramifiedH1LineModule
Source context 12 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
Lean source · statement
instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
theorem

continuousH1_smul_apply

L53 ↗
ClassFieldTower.Martinet.Shafarevich.continuousH1_smul_apply
Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1_smul_apply
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (a : ZMod p) (chi : ContinuousH1ZMod (p := p) (G := G))
    (sigma : Additive G) :
    (a • chi) sigma = a * chi sigma
abbrev

localIntrinsicInertiaSubgroup

L67 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicInertiaSubgroup
Documentation

Intrinsic local inertia, the kernel of the local residue-degree map.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
abbrev localIntrinsicInertiaSubgroup :
    Subgroup Gal(SeparableClosure K / K)
def

localIntrinsicH1InertiaRestrictionAddHom

L72 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicH1InertiaRestrictionAddHom
Documentation

Restriction of additive continuous characters to intrinsic local inertia.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def localIntrinsicH1InertiaRestrictionAddHom :
    ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K)) →+
      ContinuousH1ZMod (p := p) (G := localIntrinsicInertiaSubgroup K) where
  toFun chi :=
    { toFun := fun sigma ↦ chi (Additive.ofMul sigma.1)
      map_zero' := chi.map_zero
      map_add' := fun _ _ ↦ chi.map_add _ _
      continuous_toFun := chi.continuous_toFun.comp continuous_subtype_val }
  map_zero' := by ext sigma; rfl
  map_add' := by intro chi psi; ext sigma; rfl
def

localIntrinsicH1InertiaRestriction

L84 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicH1InertiaRestriction
Documentation

Linear restriction of additive continuous characters to local inertia.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def localIntrinsicH1InertiaRestriction :
    ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K)) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := localIntrinsicInertiaSubgroup K)
abbrev

localIntrinsicUnramifiedH1

L90 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicUnramifiedH1
Documentation

Intrinsic unramified local H¹: continuous characters trivial on inertia.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
abbrev localIntrinsicUnramifiedH1 :
    Submodule (ZMod p)
      (ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K)))
def

localResidueDegreeModPH1

L96 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1
Documentation

The reduction modulo p of local residue degree, in additive H¹ form.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def localResidueDegreeModPH1 :
    ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K))
theorem

localResidueDegreeModPH1_apply

L102 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1_apply
Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localResidueDegreeModPH1_apply
    (sigma : Gal(SeparableClosure K/K)) :
    localResidueDegreeModPH1 K p (Additive.ofMul sigma) =
      zHatReduction p (Fact.out : p.Prime).pos
        (localResidueDegree K sigma).toAdd
theorem

localResidueDegreeModPH1_mem_unramified

L110 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1_mem_unramified
Documentation

The reduced residue-degree character is unramified.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localResidueDegreeModPH1_mem_unramified :
    localResidueDegreeModPH1 K p ∈ localIntrinsicUnramifiedH1 K p
def

localResidueDegreeModPH1Line

L121 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1Line
Documentation

The reduced residue-degree character spans the intrinsic unramified line.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def localResidueDegreeModPH1Line :
    ZMod p →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K)) where
  toFun a := a • localResidueDegreeModPH1 K p
  map_add' a b := by rw [add_smul]
  map_smul' a b := by simp [smul_smul]
def

scaledZHatReductionCharacter

L128 ↗
ClassFieldTower.Martinet.Shafarevich.scaledZHatReductionCharacter
Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def scaledZHatReductionCharacter (a : ZMod p) :
    ZHatMul →ₜ* Multiplicative (ZMod p) where
  toFun z := Multiplicative.ofAdd
    (a * zHatReduction p (Fact.out : p.Prime).pos z.toAdd)
  map_one' := by
    apply Multiplicative.ext
    simp
  map_mul' x y := by
    apply Multiplicative.ext
    simp [mul_add]
  continuous_toFun := by
    let scale : Multiplicative (ZMod p) → Multiplicative (ZMod p) :=
      fun x ↦ Multiplicative.ofAdd (a * x.toAdd)
    have hscale : Continuous scale := continuous_of_discreteTopology
    exact hscale.comp
      (zHatReductionMul p (Fact.out : p.Prime).pos).continuous_toFun
theorem

continuousCharacter_zHat_eq_scaledReduction

L145 ↗
ClassFieldTower.Martinet.Shafarevich.continuousCharacter_zHat_eq_scaledReduction
Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousCharacter_zHat_eq_scaledReduction
    (f : ZHatMul →ₜ* Multiplicative (ZMod p)) :
    f = scaledZHatReductionCharacter p (f generator).toAdd
theorem

localIntrinsicUnramifiedH1_eq_smul

L176 ↗
ClassFieldTower.Martinet.Shafarevich.localIntrinsicUnramifiedH1_eq_smul
Documentation

Every intrinsic unramified local character is a scalar multiple of reduced residue degree.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localIntrinsicUnramifiedH1_eq_smul
    (chi : ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K/K)))
    (hchi : chi ∈ localIntrinsicUnramifiedH1 K p) :
    ∃ a : ZMod p, chi = a • localResidueDegreeModPH1 K p
theorem

localResidueDegreeModPH1Line_range

L226 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1Line_range
Documentation

The intrinsic unramified local H¹ submodule is exactly the residue-degree line.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localResidueDegreeModPH1Line_range :
    LinearMap.range (localResidueDegreeModPH1Line K p) =
      localIntrinsicUnramifiedH1 K p
theorem

localResidueDegreeModPH1Line_injective

L238 ↗
ClassFieldTower.Martinet.Shafarevich.localResidueDegreeModPH1Line_injective
Documentation

The reduced residue-degree parametrization is injective.

Source context 13 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open ClassFieldTower.Cohomology.ProfiniteInteger
open ClassFormation LocalClassFieldTheory
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
variable (p : ℕ) [Fact p.Prime]
local instance localUnramifiedH1LineTopology : TopologicalSpace (ZMod p) := ⊥
local instance localUnramifiedH1LineDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localUnramifiedH1LineZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localUnramifiedH1LineAddCommGroup
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    AddCommGroup (ContinuousH1ZMod (p := p) (G := G)) :=
  ContinuousAddMonoidHom.instAddCommGroup (Additive G) (ZMod p)
local instance localUnramifiedH1LineModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localResidueDegreeModPH1Line_injective :
    Function.Injective (localResidueDegreeModPH1Line K p)

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