NYLL
Module

RealCharacterInertiaExistence.lean

Nyll.SawinTotallyRealTowers.RealCharacterInertiaExistence
15 declarations indexed from sourceView source ↗

Module documentation

Arbitrary finite inertia data with a prescribed real value

The rational ideal-square radical is generated by the actual class of −1. The local restriction of the character of ℚ(√−3) has nonzero reciprocity pairing with that class. Subtracting its uniquely determined scalar multiple at three therefore corrects any finite local family to annihilate the radical. Global reciprocity realizes the corrected family, and the existing real-sign correction preserves all inertia outside an allowed set containing three.

Imports27
Imported by2

Declarations

instance

realCharacterExistenceCanonicalZModAddCommGroup

L53 ↗
ClassFieldTower.Sawin.realCharacterExistenceCanonicalZModAddCommGroup
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
Lean source · statement
instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2)
instance

radicalExistenceValuative

L57 ↗
ClassFieldTower.Sawin.radicalExistenceValuative
Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
Lean source · statement
instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F)
instance

radicalExistenceLocalField

L61 ↗
ClassFieldTower.Sawin.radicalExistenceLocalField
Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
Lean source · statement
instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F)
instance

radicalExistenceH1Module

L66 ↗
ClassFieldTower.Sawin.radicalExistenceH1Module
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
Lean source · statement
instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G))
def

radicalNegOne

L73 ↗
ClassFieldTower.Sawin.radicalNegOne
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
def radicalNegOne : idealPowerRadicalModP F 2
theorem

radicalNegOne_image

L76 ↗
ClassFieldTower.Sawin.radicalNegOne_image
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem radicalNegOne_image :
    idealPowerRadicalToAbsolutePowerClassLinearMap F 2 (radicalNegOne F) =
      Additive.ofMul (QuotientGroup.mk' (powMonoidHom 2 : Fˣ →* Fˣ).range (-1))
def

localRadicalValue

L81 ↗
ClassFieldTower.Sawin.localRadicalValue
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
def localRadicalValue (v : HeightOneSpectrum (𝓞 F))
    (χ : ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    ZMod 2
theorem

localRadicalValue_absoluteCharacter

L89 ↗
ClassFieldTower.Sawin.localRadicalValue_absoluteCharacter
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem localRadicalValue_absoluteCharacter
    (v : HeightOneSpectrum (𝓞 F))
    (χ : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod 2)) :
    localRadicalValue F v
      (h1OfCharacter (χ.comp (finitePlaceAbsoluteDecompositionInclusion F v))) =
      (globalReciprocityIdeleCharacter F 2 χ
        (IdeleGroup.finitePlaceIdele v (-1))).toAdd
theorem

localRadicalValue_sub

L125 ↗
ClassFieldTower.Sawin.localRadicalValue_sub
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem localRadicalValue_sub
    (v : HeightOneSpectrum (𝓞 F))
    (χ ψ : ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    localRadicalValue F v (χ - ψ) = localRadicalValue F v χ - localRadicalValue F v ψ
theorem

localRadicalValue_smul

L132 ↗
ClassFieldTower.Sawin.localRadicalValue_smul
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem localRadicalValue_smul
    (v : HeightOneSpectrum (𝓞 F)) (a : ZMod 2)
    (χ : ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    localRadicalValue F v (a • χ) = a * localRadicalValue F v χ
theorem

localRadicalValue_zero

L139 ↗
ClassFieldTower.Sawin.localRadicalValue_zero
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem localRadicalValue_zero (v : HeightOneSpectrum (𝓞 F)) :
    localRadicalValue F v 0 = 0
theorem

radicalFamily_negOne_eq_sum

L144 ↗
ClassFieldTower.Sawin.radicalFamily_negOne_eq_sum
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
section LocalValues
variable (F : Type) [Field F] [NumberField F]
Lean source · full declaration
theorem radicalFamily_negOne_eq_sum
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (χ : ∀ v : ↥S, ContinuousH1ZMod (p := 2)
      (G := finitePlaceAbsoluteDecompositionGroup F v.1)) :
    (absolutePowerClassDualRestriction F 2
      (finiteSupportLocalReciprocityPowerClassFunctional F 2 S
        (fun v => finitePlaceDecompositionH1ToAdic F 2 v.1 (χ v)))) (radicalNegOne F) =
      ∑ v : ↥S, localRadicalValue F v.1 (χ v) := by
  exact finiteSupportLocalReciprocityPowerClassFunctional_apply F 2 S
    (fun v => finitePlaceDecompositionH1ToAdic F 2 v.1 (χ v))
    (idealPowerRadicalToAbsolutePowerClassLinearMap F 2 (radicalNegOne F))
theorem

localRadicalValue_negThree_ne_zero

L158 ↗
ClassFieldTower.Sawin.localRadicalValue_negThree_ne_zero
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem localRadicalValue_negThree_ne_zero :
    localRadicalValue ℚ
      ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
        (⟨3, Nat.prime_three⟩ : Nat.Primes))
      (h1OfCharacter (negativeThreeCharacter.comp
        (finitePlaceAbsoluteDecompositionInclusion ℚ
          ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
            (⟨3, Nat.prime_three⟩ : Nat.Primes))))) ≠ 0
theorem

exists_localFamily_radical_annihilator_adjusted_at_three

L177 ↗
ClassFieldTower.Sawin.exists_localFamily_radical_annihilator_adjusted_at_three
Documentation

Any finite local quadratic-character family can be corrected only at three so that its actual reciprocity functional annihilates the rational ideal-square radical.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
open scoped Classical in
Lean source · full declaration
theorem exists_localFamily_radical_annihilator_adjusted_at_three
    (S : Finset (HeightOneSpectrum (𝓞 ℚ)))
    (χ : ∀ v : ↥S, finitePlaceAbsoluteDecompositionGroup ℚ v.1 →ₜ*
      Multiplicative (ZMod 2)) :
    let v₃ := (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes)
    ∃ ψ : ∀ v : ↥(insert v₃ S), finitePlaceAbsoluteDecompositionGroup ℚ v.1 →ₜ*
      Multiplicative (ZMod 2),
      (absolutePowerClassDualRestriction ℚ 2
        (finiteSupportLocalReciprocityPowerClassFunctional ℚ 2 (insert v₃ S)
          (fun v => finitePlaceDecompositionH1ToAdic ℚ 2 v.1 (h1OfCharacter (ψ v)))) = 0) ∧
      (∀ (v : ↥S) (_hv : v.1 ≠ v₃),
        ψ ⟨v.1, Finset.mem_insert_of_mem v.property⟩ = χ v) := by
  let v₃ : HeightOneSpectrum (𝓞 ℚ) :=
    (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes)
  let U := insert v₃ S
  let bχ : ∀ v : HeightOneSpectrum (𝓞 ℚ),
      ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup ℚ v) :=
    fun v => if hv : v ∈ S then h1OfCharacter (χ ⟨v, hv⟩) else 0
  let nχ : ∀ v : HeightOneSpectrum (𝓞 ℚ),
      ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup ℚ v) :=
    fun v => h1OfCharacter (negativeThreeCharacter.comp
      (finitePlaceAbsoluteDecompositionInclusion ℚ v))
  let c : ZMod 2 := ∑ v ∈ U, localRadicalValue ℚ v (bχ v)
  let d : ZMod 2 := localRadicalValue ℚ v₃ (nχ v₃)
  have hd : d ≠ 0 := localRadicalValue_negThree_ne_zero
  let a : ZMod 2 := c / d
  let fχ : ∀ v : HeightOneSpectrum (𝓞 ℚ),
      ContinuousH1ZMod (p := 2) (G := finitePlaceAbsoluteDecompositionGroup ℚ v) :=
    fun v => bχ v - if v = v₃ then a • nχ v else 0
  let ψ : ∀ v : ↥U, finitePlaceAbsoluteDecompositionGroup ℚ v.1 →ₜ*
      Multiplicative (ZMod 2) := fun v => characterOfH1 (fχ v.1)
  have hValue (v : HeightOneSpectrum (𝓞 ℚ)) :
      localRadicalValue ℚ v (fχ v) = localRadicalValue ℚ v (bχ v) -
        if v = v₃ then a * localRadicalValue ℚ v (nχ v) else 0 := by
    dsimp only [fχ]
    rw [localRadicalValue_sub]
    by_cases hv : v = v₃
    · rw [ite_eq_left hv, ite_eq_left hv, localRadicalValue_smul]
    · rw [ite_eq_right hv, ite_eq_right hv, localRadicalValue_zero]
  have hCorrection : (∑ v ∈ U,
      if v = v₃ then a * localRadicalValue ℚ v (nχ v) else 0) = a * d := by
    rw [Finset.sum_eq_single v₃]
    · rw [ite_eq_left rfl]
    · intro v hv hne
      exact ite_eq_right hne
    · intro h
      exact (h (Finset.mem_insert_self v₃ S)).elim
  have hSum : (∑ v ∈ U, localRadicalValue ℚ v (fχ v)) = 0 := by
    simp_rw [hValue]
    rw [Finset.sum_sub_distrib, hCorrection]
    change c - (c / d) * d = 0
    rw [div_mul_cancel₀ c hd, sub_self]
  have hSumSubtype : (∑ v : ↥U, localRadicalValue ℚ v.1 (fχ v.1)) = 0 :=
    (Finset.sum_coe_sort U (fun v => localRadicalValue ℚ v (fχ v))).trans hSum
  have hRoundTrip : ∀ v : ↥U, h1OfCharacter (ψ v) = fχ v.1 := by
    intro v
    ext σ
    rfl
  refine ⟨ψ, ?_, ?_⟩
  · ext x
    rcases rationalIdealSquareRadical_eq_zero_or_neg_one x with hx | hx
    · rw [hx, map_zero, LinearMap.zero_apply]
    · rw [hx]
      have h := radicalFamily_negOne_eq_sum ℚ U (fun v => h1OfCharacter (ψ v))
      simp_rw [hRoundTrip] at h
      exact h.trans hSumSubtype
  · intro v hv
    apply ContinuousMonoidHom.ext
    intro σ
    change Multiplicative.ofAdd ((fχ v.1) (Additive.ofMul σ)) = χ v σ
    dsimp only [fχ]
    rw [ite_eq_right hv, sub_zero]
    dsimp only [bχ]
    rw [dite_eq_left v.property]
    rfl
theorem

exists_absoluteCharacter_with_prescribed_inertia_and_real_value

L258 ↗
ClassFieldTower.Sawin.exists_absoluteCharacter_with_prescribed_inertia_and_real_value
Documentation

Prescribe an arbitrary finite inertia family and the real value over ℚ. The allowed prime three absorbs the radical and sign corrections, so all specified inertia values outside T are retained.

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.ProP
private local instance realCharacterExistenceCanonicalZModAddCommGroup :
    AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
private local instance radicalExistenceValuative
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    ValuativeRel (v.adicCompletion F) := finitePlaceAdicCompletionValuativeRel F v
private local instance radicalExistenceLocalField
    (F : Type) [Field F] [NumberField F] (v : HeightOneSpectrum (𝓞 F)) :
    IsNonarchimedeanLocalField (v.adicCompletion F) :=
  finitePlaceAdicCompletionIsNonarchimedeanLocalField F v
private local instance radicalExistenceH1Module
    {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod 2) (ContinuousH1ZMod (p := 2) (G := G)) := continuousH1ZModModule
Lean source · statement
theorem exists_absoluteCharacter_with_prescribed_inertia_and_real_value
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (hThree : (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes) ∈ T)
    (S : Finset (HeightOneSpectrum (𝓞 ℚ)))
    (χ : ∀ v : ↥S, finitePlaceAbsoluteDecompositionGroup ℚ v.1 →ₜ*
      Multiplicative (ZMod 2))
    (ε : Multiplicative (ZMod 2)) :
    ∃ γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2),
      (∀ v : InfinitePlace ℚ,
        γ (absoluteInfinitePlaceArtinNegOne ℚ v) = ε) ∧
      (∀ (v : ↥S), v.1 ∉ T →
        ∀ σ : finitePlaceAbsoluteInertiaSubgroup ℚ v.1,
          χ v σ.1 = γ (finitePlaceAbsoluteDecompositionInclusion ℚ v.1 σ.1)) ∧
      (∀ (v : HeightOneSpectrum (𝓞 ℚ)), v ∉ S → v ∉ T →
        ∀ σ : finitePlaceAbsoluteInertiaSubgroup ℚ v,
          γ (finitePlaceAbsoluteDecompositionInclusion ℚ v σ.1) = 1)

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