NYLL
Module

FinitePlaceH1RamificationLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FinitePlaceH1RamificationLocalization
16 declarations indexed from sourceView source ↗

Module documentation

Finite-place ramification restriction of absolute H¹ characters

Absolute continuous mod-p characters first restrict to a finite-place decomposition subgroup and then to its inertia subgroup. The resulting maps are assembled over all finite places, and their kernels recover the local unramified subspaces.

Imports9
Imported by3

Declarations

instance

finitePlaceH1RamificationCanonicalZModAddCommGroup

L36 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1RamificationCanonicalZModAddCommGroup
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

finitePlaceH1RamificationCharacterTopology

L39 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1RamificationCharacterTopology
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 KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))
instance

finitePlaceH1RamificationCharacterDiscreteTopology

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1RamificationCharacterDiscreteTopology
Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
Lean source · statement
instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))
instance

finitePlaceH1RamificationModule

L46 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1RamificationModule
Source context 9 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
Lean source · statement
instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
def

finitePlaceDecompositionCharacterToH1AddHom

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionCharacterToH1AddHom
Documentation

Reinterpret a decomposition-group multiplicative character as an additive continuous degree-one character.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def finitePlaceDecompositionCharacterToH1AddHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Additive
        (finitePlaceAbsoluteDecompositionGroup F v →ₜ*
          Multiplicative (ZMod p)) →+
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) where
  toFun chi := h1OfCharacter (Additive.toMul chi)
  map_zero' := by
    ext sigma
    rfl
  map_add' chi psi := by
    ext sigma
    rfl
def

finitePlaceDecompositionCharacterToH1

L69 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionCharacterToH1
Documentation

The character-to-H¹ reinterpretation as a ZMod p-linear map.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceDecompositionCharacterToH1
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceDecompositionContinuousZModCharacterModP F p v →ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)
theorem

finitePlaceDecompositionCharacterToH1_apply

L89 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionCharacterToH1_apply
Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceDecompositionCharacterToH1_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : finitePlaceDecompositionContinuousZModCharacterModP F p v)
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceDecompositionCharacterToH1 F p v chi (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (finitePlaceAbsoluteDecompositionGroup F v →ₜ*
              Multiplicative (ZMod p))
          from chi)) sigma :=
  rfl
def

finitePlaceAbsoluteH1DecompositionRestriction

L102 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1DecompositionRestriction
Documentation

Restriction of an absolute character to the additive H¹ of the decomposition subgroup.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1DecompositionRestriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)
theorem

finitePlaceAbsoluteH1DecompositionRestriction_apply

L111 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1DecompositionRestriction_apply
Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceAbsoluteH1DecompositionRestriction_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p)
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceAbsoluteH1DecompositionRestriction F p v chi (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
          from chi)) (finitePlaceAbsoluteDecompositionInclusion F v sigma) :=
  rfl
def

finitePlaceAbsoluteH1RamificationRestriction

L124 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamificationRestriction
Documentation

The ramification component of an absolute character at v, obtained by restricting further from decomposition to inertia.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1RamificationRestriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteInertiaSubgroup F v)
theorem

finitePlaceAbsoluteH1RamificationRestriction_apply

L133 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamificationRestriction_apply
Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceAbsoluteH1RamificationRestriction_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p)
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    finitePlaceAbsoluteH1RamificationRestriction F p v chi (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
          from chi))
        (finitePlaceAbsoluteDecompositionInclusion F v
          (finitePlaceAbsoluteInertiaInclusion F v sigma)) :=
  rfl
theorem

finitePlaceAbsoluteH1DecompositionRestriction_mem_unramified_iff

L147 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1DecompositionRestriction_mem_unramified_iff
Documentation

The decomposition restriction is unramified exactly when its inertia component vanishes.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1DecompositionRestriction_mem_unramified_iff
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p) :
    finitePlaceAbsoluteH1DecompositionRestriction F p v chi ∈
        finitePlaceUnramifiedH1 F p v ↔
      finitePlaceAbsoluteH1RamificationRestriction F p v chi = 0
abbrev

FinitePlaceH1RamificationLocalizationTarget

L156 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceH1RamificationLocalizationTarget
Documentation

The dependent product of all finite-place inertia-character spaces.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev FinitePlaceH1RamificationLocalizationTarget
def

finitePlaceAbsoluteH1RamificationRestrictionFamily

L161 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamificationRestrictionFamily
Documentation

All finite-place ramification components of an absolute continuous mod-p character.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1RamificationRestrictionFamily :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      FinitePlaceH1RamificationLocalizationTarget F p
theorem

finitePlaceAbsoluteH1RamificationRestrictionFamily_apply

L168 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamificationRestrictionFamily_apply
Documentation

Each component of the family is the ramification restriction at that place.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1RamificationRestrictionFamily_apply
    (chi : absoluteContinuousZModCharacterModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteH1RamificationRestrictionFamily F p chi v =
      finitePlaceAbsoluteH1RamificationRestriction F p v chi
theorem

finitePlaceAbsoluteH1RamificationRestrictionFamily_apply_apply

L177 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1RamificationRestrictionFamily_apply_apply
Documentation

Evaluation of a family component is restriction along inertia and decomposition inclusions.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1RamificationCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1RamificationCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1RamificationCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) :=
  discreteTopology_bot _
local instance finitePlaceH1RamificationModule
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceAbsoluteH1RamificationRestrictionFamily_apply_apply
    (chi : absoluteContinuousZModCharacterModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    finitePlaceAbsoluteH1RamificationRestrictionFamily F p chi v
        (Additive.ofMul sigma) =
      (Additive.toMul
        (show Additive
            (Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod p))
          from chi))
        (finitePlaceAbsoluteDecompositionInclusion F v
          (finitePlaceAbsoluteInertiaInclusion F v sigma)) :=
  rfl

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