Documentation

TauCeti.NumberTheory.NumberField.Global.InfinityType.Basic

Infinity types of a number field #

This file defines three carriers for the archimedean parameters of characters of a number field. They deliberately record different kinds of data:

ContinuousInfinityType K has a complex modulus exponent and a parity at every real place, and a complex modulus exponent and an integral angular frequency at every complex place. These are the parameters in the classification of continuous characters of ℝˣ and ℂˣ.
AlgebraicInfinityType K assigns an integer exponent to every embedding K → ℂ.
FiniteOrderInfinityType K assigns only a parity to every real place. There is no datum at a complex place because a finite-order continuous character of ℂˣ is trivial.

The map AlgebraicInfinityType.toContinuous performs the conjugation bookkeeping at a complex place: exponents a and b at the chosen embedding and its conjugate give modulus exponent a + b and angular frequency a - b. This map is injective. Finite-order infinity types also embed in continuous infinity types, with all modulus exponents and complex angular frequencies zero.

References #

A. Weil, Basic Number Theory, Chapter VII.
J. Tate, Fourier analysis in number fields and Hecke's zeta-functions, in J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, §2.3.

structure TauCeti.GlobalNumberFields.ContinuousInfinityType (K : Type u_1) [Field K] :

Type u_1

The archimedean parameters of a continuous character over K: a complex modulus exponent and a parity at every real place, and a complex modulus exponent and integral angular frequency at every complex place.

realExponent : { w : NumberField.InfinitePlace K // w.IsReal } → ℂ
The exponent of the absolute value at each real place.
realParity : { w : NumberField.InfinitePlace K // w.IsReal } → ZMod 2
The exponent of the sign character at each real place.
complexExponent : { w : NumberField.InfinitePlace K // w.IsComplex } → ℂ
The exponent of the absolute value at each complex place.
complexAngularFrequency : { w : NumberField.InfinitePlace K // w.IsComplex } → ℤ
The exponent of the angular character at each complex place.

Instances For

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.ext_iff {K : Type u_1} {inst✝ : Field K} {x y : ContinuousInfinityType K} :

x = y ↔ x.realExponent = y.realExponent ∧ x.realParity = y.realParity ∧ x.complexExponent = y.complexExponent ∧ x.complexAngularFrequency = y.complexAngularFrequency

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.ext {K : Type u_1} {inst✝ : Field K} {x y : ContinuousInfinityType K} (realExponent : x.realExponent = y.realExponent) (realParity : x.realParity = y.realParity) (complexExponent : x.complexExponent = y.complexExponent) (complexAngularFrequency : x.complexAngularFrequency = y.complexAngularFrequency) :

x = y

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instZero {K : Type u_1} [Field K] :

Zero (ContinuousInfinityType K)

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instAdd {K : Type u_1} [Field K] :

Add (ContinuousInfinityType K)

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instNeg {K : Type u_1} [Field K] :

Neg (ContinuousInfinityType K)

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instSub {K : Type u_1} [Field K] :

Sub (ContinuousInfinityType K)

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instSMulNat {K : Type u_1} [Field K] :

SMul ℕ (ContinuousInfinityType K)

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instSMulInt {K : Type u_1} [Field K] :

SMul ℤ (ContinuousInfinityType K)

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zero_realExponent {K : Type u_1} [Field K] :

realExponent 0 = 0

The zero continuous infinity type has zero real modulus exponents.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zero_realParity {K : Type u_1} [Field K] :

realParity 0 = 0

The zero continuous infinity type has zero real parities.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zero_complexExponent {K : Type u_1} [Field K] :

complexExponent 0 = 0

The zero continuous infinity type has zero complex modulus exponents.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zero_complexAngularFrequency {K : Type u_1} [Field K] :

complexAngularFrequency 0 = 0

The zero continuous infinity type has zero complex angular frequencies.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.add_realExponent {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t + u).realExponent = t.realExponent + u.realExponent

Real modulus exponents add pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.add_realParity {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t + u).realParity = t.realParity + u.realParity

Real parities add pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.add_complexExponent {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t + u).complexExponent = t.complexExponent + u.complexExponent

Complex modulus exponents add pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.add_complexAngularFrequency {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t + u).complexAngularFrequency = t.complexAngularFrequency + u.complexAngularFrequency

Complex angular frequencies add pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.neg_realExponent {K : Type u_1} [Field K] (t : ContinuousInfinityType K) :

(-t).realExponent = -t.realExponent

Negation negates real modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.neg_realParity {K : Type u_1} [Field K] (t : ContinuousInfinityType K) :

(-t).realParity = -t.realParity

Negation negates real parities pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.neg_complexExponent {K : Type u_1} [Field K] (t : ContinuousInfinityType K) :

(-t).complexExponent = -t.complexExponent

Negation negates complex modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.neg_complexAngularFrequency {K : Type u_1} [Field K] (t : ContinuousInfinityType K) :

(-t).complexAngularFrequency = -t.complexAngularFrequency

Negation negates complex angular frequencies pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.sub_realExponent {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t - u).realExponent = t.realExponent - u.realExponent

Real modulus exponents subtract pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.sub_realParity {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t - u).realParity = t.realParity - u.realParity

Real parities subtract pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.sub_complexExponent {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t - u).complexExponent = t.complexExponent - u.complexExponent

Complex modulus exponents subtract pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.sub_complexAngularFrequency {K : Type u_1} [Field K] (t u : ContinuousInfinityType K) :

(t - u).complexAngularFrequency = t.complexAngularFrequency - u.complexAngularFrequency

Complex angular frequencies subtract pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.nsmul_realExponent {K : Type u_1} [Field K] (n : ℕ) (t : ContinuousInfinityType K) :

(n • t).realExponent = n • t.realExponent

Natural-number multiples scale real modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.nsmul_realParity {K : Type u_1} [Field K] (n : ℕ) (t : ContinuousInfinityType K) :

(n • t).realParity = n • t.realParity

Natural-number multiples scale real parities pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.nsmul_complexExponent {K : Type u_1} [Field K] (n : ℕ) (t : ContinuousInfinityType K) :

(n • t).complexExponent = n • t.complexExponent

Natural-number multiples scale complex modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.nsmul_complexAngularFrequency {K : Type u_1} [Field K] (n : ℕ) (t : ContinuousInfinityType K) :

(n • t).complexAngularFrequency = n • t.complexAngularFrequency

Natural-number multiples scale complex angular frequencies pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zsmul_realExponent {K : Type u_1} [Field K] (n : ℤ) (t : ContinuousInfinityType K) :

(n • t).realExponent = n • t.realExponent

Integer multiples scale real modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zsmul_realParity {K : Type u_1} [Field K] (n : ℤ) (t : ContinuousInfinityType K) :

(n • t).realParity = n • t.realParity

Integer multiples scale real parities pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zsmul_complexExponent {K : Type u_1} [Field K] (n : ℤ) (t : ContinuousInfinityType K) :

(n • t).complexExponent = n • t.complexExponent

Integer multiples scale complex modulus exponents pointwise.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.zsmul_complexAngularFrequency {K : Type u_1} [Field K] (n : ℤ) (t : ContinuousInfinityType K) :

(n • t).complexAngularFrequency = n • t.complexAngularFrequency

Integer multiples scale complex angular frequencies pointwise.

@[instance_reducible]

instance TauCeti.GlobalNumberFields.ContinuousInfinityType.instAddCommGroup {K : Type u_1} [Field K] :

AddCommGroup (ContinuousInfinityType K)

def TauCeti.GlobalNumberFields.ContinuousInfinityType.equivProd {K : Type u_1} [Field K] :

ContinuousInfinityType K ≃+ (({ w : NumberField.InfinitePlace K // w.IsReal } → ℂ) × ({ w : NumberField.InfinitePlace K // w.IsReal } → ZMod 2)) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℤ)

A continuous infinity type is equivalently its four families of local parameters, as additive groups.

Instances For

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.equivProd_apply {K : Type u_1} [Field K] (t : ContinuousInfinityType K) :

equivProd t = ((t.realExponent, t.realParity), t.complexExponent, t.complexAngularFrequency)

equivProd sends a continuous infinity type to its four families of local parameters.

@[simp]

theorem TauCeti.GlobalNumberFields.ContinuousInfinityType.equivProd_symm_apply {K : Type u_1} [Field K] (t : (({ w : NumberField.InfinitePlace K // w.IsReal } → ℂ) × ({ w : NumberField.InfinitePlace K // w.IsReal } → ZMod 2)) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℂ) × ({ w : NumberField.InfinitePlace K // w.IsComplex } → ℤ)) :

equivProd.symm t = { realExponent := t.1.1, realParity := t.1.2, complexExponent := t.2.1, complexAngularFrequency := t.2.2 }

equivProd.symm assembles a continuous infinity type from its four families of local parameters.

@[reducible, inline]

abbrev TauCeti.GlobalNumberFields.AlgebraicInfinityType (K : Type u_1) [Field K] :

Type u_1

An algebraic infinity type over K: an integer exponent at every complex embedding of K.

The two embeddings belonging to one complex place are retained separately. Their sum and difference become the modulus exponent and angular frequency of the associated continuous infinity type.

Instances For

@[reducible, inline]

abbrev TauCeti.GlobalNumberFields.FiniteOrderInfinityType (K : Type u_1) [Field K] :

Type u_1

A finite-order infinity type over K: a sign parity at every real place.

There is no complex-place field: every finite-order continuous character of ℂˣ is trivial.

Instances For

noncomputable def TauCeti.GlobalNumberFields.AlgebraicInfinityType.embeddingCharacter {K : Type u_1} [Field K] [NumberField K] (n : AlgebraicInfinityType K) :

Kˣ →* ℂ ˣ

The multiplicative monomial of an algebraic infinity type on global nonzero elements: x ↦ ∏ σ, σ(x) ^ n σ, with its nonzero value bundled as a complex unit.

Instances For

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.embeddingCharacter_zero {K : Type u_1} [Field K] [NumberField K] :

embeddingCharacter 0 = 1

The zero algebraic infinity type gives the trivial embedding character.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.embeddingCharacter_add {K : Type u_1} [Field K] [NumberField K] (n m : AlgebraicInfinityType K) :

(n + m).embeddingCharacter = n.embeddingCharacter * m.embeddingCharacter

Adding algebraic infinity types multiplies their embedding characters.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.embeddingCharacter_neg {K : Type u_1} [Field K] [NumberField K] (n : AlgebraicInfinityType K) :

(-n).embeddingCharacter = n.embeddingCharacter⁻¹

Negating an algebraic infinity type inverts its embedding character.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.coe_embeddingCharacter_apply {K : Type u_1} [Field K] [NumberField K] (n : AlgebraicInfinityType K) (x : Kˣ) :

↑(n.embeddingCharacter x) = ∏ σ : K →+* ℂ, σ ↑x ^ n σ

The embedding character evaluates as the monomial in the complex embeddings.

noncomputable def TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous {K : Type u_1} [Field K] :

AlgebraicInfinityType K →+ ContinuousInfinityType K

The continuous infinity type associated to an algebraic infinity type. At a real place the integer exponent gives both the modulus exponent and its parity. At a complex place, exponents a and b at the chosen embedding and its conjugate give modulus exponent a + b and angular frequency a - b.

Instances For

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous_realExponent {K : Type u_1} [Field K] (n : AlgebraicInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :

(toContinuous n).realExponent w = ↑(n (↑w).embedding)

The real modulus exponent of an algebraic infinity type is its exponent at the real embedding.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous_realParity {K : Type u_1} [Field K] (n : AlgebraicInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :

(toContinuous n).realParity w = ↑(n (↑w).embedding)

The real parity of an algebraic infinity type is its embedding exponent modulo two.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous_complexExponent {K : Type u_1} [Field K] (n : AlgebraicInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :

(toContinuous n).complexExponent w = ↑(n (↑w).embedding) + ↑(n (NumberField.ComplexEmbedding.conjugate (↑w).embedding))

The complex modulus exponent of an algebraic infinity type is the sum of its two conjugate embedding exponents.

@[simp]

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous_complexAngularFrequency {K : Type u_1} [Field K] (n : AlgebraicInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :

(toContinuous n).complexAngularFrequency w = n (↑w).embedding - n (NumberField.ComplexEmbedding.conjugate (↑w).embedding)

The complex angular frequency of an algebraic infinity type is the difference of its two conjugate embedding exponents.

theorem TauCeti.GlobalNumberFields.AlgebraicInfinityType.toContinuous_injective {K : Type u_1} [Field K] :

Function.Injective ⇑toContinuous

Algebraic infinity types are determined by their associated continuous infinity types.

def TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous {K : Type u_1} [Field K] :

FiniteOrderInfinityType K →+ ContinuousInfinityType K

A finite-order infinity type as a continuous infinity type: its real signs are retained, and all modulus exponents and complex angular frequencies are zero.

Instances For

@[simp]

theorem TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous_realExponent {K : Type u_1} [Field K] (ε : FiniteOrderInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :

(toContinuous ε).realExponent w = 0

The continuous real exponent of a finite-order infinity type is zero.

@[simp]

theorem TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous_realParity {K : Type u_1} [Field K] (ε : FiniteOrderInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsReal }) :

(toContinuous ε).realParity w = ε w

Passing a finite-order infinity type to continuous parameters preserves its real parity.

@[simp]

theorem TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous_complexExponent {K : Type u_1} [Field K] (ε : FiniteOrderInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :

(toContinuous ε).complexExponent w = 0

The continuous complex exponent of a finite-order infinity type is zero.

@[simp]

theorem TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous_complexAngularFrequency {K : Type u_1} [Field K] (ε : FiniteOrderInfinityType K) (w : { w : NumberField.InfinitePlace K // w.IsComplex }) :

(toContinuous ε).complexAngularFrequency w = 0

The continuous complex angular frequency of a finite-order infinity type is zero.

theorem TauCeti.GlobalNumberFields.FiniteOrderInfinityType.toContinuous_injective {K : Type u_1} [Field K] :

Function.Injective ⇑toContinuous

Finite-order infinity types are determined by their continuous parameters.