NYLL
Module

FinitePlaceAdicInertiaTransport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceAdicInertiaTransport
14 declarations indexed from sourceView source ↗

Module documentation

Inertia in the actual adic completion model

The canonical comparison of the two completions preserves their valuation relations. Uniqueness of the separable-closure valuation and naturality of residue degree therefore identify their inertia groups. This gives the exact unramified-H¹ criterion for the actual decomposition-to-adic transport.

Imports6
Imported by4

Declarations

instance

finitePlaceAdicInertiaSourceCharZero

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaSourceCharZero
Source context 9 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
Lean source · statement
instance finitePlaceAdicInertiaSourceCharZero : CharZero C
instance

finitePlaceAdicInertiaSourceValuativeRel

L36 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaSourceValuativeRel
Source context 10 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
Lean source · statement
instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C
instance

finitePlaceAdicInertiaSourceLocalField

L38 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaSourceLocalField
Source context 11 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
Lean source · statement
instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C
instance

finitePlaceAdicInertiaTargetValuativeRel

L40 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaTargetValuativeRel
Source context 12 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
Lean source · statement
instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C'
instance

finitePlaceAdicInertiaTargetLocalField

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaTargetLocalField
Source context 13 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C'
def

finitePlaceCompletionSeparableClosureRingEquiv

L47 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionSeparableClosureRingEquiv
Documentation

The completion comparison on separable closures, induced by the actual algebraic-closure comparison.

Source context 14 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
def finitePlaceCompletionSeparableClosureRingEquiv :
    SeparableClosure C ≃+* SeparableClosure C'
theorem

finitePlaceCompletionSeparableClosureRingEquiv_algebraMap

L54 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionSeparableClosureRingEquiv_algebraMap
Documentation

The comparison extends the canonical comparison of completed base fields.

Source context 14 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
theorem finitePlaceCompletionSeparableClosureRingEquiv_algebraMap (x : C) :
    finitePlaceCompletionSeparableClosureRingEquiv F v (algebraMap C (SeparableClosure C) x) =
      algebraMap C' (SeparableClosure C') (relativeFinitePlaceCompletionAlgEquiv v x)
theorem

finitePlaceCompletionSeparableGalois_conjugation

L66 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionSeparableGalois_conjugation
Documentation

Restricting semilinear conjugation to the separable parts commutes with the standard absolute-Galois comparison.

Source context 14 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
theorem finitePlaceCompletionSeparableGalois_conjugation
    (sigma : Field.absoluteGaloisGroup C) :
    LocalClassFieldTheory.semilinearGaloisGroupCongr C C'
      (SeparableClosure C) (SeparableClosure C')
      (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv
      (finitePlaceCompletionSeparableClosureRingEquiv F v)
      (finitePlaceCompletionSeparableClosureRingEquiv_algebraMap F v)
      (RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv C sigma) =
    RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv C'
      (finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv F v sigma)
theorem

finitePlaceCompletionResidueDegree_conjugation

L80 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionResidueDegree_conjugation
Documentation

The actual comparison of completion models preserves residue degree.

Source context 14 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
theorem finitePlaceCompletionResidueDegree_conjugation
    (sigma : Field.absoluteGaloisGroup C) :
    localResidueDegree C'
      (RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv C'
        (finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv F v sigma)) =
    localResidueDegree C
      (RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv
        C sigma)
theorem

finitePlaceDecompositionAdic_mem_inertia_iff

L100 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionAdic_mem_inertia_iff
Documentation

Actual finite-place inertia is precisely intrinsic adic inertia.

Source context 14 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
theorem finitePlaceDecompositionAdic_mem_inertia_iff
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv C'
        (finitePlaceDecompositionAdicContinuousMulEquiv F v sigma) ∈
      localIntrinsicInertiaSubgroup C' ↔
    sigma ∈ finitePlaceAbsoluteInertiaSubgroup F v
instance

finitePlaceAdicInertiaCoefficientTopology

L117 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaCoefficientTopology
Source context 15 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (n : ℕ+) [Fact (n : ℕ).Prime]
Lean source · statement
instance finitePlaceAdicInertiaCoefficientTopology : TopologicalSpace (ZMod (n : ℕ))
instance

finitePlaceAdicInertiaCoefficientDiscrete

L118 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaCoefficientDiscrete
Source context 16 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance finitePlaceAdicInertiaCoefficientTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance finitePlaceAdicInertiaCoefficientDiscrete : DiscreteTopology (ZMod (n : ℕ))
instance

finitePlaceAdicInertiaH1Module

L120 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicInertiaH1Module
Source context 17 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance finitePlaceAdicInertiaCoefficientTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceAdicInertiaCoefficientDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
Lean source · statement
instance finitePlaceAdicInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G))
theorem

finitePlaceDecompositionH1ToAdic_mem_unramified_iff

L125 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1ToAdic_mem_unramified_iff
Documentation

The actual adic H¹ transport preserves and reflects unramified characters.

Source context 18 commands

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

open NumberField IsDedekindDomain LocalClassFieldTheory
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (𝓞 F))
local notation "C" => AbsoluteValue.Completion (HeightOneSpectrum.adicAbv F v)
local notation "C'" => v.adicCompletion F
local instance finitePlaceAdicInertiaSourceCharZero : CharZero C :=
  charZero_of_injective_algebraMap (algebraMap F C).injective
local instance finitePlaceAdicInertiaSourceValuativeRel : ValuativeRel C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAdicInertiaSourceLocalField : IsNonarchimedeanLocalField C :=
  GlobalClassFieldTheory.Reciprocity.finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAdicInertiaTargetValuativeRel : ValuativeRel C' :=
  finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAdicInertiaTargetLocalField : IsNonarchimedeanLocalField C' :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (n : ℕ+) [Fact (n : ℕ).Prime]
local instance finitePlaceAdicInertiaCoefficientTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finitePlaceAdicInertiaCoefficientDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
local instance finitePlaceAdicInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod (n : ℕ)) (ContinuousH1ZMod (p := (n : ℕ)) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem finitePlaceDecompositionH1ToAdic_mem_unramified_iff
    (chi : ContinuousH1ZMod (p := (n : ℕ)) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    finitePlaceDecompositionH1ToAdic F (n : ℕ) v chi ∈ localStandardUnramifiedH1 C' n ↔
      chi ∈ finitePlaceUnramifiedH1 F (n : ℕ) v

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