Module

ArithmeticStageH2LocalRamificationCharacter.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageH2LocalRamificationCharacter

5 declarations indexed from sourceView source ↗

Module documentation

The inertia character of an arithmetic-stage local lift

Compare a local solution with the unramified solution constructed from the vanishing of unramified local H². Their difference is a continuous ZMod p-valued character on the absolute decomposition group. Its restriction to inertia records the given solution's ramification, independently of the chosen unramified reference solution.

Imports3

Imported by2

instance

arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup

L42 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup

Source context 13 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
variable (xU : continuousCohomologyZModPLifted p
  (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
variable (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
variable (s : finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU)
variable (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
  arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v)

Lean source · statement

instance arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup :
    AddCommGroup (ZMod p)

def

arithmeticStageH2LocalRamificationCharacter

L48 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocalRamificationCharacter

Documentation

The ramification character of a local solution, obtained by subtracting the constructed unramified solution and restricting to absolute inertia.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
variable (xU : continuousCohomologyZModPLifted p
  (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
variable (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
variable (s : finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU)
variable (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
  arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v)
local instance arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup :
    AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

def arithmeticStageH2LocalRamificationCharacter :
    finitePlaceAbsoluteInertiaSubgroup F v →ₜ* Multiplicative (ZMod p)

theorem

arithmeticStageH2LocalRamificationCharacter_apply

L58 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocalRamificationCharacter_apply

Documentation

On inertia, the character is just the given lift's coefficient coordinate; the unramified reference contributes zero.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
variable (xU : continuousCohomologyZModPLifted p
  (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
variable (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
variable (s : finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU)
variable (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
  arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v)
local instance arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup :
    AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

theorem arithmeticStageH2LocalRamificationCharacter_apply
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    arithmeticStageH2LocalRamificationCharacter F p U xU v s hs sigma =
      Multiplicative.ofAdd (s sigma.1).left.down

theorem

arithmeticStageH2LocalRamificationCharacter_eq_one_iff

L70 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocalRamificationCharacter_eq_one_iff

Documentation

The local solution is unramified precisely when its inertia character is trivial.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
variable (xU : continuousCohomologyZModPLifted p
  (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
variable (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
variable (s : finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU)
variable (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
  arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v)
local instance arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup :
    AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

theorem arithmeticStageH2LocalRamificationCharacter_eq_one_iff :
    arithmeticStageH2LocalRamificationCharacter F p U xU v s hs = 1 ↔
      finitePlaceAbsoluteInertiaSubgroup F v ≤ s.toMonoidHom.ker

theorem

arithmeticStageH2LocalRamificationCharacter_extends

L81 ↗

ClassFieldTower.Martinet.Shafarevich.arithmeticStageH2LocalRamificationCharacter_extends

Documentation

The ramification character extends to the absolute decomposition group, with an explicit extension supplied by the difference of the two local lifts.

Source context 14 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology ClassFieldTower.Martinet ClassFieldTower.ProP
open ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
variable (xU : continuousCohomologyZModPLifted p
  (MaxEverywhereUnramifiedProPGaloisGroup F p ⧸
    (U : Subgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))) 2)
variable (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
variable (s : finitePlaceAbsoluteDecompositionGroup F v →ₜ* DegreeTwoCentralExtension xU)
variable (hs : (H2CocycleExtension.projection (degreeTwoCocycleRepresentative xU)).comp s =
  arithmeticStageFinitePlaceAbsoluteQuotientMap F p U v)
local instance arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup :
    AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

theorem arithmeticStageH2LocalRamificationCharacter_extends :
    ∃ chi : finitePlaceAbsoluteDecompositionGroup F v →ₜ* Multiplicative (ZMod p),
      chi.comp (subgroupInclusion (finitePlaceAbsoluteInertiaSubgroup F v)) =
        arithmeticStageH2LocalRamificationCharacter F p U xU v s hs

Module documentation

The inertia character of an arithmetic-stage local lift

Declarations

arithmeticStageH2LocalRamificationCanonicalZModAddCommGroup

arithmeticStageH2LocalRamificationCharacter

arithmeticStageH2LocalRamificationCharacter_apply

arithmeticStageH2LocalRamificationCharacter_eq_one_iff

arithmeticStageH2LocalRamificationCharacter_extends