Lean declarations

theorem Langlands.AlgebraicGeometry.trivialCoaction_apply LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Comodule
```
theorem trivialCoaction_apply (v : V) :
    trivialCoaction R B V v = v ⊗ₜ[R] (1 : B)
```
def Langlands.AlgebraicGeometry.trivialCoaction LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Comodule
The coaction of the **trivial comodule**: `v ↦ v ⊗ 1`.
```
def trivialCoaction : V →ₗ[R] V ⊗[R] B :=
  (TensorProduct.mk R V B).flip 1
```

def Langlands.AlgebraicGeometry.trivialComodule LanglandsLean @ main, LanglandsLean.AlgebraicGeometry.Comodule

def trivialComodule : Comodule R B V where
  coaction := trivialCoaction R B V
  coassoc := by
    ext v
    simp [trivialCoaction, Algebra.TensorProduct.one_def]
  counit := by
    ext v
    simp [trivialCoaction]

Modules: LanglandsLean.AlgebraicGeometry.Comodule

Trivial Representation as a Comodule

Let \(R\) be a commutative semiring, let \(A\) be a bialgebra over \(R\), and let \(V\) be an \(R\)-module. The trivial \(A\)-comodule on \(V\) has coaction

\[ \rho(v) = v \otimes 1. \]

This satisfies the axioms of an \(A\)-comodule: coassociativity follows from \[ \Delta(1)=1\otimes 1, \] and the counit axiom follows from \(\varepsilon(1)=1\).

When \(A = \mathcal{O}(G)\) is the coordinate Hopf algebra of an affine group scheme \(G\), this comodule corresponds to the representation on which every \(R\)-point of \(G\) acts by the identity on \(V\).