Trivial point representations

This file synchronizes the trivial operations across the fixed-object correspondence between point representations of an affine group and comodules over its commutative Hopf algebra.

Every module has a trivial point representation, in which every point acts by the identity on scalar extension. This construction agrees with the point representation induced by the trivial comodule. No finiteness, freeness, projectivity, flatness, or nontriviality hypothesis is used.

Main declarations

• HopfAlgebra.PointRepresentation.trivial: the identity action on scalar extensions of an arbitrary module.
• HopfAlgebra.PointRepresentation.ofComodule_trivial and HopfAlgebra.PointRepresentation.toComodule_trivial: compatibility with the trivial comodule in both directions.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 4(a), Remark 4.1.
• J. S. Milne, Reductive Groups, §§5.1--5.4.

noncomputable def TauCeti.HopfAlgebra.PointRepresentation.trivial {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] : PointRepresentation

The trivial point representation on an arbitrary module. Every point acts by the identity linear automorphism after scalar extension.

Equations

• TauCeti.HopfAlgebra.PointRepresentation.trivial = TauCeti.HopfAlgebra.PointRepresentation.ofComodule TauCeti.Comodule.trivial

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.trivial_action {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (A : CommAlgCat R) (x : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom (trivial.action A)) x = 1

Every point acts as the identity in the trivial point representation.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_trivial {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] : ofComodule Comodule.trivial = trivial

The point representation induced by the trivial comodule is the trivial point representation.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.toComodule_trivial {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] : trivial.toComodule = Comodule.trivial

Recovering the comodule of the trivial point representation gives the trivial comodule.