NYLL
Module

FinitePlaceAbsoluteArtinCompatibility.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceAbsoluteArtinCompatibility
11 declarations indexed from sourceView source ↗

Module documentation

Actual global--local Artin compatibility for finite-place characters

The selected algebraic-localization embedding first gives equality of the finite Artin actions. Finite projections identify the maximal-abelian global value, and semilinear naturality transports its representative to the concrete adic completion. Consequently actual global character restriction and local reciprocity evaluate to the same value, without roots of unity in the base field.

Imports8
Imported by3

Declarations

def

finitePlaceAlgebraicClosureToAbsoluteCompletion

L37 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureToAbsoluteCompletion
Documentation

The selected global algebraic closure embedded into the absolute-value completion model used by finite global reciprocity.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
Lean source · full declaration
def finitePlaceAlgebraicClosureToAbsoluteCompletion :
    AlgebraicClosure F →ₐ[F] AlgebraicClosure (HeightOneSpectrum.adicAbv F v).Completion where
  toRingHom := (finitePlaceCompletionAlgebraicClosureRingEquiv F v).symm.toRingHom.comp
    (finitePlaceAlgebraicClosureEmbedding F v)
  commutes' x := by
    apply (finitePlaceCompletionAlgebraicClosureRingEquiv F v).injective
    change (finitePlaceCompletionAlgebraicClosureRingEquiv F v)
      ((finitePlaceCompletionAlgebraicClosureRingEquiv F v).symm
        (finitePlaceAlgebraicClosureEmbedding F v (algebraMap F (AlgebraicClosure F) x))) = _
    rw [RingEquiv.apply_symm_apply, finitePlaceAlgebraicClosureEmbedding_algebraMap]
    change _ = finitePlaceCompletionAlgebraicClosureRingEquiv F v
      (algebraMap (HeightOneSpectrum.adicAbv F v).Completion _ (algebraMap F _ x))
    rw [finitePlaceCompletionAlgebraicClosureRingEquiv_algebraMap,
      (relativeFinitePlaceCompletionAlgEquiv v).commutes]
theorem

finitePlaceAlgebraicClosureToAbsoluteCompletion_action

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureToAbsoluteCompletion_action
Documentation

The same embedding intertwines the actual decomposition action.

Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
Lean source · statement
theorem finitePlaceAlgebraicClosureToAbsoluteCompletion_action
    (sigma : Gal(AlgebraicClosure
      (HeightOneSpectrum.adicAbv F v).Completion/(HeightOneSpectrum.adicAbv F v).Completion))
    (x : AlgebraicClosure F) :
    sigma (finitePlaceAlgebraicClosureToAbsoluteCompletion F v x) =
      finitePlaceAlgebraicClosureToAbsoluteCompletion F v
        (((finitePlaceDecompositionGroupContinuousMulEquivAbsoluteGaloisGroup F v).symm
          sigma).val x)
instance

finitePlaceAbsoluteCompatibilitySourceValuativeRel

L83 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilitySourceValuativeRel
Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
Lean source · statement
instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion
instance

finitePlaceAbsoluteCompatibilitySourceLocalField

L87 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilitySourceLocalField
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
Lean source · statement
instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion
theorem

finitePlaceAbsoluteArtin_lift_maximalAbelian

L93 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteArtin_lift_maximalAbelian
Documentation

An actual local Artin representative restricts to the one-place maximal abelian global Artin value.

Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
Lean source · full declaration
theorem finitePlaceAbsoluteArtin_lift_maximalAbelian
    (a : (v.adicCompletion F)ˣ)
    (sigma : Gal(AlgebraicClosure
      (HeightOneSpectrum.adicAbv F v).Completion/(HeightOneSpectrum.adicAbv F v).Completion))
    (hsigma : (QuotientGroup.mk
        (show Field.absoluteGaloisGroup (HeightOneSpectrum.adicAbv F v).Completion from sigma) :
        Field.absoluteGaloisGroupAbelianization (HeightOneSpectrum.adicAbv F v).Completion) =
      absoluteLocalArtinMap (HeightOneSpectrum.adicAbv F v).Completion
        (finitePlaceLocalArtinInput v a)) :
    globalMaximalAbelianRestriction F
        ((finitePlaceDecompositionGroupContinuousMulEquivAbsoluteGaloisGroup F v).symm sigma).val =
      maximalAbelianGlobalArtin F (IdeleGroup.finitePlaceIdeleClass v a) := by
  let delta := (finitePlaceDecompositionGroupContinuousMulEquivAbsoluteGaloisGroup F v).symm sigma
  apply maximalAbelianGalois_ext_of_finite_restrictions F
  intro E
  let : NumberField E := NumberField.of_module_finite F E
  rw [maximalAbelianGlobalArtin_finitePlace_finiteProjection]
  let i : E →ₐ[F] AlgebraicClosure F :=
    (separableClosure F (AlgebraicClosure F)).val.comp
      ((_root_.maximalAbelianExtension F).val.comp E.val)
  apply AlgEquiv.ext
  intro z
  apply i.injective
  have hfinite := finitePlaceAbsoluteArtin_lift_action F E v
    ((finitePlaceAlgebraicClosureToAbsoluteCompletion F v).comp i) a sigma hsigma z
  have haction := finitePlaceAlgebraicClosureToAbsoluteCompletion_action F v sigma (i z)
  have hglobal : delta.val (i z) =
      i (chosenFinitePlaceArtinMonoidHom (K := F) (L := E) v a z) :=
    (finitePlaceAlgebraicClosureToAbsoluteCompletion F v).injective
      (haction.symm.trans hfinite)
  let s := RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv
    F delta.val
  have hE := AlgEquiv.restrictNormal_commutes (globalMaximalAbelianRestriction F delta.val) E z
  have hM := AlgEquiv.restrictNormal_commutes s (_root_.maximalAbelianExtension F)
    (algebraMap E (_root_.maximalAbelianExtension F) z)
  have hrestriction : i (AlgEquiv.restrictNormalHom E
      (globalMaximalAbelianRestriction F delta.val) z) = delta.val (i z) := by
    exact (congrArg (fun x : _root_.maximalAbelianExtension F ↦
        (((x : SeparableClosure F) : AlgebraicClosure F))) hE).trans
      (congrArg (fun x : SeparableClosure F ↦ (x : AlgebraicClosure F)) hM)
  exact hrestriction.trans hglobal
instance

finitePlaceAbsoluteCompatibilityTargetValuativeRel

L135 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilityTargetValuativeRel
Source context 7 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
Lean source · statement
instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F)
instance

finitePlaceAbsoluteCompatibilityTargetLocalField

L138 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilityTargetLocalField
Source context 8 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance finitePlaceAbsoluteCompatibilityTargetLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F)
theorem

finitePlaceCompletionArtin_lift

L144 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionArtin_lift
Documentation

The actual completion comparison sends an Artin representative to one for the concrete adic completion.

Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAbsoluteCompatibilityTargetLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · full declaration
theorem finitePlaceCompletionArtin_lift
    (a : (v.adicCompletion F)ˣ)
    (sigma : Gal(AlgebraicClosure
      (HeightOneSpectrum.adicAbv F v).Completion/(HeightOneSpectrum.adicAbv F v).Completion))
    (hsigma : (QuotientGroup.mk
        (show Field.absoluteGaloisGroup (HeightOneSpectrum.adicAbv F v).Completion from sigma) :
        Field.absoluteGaloisGroupAbelianization (HeightOneSpectrum.adicAbv F v).Completion) =
      absoluteLocalArtinMap (HeightOneSpectrum.adicAbv F v).Completion
        (finitePlaceLocalArtinInput v a)) :
    (QuotientGroup.mk (finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv F v sigma) :
      Field.absoluteGaloisGroupAbelianization (v.adicCompletion F)) =
      absoluteLocalArtinMap (v.adicCompletion F) a := by
  let C := (HeightOneSpectrum.adicAbv F v).Completion
  let c := (relativeFinitePlaceCompletionAlgEquiv v).toRingEquiv
  have h := absoluteLocalArtinMap_semilinear_lift C (v.adicCompletion F) c
    (finitePlaceCompletionAlgebraicClosureRingEquiv F v)
    (finitePlaceCompletionAlgebraicClosureRingEquiv_algebraMap F v)
    (finitePlaceCompletion_semilinearValuationCompatible F v)
    (finitePlaceLocalArtinInput v a) sigma hsigma
  have ha : Units.map c.toMonoidHom (finitePlaceLocalArtinInput v a) = a := by
    have hc : c = finitePlaceCompletionRingEquiv v :=
      (finitePlaceCompletionRingEquiv_eq_relative v).symm
    rw [hc]
    exact (finitePlaceCompletionUnitsContinuousMulEquiv v).apply_symm_apply a
  rw [ha] at h
  exact h
instance

finitePlaceAbsoluteCompatibilityCharacterTopology

L173 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilityCharacterTopology
Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAbsoluteCompatibilityTargetLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceAbsoluteCompatibilityCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))
instance

finitePlaceAbsoluteCompatibilityCharacterDiscreteTopology

L176 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteCompatibilityCharacterDiscreteTopology
Source context 11 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAbsoluteCompatibilityTargetLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceAbsoluteCompatibilityCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
Lean source · statement
instance finitePlaceAbsoluteCompatibilityCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))
theorem

localReciprocityUnitCharacter_globalMaximalAbelian

L181 ↗
ClassFieldTower.Martinet.Shafarevich.localReciprocityUnitCharacter_globalMaximalAbelian
Documentation

Actual global--local Artin compatibility evaluated by a continuous mod-p character of the maximal abelian global extension.

Source context 12 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain LocalClassFieldTheory GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
variable (v : HeightOneSpectrum (RingOfIntegers F))
local instance finitePlaceAbsoluteCompatibilitySourceValuativeRel :
    ValuativeRel (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionValuativeRel v
local instance finitePlaceAbsoluteCompatibilitySourceLocalField :
    IsNonarchimedeanLocalField (HeightOneSpectrum.adicAbv F v).Completion :=
  finitePlaceLocalArtinCompletionIsNonarchimedeanLocalField v
local instance finitePlaceAbsoluteCompatibilityTargetValuativeRel :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
local instance finitePlaceAbsoluteCompatibilityTargetLocalField :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceAbsoluteCompatibilityCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceAbsoluteCompatibilityCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
Lean source · statement
theorem localReciprocityUnitCharacter_globalMaximalAbelian
    (psi : Gal(_root_.maximalAbelianExtension F/F) →ₜ* Multiplicative (ZMod p))
    (a : (v.adicCompletion F)ˣ) :
    localReciprocityUnitCharacter (v.adicCompletion F) p
        (finitePlaceAbsoluteH1AdicRestriction F p v
          (Additive.ofMul (psi.comp (globalMaximalAbelianRestriction F)))) a =
      psi (maximalAbelianGlobalArtin F (IdeleGroup.finitePlaceIdeleClass v a))

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