Lean declarations

lemma Polynomial.gaAntipode_X LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
```
@[simp] lemma gaAntipode_X : gaAntipode R (X : R[X]) = -(X : R[X])
```

lemma Polynomial.gaComul_X LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga

@[simp] lemma gaComul_X :
    gaComul R (X : Polynomial R) =
      (X : Polynomial R) ⊗ₜ[R] (1 : Polynomial R) +
        (1 : Polynomial R) ⊗ₜ[R] (X : Polynomial R)

lemma Polynomial.gaCounit_X LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
```
@[simp] lemma gaCounit_X : gaCounit R (X : R[X]) = 0
```

def Polynomial.gaComul LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga

noncomputable def gaComul :
    Polynomial R →ₐ[R] TensorProduct R (Polynomial R) (Polynomial R) :=
  aeval (R := R) (A := TensorProduct R (Polynomial R) (Polynomial R))
    ((X : Polynomial R) ⊗ₜ[R] (1 : Polynomial R) +
      (1 : Polynomial R) ⊗ₜ[R] (X : Polynomial R))

def Polynomial.gaCounit LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
```
noncomputable def gaCounit : R[X] →ₐ[R] R :=
  aeval (R := R) (A := R) (0 : R)
```

def Polynomial.gaAntipode LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga

noncomputable def gaAntipode : R[X] →ₐ[R] R[X] :=
  aeval (R := R) (A := R[X]) (-(X : R[X]))

instance Polynomial.instBialgebra LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
The bialgebra structure on `R[X]` with primitive `X`.
```
noncomputable instance instBialgebra : Bialgebra R R[X]
```
instance Polynomial.instHopfAlgebra LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
The Hopf algebra structure on `R[X]` with antipode `X ↦ -X`.
```
noncomputable instance instHopfAlgebra : HopfAlgebra R R[X]
```
def Langlands.AlgebraicGeometry.Examples.additiveGroup LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
The additive group scheme `G_{a,R} = Spec R[X]` over `Spec R`.
```
noncomputable def additiveGroup :
    Over (Scheme.Spec.obj (op R)) :=
  specObjOver R (Polynomial R)
```
instance Langlands.AlgebraicGeometry.Examples.additiveGroup.instGrpObj LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
```
noncomputable instance additiveGroup.instGrpObj :
    GrpObj (additiveGroup R) :=
  hopfSpecGrpObj R (Polynomial R)
```
noncomputable abbrev Langlands.AlgebraicGeometry.Examples.Ga LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Examples.Ga
The underlying scheme of `additiveGroup R`: `Spec R[X]`.
```
noncomputable abbrev Ga : Scheme.{u}
```

Modules: LanglandsLean.AlgebraicGeometry.Examples.Ga

Additive Group Scheme \(\mathbb{G}_a\)

Let \(S\) be a scheme. The additive group scheme over \(S\), denoted \(\mathbb{G}_{a,S}\), is defined by base change from the integers:

\[ \mathbb{G}_{a,S} \;=\; S \,\times_{\operatorname{Spec} \mathbb{Z}}\, \operatorname{Spec} \mathbb{Z}[T]. \]

Its coordinate Hopf algebra over the base is the polynomial ring in one variable \(T\), with the additive Hopf structure:

\[ \Delta(T) = T \otimes 1 + 1 \otimes T, \qquad \varepsilon(T) = 0, \qquad S(T) = -T. \]

The structure morphism \(\mathbb{G}_{a,S} \to S\) is the first projection of the fiber product; it is affine (Spec of a polynomial ring is affine relative to the base) and locally of finite type (a polynomial ring in one variable is finitely generated).

Hence \(\mathbb{G}_{a,S}\) is an algebraic group over \(S\) (or, in characteristic \(0\), a smooth one-dimensional algebraic group). Its functor of points is identified by the additive points formula.

Used by

Points of 𝔾_a Are the Additive Group of R