Detecting subcomodules on geometric points

Let C be a reduced commutative algebra of finite type over a field k, equipped with a coalgebra structure, and let M be a right C-comodule. A k-submodule N of M is a subcomodule if its scalar extension is preserved by every point of C valued in an algebraically closed extension of k.

The substantive direction is descent from pointwise stability. For m ∈ N, apply the quotient map M ⟶ M/N to coact m. Every coordinate of the resulting tensor vanishes at every geometric point, because the corresponding point action preserves the scalar extension of N. Reduced finite-type point separation makes every coordinate zero. Right exactness of tensor product then identifies coact m with a tensor in N ⊗ C.

Main declarations

• Submodule.coact_mem_range_of_forall_endOfPoint_tmul_mem_baseChange: pointwise stability implies the tensor-product stability condition defining a subcomodule.
• TauCeti.Subcomodule.ofEndOfPointStable: promote a point-stable submodule to a subcomodule.
• TauCeti.Subcomodule.endOfPoint_mapsTo_baseChange: every algebra-valued point preserves the scalar extension of a subcomodule.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.2.

This supplies the point-separation step in Layer 6 of the ReductiveGroups roadmap: for a normal closed subgroup, pointwise normality makes its fixed subspace stable under the ambient group, and the result here promotes that stable subspace to an ambient-group subcomodule.

theorem Submodule.coact_mem_range_of_forall_endOfPoint_tmul_mem_baseChange {k : Type u} {C : Type v} {M : Type w} {K : Type x} [Field k] [CommRing C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] [IsReduced C] [AddCommGroup M] [Module k M] [TauCeti.Comodule k C M] [Field K] [Algebra k K] [IsAlgClosed K] (N : Submodule k M) (hN : ∀ (g : C →ₐ[k] K) {m : M}, m ∈ N → (TauCeti.Comodule.endOfPoint M g) (1 ⊗ₜ[k] m) ∈ baseChange K N) {m : M} (hm : m ∈ N) : TauCeti.Comodule.coact m ∈ (TensorProduct.map N.subtype LinearMap.id).range

If every geometric point preserves the scalar extension of a submodule, the coaction of each element of that submodule belongs to its tensor product with the coefficient coalgebra.

It is enough to test the pure tensors 1 ⊗ m: the point action is linear over the value field, so this is equivalent to preservation of the whole scalar-extended submodule.

theorem TauCeti.Subcomodule.endOfPoint_tmul_mem_baseChange {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] (N : Subcomodule R C M) (g : C →ₐ[R] A) (a : A) {m : M} (hm : m ∈ N) : (Comodule.endOfPoint M g) (a ⊗ₜ[R] m) ∈ Submodule.baseChange A N.toSubmodule

Every algebra-valued point preserves the scalar extension of a subcomodule.

theorem TauCeti.Subcomodule.endOfPoint_mapsTo_baseChange {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] (N : Subcomodule R C M) (g : C →ₐ[R] A) : Set.MapsTo ⇑(Comodule.endOfPoint M g) ↑(Submodule.baseChange A N.toSubmodule) ↑(Submodule.baseChange A N.toSubmodule)

Every algebra-valued point maps the scalar extension of a subcomodule into itself.

def TauCeti.Subcomodule.ofEndOfPointStable {k : Type u} {C : Type v} {M : Type w} {K : Type x} [Field k] [CommRing C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] [IsReduced C] [AddCommGroup M] [Module k M] [Comodule k C M] [Field K] [Algebra k K] [IsAlgClosed K] (N : Submodule k M) (hN : ∀ (g : C →ₐ[k] K) {m : M}, m ∈ N → (Comodule.endOfPoint M g) (1 ⊗ₜ[k] m) ∈ Submodule.baseChange K N) : Subcomodule k C M

Promote a submodule whose scalar extension is preserved by every geometric point to a subcomodule.

Equations

• TauCeti.Subcomodule.ofEndOfPointStable N hN = TauCeti.Subcomodule.ofSubmodule N ⋯

@[simp]

theorem TauCeti.Subcomodule.ofEndOfPointStable_toSubmodule {k : Type u} {C : Type v} {M : Type w} {K : Type x} [Field k] [CommRing C] [Algebra k C] [Coalgebra k C] [Algebra.FiniteType k C] [IsReduced C] [AddCommGroup M] [Module k M] [Comodule k C M] [Field K] [Algebra k K] [IsAlgClosed K] (N : Submodule k M) (hN : ∀ (g : C →ₐ[k] K) {m : M}, m ∈ N → (Comodule.endOfPoint M g) (1 ⊗ₜ[k] m) ∈ Submodule.baseChange K N) : (ofEndOfPointStable N hN).toSubmodule = N

The point-stable subcomodule has the prescribed underlying submodule.