NYLL
Module

FiniteSupportGlobalReciprocity.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FiniteSupportGlobalReciprocity
8 declarations indexed from sourceView source ↗

Module documentation

Finite local products of global characters annihilate the radical

Restrict a principal-trivial continuous idele character to finitely many one-place factors. If the original character kills integral units outside that set, the quotient of the original and restricted characters kills every local integral unit. The integral-character radical theorem then shows that the finite local product is one on every ideal-power radical representative.

The comparison is built directly from the same idele character on both sides; no local-global Artin comparison hypothesis is introduced. This is the reciprocity input for independence of a chosen global lift and for additivity of the obstruction functional.

Imports1
Imported by4

Declarations

theorem

finitePlaceIdele_continuous

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceIdele_continuous
Documentation

Inserting a finite-place unit is continuous for the actual restricted- product idele topology.

Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem finitePlaceIdele_continuous (v : HeightOneSpectrum (𝓞 F)) :
    Continuous (IdeleGroup.finitePlaceIdele v)
instance

finiteRestrictionZModAddCommGroup

L64 ↗
ClassFieldTower.Martinet.Shafarevich.finiteRestrictionZModAddCommGroup
Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
Lean source · statement
instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ))
instance

finiteRestrictionTopology

L67 ↗
ClassFieldTower.Martinet.Shafarevich.finiteRestrictionTopology
Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
Lean source · statement
instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ))
instance

finiteRestrictionDiscrete

L68 ↗
ClassFieldTower.Martinet.Shafarevich.finiteRestrictionDiscrete
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
Lean source · statement
instance finiteRestrictionDiscrete : DiscreteTopology (ZMod (n : ℕ))
def

finiteSupportIdeleRestrictionCharacter

L75 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleRestrictionCharacter
Documentation

The finite product of the given idele character's one-place restrictions.

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finiteRestrictionDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (psi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
Lean source · full declaration
def finiteSupportIdeleRestrictionCharacter :
    IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)) where
  toFun x := ∏ v : ↥S, psi (IdeleGroup.finitePlaceIdele v.1 (IdeleGroup.finiteComponent v.1 x))
  map_one' := by simp only [map_one, Finset.prod_const_one]
  map_mul' x y := by simp only [map_mul, Finset.prod_mul_distrib]
  continuous_toFun := continuous_finsetProd Finset.univ fun v _ =>
    psi.continuous.comp ((finitePlaceIdele_continuous F v.1).comp
      (IdeleGroup.finiteComponentContinuous v.1).continuous)
theorem

finiteSupportIdeleRestrictionCharacter_finitePlace

L86 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleRestrictionCharacter_finitePlace
Documentation

A one-place restriction is retained exactly when its place is in the set.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finiteRestrictionDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (psi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
open scoped Classical in
Lean source · full declaration
theorem finiteSupportIdeleRestrictionCharacter_finitePlace
    (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ) :
    finiteSupportIdeleRestrictionCharacter F n S psi (IdeleGroup.finitePlaceIdele v a) =
      if v ∈ S then psi (IdeleGroup.finitePlaceIdele v a) else 1 := by
  by_cases hv : v ∈ S
  · rw [ite_eq_left hv]
    change (∏ w : ↥S, psi (IdeleGroup.finitePlaceIdele w.1
      (IdeleGroup.finiteComponent w.1 (IdeleGroup.finitePlaceIdele v a)))) = _
    rw [Finset.prod_eq_single (⟨v, hv⟩ : ↥S)]
    · rw [IdeleGroup.finitePlaceIdele_finiteComponent_same]
    · intro w _ hw
      rw [IdeleGroup.finitePlaceIdele_finiteComponent_of_ne v w.1 a
        (fun h => hw (Subtype.ext h)), map_one, map_one]
    · intro h
      exact (h (Finset.mem_univ _)).elim
  · rw [ite_eq_right hv]
    apply Finset.prod_eq_one
    intro w _
    rw [IdeleGroup.finitePlaceIdele_finiteComponent_of_ne v w.1 a
      (fun h => hv (h ▸ w.2)), map_one, map_one]
theorem

finiteSupportIdeleRestrictionCharacter_principal_radical

L111 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupportIdeleRestrictionCharacter_principal_radical
Documentation

Principal triviality and unramifiedness outside the finite set force the restricted character to annihilate principal radical representatives.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finiteRestrictionDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (psi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
include hpOdd
Lean source · statement
theorem finiteSupportIdeleRestrictionCharacter_principal_radical
    (hprincipal : ∀ a : Fˣ, psi (IdeleGroup.principalIdele F a) = 1)
    (houtside : ∀ (v : HeightOneSpectrum (𝓞 F)), v ∉ S →
      ∀ a : (v.adicCompletion F)ˣ, a ∈ (v.adicCompletionIntegers F).units →
        psi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : (idealNthPowerRadicalKummerSubgroup F n).1) :
    finiteSupportIdeleRestrictionCharacter F n S psi
      (IdeleGroup.principalIdele F a.1) = 1
theorem

principalTrivialIdeleCharacter_finite_product_radical

L137 ↗
ClassFieldTower.Martinet.Shafarevich.principalTrivialIdeleCharacter_finite_product_radical
Documentation

The finite local evaluation product of a principal-trivial character is one on the ideal-power radical when it is unramified outside that set.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology BigOperators RestrictedProduct
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]
variable (n : ℕ+) [Fact (n : ℕ).Prime] (hpOdd : Odd (n : ℕ))
local instance finiteRestrictionZModAddCommGroup : AddCommGroup (ZMod (n : ℕ)) :=
  (ZMod.instField (n : ℕ)).toDivisionRing.toAddCommGroup
local instance finiteRestrictionTopology : TopologicalSpace (ZMod (n : ℕ)) := ⊥
local instance finiteRestrictionDiscrete : DiscreteTopology (ZMod (n : ℕ)) :=
  discreteTopology_bot _
variable (S : Finset (HeightOneSpectrum (𝓞 F)))
variable (psi : IdeleGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
include hpOdd
Lean source · statement
theorem principalTrivialIdeleCharacter_finite_product_radical
    (hprincipal : ∀ a : Fˣ, psi (IdeleGroup.principalIdele F a) = 1)
    (houtside : ∀ (v : HeightOneSpectrum (𝓞 F)), v ∉ S →
      ∀ a : (v.adicCompletion F)ˣ, a ∈ (v.adicCompletionIntegers F).units →
        psi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : (idealNthPowerRadicalKummerSubgroup F n).1) :
    (∏ v : ↥S, psi (IdeleGroup.finitePlaceIdele v.1
      (Units.map (algebraMap F (v.1.adicCompletion F)).toMonoidHom a.1))) = 1

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