The additive group scheme

For a commutative ring R, the one-dimensional additive group is represented by the symmetric Hopf algebra

R[x] = SymmetricAlgebra R R, with x = SymmetricAlgebra.ι R R 1.

The generator is primitive, its counit is zero, and its antipode is -x. Applying relative spectrum packages this Hopf algebra as a group object over Spec R. This file exposes the underlying spectrum, structural morphism, multiplication source, and the three group operations through Tau Ceti's generic Hopf-spectrum projection interface, which is otherwise out of reach: the resulting group scheme is a def whose body is not exposed outside this module.

The singleton basis of R identifies the coordinate algebra with a polynomial algebra on the same-universe singleton ULift (Fin 1). Contravariant spectrum and Mathlib's affine-space spectrum isomorphism then identify the underlying scheme with affine one-space over Spec R. The identification is packaged in Over (Spec R), so compatibility with the structural morphism is part of the isomorphism. This uses only the algebra equivalence: the standard bialgebra instance on MvPolynomial has group-like variables and is not the additive Hopf structure.

For a same-universe commutative R-algebra A, Mathlib's spectrum-points equivalence followed by AdditiveGroup.gaPointsMulEquiv identifies scheme-valued points with (A, +). The resulting identification is natural in A. The construction includes the zero ring and zero value algebra. The same-universe restriction comes from the current hopfSpec, Spec.mapMulEquiv, and affine-space APIs.

Main declarations

• TauCeti.AdditiveGroup.coordinateHopfAlgebra: the symmetric Hopf algebra representing G_a.
• TauCeti.AdditiveGroup.coordinateAlgEquiv: its rank-one polynomial presentation.
• TauCeti.AdditiveGroup.connectedSpace_primeSpectrum_coordinateHopfAlgebra: its prime spectrum is connected over a domain.
• TauCeti.AdditiveGroup.isReduced_coordinateHopfAlgebra: it is reduced over a reduced ring.
• TauCeti.AdditiveGroup.groupScheme: the additive group scheme over Spec R.
• TauCeti.AdditiveGroup.groupSchemeAffineSpaceIso: its canonical identification with affine one-space over the base.
• TauCeti.AdditiveGroup.groupScheme_one_left, TauCeti.AdditiveGroup.groupScheme_mul_left, and TauCeti.AdditiveGroup.groupScheme_inv_left: the underlying scheme maps of its operations.
• TauCeti.AdditiveGroup.isAffine_groupScheme and TauCeti.AdditiveGroup.locallyOfFinitePresentation_groupScheme: affineness and local finite presentation. Local finite type follows by instance search.
• TauCeti.AdditiveGroup.groupSchemePointMulEquiv: the canonical passage between algebra points and scheme-valued points.
• TauCeti.AdditiveGroup.schemePointsMulEquiv: scheme-valued points are the additive group of the value algebra.
• TauCeti.AdditiveGroup.gaSchemePointParamMul: the scheme-valued point whose parameter is the product of two parameters in the value algebra.
• TauCeti.AdditiveGroup.schemePointsMulEquiv_mapValue: covariance in the value algebra.

References

The Hopf structure and algebra-valued point calculation are TauCeti.Algebra.HopfAlgebra.SymmetricAlgebra.Basic and TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Basic. The operation formulas specialize TauCeti.AlgebraicGeometry.AffineGroupScheme.HopfSpec. The affine coordinate presentation follows the spectrum-transport pattern in TauCetiProject/TauCeti, revision 90f7e09cf472553c4d268db39fcae6b84bd91e04, TauCeti/Algebra/AlgebraicGroup/GeneralLinear/Scheme.lean (Apache 2.0), specialized to Mathlib's rank-one symmetric-algebra and affine-space equivalences. The scheme-valued-points interface follows the Lean Zulip discussion #Is there code for X? > Algebraic groups.

@[reducible, inline]

abbrev TauCeti.AdditiveGroup.CoordinateIndex : Type u

A singleton coordinate index in the same universe as the base ring.

Equations

• TauCeti.AdditiveGroup.CoordinateIndex = ULift.{?u.1, 0} (Fin 1)

noncomputable def TauCeti.AdditiveGroup.coordinateAlgEquiv (R : Type u) [CommSemiring R] : SymmetricAlgebra R R ≃ₐ[R] MvPolynomial CoordinateIndex R

The rank-one symmetric algebra is the polynomial algebra on a same-universe singleton.

Equations

• TauCeti.AdditiveGroup.coordinateAlgEquiv R = SymmetricAlgebra.equivMvPolynomial (TauCeti.AdditiveGroup.coordinateBasis✝ R)

@[simp]

theorem TauCeti.AdditiveGroup.coordinateAlgEquiv_ι_one (R : Type u) [CommSemiring R] : (coordinateAlgEquiv R) ((SymmetricAlgebra.ι R R) 1) = MvPolynomial.X default

The polynomial presentation sends the additive coordinate ι(1) to the unique variable.

@[reducible, inline]

noncomputable abbrev TauCeti.AdditiveGroup.coordinateHopfAlgebra (R : Type u) [CommRing R] : CommHopfAlgCat R

The commutative Hopf algebra representing the one-dimensional additive group. Its carrier is SymmetricAlgebra R R, with primitive generator SymmetricAlgebra.ι R R 1.

Equations

• TauCeti.AdditiveGroup.coordinateHopfAlgebra R = ↧(SymmetricAlgebra R R)

instance TauCeti.AdditiveGroup.instSmoothSymmetricAlgebra (R : Type u) [CommRing R] : Algebra.Smooth R (SymmetricAlgebra R R)

The coordinate algebra of 𝔾ₐ is smooth: it is the polynomial algebra on the single generator x.

theorem TauCeti.AdditiveGroup.connectedSpace_primeSpectrum_coordinateHopfAlgebra (R : Type u) [CommRing R] [IsDomain R] : ConnectedSpace (PrimeSpectrum ↑(coordinateHopfAlgebra R))

The coordinate Hopf algebra of 𝔾ₐ has connected prime spectrum over a domain.

theorem TauCeti.AdditiveGroup.isReduced_coordinateHopfAlgebra (R : Type u) [CommRing R] [IsReduced R] : IsReduced ↑(coordinateHopfAlgebra R)

The coordinate Hopf algebra of 𝔾ₐ is reduced over a reduced ring: it is the polynomial algebra on the single generator x.

noncomputable def TauCeti.AdditiveGroup.groupScheme (R : Type u) [CommRing R] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The additive group scheme obtained by applying relative spectrum to the symmetric Hopf algebra on one generator.

The same-universe restriction is imposed by Mathlib's current hopfSpec construction.

Equations

• TauCeti.AdditiveGroup.groupScheme R = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (TauCeti.AdditiveGroup.coordinateHopfAlgebra R))

theorem TauCeti.AdditiveGroup.groupScheme_def (R : Type u) [CommRing R] : groupScheme R = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (coordinateHopfAlgebra R))

The additive group scheme is the relative spectrum of its coordinate Hopf algebra.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_X_left (R : Type u) [CommRing R] : (groupScheme R).X.left = AlgebraicGeometry.Spec ↧(SymmetricAlgebra R R)

The scheme underlying the additive group scheme is the spectrum of its symmetric coordinate algebra.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_X_hom (R : Type u) [CommRing R] : (groupScheme R).X.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (SymmetricAlgebra R R))))

The structural morphism of the additive group scheme is induced by the symmetric algebra's R-algebra structure map.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_tensor_X_left (R : Type u) [CommRing R] : (CategoryTheory.MonoidalCategoryStruct.tensorObj (groupScheme R).X (groupScheme R).X).left = CategoryTheory.Limits.pullback (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (SymmetricAlgebra R R)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (SymmetricAlgebra R R))))

The source of multiplication is the standard affine fibre product of two copies of the coordinate spectrum over Spec R.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_one_left (R : Type u) [CommRing R] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.counitAlgHom R (SymmetricAlgebra R R)))) (CategoryTheory.eqToHom ⋯)

The unit of the additive group scheme is induced contravariantly by the symmetric-algebra counit.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_mul_left (R : Type u) [CommRing R] : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R (SymmetricAlgebra R R) (SymmetricAlgebra R R)).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Bialgebra.comulAlgHom R (SymmetricAlgebra R R)))) (CategoryTheory.eqToHom ⋯)))

Multiplication on the additive group scheme is induced contravariantly by the primitive comultiplication. The first two maps identify its source with the spectrum of the tensor square.

@[simp]

theorem TauCeti.AdditiveGroup.groupScheme_inv_left (R : Type u) [CommRing R] : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(HopfAlgebra.antipodeAlgHom R (SymmetricAlgebra R R)))) (CategoryTheory.eqToHom ⋯))

Inversion on the additive group scheme is induced contravariantly by the antipode x ↦ -x.

noncomputable def TauCeti.AdditiveGroup.groupSchemeAffineSpaceIso (R : Type u) [CommRing R] : (groupScheme R).X ≅ (AlgebraicGeometry.AffineSpace CoordinateIndex (AlgebraicGeometry.Spec ↧R)).asOver (AlgebraicGeometry.Spec ↧R)

The additive group scheme's underlying scheme is canonically affine one-space over Spec R.

This is an isomorphism in Over (Spec R), not an isomorphism of Hopf algebras or group objects. The polynomial presentation is used only as an algebra presentation.

Equations

• TauCeti.AdditiveGroup.groupSchemeAffineSpaceIso R = CategoryTheory.Over.isoMk (TauCeti.AdditiveGroup.groupSchemeAffineSpaceIsoLeft✝ R) ⋯

@[simp]

theorem TauCeti.AdditiveGroup.groupSchemeAffineSpaceIso_hom_left (R : Type u) [CommRing R] : CategoryTheory.Over.Hom.left (groupSchemeAffineSpaceIso R).hom = (CategoryTheory.eqToIso ⋯ ≪≫ AlgebraicGeometry.Scheme.Spec.mapIso (coordinateAlgEquiv R).symm.toRingEquiv.toCommRingCatIso.op ≪≫ (AlgebraicGeometry.AffineSpace.SpecIso CoordinateIndex ↧R).symm).hom

The underlying scheme map of the affine-one-space identification is the contravariant spectrum map from the rank-one polynomial presentation, followed by Mathlib's affine-space spectrum isomorphism.

instance TauCeti.AdditiveGroup.isAffine_groupScheme (R : Type u) [CommRing R] : AlgebraicGeometry.IsAffine (groupScheme R).X.left

The additive group scheme is affine.

instance TauCeti.AdditiveGroup.locallyOfFinitePresentation_groupScheme (R : Type u) [CommRing R] : AlgebraicGeometry.LocallyOfFinitePresentation (groupScheme R).X.hom

The structural morphism of the additive group scheme is locally of finite presentation.

noncomputable def TauCeti.AdditiveGroup.groupSchemePointMulEquiv {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : WithConv (SymmetricAlgebra R R →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X)

Mathlib's spectrum-points equivalence, with its target presented as the underlying object of the additive group scheme. It sends an algebra point to its contravariant spectrum morphism.

The retyping is what makes the equivalence usable: groupScheme is not exposed outside this module, so AlgebraicGeometry.Spec.mapMulEquiv cannot be applied to a point of (groupScheme R).X downstream.

Equations

• TauCeti.AdditiveGroup.groupSchemePointMulEquiv A = TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation (TauCeti.AdditiveGroup.coordinateHopfAlgebra R) A ⋯

@[simp]

theorem TauCeti.AdditiveGroup.groupSchemePointMulEquiv_apply_left {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (f : WithConv (SymmetricAlgebra R R →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv A) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying map of the spectrum point associated to an algebra point.

noncomputable def TauCeti.AdditiveGroup.schemePointsMulEquiv {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) ≃* Multiplicative A

The group of scheme-valued points of the additive group scheme is the additive group of the value algebra.

The source consists of morphisms over Spec R from Spec A to the underlying object of groupScheme R. It is written multiplicatively to match the group law on a hom-set into a group object.

Equations

• TauCeti.AdditiveGroup.schemePointsMulEquiv A = (TauCeti.AdditiveGroup.groupSchemePointMulEquiv A).symm.trans TauCeti.AdditiveGroup.gaPointsMulEquiv

noncomputable def TauCeti.AdditiveGroup.gaSchemePointParamMul {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X

The scheme-valued point whose additive parameter is the product of the parameters of p and q in the value algebra. This is not the group operation on scheme-valued points, which adds parameters.

Equations

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

@[simp]

theorem TauCeti.AdditiveGroup.gaSchemePointParamMul_groupSchemePointMulEquiv {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (F G : WithConv (↑(coordinateHopfAlgebra R) →ₐ[R] A)) : gaSchemePointParamMul A ((groupSchemePointMulEquiv A) F) ((groupSchemePointMulEquiv A) G) = (groupSchemePointMulEquiv A) (gaPointParamMul F G)

Scheme-point parameter multiplication transports algebra-point parameter multiplication through the canonical spectrum-points equivalence.

@[simp]

theorem TauCeti.AdditiveGroup.schemePointsMulEquiv_gaSchemePointParamMul {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : (schemePointsMulEquiv A) (gaSchemePointParamMul A p q) = Multiplicative.ofAdd (Multiplicative.toAdd ((schemePointsMulEquiv A) p) * Multiplicative.toAdd ((schemePointsMulEquiv A) q))

Under the scheme-points equivalence, gaSchemePointParamMul p q has parameter equal to the product of the parameters of p and q in the value algebra.

theorem TauCeti.AdditiveGroup.toAdd_schemePointsMulEquiv {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : Multiplicative.toAdd ((schemePointsMulEquiv A) p) = ((groupSchemePointMulEquiv A).symm p).ofConv ((SymmetricAlgebra.ι R R) 1)

A scheme-valued point corresponds to the value at the additive coordinate ι(1) of its canonical algebra point.

@[simp]

theorem TauCeti.AdditiveGroup.schemePointsMulEquiv_groupSchemePointMulEquiv {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (q : WithConv (↑(coordinateHopfAlgebra R) →ₐ[R] A)) : (schemePointsMulEquiv A) ((groupSchemePointMulEquiv A) q) = gaPointsMulEquiv q

Evaluating the scheme-points equivalence on a point presented by groupSchemePointMulEquiv recovers the canonical algebra point.

theorem TauCeti.AdditiveGroup.schemePointsMulEquiv_apply {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : (schemePointsMulEquiv A) p = gaPointsMulEquiv ((groupSchemePointMulEquiv A).symm p)

Evaluating the scheme-points equivalence directly on a scheme morphism.

theorem TauCeti.AdditiveGroup.schemePointsMulEquiv_symm_apply {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] (a : Multiplicative A) : (schemePointsMulEquiv A).symm a = (groupSchemePointMulEquiv A) (gaPointsMulEquiv.symm a)

The inverse scheme-points equivalence sends an element of the value algebra to the spectrum map induced by the corresponding symmetric-algebra point.

theorem TauCeti.AdditiveGroup.schemePointsMulEquiv_mapValue {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : (schemePointsMulEquiv B) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = Multiplicative.ofAdd (φ (Multiplicative.toAdd ((schemePointsMulEquiv A) p)))

The scheme-valued point identification is covariantly natural in the value algebra. An R-algebra map A → B becomes precomposition by the reversed spectrum map, and sends the corresponding additive value a to its image in B.

theorem TauCeti.AdditiveGroup.mapValue_gaSchemePointParamMul {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (p q : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R).X) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) (gaSchemePointParamMul A p q) = gaSchemePointParamMul B (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) q)

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