Finite comodule actions separate points

An algebra-valued point of an algebra-coalgebra acts on every scalar-extended comodule. Equality of two such actions on one comodule forces the points to agree on that comodule's matrix coefficients. Consequently, a comodule whose matrix coefficients generate the algebra separates points.

Finite projective comodules over a commutative semiring admit the converse characterization. Over a commutative principal ideal domain, the finite restricted regular comodules of a free coalgebra collectively separate all algebra-valued points. Indeed, the fundamental theorem of coalgebras places any coefficient in a finite subcoalgebra. Its restricted regular comodule has that coefficient in its matrix-coefficient algebra, so equality of the two actions there detects equality at the chosen coefficient.

This is the injectivity input for the Tannakian reconstruction target in Layer 1 of the reductive-groups roadmap: once a point is packaged as a tensor automorphism of the scalar-extension fibre functor, its components on finite-dimensional comodules determine the point uniquely.

Main declarations

• TauCeti.Comodule.eqOn_matrixCoefficientSubalgebra_of_endOfPoint_eq: equal point actions imply equality on the algebra generated by the comodule's matrix coefficients.
• TauCeti.Comodule.eq_of_endOfPoint_eq_of_matrixCoefficientSubalgebra_eq_top: a coefficient-generating comodule separates points.
• TauCeti.Comodule.endOfPoint_eq_iff_eqOn_matrixCoefficientSubalgebra: equality of actions is characterized by the coefficient algebra for finite projective comodules.
• TauCeti.Comodule.eq_of_forall_finiteSubcoalgebra_endOfPoint_eq_of_exists_mem: under an elementwise finite-subcoalgebra covering hypothesis, the restricted regular comodules collectively separate algebra-valued points.
• TauCeti.Comodule.eq_of_forall_finiteSubcoalgebra_endOfPoint_eq: the restricted regular comodules of finite subcoalgebras of a free coalgebra collectively separate algebra-valued points over a commutative principal ideal domain.

References

• J. S. Milne, Algebraic Groups (2017), Sections 4.5 and 9.4.
• M. Sweedler, Hopf Algebras, Chapter 2.

theorem TauCeti.Comodule.eqOn_matrixCoefficientSubalgebra_of_endOfPoint_eq {R : Type u} {C : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [CommSemiring A] [Algebra R A] (g h : C →ₐ[R] A) (haction : endOfPoint M g = endOfPoint M h) : Set.EqOn ⇑g ⇑h ↑matrixCoefficientSubalgebra

If two points induce the same endomorphism on a comodule, then they agree on the algebra generated by that comodule's matrix coefficients.

theorem TauCeti.Comodule.eq_of_endOfPoint_eq_of_matrixCoefficientSubalgebra_eq_top {R : Type u} {C : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [CommSemiring A] [Algebra R A] (g h : C →ₐ[R] A) (haction : endOfPoint M g = endOfPoint M h) (hgenerate : matrixCoefficientSubalgebra = ⊤) : g = h

A comodule whose matrix coefficients generate the ambient algebra separates algebra-valued points: equal induced endomorphisms come only from equal points.

@[simp]

theorem TauCeti.Comodule.endOfPoint_eq_iff_eqOn_matrixCoefficientSubalgebra {R : Type u} {C : Type v} {A : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [CommSemiring A] [Algebra R A] {M : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [Module.Projective R M] [Module.Finite R M] (g h : C →ₐ[R] A) : endOfPoint M g = endOfPoint M h ↔ Set.EqOn ⇑g ⇑h ↑matrixCoefficientSubalgebra

For a finite projective comodule over a commutative semiring, two points induce the same endomorphism exactly when they agree on the algebra generated by the comodule's matrix coefficients.

theorem TauCeti.Comodule.eq_of_forall_finiteSubcoalgebra_endOfPoint_eq_of_exists_mem {R : Type u} {C : Type v} {A : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [Module.Flat R C] [CommSemiring A] [Algebra R A] (g h : C →ₐ[R] A) (haction : ∀ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule → endOfPoint (↥D.toRegularSubcomodule) g = endOfPoint (↥D.toRegularSubcomodule) h) (hcover : ∀ (c : C), ∃ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule ∧ c ∈ D) : g = h

If every element belongs to a module-finite subcoalgebra, then the actions on the restricted regular comodules of all module-finite subcoalgebras jointly determine an algebra-valued point.

theorem TauCeti.Comodule.eq_of_forall_finiteSubcoalgebra_endOfPoint_eq {R : Type u} {C : Type v} {A : Type w} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [Semiring C] [Algebra R C] [Coalgebra R C] [Module.Free R C] [CommSemiring A] [Algebra R A] (g h : C →ₐ[R] A) : have x := Algebra.semiringToRing R; (∀ (D : Subcoalgebra R C), Module.Finite R ↥D.toSubmodule → endOfPoint (↥D.toRegularSubcomodule) g = endOfPoint (↥D.toRegularSubcomodule) h) → g = h

Over a commutative principal ideal domain, the actions on the restricted regular comodules of all finite subcoalgebras of a free coalgebra jointly determine an algebra-valued point. In particular, the family of finite free comodules separates points.