Documentation

TauCeti.Algebra.AlgebraicGroup.Trivial

The trivial affine group #

This file records the functor-of-points calculation for the trivial affine group scheme. Its coordinate Hopf algebra is the base ring R, with Mathlib's canonical Hopf algebra structure on R over itself. For every commutative R-algebra A, there is exactly one R-algebra homomorphism R →ₐ[R] A, namely Algebra.ofId R A; consequently the convolution group of A-points is the one-element group PUnit.

The scheme Spec R over Spec R represents the trivial group-valued functor and is the terminal affine group scheme over R.

Main declarations #

References #

This uses Mathlib's Algebra.ofId, its Subsingleton (R →ₐ[R] A) instance, and the canonical Hopf algebra structure on R over itself from Mathlib.RingTheory.HopfAlgebra.Basic.

source
@[simp]
theorem WithConv.ofConv_eq_ofId {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (f : WithConv (R →ₐ[R] A)) :
f.ofConv = Algebra.ofId R A

The underlying algebra map of a convolution point out of the base ring is Algebra.ofId. The value algebra need not be commutative.

source
theorem WithConv.convPoint_eq_one {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : WithConv (R →ₐ[R] A)) :
f = 1

The unique convolution point is the identity point.

source
@[simp]
theorem WithConv.convPoint_eq_one_iff {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : WithConv (R →ₐ[R] A)) :
f = 1 ↔ True

The identity normal form for trivial-group convolution points, as a simp proposition.

source
noncomputable def TauCeti.TrivialGroup.pointsMulEquiv {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] :
WithConv (R →ₐ[R] A) ≃* PUnit.{1}

The functor of points of the trivial affine group is the one-element group.

The source is the convolution group of R-algebra maps out of the Hopf algebra R; since there is only one such algebra map, the convolution group is multiplicatively equivalent to PUnit.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.TrivialGroup.pointsMulEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (f : WithConv (R →ₐ[R] A)) :
    pointsMulEquiv f = PUnit.unit

    The equivalence sends every convolution point to the unique element of PUnit.

    source
    @[simp]
    theorem TauCeti.TrivialGroup.pointsMulEquiv_symm_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (u : PUnit.{1}) :
    pointsMulEquiv.symm u = WithConv.toConv (Algebra.ofId R A)

    The inverse equivalence sends the unique element of PUnit to Algebra.ofId R A.

    source
    theorem TauCeti.TrivialGroup.pointsMulEquiv_mapValue {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type w} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (R →ₐ[R] A)) :
    pointsMulEquiv ((AlgHom.mapValue φ) f) = pointsMulEquiv f

    The trivial-group points equivalence is natural in the value algebra.

    source
    theorem TauCeti.TrivialGroup.mapValue_pointsMulEquiv_symm_apply {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type w} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (u : PUnit.{1}) :
    (AlgHom.mapValue φ) (pointsMulEquiv.symm u) = pointsMulEquiv.symm u

    Naturality of the inverse trivial-group points equivalence in the value algebra.