Documentation

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.PowerEndomorphism

Power endomorphisms of 𝔾ₘ and the ring map ℤ → End(𝔾ₘ) #

TauCeti.Algebra.AlgebraicGroup.Cocharacter introduces, for the multiplicative group 𝔾ₘ = D(Multiplicative ℤ), the nth power endomorphism DiagonalizableGroup.powEnd n, defined through the diagonalizable-group functoriality as the character of 𝔾ₘ at the generator power Multiplicative.ofAdd n. It records that these power endomorphisms compose by multiplying exponents (powEnd_comp) with powEnd 1 = id (powEnd_one) — the multiplicative half of the ring End(𝔾ₘ) ≅ ℤ "on the level of power maps".

This file completes that picture. The key bridge is that the abstractly-defined endomorphism powEnd z acts on the convolution group of points as the genuine zth power map: powEnd z f = f ^ z (DiagonalizableGroup.powEnd_apply). From this the remaining ring structure follows: powEnd 0 is the trivial homomorphism (powEnd_zero), the exponent-additive law powEnd (a + b) = powEnd a * powEnd b holds for the pointwise product of endomorphisms (powEnd_add), and powEnd (-a) inverts pointwise (powEnd_neg). Passing to additive notation on the abelian group of 𝔾ₘ-points, the family realizes the canonical integer action (toAdditive_powEnd_eq_intCast), i.e. the power endomorphisms are the power-map realization of Mathlib's canonical ring homomorphism Int.castRingHom into End(𝔾ₘ(A)). On the group of points of a fixed algebra A this map need not be injective (for instance when Aˣ has finite exponent), so it is honestly only a ring homomorphism, not an isomorphism.

The power-map description also reads off the character–cocharacter pairing directly: composing a character m after a cocharacter ψ of D(M) raises a 𝔾ₘ-point to the ⟨m, ψ⟩ power (DiagonalizableGroup.charPoints_cocharPoints_apply).

This improves the existing power-endomorphism and character–cocharacter pairing API supporting the reductive-groups roadmap (ReductiveGroups/README.md in TauCetiRoadmap, Layer 4: "Tori ... the character lattice X*(T) and cocharacter lattice X_*(T) with their perfect pairing").

Main results #

References #

The power endomorphism DiagonalizableGroup.powEnd, the 𝔾ₘ-points extensionality DiagonalizableGroup.pointsMulEquiv_ext, and the character–cocharacter pairing are Tau Ceti's TauCeti.Algebra.AlgebraicGroup.Cocharacter. The additive reinterpretation MonoidHom.toAdditive and ofMul_zpow are Mathlib's.

source
@[instance_reducible]
noncomputable def TauCeti.DiagonalizableGroup.multiplicativeGroupPointsCommGroup {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] :
CommGroup (WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A))

The convolution group structure on the points of 𝔾ₘ.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.powEnd_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (z : ℤ) (f : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)) :
    (powEnd z) f = f ^ z

    The power endomorphism is the power map. The zth power endomorphism of 𝔾ₘ = D(Multiplicative ℤ), defined through the diagonalizable-group functoriality, acts on the convolution group of points as the genuine zth power f ↦ f ^ z.

    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.powEnd_zero {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] :
    powEnd 0 = 1

    The zeroth power endomorphism is the trivial homomorphism. This is the additive unit of the endomorphism ring, complementing powEnd_one (its multiplicative unit).

    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.powEnd_add {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (a b : ℤ) :
    powEnd (a + b) = powEnd a * powEnd b

    Power endomorphisms add exponents under the pointwise product. In the abelian group of endomorphisms of 𝔾ₘ (pointwise multiplication of homomorphisms into the commutative group of points), powEnd (a + b) = powEnd a * powEnd b. This is the addition of the endomorphism ring End(𝔾ₘ) ≅ ℤ, complementing the multiplication powEnd_comp.

    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.powEnd_neg {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (a : ℤ) :
    powEnd (-a) = (powEnd a)⁻¹

    The power endomorphism of a negated exponent is the pointwise inverse endomorphism: powEnd (-a) sends a point to the inverse of its image under powEnd a.

    source
    @[simp]
    theorem TauCeti.DiagonalizableGroup.toAdditive_powEnd_eq_intCast {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (z : ℤ) :
    MonoidHom.toAdditive (powEnd z) = (Int.castRingHom (AddMonoid.End (Additive (WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A))))) z

    The power endomorphism is the canonical integer action. The additive form of powEnd z is the canonical integer endomorphism. Together with powEnd_zero, powEnd_one, powEnd_add, and powEnd_comp, this exhibits z ↦ powEnd z as the power-endomorphism realization of the canonical ring homomorphism Int.castRingHom into End(𝔾ₘ(A)); on a fixed algebra A this map need not be injective, for example when Aˣ has finite exponent.

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

    The character–cocharacter pairing is the exponent of a power map. For a character m : M and a cocharacter ψ : M →* Multiplicative ℤ of the diagonalizable group D(M), composing the character after the cocharacter raises a 𝔾ₘ-point to the ⟨m, ψ⟩ power, where ⟨m, ψ⟩ = pairing m ψ. This is the pointwise form of charPoints_comp_cocharPoints, reading the pairing off as the power to which the composite endomorphism raises a point.