Base change of comodules and their coefficient coalgebras

Let H be a coalgebra over a commutative semiring R, let A be a commutative R-algebra, and let M be a right H-comodule. Extending scalars in both the coefficient coalgebra and the underlying module gives a right comodule

A ⊗[R] M  over  A ⊗[R] H.

The coaction is scalar extension of the original coaction followed by the canonical distributivity equivalence

A ⊗[R] (M ⊗[R] H) ≃ (A ⊗[R] M) ⊗[A] (A ⊗[R] H).

This is coefficient-ring base change, rather than the existing scalar-extension functor that only changes the module on which an H-valued point acts. It is the representation transport needed to compare geometric unipotence before and after a field extension.

Main declarations

• TauCeti.Comodule.baseChangeCoact: the base-changed coaction.
• TauCeti.Comodule.baseChange: the induced comodule structure over the base-changed coefficient coalgebra, selected explicitly as a local instance.
• TauCeti.Comodule.baseChangeCoact_tmul: the coaction formula on pure tensors.
• TauCeti.Comodule.baseChange_self: base change of the regular comodule agrees with the regular comodule of the base-changed coalgebra.
• TauCeti.Comodule.Hom.baseChange: base change of a comodule morphism.

References

• M. Sweedler, Hopf Algebras, Chapter 2.

This supplies a prerequisite for base-change invariance of geometric unipotence and hence for comparison of unipotent radicals in Layer 5 of the ReductiveGroups roadmap.

noncomputable def TauCeti.Comodule.baseChangeCoact {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : TensorProduct R A M →ₗ[A] TensorProduct A (TensorProduct R A M) (TensorProduct R A H)

The scalar extension of a coaction, with the scalar extension distributed across its two tensor factors.

Equations

• TauCeti.Comodule.baseChangeCoact A = ↑(TensorProduct.AlgebraTensorModule.distribBaseChange R A M H) ∘ₗ LinearMap.baseChange A TauCeti.Comodule.coact

@[simp]

theorem TauCeti.Comodule.baseChangeCoact_tmul {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (a : A) (m : M) : (baseChangeCoact A) (a ⊗ₜ[R] m) = (TensorProduct.AlgebraTensorModule.distribBaseChange R A M H) (a ⊗ₜ[R] coact m)

On a pure tensor, the base-changed coaction applies the old coaction and distributes the new scalar across the two extended tensor factors.

@[instance_reducible]

noncomputable def TauCeti.Comodule.baseChange {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : Comodule A (TensorProduct R A H) (TensorProduct R A M)

Extending the coefficient coalgebra and the underlying module of a comodule along the same scalar morphism gives a comodule over the base-changed coalgebra.

This is deliberately not a global instance because a module can carry multiple coactions. Downstream code should select it explicitly, typically as a local instance.

Equations

• TauCeti.Comodule.baseChange A = { coact := TauCeti.Comodule.baseChangeCoact A, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.baseChange_coact {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : coact = baseChangeCoact A

The coaction of the base-changed comodule is scalar extension of the original coaction, followed by distribution across the two tensor factors.

theorem TauCeti.Comodule.baseChange_self {R : Type u} {H : Type v} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] : baseChange A = instSelf A (TensorProduct R A H)

Base change of the regular comodule is the regular comodule of the base-changed coalgebra.

noncomputable def TauCeti.Comodule.Hom.baseChange {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {N : Type y} [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) : Hom A (TensorProduct R A H) (TensorProduct R A M) (TensorProduct R A N)

Base change of a comodule morphism, extending its source and target modules together with its coefficient coalgebra along the same scalar morphism.

Equations

• TauCeti.Comodule.Hom.baseChange A f = { toLinearMap := LinearMap.baseChange A f.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Hom.baseChange_toLinearMap {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {N : Type y} [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) : (baseChange A f).toLinearMap = LinearMap.baseChange A f.toLinearMap

The underlying linear map of a base-changed comodule morphism is the base change of its underlying linear map.

theorem TauCeti.Comodule.Hom.baseChange_id {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] : baseChange A (id R H M) = id A (TensorProduct R A H) (TensorProduct R A M)

Base change preserves the identity comodule morphism.

@[simp]

theorem TauCeti.Comodule.Hom.baseChange_comp {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {N : Type y} [AddCommMonoid N] [Module R N] [Comodule R H N] {P : Type z} [AddCommMonoid P] [Module R P] [Comodule R H P] (g : Hom R H N P) (f : Hom R H M N) : baseChange A (g.comp f) = (baseChange A g).comp (baseChange A f)

Base change preserves composition of comodule morphisms.

@[simp]

theorem TauCeti.Comodule.Hom.baseChange_tmul {R : Type u} {H : Type v} {M : Type w} (A : Type x) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid H] [Module R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] {N : Type y} [AddCommMonoid N] [Module R N] [Comodule R H N] (f : Hom R H M N) (a : A) (m : M) : (baseChange A f) (a ⊗ₜ[R] m) = a ⊗ₜ[R] f m

A base-changed comodule morphism acts on a pure tensor by applying the original morphism to the module factor.