The points action of a comodule, by automorphisms

Over a Hopf algebra the points form a group under convolution — the points of the corresponding affine group scheme, when H is commutative — so the points action of a comodule (TauCeti.Comodule.endOfPoint, TauCeti.Comodule.pointsRepresentation) lands in the units of the endomorphism monoid: the action upgrades to linear automorphisms of the scalar extension via Representation.asGroupHom, with inverses provided by the group structure rather than by an antipode computation. For points valued in the base ring, the scalar-extension action transports across R ⊗[R] V ≃ₗ[R] V to a representation on V itself.

Main declarations

• TauCeti.Comodule.pointsAction: the action of the group of points by linear automorphisms of A ⊗[R] V.
• TauCeti.Comodule.pointsAction_corestrict: compatibility of point actions with corestriction and precomposition, also provided for bundled finite comodules by TauCeti.Comodule.pointsAction_corestrict_obj.
• TauCeti.Comodule.basePointsRepresentation: the action of base-valued points on the original comodule.
• TauCeti.Comodule.basePointsRepresentation_apply_of_mem_weightSpace: base-valued points act on a weight vector through the value of the point on its weight.
• TauCeti.Comodule.coact_eq_tmul_one_iff_forall_pointsAction_tmul_eq: geometric fixed-vector detection in terms of the convolution-group action.
• TauCeti.Comodule.coact_eq_tmul_one_iff_forall_basePointsRepresentation_eq: base-valued points detect fixed vectors over an algebraically closed base field.
• Submodule.exists_mem_groupLikeWeightSpace_of_basePointsRepresentation_stable and TauCeti.Comodule.hasNonzeroWeightVector_of_basePointsRepresentation_stable: a nonzero vector spanning a point-stable line is a weight vector.
• TauCeti.Comodule.iSup_groupLikeWeightSpace_eq_top_of_isSemisimple: a finite-dimensional comodule on which the base-valued points act by commuting semisimple operators is spanned by its weight spaces.

noncomputable def TauCeti.Comodule.pointsAction {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] : WithConv (H →ₐ[R] A) →* TensorProduct R A V ≃ₗ[A] TensorProduct R A V

Over a Hopf algebra the points act by linear automorphisms of the scalar extension: the group of points lands in the units of the endomorphism monoid, with inverses provided by the group structure rather than by an antipode computation.

@[simp]

theorem TauCeti.Comodule.pointsAction_toLinearMap {R : Type u_1} {H : Type u_2} (V : Type u_3) {A : Type u_4} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid V] [Module R V] [Comodule R H V] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) : ↑((pointsAction V) g) = endOfPoint V g.ofConv

noncomputable def TauCeti.Comodule.basePointsRepresentation {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (M : Type w) [AddCommMonoid M] [Module R M] [Comodule R H M] : WithConv (H →ₐ[R] R) →* Module.End R M

The representation of the group of base-valued points on the original comodule.

pointsRepresentation acts on R ⊗[R] M; this is its transport across the canonical equivalence R ⊗[R] M ≃ₗ[R] M.

theorem TauCeti.Comodule.basePointsRepresentation_apply {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (m : M) : ((basePointsRepresentation M) g) m = (TensorProduct.lid R M) ((endOfPoint M g.ofConv) (1 ⊗ₜ[R] m))

A base-valued point acts on m by contracting the coefficient leg of its coaction.

theorem TauCeti.Comodule.basePointsRepresentation_mem {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (N : Subcomodule R H M) (g : WithConv (H →ₐ[R] R)) {m : M} (hm : m ∈ N) : ((basePointsRepresentation M) g) m ∈ N

Every subcomodule is stable under the action of base-valued points.

@[simp]

theorem TauCeti.Comodule.isUnimodular_basePointsRepresentation_iff {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (m : M) : Module.IsUnimodular R (((basePointsRepresentation M) g) m) ↔ Module.IsUnimodular R m

Acting by a base-valued point preserves unimodularity of vectors.

theorem TauCeti.Comodule.basePointsRepresentation_apply_of_mem_weightSpace {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) {c : GroupLike R H} {m : M} (hm : m ∈ c.weightSpace) : ((basePointsRepresentation M) g) m = g.ofConv ↑c • m

A base-valued point acts on a vector of group-like weight c by the scalar g c.

@[simp]

theorem TauCeti.Comodule.endOfPoint_one_tmul_eq_one_tmul_basePointsRepresentation {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (m : M) : (TensorProduct.comm R M R) ((LinearMap.lTensor M g.ofConv.toLinearMap) (coact m)) = 1 ⊗ₜ[R] ((basePointsRepresentation M) g) m

The scalar-extension action of a base-valued point is the pure tensor of its action on the original comodule.

theorem TauCeti.Comodule.endOfPoint_mapValue_algebraOfId_tmul {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] {A : Type u_5} [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] R)) (a : A) (m : M) : (endOfPoint M ((Algebra.ofId R A).mapValue g).ofConv) (a ⊗ₜ[R] m) = a ⊗ₜ[R] ((basePointsRepresentation M) g) m

A constant algebra-valued point acts on a pure tensor by the original base-valued action.

@[simp]

theorem TauCeti.Comodule.apply_matrixCoefficient {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H M] (g : WithConv (H →ₐ[R] R)) (φ : Module.Dual R M) (m : M) : g.ofConv (matrixCoefficient φ m) = φ (((basePointsRepresentation M) g) m)

Evaluating a matrix coefficient at a base-valued point pairs the functional with the point's action on the vector.

@[simp]

theorem TauCeti.Comodule.basePointsRepresentation_corestrict {R : Type u} [CommSemiring R] {H₁ : Type v} {H₂ : Type x} [Semiring H₁] [Semiring H₂] [HopfAlgebra R H₁] [HopfAlgebra R H₂] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R H₁ M] (φ : H₁ →ₐc[R] H₂) (g : WithConv (H₂ →ₐ[R] R)) : (basePointsRepresentation M) g = (basePointsRepresentation M) (φ.mapDomain g)

Acting by a base-valued point on a corestricted comodule agrees with acting by the point precomposed with the bialgebra morphism.

theorem TauCeti.Comodule.basePointsRepresentation_eq_of_coact_eq_tmul_one {R : Type u} {H : Type v} {M : Type w} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] (m : M) (hm : coact m = m ⊗ₜ[R] 1) (g : WithConv (H →ₐ[R] R)) : ((basePointsRepresentation M) g) m = m

A vector fixed by the coaction is fixed by every base-valued point.

theorem TauCeti.Comodule.coact_eq_tmul_one_iff_forall_pointsAction_tmul_eq {k : Type u} {H : Type v} {M : Type w} {K : Type x} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [Field K] [Algebra k K] [IsAlgClosed K] (m : M) : coact m = m ⊗ₜ[k] 1 ↔ ∀ (g : WithConv (H →ₐ[k] K)), ((pointsAction M) g) (1 ⊗ₜ[k] m) = 1 ⊗ₜ[k] m

For a Hopf-algebra comodule, a vector is fixed by the coaction exactly when every point in the convolution group fixes its scalar extension.

theorem TauCeti.Comodule.coact_eq_tmul_one_iff_forall_basePointsRepresentation_eq {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] [IsReduced H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] (m : M) : coact m = m ⊗ₜ[k] 1 ↔ ∀ (g : ↑(HopfAlgebra.points ↧k)), ((basePointsRepresentation M) g) m = m

Over an algebraically closed base field, base-valued points detect fixed vectors of a reduced finite-type Hopf-algebra comodule.

theorem Submodule.exists_mem_groupLikeWeightSpace_of_basePointsRepresentation_stable {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [TauCeti.Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (p : Submodule k M) (v : M) (hv : v ≠ 0) (hspan : p = k ∙ v) (hact : ∀ (g : WithConv (H →ₐ[k] k)) {m : M}, m ∈ p → ((TauCeti.Comodule.basePointsRepresentation M) g) m ∈ p) : ∃ (c : GroupLike k H), v ∈ c.weightSpace

A nonzero vector spanning a submodule preserved by every base-valued point lies in a group-like weight space.

theorem TauCeti.Comodule.hasNonzeroWeightVector_of_basePointsRepresentation_stable {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (p : Submodule k M) (v : M) (hv : v ≠ 0) (hspan : p = k ∙ v) (hact : ∀ (g : WithConv (H →ₐ[k] k)) {m : M}, m ∈ p → ((basePointsRepresentation M) g) m ∈ p) : HasNonzeroWeightVector k H M

A nonzero vector spanning a submodule preserved by every base-valued point is a weight vector.

theorem TauCeti.Comodule.iSup_groupLikeWeightSpace_eq_top_of_isSemisimple {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] (hcomm : Pairwise fun (g h : WithConv (H →ₐ[k] k)) => Commute ((basePointsRepresentation M) g) ((basePointsRepresentation M) h)) (hss : ∀ (g : WithConv (H →ₐ[k] k)), ((basePointsRepresentation M) g).IsSemisimple) : ⨆ (c : GroupLike k H), c.weightSpace = ⊤

If the base-valued points of a reduced finite-type Hopf algebra over an algebraically closed field act on a finite-dimensional comodule by pairwise-commuting semisimple operators, then the comodule is spanned by its group-like weight spaces.

theorem TauCeti.Comodule.pointsAction_corestrict {R : Type u} {H₁ : Type v} {H₂ : Type w} {A : Type x} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [Algebra R A] [HopfAlgebra R H₁] [HopfAlgebra R H₂] {V : Type u_5} [AddCommMonoid V] [Module R V] [Comodule R H₁ V] (φ : H₁ →ₐc[R] H₂) (g : WithConv (H₂ →ₐ[R] A)) : (pointsAction V) g = (pointsAction V) (φ.mapDomain g)

The linear action of a precomposed point agrees with the action of the original point on the corestricted comodule.

@[simp]

theorem TauCeti.Comodule.pointsAction_corestrict_toConv_comp {R : Type u} {H₁ : Type v} {H₂ : Type w} {A : Type x} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [Algebra R A] [HopfAlgebra R H₁] [HopfAlgebra R H₂] {V : Type u_5} [AddCommMonoid V] [Module R V] [Comodule R H₁ V] (φ : H₁ →ₐc[R] H₂) (g : WithConv (H₂ →ₐ[R] A)) : (pointsAction V) g = (pointsAction V) (WithConv.toConv (g.ofConv.comp ↑φ))

Simp-normal form of pointsAction_corestrict, with the precomposed point written after normalization by BialgHom.mapDomain_apply.

theorem TauCeti.Comodule.pointsAction_corestrict_obj {R : Type u} {H₁ : Type v} {H₂ : Type w} {A : Type x} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [Algebra R A] [HopfAlgebra R H₁] [HopfAlgebra R H₂] (φ : H₁ →ₐc[R] H₂) (M : FGComoduleCat R H₁) (g : WithConv (H₂ →ₐ[R] A)) : (pointsAction ↑((FGComoduleCat.corestrict φ.toCoalgHom).obj M)) g = (pointsAction ↑M) (φ.mapDomain g)

Bundled finite-comodule form of pointsAction_corestrict. This avoids exposing the definitionally equal comodule instance carried by the corestricted object to callers.

@[simp]

theorem TauCeti.Comodule.pointsAction_corestrict_obj_toConv_comp {R : Type u} {H₁ : Type v} {H₂ : Type w} {A : Type x} [CommSemiring R] [Semiring H₁] [Semiring H₂] [CommSemiring A] [Algebra R A] [HopfAlgebra R H₁] [HopfAlgebra R H₂] (φ : H₁ →ₐc[R] H₂) (M : FGComoduleCat R H₁) (g : WithConv (H₂ →ₐ[R] A)) : (pointsAction ↑((FGComoduleCat.corestrict φ.toCoalgHom).obj M)) g = (pointsAction ↑M) (WithConv.toConv (g.ofConv.comp ↑φ))

Simp-normal form of pointsAction_corestrict_obj, with the precomposed point written after normalization by BialgHom.mapDomain_apply.