Documentation

TauCeti.Algebra.AlgebraicGroup.RootsOfUnity.BaseChange

Base change of the roots-of-unity group scheme #

This file records the base-changed functor-of-points calculation for the diagonalizable group μ_n = D(Multiplicative (ZMod n)). If K is a k-algebra and A is a commutative K-algebra, then the A-points of the base-changed Hopf algebra K ⊗[k] k[Multiplicative (ZMod n)] are the usual subgroup rootsOfUnity n A.

The construction first restricts a base-changed point along 1 ⊗ _ : k[Multiplicative (ZMod n)] → K ⊗[k] k[Multiplicative (ZMod n)], then applies RootsOfUnityGroup.pointsMulEquiv. The characteristic lemmas spell out that the equivalence reads a point on the base-changed standard generator 1 ⊗ single (ofAdd 1) 1, how the inverse point evaluates on scalar multiples of that generator.

This is part of the ReductiveGroups roadmap worked examples: μ_n = D(ℤ/n) in the diagonalizable-groups lane, together with the Layer 0 base-change target for Hopf algebras and their functors of points.

Main declarations #

References #

The generic algebra base-change calculation is Tau Ceti's AlgHom.baseChangePointsMulEquiv, and the roots-of-unity points calculation is RootsOfUnityGroup.pointsMulEquiv. This specialization follows the API pattern of DiagonalizableGroup.baseChangePointsMulEquiv in TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.BaseChange.

source
noncomputable def TauCeti.RootsOfUnityGroup.baseChangePointsMulEquiv {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (n : ℕ) :
WithConv (TensorProduct k K (MonoidAlgebra k (Multiplicative (ZMod n))) →ₐ[K] A) ≃* ↥(rootsOfUnity n A)

The A-points of the base change K ⊗[k] k[Multiplicative (ZMod n)] of μ_n are the subgroup of nth roots of unity in A.

The source is the convolution group of K-algebra maps out of the base-changed Hopf algebra. The target is Mathlib's subgroup of units whose nth power is one.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.RootsOfUnityGroup.baseChangePointsMulEquiv_apply {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (n : ℕ) (f : WithConv (TensorProduct k K (MonoidAlgebra k (Multiplicative (ZMod n))) →ₐ[K] A)) :
    ↑↑((baseChangePointsMulEquiv n) f) = f.ofConv (1 ⊗ₜ[k] MonoidAlgebra.single (generator n) 1)

    The base-changed roots-of-unity points equivalence reads a point by evaluating it on the base-changed standard generator 1 ⊗ single (ofAdd 1) 1.

    source
    @[simp]
    theorem TauCeti.RootsOfUnityGroup.baseChangePointsMulEquiv_symm_apply_tmul_single_generator {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) (s : K) (r : k) :
    ((baseChangePointsMulEquiv n).symm ζ).ofConv (s ⊗ₜ[k] MonoidAlgebra.single (generator n) r) = s • r • ↑↑ζ

    The inverse base-changed roots-of-unity points equivalence evaluates scalar multiples of the standard generator by scalar multiplication of the chosen root of unity.

    source
    theorem TauCeti.RootsOfUnityGroup.baseChangePointsMulEquiv_symm_apply_single_generator {k : Type u} {K : Type v} {A : Type w} [CommSemiring k] [CommSemiring K] [CommSemiring A] [Algebra k K] [Algebra K A] [Algebra k A] [IsScalarTower k K A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) :
    ((baseChangePointsMulEquiv n).symm ζ).ofConv (1 ⊗ₜ[k] MonoidAlgebra.single (generator n) 1) = ↑↑ζ

    The inverse base-changed roots-of-unity points equivalence takes the standard generator to the chosen root of unity.