The additive group

The affine scheme Spec (SymmetricAlgebra R M) is the additive (vector) group on M. Its functor of points is computed here: for a commutative R-algebra A, the convolution monoid of R-algebra maps SymmetricAlgebra R M →ₐ[R] A is the additive monoid of R-linear maps M →ₗ[R] A, with convolution corresponding to addition. Taking M = R recovers the one-dimensional additive group 𝔾ₐ = Spec R[X], whose A-valued points are (A, +); the R-points are this construction specialized to A = R.

Main declarations

• TauCeti.AdditiveGroup.pointsMulEquiv: the convolution monoid of points SymmetricAlgebra R M →ₐ[R] A is the additive monoid M →ₗ[R] A.
• TauCeti.AdditiveGroup.gaPointsMulEquiv: the monoid of A-valued points of 𝔾ₐ over R is the additive monoid of A.
• TauCeti.AdditiveGroup.gaPointParamMul: multiplication of the parameters of two 𝔾ₐ-points.
• TauCeti.AdditiveGroup.pointsMulEquiv_mapValue: the points equivalence is natural in the value algebra.

See also

The symmetric-algebra Hopf structure is supplied by TauCeti.Algebra.HopfAlgebra.SymmetricAlgebra.Basic, on top of Mathlib's symmetric-algebra bialgebra and convolution monoid APIs.

noncomputable def TauCeti.AdditiveGroup.pointsMulEquiv {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] : WithConv (SymmetricAlgebra R M →ₐ[R] A) ≃* Multiplicative (M →ₗ[R] A)

The convolution monoid of points of a vector group. For a commutative R-algebra A, the convolution monoid of R-algebra maps out of SymmetricAlgebra R M is the additive monoid of R-linear maps M →ₗ[R] A: a point F corresponds to the linear map x ↦ F (ι x), and convolution of points corresponds to addition of linear maps.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AdditiveGroup.toAdd_pointsMulEquiv {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) : Multiplicative.toAdd (pointsMulEquiv F) = SymmetricAlgebra.lift.symm F.ofConv

A point of the additive group, as a linear map, is x ↦ F (ι x).

theorem TauCeti.AdditiveGroup.toAdd_pointsMulEquiv_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) (x : M) : (Multiplicative.toAdd (pointsMulEquiv F)) x = F.ofConv ((SymmetricAlgebra.ι R M) x)

The linear map underlying a point evaluates as x ↦ F (ι x).

@[simp]

theorem TauCeti.AdditiveGroup.pointsMulEquiv_symm_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] (φ : Multiplicative (M →ₗ[R] A)) : pointsMulEquiv.symm φ = WithConv.toConv (SymmetricAlgebra.lift (Multiplicative.toAdd φ))

The inverse equivalence sends a linear map to the corresponding algebra map.

theorem TauCeti.AdditiveGroup.toAdd_pointsMulEquiv_mapValue {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) : Multiplicative.toAdd (pointsMulEquiv ((AlgHom.mapValue φ) F)) = φ.toLinearMap ∘ₗ Multiplicative.toAdd (pointsMulEquiv F)

Reading a vector-group point as a linear map is natural in the value algebra: post-composing the point with an R-algebra map post-composes the corresponding linear map.

theorem TauCeti.AdditiveGroup.pointsMulEquiv_mapValue {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) : pointsMulEquiv ((AlgHom.mapValue φ) F) = Multiplicative.ofAdd (φ.toLinearMap ∘ₗ Multiplicative.toAdd (pointsMulEquiv F))

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

theorem TauCeti.AdditiveGroup.mapValue_pointsMulEquiv_symm_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (ψ : Multiplicative (M →ₗ[R] A)) : (AlgHom.mapValue φ) (pointsMulEquiv.symm ψ) = pointsMulEquiv.symm (Multiplicative.ofAdd (φ.toLinearMap ∘ₗ Multiplicative.toAdd ψ))

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

@[simp]

theorem TauCeti.AdditiveGroup.pointsMulEquiv_inv {R : Type u} [CommRing R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommRing A] [Algebra R A] (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) : pointsMulEquiv F⁻¹ = (pointsMulEquiv F)⁻¹

Over commutative rings, pointsMulEquiv identifies the convolution inverse of a point with negation of the corresponding linear map.

theorem TauCeti.AdditiveGroup.toAdd_pointsMulEquiv_inv {R : Type u} [CommRing R] {M : Type v} [AddCommMonoid M] [Module R M] {A : Type w} [CommRing A] [Algebra R A] (F : WithConv (SymmetricAlgebra R M →ₐ[R] A)) : Multiplicative.toAdd (pointsMulEquiv F⁻¹) = -Multiplicative.toAdd (pointsMulEquiv F)

In additive notation, the convolution inverse of a point corresponds to negating its linear map of generator values.

noncomputable def TauCeti.AdditiveGroup.gaPointsMulEquiv {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] : WithConv (SymmetricAlgebra R R →ₐ[R] A) ≃* Multiplicative A

The one-dimensional additive monoid of points for 𝔾ₐ = Spec (SymmetricAlgebra R R). Specializing the vector group to M = R, the convolution monoid of A-valued points over R is the additive monoid (A, +).

Equations

• TauCeti.AdditiveGroup.gaPointsMulEquiv = TauCeti.AdditiveGroup.pointsMulEquiv.trans (AddEquiv.toMultiplicative (LinearMap.ringLmapEquivSelf R R A).toAddEquiv)

@[simp]

theorem TauCeti.AdditiveGroup.toAdd_gaPointsMulEquiv {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : Multiplicative.toAdd (gaPointsMulEquiv F) = F.ofConv ((SymmetricAlgebra.ι R R) 1)

A point of 𝔾ₐ is the additive group element obtained by evaluating it at the generator ι 1.

@[simp]

theorem TauCeti.AdditiveGroup.gaPointsMulEquiv_symm_apply_ι {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] (a : Multiplicative A) : (gaPointsMulEquiv.symm a).ofConv ((SymmetricAlgebra.ι R R) 1) = Multiplicative.toAdd a

The inverse equivalence sends an element of the value algebra to the corresponding A-valued point of 𝔾ₐ.

theorem TauCeti.AdditiveGroup.toAdd_gaPointsMulEquiv_mapValue {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : Multiplicative.toAdd (gaPointsMulEquiv ((AlgHom.mapValue φ) F)) = φ (Multiplicative.toAdd (gaPointsMulEquiv F))

Reading a 𝔾ₐ-point as an element of the value algebra is natural in the value algebra: post-composing the point with an R-algebra map applies that map to the corresponding element.

theorem TauCeti.AdditiveGroup.gaPointsMulEquiv_mapValue {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : gaPointsMulEquiv ((AlgHom.mapValue φ) F) = Multiplicative.ofAdd (φ (Multiplicative.toAdd (gaPointsMulEquiv F)))

The 𝔾ₐ points equivalence is natural in the value algebra.

theorem TauCeti.AdditiveGroup.mapValue_gaPointsMulEquiv_symm_apply {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (a : Multiplicative A) : (AlgHom.mapValue φ) (gaPointsMulEquiv.symm a) = gaPointsMulEquiv.symm (Multiplicative.ofAdd (φ (Multiplicative.toAdd a)))

Naturality of the inverse 𝔾ₐ points equivalence in the value algebra.

noncomputable def TauCeti.AdditiveGroup.gaPointParamMul {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] (F G : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : WithConv (SymmetricAlgebra R R →ₐ[R] A)

The A-valued point of 𝔾ₐ whose parameter is the product of the parameters of F and G.

This is not the convolution multiplication of 𝔾ₐ(A): convolution corresponds to addition, whereas gaPointParamMul F G records multiplication in the value algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AdditiveGroup.gaPointsMulEquiv_gaPointParamMul {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] (F G : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : gaPointsMulEquiv (gaPointParamMul F G) = Multiplicative.ofAdd (Multiplicative.toAdd (gaPointsMulEquiv F) * Multiplicative.toAdd (gaPointsMulEquiv G))

Under the points equivalence, gaPointParamMul is multiplication in the value algebra.

@[simp]

theorem TauCeti.AdditiveGroup.gaPointParamMul_apply_ι {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] (F G : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : (gaPointParamMul F G).ofConv ((SymmetricAlgebra.ι R R) 1) = F.ofConv ((SymmetricAlgebra.ι R R) 1) * G.ofConv ((SymmetricAlgebra.ι R R) 1)

The value of gaPointParamMul F G on the additive coordinate is the product of the two original coordinate values.

theorem TauCeti.AdditiveGroup.mapValue_gaPointParamMul {R : Type u} [CommSemiring R] {A : Type w} [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : A →ₐ[R] B) (F G : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : (AlgHom.mapValue φ) (gaPointParamMul F G) = gaPointParamMul ((AlgHom.mapValue φ) F) ((AlgHom.mapValue φ) G)

Multiplication of 𝔾ₐ-point parameters is natural in the value algebra.

@[simp]

theorem TauCeti.AdditiveGroup.gaPointsMulEquiv_inv {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : gaPointsMulEquiv F⁻¹ = (gaPointsMulEquiv F)⁻¹

Over commutative rings, gaPointsMulEquiv identifies the convolution inverse of a 𝔾ₐ-point with negation in the value ring.

theorem TauCeti.AdditiveGroup.toAdd_gaPointsMulEquiv_inv {R : Type u} [CommRing R] {A : Type w} [CommRing A] [Algebra R A] (F : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : Multiplicative.toAdd (gaPointsMulEquiv F⁻¹) = -Multiplicative.toAdd (gaPointsMulEquiv F)

In additive notation, the convolution inverse of a 𝔾ₐ-point is the negative of its value on the generator ι 1.