NYLL
Module

RealAbsoluteCharacterRadicalReciprocity.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.RealAbsoluteCharacterRadicalReciprocity
4 declarations indexed from sourceView source ↗

Module documentation

Real-split quadratic characters annihilate the finite-support radical

The quotient of a principal-trivial idele character by its finite restriction has the same real signs, since that restriction has only finite coordinates. The real-signed quadratic idele theorem therefore annihilates its ideal-square radical. Actual real and finite Artin comparisons give this reciprocity statement for a real-split absolute quadratic character.

Imports23
Imported by1

Declarations

instance

realAbsoluteCanonicalZModAddCommGroup

L50 ↗
ClassFieldTower.Martinet.Shafarevich.realAbsoluteCanonicalZModAddCommGroup
Source context 5 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
instance realAbsoluteCanonicalZModAddCommGroup : AddCommGroup (ZMod 2)
theorem

two_finite_restriction_principal_radical

L53 ↗
ClassFieldTower.Martinet.Shafarevich.two_finite_restriction_principal_radical
Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
local instance realAbsoluteCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
Lean source · statement
theorem two_finite_restriction_principal_radical
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (psi : IdeleGroup F →ₜ* Multiplicative (ZMod 2))
    (hprincipal : ∀ a : Fˣ, psi (IdeleGroup.principalIdele F a) = 1)
    (hsign : ∀ v : InfinitePlace F, v.IsReal →
      psi (IdeleGroup.infinitePlaceIdele v (-1)) = 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 (2 : ℕ+)).1) :
    (∏ v : ↥S, psi (IdeleGroup.finitePlaceIdele v.1
      (Units.map (algebraMap F (v.1.adicCompletion F)).toMonoidHom a.1))) = 1
theorem

finiteSupport_absolute_eq_restriction

L101 ↗
ClassFieldTower.Martinet.Shafarevich.finiteSupport_absolute_eq_restriction
Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
local instance realAbsoluteCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
Lean source · full declaration
theorem finiteSupport_absolute_eq_restriction
    (n : ℕ+) [Fact (n : ℕ).Prime]
    (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod (n : ℕ)))
    (S : Finset (HeightOneSpectrum (𝓞 F))) :
    finiteSupportLocalReciprocityIdeleCharacter F (n : ℕ) S
      (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F (n : ℕ) v.1 (Additive.ofMul chi)) =
      finiteSupportIdeleRestrictionCharacter F n S
        (globalReciprocityIdeleCharacter F (n : ℕ) chi) := by
  ext z
  rw [finiteSupportLocalReciprocityIdeleCharacter_apply]
  change _ = ∏ v : ↥S, globalReciprocityIdeleCharacter F (n : ℕ) chi
    (IdeleGroup.finitePlaceIdele v.1 (IdeleGroup.finiteComponent v.1 z))
  apply Finset.prod_congr rfl
  intro v hv
  exact localReciprocityUnitCharacter_absoluteCharacter F n chi v.1
    (IdeleGroup.finiteComponent v.1 z)
theorem

absoluteCharacter_two_finiteSupport_radical_annihilator

L120 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteCharacter_two_finiteSupport_radical_annihilator
Documentation

A real-split absolute quadratic character unramified outside S has a finite-support reciprocity functional annihilating the actual ideal-square radical.

Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory
variable (F : Type) [Field F] [NumberField F]
local instance realAbsoluteCanonicalZModAddCommGroup : AddCommGroup (ZMod 2) :=
  (ZMod.instField 2).toDivisionRing.toAddCommGroup
Lean source · full declaration
theorem absoluteCharacter_two_finiteSupport_radical_annihilator
    [IsTotallyReal F]
    (chi : Field.absoluteGaloisGroup F →ₜ* Multiplicative (ZMod 2))
    (S : Finset (HeightOneSpectrum (𝓞 F)))
    (hreal : ∀ v : InfinitePlace F,
      chi (ClassFieldTower.Sawin.absoluteInfinitePlaceArtinNegOne F v) = 1)
    (houtside : ∀ v : HeightOneSpectrum (𝓞 F), v ∉ S →
      ∀ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
        chi (finitePlaceAbsoluteDecompositionInclusion F v sigma.1) = 1) :
    absolutePowerClassDualRestriction F 2
      (finiteSupportLocalReciprocityPowerClassFunctional F 2 S
        (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi))) = 0 := by
  ext x
  change finiteSupportLocalReciprocityPowerClassFunctional F 2 S
    (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi))
    (idealPowerRadicalToAbsolutePowerClassLinearMap F 2 x) = 0
  obtain ⟨a, ha⟩ := QuotientGroup.mk_surjective (Additive.toMul x)
  have hx : Additive.ofMul (QuotientGroup.mk a) = x := congrArg Additive.ofMul ha
  rw [← hx]
  let qa : absolutePowerClassModP F 2 :=
    Additive.ofMul (QuotientGroup.mk' (powMonoidHom 2 : Fˣ →* Fˣ).range a.1)
  change finiteSupportLocalReciprocityPowerClassFunctional F 2 S
    (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi)) qa = 0
  have hprincipal :
      (finiteSupportLocalReciprocityIdeleCharacter F 2 S
        (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi))
        (IdeleGroup.principalIdele F a.1)).toAdd =
        finiteSupportLocalReciprocityPowerClassFunctional F 2 S
          (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi)) qa :=
    finiteSupportLocalReciprocityIdeleCharacter_principal_functional F 2 S
      (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi)) a.1
  rw [← hprincipal]
  have hsign : ∀ v : InfinitePlace F, v.IsReal →
      globalReciprocityIdeleCharacter F 2 chi (IdeleGroup.infinitePlaceIdele v (-1)) = 1 := by
    intro v hv
    exact (ClassFieldTower.Sawin.globalReciprocityIdeleCharacter_infinite_neg_one F 2 chi v).trans
      (hreal v)
  have hprod := two_finite_restriction_principal_radical F S
    (globalReciprocityIdeleCharacter F 2 chi)
    (globalReciprocityIdeleCharacter_principal F 2 chi) hsign
    (fun v hv u hu ↦ globalReciprocityIdeleCharacter_integral_eq_one_of_inertia
      F (2 : ℕ+) chi v (houtside v hv) u hu) a
  have heq : finiteSupportLocalReciprocityIdeleCharacter F 2 S
      (fun v ↦ finitePlaceAbsoluteH1AdicRestriction F 2 v.1 (Additive.ofMul chi))
      (IdeleGroup.principalIdele F a.1) = 1 := by
    have hchar := finiteSupport_absolute_eq_restriction F (2 : ℕ+) chi S
    simp only [PNat.val_ofNat] at hchar
    have heval := congrArg (fun f : IdeleGroup F →ₜ* Multiplicative (ZMod 2) ↦
      f (IdeleGroup.principalIdele F a.1)) hchar
    exact heval.trans hprod
  exact congrArg Multiplicative.toAdd heq

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