Module

RealSignedIdeleCharacter.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.RealSignedIdeleCharacter

5 declarations indexed from sourceView source ↗

Module documentation

Real-sign-trivial quadratic idele characters

Positive real units and all complex units have square roots. A quadratic character killing the real sign generators therefore kills every infinite idele. Finite integral-unit triviality then kills integral ideles and the principal ideles of the ideal-square radical, by the actual ideal map.

Imports13

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdeleIntegralCharacterRadical
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadical
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.Core
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.IdealMap
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormApproximation.InfinitePlaces
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SinglePlace
Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Basic
Mathlib.Algebra.BigOperators.Pi
Mathlib.Algebra.Group.Hom.Defs
Mathlib.Algebra.Group.Prod
Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
Mathlib.Topology.Algebra.Group.Units
Mathlib.Topology.Instances.ZMod

Imported by2

theorem

ideleCharacter_two_positive_eq_one

L38 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_two_positive_eq_one

Source context 4 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem ideleCharacter_two_positive_eq_one
    (chi : IdeleGroup F →* Multiplicative (ZMod 2))
    (v : InfinitePlace F) (a : v.Completionˣ)
    (ha : a ∈ RayClass.infinitePositiveSubgroup v) :
    chi (IdeleGroup.infinitePlaceIdele v a) = 1

theorem

ideleCharacter_two_infinitePlace_eq_one

L49 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_two_infinitePlace_eq_one

Documentation

Killing the real sign generator kills the whole corresponding local factor; at a complex place the square-root construction requires no sign condition.

Source context 4 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem ideleCharacter_two_infinitePlace_eq_one
    (chi : IdeleGroup F →* Multiplicative (ZMod 2))
    (v : InfinitePlace F)
    (hsign : v.IsReal → chi (IdeleGroup.infinitePlaceIdele v (-1)) = 1)
    (a : v.Completionˣ) : chi (IdeleGroup.infinitePlaceIdele v a) = 1

theorem

ideleCharacter_two_infinite_eq_one

L81 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_two_infinite_eq_one

Documentation

A quadratic idele character trivial on all real signs kills every infinite idele.

Source context 4 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem ideleCharacter_two_infinite_eq_one
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod 2))
    (hsign : ∀ v : InfinitePlace F, v.IsReal →
      chi (IdeleGroup.infinitePlaceIdele v (-1)) = 1)
    (a : InfiniteIdeleGroup F) : chi (a, 1) = 1

theorem

ideleCharacter_two_integral_eq_one

L103 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_two_integral_eq_one

Documentation

Real-sign and finite integral-unit triviality kill the full integral idele subgroup.

Source context 4 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem ideleCharacter_two_integral_eq_one
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod 2))
    (hsign : ∀ v : InfinitePlace F, v.IsReal →
      chi (IdeleGroup.infinitePlaceIdele v (-1)) = 1)
    (hfinite : ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
      a ∈ (v.adicCompletionIntegers F).units → chi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : IdeleGroup F) (ha : a ∈ IdeleGroup.integralAtFinitePlaces (K := F)) :
    chi a = 1

theorem

ideleCharacter_two_principal_radical_eq_one_of_integral_local

L123 ↗

ClassFieldTower.Martinet.Shafarevich.ideleCharacter_two_principal_radical_eq_one_of_integral_local

Documentation

The actual fractional-ideal map then kills principal ideles of ideal-square radical elements, with no oddness assumption.

Source context 4 commands

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

open NumberField IsDedekindDomain
open scoped NumberField BigOperators
namespace ClassFieldTower.Martinet.Shafarevich
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem ideleCharacter_two_principal_radical_eq_one_of_integral_local
    (chi : IdeleGroup F →ₜ* Multiplicative (ZMod 2))
    (hsign : ∀ v : InfinitePlace F, v.IsReal →
      chi (IdeleGroup.infinitePlaceIdele v (-1)) = 1)
    (hfinite : ∀ (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ),
      a ∈ (v.adicCompletionIntegers F).units → chi (IdeleGroup.finitePlaceIdele v a) = 1)
    (a : (idealNthPowerRadicalKummerSubgroup F (2 : ℕ+)).1) :
    chi (IdeleGroup.principalIdele F a.1) = 1

Module documentation

Real-sign-trivial quadratic idele characters

Declarations

ideleCharacter_two_positive_eq_one

ideleCharacter_two_infinitePlace_eq_one

ideleCharacter_two_infinite_eq_one

ideleCharacter_two_integral_eq_one

ideleCharacter_two_principal_radical_eq_one_of_integral_local