The graded symmetric algebra of a comodule

The symmetric algebra of a right comodule over a commutative bialgebra has a multiplicative coaction extending the coaction of its generators. Every homogeneous piece is stable under this coaction. Applied to the dual of a finite-dimensional representation, this is the graded homogeneous-coordinate algebra for its projective space, used in constructing projective orbits and homogeneous spaces.

The construction works over commutative semirings and requires neither freeness nor flatness. The comodule structure is selected explicitly, rather than installed as a global instance. Comodule morphisms induce morphisms of symmetric algebras, and algebra-valued points act by algebra homomorphisms on scalar extensions.

The construction and proof organization adapt TauCeti.Algebra.Coalgebra.Comodule.ExteriorAlgebra.Basic; the symmetric algebra uses Mathlib's SymmetricAlgebra.lift without the square-zero relation needed for the exterior algebra.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• J. S. Milne, Algebraic Groups (2017), §§7.d--7.f, for projective orbits and linear actions.

noncomputable def TauCeti.Comodule.symmetricAlgebraCoact (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : SymmetricAlgebra R M →ₐ[R] TensorProduct R (SymmetricAlgebra R M) H

The coaction of the symmetric algebra of a comodule, as an algebra homomorphism: it sends a generator ι m to ι m₍₀₎ ⊗ m₍₁₎, the coaction of m followed by the inclusion of generators.

Equations

• TauCeti.Comodule.symmetricAlgebraCoact R H M = SymmetricAlgebra.lift (LinearMap.rTensor H (SymmetricAlgebra.ι R M) ∘ₗ TauCeti.Comodule.coact)

@[simp]

theorem TauCeti.Comodule.symmetricAlgebraCoact_ι {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) : (symmetricAlgebraCoact R H M) ((SymmetricAlgebra.ι R M) m) = (LinearMap.rTensor H (SymmetricAlgebra.ι R M)) (coact m)

@[implicit_reducible]

noncomputable def TauCeti.Comodule.symmetricAlgebra (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : Comodule R H (SymmetricAlgebra R M)

The symmetric algebra of a right comodule over a commutative bialgebra, with the multiplicative coaction symmetricAlgebraCoact.

Following Comodule.tensor, this is deliberately not a global instance. Select it explicitly, or register it as a local instance.

Equations

• TauCeti.Comodule.symmetricAlgebra R H M = { coact := (TauCeti.Comodule.symmetricAlgebraCoact R H M).toLinearMap, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.symmetricAlgebra_coact {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : coact = (symmetricAlgebraCoact R H M).toLinearMap

The coaction of the symmetric-algebra comodule is symmetricAlgebraCoact.

noncomputable def TauCeti.Comodule.Hom.symmetricAlgebraι (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : Hom R H M (SymmetricAlgebra R M)

The inclusion ι : M → SymmetricAlgebra R M of generators, as a comodule morphism.

Equations

• TauCeti.Comodule.Hom.symmetricAlgebraι R H M = { toLinearMap := SymmetricAlgebra.ι R M, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraι_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : (symmetricAlgebraι R H M).toLinearMap = SymmetricAlgebra.ι R M

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraι_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) : (symmetricAlgebraι R H M) m = (SymmetricAlgebra.ι R M) m

noncomputable def TauCeti.Comodule.Hom.symmetricAlgebraMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) : Hom R H (SymmetricAlgebra R M) (SymmetricAlgebra R N)

The map of symmetric algebras induced by a comodule morphism, as a comodule morphism.

Equations

• f.symmetricAlgebraMap = { toLinearMap := (SymmetricAlgebra.map R f.toLinearMap).toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraMap_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) : f.symmetricAlgebraMap.toLinearMap = (SymmetricAlgebra.map R f.toLinearMap).toLinearMap

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraMap_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) (x : SymmetricAlgebra R M) : f.symmetricAlgebraMap x = (SymmetricAlgebra.map R f.toLinearMap) x

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraMap_id {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : symmetricAlgebraMap (CategoryTheory.CategoryStruct.id (ComoduleCat.of R H M)) = CategoryTheory.CategoryStruct.id (ComoduleCat.of R H (SymmetricAlgebra R M))

The symmetric-algebra functor on comodules preserves identities.

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraMap_comp {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [AddCommMonoid N] [Module R N] [Comodule R H N] [AddCommMonoid P] [Module R P] [Comodule R H P] (g : Hom R H N P) (f : Hom R H M N) : (g.comp f).symmetricAlgebraMap = g.symmetricAlgebraMap.comp f.symmetricAlgebraMap

The symmetric-algebra functor on comodules preserves composition.

@[simp]

theorem TauCeti.Comodule.Hom.symmetricAlgebraMap_comp_symmetricAlgebraι {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) : f.symmetricAlgebraMap.comp (symmetricAlgebraι R H M) = (symmetricAlgebraι R H N).comp f

The symmetric-algebra functor is compatible with the inclusion of generators.

theorem TauCeti.Comodule.symmetricAlgebraCoact_mem_decomposeTensor {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} {x : SymmetricAlgebra R M} (hx : x ∈ SymmetricAlgebra.homogeneousSubmodule R M n) : (symmetricAlgebraCoact R H M) x ∈ DirectSum.decomposeTensor (SymmetricAlgebra.homogeneousSubmodule R M) H n

The coaction preserves the symmetric grading: the coaction of a degree-n element lies in the image of the degree-n piece tensored with H.

noncomputable def TauCeti.Comodule.symmetricPowerSubcomodule (R : Type u_1) (H : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (n : ℕ) : Subcomodule R H (SymmetricAlgebra R M)

The degree-n homogeneous piece as a subcomodule of the symmetric algebra.

Equations

• TauCeti.Comodule.symmetricPowerSubcomodule R H M n = TauCeti.Subcomodule.ofSubmodule (TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) ⋯

@[simp]

theorem TauCeti.Comodule.symmetricPowerSubcomodule_toSubmodule {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (n : ℕ) : (symmetricPowerSubcomodule R H M n).toSubmodule = SymmetricAlgebra.homogeneousSubmodule R M n

@[simp]

theorem TauCeti.Comodule.mem_symmetricPowerSubcomodule {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {n : ℕ} {x : SymmetricAlgebra R M} : x ∈ symmetricPowerSubcomodule R H M n ↔ x ∈ SymmetricAlgebra.homogeneousSubmodule R M n

noncomputable def TauCeti.Comodule.symmetricAlgebraEndOfPoint {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) : TensorProduct R A (SymmetricAlgebra R M) →ₐ[A] TensorProduct R A (SymmetricAlgebra R M)

The action of an A-point g of H on the scalar extension A ⊗[R] SymmetricAlgebra R M, as an A-algebra homomorphism. Its underlying linear map is endOfPoint (symmetricAlgebraEndOfPoint_toLinearMap), so points act on the symmetric algebra multiplicatively.

Equations

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

theorem TauCeti.Comodule.symmetricAlgebraEndOfPoint_toLinearMap {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) : (symmetricAlgebraEndOfPoint g).toLinearMap = endOfPoint (SymmetricAlgebra R M) g

The algebra homomorphism symmetricAlgebraEndOfPoint g is the action endOfPoint of the point g on the symmetric-algebra comodule.

@[simp]

theorem TauCeti.Comodule.symmetricAlgebraEndOfPoint_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring H] [Bialgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {A : Type u_6} [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) (x : TensorProduct R A (SymmetricAlgebra R M)) : (symmetricAlgebraEndOfPoint g) x = (endOfPoint (SymmetricAlgebra R M) g) x