Point representations and comodules

Let H be a commutative Hopf algebra over a commutative ring R, and let V be an R-module. This file identifies natural actions of the represented point groups

A ↦ Hom_{R-alg}(H, A)

on the scalar extensions A ⊗[R] V with right H-comodule structures on V. The base ring, Hopf algebra, and module may lie in separate universes. The value-algebra category is placed in their maximum universe, so the universal values H, R, and H ⊗[R] H are accessed through their canonical universe lifts.

The action associated to a coaction ρ(v) = ∑ v₀ ⊗ v₁ is characterized by

(a ⊗ v) ↦ ∑ a * x(v₁) ⊗ v₀

at a point x : H →ₐ[R] A. Conversely, the coaction is recovered by evaluating at the universal point id_H and flipping the two tensor factors. The constructions are inverse without any finiteness, freeness, projectivity, flatness, or nontriviality hypothesis.

Main declarations

• HopfAlgebra.PointRepresentation: a natural action on the scalar extensions of V.
• HopfAlgebra.PointRepresentation.ofComodule: the point representation induced by a coaction.
• HopfAlgebra.PointRepresentation.ofComodule_action_val_eq_endOfPoint: identification of the induced representation action with the underlying comodule point action.
• HopfAlgebra.PointRepresentation.toComodule: recovery of a coaction from the universal point.
• HopfAlgebra.pointRepresentationEquivComodule: the fixed-object representation--comodule correspondence.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter VIII, §§2, 4, and 6.
• J. S. Milne, Algebraic Groups (2017), Chapter 4(a), Remark 4.1.

@[reducible, inline]

noncomputable abbrev TauCeti.HopfAlgebra.PointRepresentation {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] : Type (max (max (u + 1) (v + 1)) (w + 1))

A point representation of the affine group represented by H on an R-module V.

It is a natural family of group homomorphisms from the convolution group of A-points to the linear automorphisms of A ⊗[R] V, for every commutative R-algebra A.

Equations

• TauCeti.HopfAlgebra.PointRepresentation = (TauCeti.HopfAlgebra.pointsFunctor ⟶ TauCeti.GeneralLinear.scalarExtensionAutomorphismsFunctor)

noncomputable def TauCeti.HopfAlgebra.PointRepresentation.action {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) (A : CommAlgCat R) : points A ⟶ GeneralLinear.scalarExtensionAutomorphisms A

The group homomorphism at a value algebra, with the opaque functor object equalities removed.

Equations

• Theta.action A = CategoryTheory.CategoryStruct.comp (Theta.app A) (CategoryTheory.eqToHom ⋯)

theorem TauCeti.HopfAlgebra.PointRepresentation.action_def {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) (A : CommAlgCat R) : Theta.action A = CategoryTheory.CategoryStruct.comp (Theta.app A) (CategoryTheory.eqToHom ⋯)

The concrete point action is the natural-transformation component followed by the canonical scalar-extension functor-object transport.

theorem TauCeti.HopfAlgebra.PointRepresentation.ext {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {Theta Psi : PointRepresentation} (h : ∀ (A : CommAlgCat R) (x : ↑(points A)), (CategoryTheory.ConcreteCategory.hom (Theta.action A)) x = (CategoryTheory.ConcreteCategory.hom (Psi.action A)) x) : Theta = Psi

Point representations are equal when their concrete actions agree at every value algebra and point.

theorem TauCeti.HopfAlgebra.PointRepresentation.ext_iff {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] {Theta Psi : PointRepresentation} : Theta = Psi ↔ ∀ (A : CommAlgCat R) (x : ↑(points A)), (CategoryTheory.ConcreteCategory.hom (Theta.action A)) x = (CategoryTheory.ConcreteCategory.hom (Psi.action A)) x

theorem TauCeti.HopfAlgebra.PointRepresentation.action_naturality {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) {A B : CommAlgCat R} (phi : A ⟶ B) (x : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom (GeneralLinear.mapScalarExtensionAutomorphisms phi)) ((CategoryTheory.ConcreteCategory.hom (Theta.action A)) x) = (CategoryTheory.ConcreteCategory.hom (Theta.action B)) ((CategoryTheory.ConcreteCategory.hom (mapPoints phi)) x)

Naturality of a point representation, expressed using the concrete point and scalar-extension groups.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.action_mapPoints_one_tmul {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) {A B : CommAlgCat R} (phi : A ⟶ B) (x : ↑(points A)) (v : V) : ↑((CategoryTheory.ConcreteCategory.hom (Theta.action B)) ((CategoryTheory.ConcreteCategory.hom (mapPoints phi)) x)) (1 ⊗ₜ[R] v) = (GeneralLinear.scalarExtensionMap phi) (↑((CategoryTheory.ConcreteCategory.hom (Theta.action A)) x) (1 ⊗ₜ[R] v))

Naturality determines the action of a transported point on the canonical copy of V.

noncomputable def TauCeti.HopfAlgebra.PointRepresentation.ofComodule {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) : PointRepresentation

The natural point representation induced by a right H-comodule structure.

Equations

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

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_action_tmul {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) (A : CommAlgCat R) (x : ↑(points A)) (a : ↑A) (v : V) : ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action A)) x) (a ⊗ₜ[R] v) = a • (TensorProduct.comm R V ↑A) ((TensorProduct.map LinearMap.id x.ofConv.toLinearMap) (Comodule.coact v))

The action induced by a coaction, evaluated on a pure tensor.

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_action_val_eq_endOfPoint {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) (A : CommAlgCat R) (x : ↑(points A)) : ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action A)) x) = Comodule.endOfPoint V x.ofConv

The underlying linear map of the action induced by a coaction is the corresponding comodule point-action endomorphism.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_action_universal_one_tmul {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) (v : V) : ↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action ↧(ULift.{max u v w, v} H))) (WithConv.toConv ↑ULift.algEquiv.{u, v, max (max u v) w}.symm)) (1 ⊗ₜ[R] v) = (TensorProduct.comm R V (ULift.{max u v w, v} H)) ((TensorProduct.map LinearMap.id ULift.algEquiv.{u, v, max (max u v) w}.symm.toLinearMap) (Comodule.coact v))

At the universal point, the action induced by a coaction is the flipped coaction.

@[irreducible]

noncomputable def TauCeti.HopfAlgebra.PointRepresentation.toComodule {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) : Comodule R H V

Recover a right H-comodule structure from a natural point representation by evaluating at the universal point and flipping the tensor factors. The definition is intentionally opaque; use toComodule_coact_apply to expose its coaction.

Equations

• Theta.toComodule = { coact := TauCeti.HopfAlgebra.PointRepresentation.recoveredCoaction✝ Theta, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.toComodule_coact_apply {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) (v : V) : Comodule.coact v = (TensorProduct.comm R H V) ((TensorProduct.map ULift.algEquiv.{u, v, max (max u v) w}.toLinearMap LinearMap.id) (↑((CategoryTheory.ConcreteCategory.hom (Theta.action ↧(ULift.{max u v w, v} H))) (WithConv.toConv ↑ULift.algEquiv.{u, v, max (max u v) w}.symm)) (1 ⊗ₜ[R] v)))

The coaction recovered from a point representation is the flipped universal-point action.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.toComodule_ofComodule {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) : (ofComodule rho).toComodule = rho

Recovering a comodule from its induced point representation returns the original comodule.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_toComodule {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) : ofComodule Theta.toComodule = Theta

Reconstructing the point representation from its recovered comodule returns the original natural action.

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

Natural point representations on V are equivalent to right H-comodule structures on V.

Equations

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

@[simp]

theorem TauCeti.HopfAlgebra.pointRepresentationEquivComodule_apply {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (Theta : PointRepresentation) : pointRepresentationEquivComodule Theta = Theta.toComodule

The forward map of the representation--comodule equivalence recovers the coaction at the universal point.

@[simp]

theorem TauCeti.HopfAlgebra.pointRepresentationEquivComodule_symm_apply {R : Type u} {H : Type v} {V : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] (rho : Comodule R H V) : pointRepresentationEquivComodule.symm rho = PointRepresentation.ofComodule rho

The inverse map of the representation--comodule equivalence is the point action induced by a coaction.