Multiplication of regular subcomodules

For a bialgebra H, multiplication is a morphism from the tensor square of the regular right comodule to the regular right comodule. Consequently, if N and P are subcomodules of the regular comodule and a third subcomodule Q contains all products n * p, multiplication corestricts to a comodule morphism N ⊗ P ⟶ Q.

When H is free over the base semiring and N and P are finite submodules, the products of their elements lie in some finite regular subcomodule. This packages the multiplication map needed to compare tensor-compatible natural transformations on finite regular subcomodules.

Main declarations

• TauCeti.Subcomodule.mulHom: multiplication corestricted to a containing regular subcomodule.
• TauCeti.Subcomodule.exists_finite_mul_le_of_exists_mem: pairwise products lie in a finite regular subcomodule whenever every element does.
• TauCeti.Subcomodule.exists_finite_mul_le: two finite submodules have all their pairwise products in a third finite regular subcomodule.

References

The regular-comodule multiplication is the coalgebra-homomorphism part of the bialgebra axioms; see Sweedler, Hopf Algebras, Chapter 2. The finite containment argument uses the finite-subcomodule theorem from the same chapter.

This advances the Layer 1 Tannakian reconstruction milestone of the reductive-groups roadmap, ReductiveGroups/README.md in TauCetiRoadmap: tensor naturality applied to these multiplication morphisms supplies the multiplicativity law for the reconstructed point.

theorem TauCeti.Subcomodule.mulMap_mem {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] (N P Q : Subcomodule R H H) (h : ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q) (x : TensorProduct R ↥N ↥P) : (N.toSubmodule.mulMap P.toSubmodule) x ∈ Q

If a regular subcomodule contains every pairwise product from N and P, it contains every value of Submodule.mulMap N.toSubmodule P.toSubmodule.

noncomputable def TauCeti.Subcomodule.mulHom {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] (N P Q : Subcomodule R H H) [Module.Flat R H] (h : ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q) : Comodule.Hom R H (TensorProduct R ↥N ↥P) ↥Q

Multiplication from N ⊗ P, corestricted to a regular subcomodule Q containing every product n * p.

Equations

• N.mulHom P Q h = (TauCeti.Comodule.Hom.regularMul.comp (N.subtype.tensorMap P.subtype)).codRestrict Q ⋯

@[simp]

theorem TauCeti.Subcomodule.mulHom_tmul {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] (N P Q : Subcomodule R H H) [Module.Flat R H] (h : ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q) (n : ↥N) (p : ↥P) : ↑((N.mulHom P Q h) (n ⊗ₜ[R] p)) = ↑n * ↑p

Corestricted regular multiplication sends a pure tensor to the product of its factors.

@[simp]

theorem TauCeti.Subcomodule.mulHom_toLinearMap {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Bialgebra R H] (N P Q : Subcomodule R H H) [Module.Flat R H] (h : ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q) : (N.mulHom P Q h).toLinearMap = LinearMap.codRestrict Q.toSubmodule (N.toSubmodule.mulMap P.toSubmodule) ⋯

The underlying linear map of corestricted regular multiplication is Mathlib's Submodule.mulMap, with codomain restricted to Q.

theorem TauCeti.Subcomodule.exists_finite_mul_le_of_exists_mem {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] (hH : ∀ (h : H), ∃ (Q : Subcomodule R H H), Module.Finite R ↥Q.toSubmodule ∧ h ∈ Q) (N P : Submodule R H) [Module.Finite R ↥N] [Module.Finite R ↥P] : ∃ (Q : Subcomodule R H H), Module.Finite R ↥Q.toSubmodule ∧ ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q

If every element of H belongs to a finite regular subcomodule, then pairwise products from two finite submodules lie in a finite regular subcomodule.

theorem TauCeti.Subcomodule.exists_finite_mul_le {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [Module.Free R H] (N P : Submodule R H) [Module.Finite R ↥N] [Module.Finite R ↥P] : ∃ (Q : Subcomodule R H H), Module.Finite R ↥Q.toSubmodule ∧ ∀ (n : ↥N) (p : ↥P), ↑n * ↑p ∈ Q

If H is free over R, pairwise products from two finite submodules lie in a finite regular subcomodule.