Characters, cocharacters, and their pairing for the diagonalizable group

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Basic computes the functor of points of the diagonalizable group D(M) = Spec R[M], and TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Functoriality records its contravariant functoriality DiagonalizableGroup.pointsMap. This file uses that functoriality to build the character lattice X*(D(M)), the cocharacter lattice X_*(D(M)), and their pairing into the endomorphism lattice of the multiplicative group, all realized on the functor of points.

Throughout, the multiplicative group is 𝔾ₘ = D(Multiplicative ℤ) in its group-algebra presentation, so its A-points are the units Aˣ (its character group Multiplicative ℤ →* Aˣ being determined by the value on the generator, Mathlib's MonoidHom.apply_mint). Its canonical Laurent-polynomial API is TauCeti.MultiplicativeGroup, matched to this presentation by TauCeti.DiagonalizableGroup.multiplicativeGroup_pointEquiv_apply.

• A character of D(M) is an element m : M, giving the homomorphism of group functors D(M) → 𝔾ₘ whose action on points is evaluation of a character χ : M →* Aˣ at m.
• A cocharacter of D(M) is a homomorphism ψ : M →* Multiplicative ℤ, giving the homomorphism of group functors 𝔾ₘ → D(M); on points it sends a unit u to the character m ↦ u ^ (ψ m).toAdd.
• The n-th power endomorphism powEnd n of 𝔾ₘ acts as u ↦ u ^ n on points; power endomorphisms compose by multiplication of exponents (powEnd_comp, powEnd_one), which is the ring End(𝔾ₘ) ≅ ℤ on the level of power maps.
• The pairing ⟨m, ψ⟩ = (ψ m).toAdd : ℤ is realized as the composite endomorphism character m ∘ cocharacter ψ = powEnd ⟨m, ψ⟩ of 𝔾ₘ (charPoints_comp_cocharPoints). For M = Multiplicative ℤ, so X*(𝔾ₘ) = X_*(𝔾ₘ) = ℤ, the pairing is multiplication (pairing_ofAdd): the rank-1 root datum input.

Main declarations

• TauCeti.DiagonalizableGroup.charPoints: the character of D(M) at m : M, on points.
• TauCeti.DiagonalizableGroup.cocharPoints: the cocharacter of D(M) at ψ, on points.
• TauCeti.DiagonalizableGroup.powEnd: the n-th power endomorphism of 𝔾ₘ, on points.
• TauCeti.DiagonalizableGroup.pairing: the character–cocharacter pairing ⟨m, ψ⟩ : ℤ.
• TauCeti.DiagonalizableGroup.charPoints_comp_cocharPoints: the pairing is realized as the composite endomorphism character m ∘ cocharacter ψ = powEnd ⟨m, ψ⟩.

See also

• TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Functoriality: contravariant points functoriality DiagonalizableGroup.pointsMap.
• Mathlib.Data.Int.Cast.Lemmas: the one-generator universal property zpowersHom and MonoidHom.apply_mint.

Characters

noncomputable def TauCeti.DiagonalizableGroup.charPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (m : M) : WithConv (MonoidAlgebra R M →ₐ[R] A) →* WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)

The character of D(M) attached to an element m : M, on points. As a homomorphism of group functors D(M) → 𝔾ₘ, it is induced (contravariantly) by the generator homomorphism zpowersHom M m : Multiplicative ℤ →* M, Multiplicative.ofAdd 1 ↦ m.

Equations

• TauCeti.DiagonalizableGroup.charPoints m = TauCeti.DiagonalizableGroup.pointsMap ((zpowersHom M) m)

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_charPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (m : M) (f : WithConv (MonoidAlgebra R M →ₐ[R] A)) : (pointsMulEquiv ((charPoints m) f)) (Multiplicative.ofAdd 1) = (pointsMulEquiv f) m

A character acts on points by evaluation. Reading the resulting 𝔾ₘ-point on the generator gives the value of the original character χ : M →* Aˣ at m.

Cocharacters

noncomputable def TauCeti.DiagonalizableGroup.cocharPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (ψ : M →* Multiplicative ℤ) : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A) →* WithConv (MonoidAlgebra R M →ₐ[R] A)

The cocharacter of D(M) attached to a homomorphism ψ : M →* Multiplicative ℤ, on points. As a homomorphism of group functors 𝔾ₘ → D(M), it is induced (contravariantly) by ψ.

Equations

• TauCeti.DiagonalizableGroup.cocharPoints ψ = TauCeti.DiagonalizableGroup.pointsMap ψ

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_cocharPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (ψ : M →* Multiplicative ℤ) (f : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)) (m : M) : (pointsMulEquiv ((cocharPoints ψ) f)) m = (pointsMulEquiv f) (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd (ψ m)

A cocharacter acts on points by a power character. The 𝔾ₘ-point with generator value u is sent to the character m ↦ u ^ (ψ m).toAdd.

Power endomorphisms of 𝔾ₘ

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_ext {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {f g : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)} (h : (pointsMulEquiv f) (Multiplicative.ofAdd 1) = (pointsMulEquiv g) (Multiplicative.ofAdd 1)) : f = g

Extensionality for 𝔾ₘ = D(Multiplicative ℤ) points. Two points are equal once they read off the same unit on the group-algebra generator Multiplicative.ofAdd 1: a character of Multiplicative ℤ is determined by its value at the generator (MonoidHom.ext_mint), and points are equivalent to characters.

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_ext_iff {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {f g : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)} : f = g ↔ (pointsMulEquiv f) (Multiplicative.ofAdd 1) = (pointsMulEquiv g) (Multiplicative.ofAdd 1)

noncomputable def TauCeti.DiagonalizableGroup.powEnd {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℤ) : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A) →* WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)

The n-th power endomorphism of 𝔾ₘ, on points. Because 𝔾ₘ = D(Multiplicative ℤ), this is exactly the character of 𝔾ₘ at the generator power Multiplicative.ofAdd n (charPoints (Multiplicative.ofAdd n), recorded by powEnd_eq_charPoints); on points it acts as u ↦ u ^ n.

Equations

• TauCeti.DiagonalizableGroup.powEnd n = TauCeti.DiagonalizableGroup.charPoints (Multiplicative.ofAdd n)

theorem TauCeti.DiagonalizableGroup.powEnd_eq_charPoints {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℤ) : powEnd n = charPoints (Multiplicative.ofAdd n)

The n-th power endomorphism of 𝔾ₘ is the character of 𝔾ₘ at Multiplicative.ofAdd n.

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_powEnd {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℤ) (f : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)) : (pointsMulEquiv ((powEnd n) f)) (Multiplicative.ofAdd 1) = (pointsMulEquiv f) (Multiplicative.ofAdd 1) ^ n

The power endomorphism acts as u ↦ u ^ n on points.

@[simp]

theorem TauCeti.DiagonalizableGroup.powEnd_one {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] : powEnd 1 = MonoidHom.id (WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A))

The first power endomorphism is the identity.

theorem TauCeti.DiagonalizableGroup.powEnd_comp {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (a b : ℤ) : (powEnd a).comp (powEnd b) = powEnd (a * b)

Power endomorphisms compose by multiplying exponents: powEnd a ∘ powEnd b = powEnd (a*b). This is the multiplication of the endomorphism ring End(𝔾ₘ) ≅ ℤ on power maps.

The character–cocharacter pairing

def TauCeti.DiagonalizableGroup.pairing {M : Type w} [CommGroup M] (m : M) (ψ : M →* Multiplicative ℤ) : ℤ

The character–cocharacter pairing ⟨m, ψ⟩ : ℤ of a character m : M of D(M) with a cocharacter ψ : M →* Multiplicative ℤ.

Equations

• TauCeti.DiagonalizableGroup.pairing m ψ = Multiplicative.toAdd (ψ m)

theorem TauCeti.DiagonalizableGroup.pairing_def {M : Type w} [CommGroup M] (m : M) (ψ : M →* Multiplicative ℤ) : pairing m ψ = Multiplicative.toAdd (ψ m)

The pairing ⟨m, ψ⟩ is the integer (ψ m).toAdd.

@[simp]

theorem TauCeti.DiagonalizableGroup.pairing_mul_left {M : Type w} [CommGroup M] (m m' : M) (ψ : M →* Multiplicative ℤ) : pairing (m * m') ψ = pairing m ψ + pairing m' ψ

The pairing is additive in the character: ⟨m * m', ψ⟩ = ⟨m, ψ⟩ + ⟨m', ψ⟩.

@[simp]

theorem TauCeti.DiagonalizableGroup.pairing_one_left {M : Type w} [CommGroup M] (ψ : M →* Multiplicative ℤ) : pairing 1 ψ = 0

The pairing vanishes on the identity character: ⟨1, ψ⟩ = 0.

@[simp]

theorem TauCeti.DiagonalizableGroup.pairing_mul_right {M : Type w} [CommGroup M] (m : M) (ψ ψ' : M →* Multiplicative ℤ) : pairing m (ψ * ψ') = pairing m ψ + pairing m ψ'

The pairing is additive in the cocharacter: ⟨m, ψ * ψ'⟩ = ⟨m, ψ⟩ + ⟨m, ψ'⟩.

@[simp]

theorem TauCeti.DiagonalizableGroup.pairing_one_right {M : Type w} [CommGroup M] (m : M) : pairing m 1 = 0

The pairing vanishes on the identity cocharacter: ⟨m, 1⟩ = 0.

theorem TauCeti.DiagonalizableGroup.charPoints_comp_cocharPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (m : M) (ψ : M →* Multiplicative ℤ) : (charPoints m).comp (cocharPoints ψ) = powEnd (pairing m ψ)

The pairing is realized as a power endomorphism of 𝔾ₘ. Composing the character m after the cocharacter ψ is the ⟨m, ψ⟩-power endomorphism of 𝔾ₘ, so on points it is u ↦ u ^ ⟨m, ψ⟩. This realizes the character–cocharacter pairing X*(D(M)) × X_*(D(M)) → End(𝔾ₘ), valued in the power endomorphisms (the ring End(𝔾ₘ) ≅ ℤ on the level of power maps).

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_charPoints_cocharPoints {R : Type u} {A : Type v} {M : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup M] (m : M) (ψ : M →* Multiplicative ℤ) (f : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)) : (pointsMulEquiv ((charPoints m) ((cocharPoints ψ) f))) (Multiplicative.ofAdd 1) = (pointsMulEquiv f) (Multiplicative.ofAdd 1) ^ pairing m ψ

The pairing evaluated through charPoints_comp_cocharPoints: on points, the composite of the cocharacter ψ and the character m raises a unit to the ⟨m, ψ⟩ power.

theorem TauCeti.DiagonalizableGroup.pairing_ofAdd (a : ℤ) (ψ : Multiplicative ℤ →* Multiplicative ℤ) : pairing (Multiplicative.ofAdd a) ψ = a * Multiplicative.toAdd (ψ (Multiplicative.ofAdd 1))

The rank-1 pairing is multiplication. For 𝔾ₘ = D(Multiplicative ℤ), with character lattice X*(𝔾ₘ) = ℤ (via Multiplicative.ofAdd) and cocharacter lattice X_*(𝔾ₘ) = ℤ (via ψ ↦ (ψ (Multiplicative.ofAdd 1)).toAdd), the pairing is the product of the two integers.