Documentation

TauCeti.Algebra.AlgebraicGroup.RootsOfUnity.Basic

The roots-of-unity group scheme #

This file records the functor-of-points calculation for the diagonalizable group D(Multiplicative (ZMod n)). For positive n, this is the usual finite diagonalizable group scheme μ_n: for every commutative R-algebra A, its convolution group of A-points is the group of nth roots of unity in A.

The result is deliberately just the points calculation. The represented Hopf algebra is the group algebra R[Multiplicative (ZMod n)]; identifying it with the more classical coordinate ring R[X]/(X^n - 1) is separate quotient-polynomial infrastructure.

Main definitions #

This is a worked-example check for the reductive-groups roadmap, Layer 4: "μ_n = D(ℤ/n)" in the diagonalizable-groups lane, together with the Layer 0 functor-of-points calculation.

References #

The diagonalizable-group points calculation is Tau Ceti's DiagonalizableGroup.pointsMulEquiv. The internal cyclic character group calculation uses Mathlib's IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator, from Mathlib.RingTheory.RootsOfUnity.Basic.

source
@[reducible, inline]
abbrev TauCeti.RootsOfUnityGroup.generator (n : ℕ) :
Multiplicative (ZMod n)

The standard generator of the character group defining μ_n = D(ℤ/n).

Equations
Instances For
    source
    noncomputable def TauCeti.RootsOfUnityGroup.pointsMulEquiv {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) :
    WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A) ≃* ↥(rootsOfUnity n A)

    The functor of points of μ_n = D(ℤ/n) is the group of nth roots of unity.

    The source is the convolution group of R-algebra maps out of the group algebra R[Multiplicative (ZMod n)], and the target is Mathlib's subgroup of units whose nth power is one.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) :
      ↑↑((pointsMulEquiv n) f) = f.ofConv (MonoidAlgebra.single (generator n) 1)

      The points equivalence sends a point to its value on the standard generator.

      source
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_mapValue {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (n : ℕ) (φ : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) :
      (pointsMulEquiv n) ((AlgHom.mapValue φ) f) = (restrictRootsOfUnity (↑φ.toRingHom) n) ((pointsMulEquiv n) f)

      The points equivalence is natural in the value algebra.

      source
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_generator {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single (generator n) 1) = ↑↑ζ

      The inverse points equivalence sends a root of unity to the point taking the standard generator to that root.

      source
      @[simp]
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_generator_smul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) (r : R) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single (generator n) r) = r • ↑↑ζ

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

      source
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_zmod_val {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) [NeZero n] (ζ : ↥(rootsOfUnity n A)) (x : Multiplicative (ZMod n)) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single x 1) = ↑(↑ζ ^ (Multiplicative.toAdd x).val)

      The inverse μ_n points equivalence evaluates the group-like generator indexed by x : Multiplicative (ZMod n) as the corresponding power of the chosen root of unity.

      For x = generator n, this specializes to RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_generator.

      source
      @[simp]
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_zmod_val_smul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) [NeZero n] (ζ : ↥(rootsOfUnity n A)) (x : Multiplicative (ZMod n)) (r : R) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single x r) = r • ↑(↑ζ ^ (Multiplicative.toAdd x).val)

      The inverse μ_n points equivalence evaluates scalar multiples of the group-like generator indexed by x : Multiplicative (ZMod n) by scalar multiplication of the corresponding power of the chosen root of unity.

      source
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_ofAdd_val {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) [NeZero n] (ζ : ↥(rootsOfUnity n A)) (j : ZMod n) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single (Multiplicative.ofAdd j) 1) = ↑(↑ζ ^ j.val)

      The previous normal form, specialized to an additive residue class j : ZMod n.

      source
      theorem TauCeti.RootsOfUnityGroup.pointsMulEquiv_symm_apply_single_ofAdd_val_smul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) [NeZero n] (ζ : ↥(rootsOfUnity n A)) (j : ZMod n) (r : R) :
      ((pointsMulEquiv n).symm ζ).ofConv (MonoidAlgebra.single (Multiplicative.ofAdd j) r) = r • ↑(↑ζ ^ j.val)

      The scalar version of pointsMulEquiv_symm_apply_single_ofAdd_val.

      source
      theorem TauCeti.RootsOfUnityGroup.mapValue_pointsMulEquiv_symm_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (n : ℕ) (φ : A →ₐ[R] B) (ζ : ↥(rootsOfUnity n A)) :
      (AlgHom.mapValue φ) ((pointsMulEquiv n).symm ζ) = (pointsMulEquiv n).symm ((restrictRootsOfUnity (↑φ.toRingHom) n) ζ)

      Naturality of the inverse μ_n points equivalence in the value algebra: post-composing the point attached to ζ gives the point attached to the image of ζ.

      source
      theorem TauCeti.RootsOfUnityGroup.mapValue_pointsMulEquiv_symm_apply_single_zmod_val {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (n : ℕ) [NeZero n] (φ : A →ₐ[R] B) (ζ : ↥(rootsOfUnity n A)) (x : Multiplicative (ZMod n)) :
      ((AlgHom.mapValue φ) ((pointsMulEquiv n).symm ζ)).ofConv (MonoidAlgebra.single x 1) = φ ↑(↑ζ ^ (Multiplicative.toAdd x).val)

      Naturality of the inverse μ_n points equivalence, evaluated on an arbitrary cyclic group-algebra generator.

      source
      theorem TauCeti.RootsOfUnityGroup.mapValue_pointsMulEquiv_symm_apply_single_zmod_val_smul {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (n : ℕ) [NeZero n] (φ : A →ₐ[R] B) (ζ : ↥(rootsOfUnity n A)) (x : Multiplicative (ZMod n)) (r : R) :
      ((AlgHom.mapValue φ) ((pointsMulEquiv n).symm ζ)).ofConv (MonoidAlgebra.single x r) = φ (r • ↑(↑ζ ^ (Multiplicative.toAdd x).val))

      Naturality of the inverse μ_n points equivalence on scalar multiples of arbitrary cyclic group-algebra generators.