Module

AbsoluteCharacterRealValue.lean

Nyll.SawinTotallyRealTowers.AbsoluteCharacterRealValue

4 declarations indexed from sourceView source ↗

Module documentation

Prescribing the real value of an absolute quadratic character

Multiplication by the actual character of negative three switches the real value and leaves inertia at every finite place other than three unchanged. This constructs a character with any specified real value, starting with an arbitrary continuous quadratic character and imposing no arithmetic condition on that input.

Imports11

Nyll.SawinTotallyRealTowers.NegativeThreeCharacter
Nyll.SawinTotallyRealTowers.AbsoluteRealKernelField
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceH2Localization
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceUnramifiedH1
Mathlib.Algebra.Group.TypeTags.Basic
Mathlib.Data.Nat.Prime.Defs
Mathlib.FieldTheory.AbsoluteGaloisGroup
Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
Mathlib.NumberTheory.Padics.HeightOneSpectrum
Mathlib.Tactic.FinCases
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by2

theorem

quadratic_mul_eq_of_ne

L36 ↗

ClassFieldTower.Sawin.quadratic_mul_eq_of_ne

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

theorem quadratic_mul_eq_of_ne
    (a b c : Multiplicative (ZMod 2)) (hab : a ≠ b) (hc : c ≠ 1) :
    a * c = b

def

absoluteCharacterWithRealValue

L60 ↗

ClassFieldTower.Sawin.absoluteCharacterWithRealValue

Documentation

Prescribe the value at the unique real place by either keeping the input character or multiplying it by the character of negative three.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

def absoluteCharacterWithRealValue
    (γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2))
    (ε : Multiplicative (ZMod 2)) :
    Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2)

theorem

absoluteCharacterWithRealValue_infinite

L69 ↗

ClassFieldTower.Sawin.absoluteCharacterWithRealValue_infinite

Documentation

The constructed character has the specified value on every real Artin value of negative one over the rationals.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

theorem absoluteCharacterWithRealValue_infinite
    (γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2))
    (ε : Multiplicative (ZMod 2)) (v : InfinitePlace ℚ) :
    absoluteCharacterWithRealValue γ ε (absoluteInfinitePlaceArtinNegOne ℚ v) = ε

theorem

absoluteCharacterWithRealValue_inertia

L85 ↗

ClassFieldTower.Sawin.absoluteCharacterWithRealValue_inertia

Documentation

Prescribing the real value preserves the original character on absolute inertia away from three, including at the prime two.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich

Lean source · statement

theorem absoluteCharacterWithRealValue_inertia
    (γ : Field.absoluteGaloisGroup ℚ →ₜ* Multiplicative (ZMod 2))
    (ε : Multiplicative (ZMod 2)) (v : HeightOneSpectrum (𝓞 ℚ))
    (hv : v ≠ (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
      (⟨3, Nat.prime_three⟩ : Nat.Primes))
    (σ : finitePlaceAbsoluteInertiaSubgroup ℚ v) :
    absoluteCharacterWithRealValue γ ε
        (finitePlaceAbsoluteDecompositionInclusion ℚ v
          (finitePlaceAbsoluteInertiaInclusion ℚ v σ)) =
      γ (finitePlaceAbsoluteDecompositionInclusion ℚ v
        (finitePlaceAbsoluteInertiaInclusion ℚ v σ))

Module documentation

Prescribing the real value of an absolute quadratic character

Declarations

quadratic_mul_eq_of_ne

absoluteCharacterWithRealValue

absoluteCharacterWithRealValue_infinite

absoluteCharacterWithRealValue_inertia