Invariants of normal closed subgroups

Let H be a commutative Hopf algebra and M an H-comodule. A point of the affine group represented by H acts naturally on M itself when its value algebra is the base ring. For a Hopf ideal I, this file defines the submodule fixed by the base-valued points of the closed subgroup cut out by I.

When I is normal, its point subgroup is normal over every value algebra. The standard theorem that the invariants of a normal subgroup form a subrepresentation therefore shows that this fixed submodule is preserved by every ambient point. This is the pointwise algebraic-group input to the direct proof that GLₙ is reductive: the fixed vectors of a normal unipotent subgroup in the standard representation form an ambient subrepresentation.

The definition deliberately says basePointFixedSubmodule: without a point-separation hypothesis, base-valued points need not detect scheme-theoretic invariants. The normality and stability results require no reducedness, finite-type, or field hypotheses.

For a reduced ambient group of finite type over an algebraically closed field, HopfIdeal.IsNormal.weightSpaceOneSubcomodule instead constructs the scheme-theoretic invariant representation. It is the subgroup's trivial-character weight space, which normality makes ambient-stable. The subgroup itself need not be reduced. Its points over every commutative value algebra act trivially on these invariant vectors.

The group-representation step is Mathlib's Representation.toInvariants; this file adds the Hopf-ideal and comodule interface around it rather than repeating the normal-subgroup conjugation argument.

Main declarations

• TauCeti.HopfIdeal.basePointFixedSubmodule: the vectors fixed by the base-valued points cut out by a Hopf ideal.
• TauCeti.HopfIdeal.mem_basePointFixedSubmodule_iff_quotient_coact_eq_tmul_one: geometric-point detection identifies the pointwise and scheme-theoretic fixed-vector conditions.
• TauCeti.HopfIdeal.IsNormal.basePointFixedSubrepresentation: Mathlib's representation on the invariants of the point subgroup cut out by a normal Hopf ideal.
• TauCeti.HopfIdeal.IsNormal.basePointsRepresentation_mem_basePointFixedSubmodule: the ambient base-point action preserves the base-point-fixed submodule.
• TauCeti.HopfIdeal.IsNormal.endOfPoint_one_tmul_mem_basePointFixedSubmodule_baseChange: pointwise stability in the scalar-extension form used to detect subcomodules.
• TauCeti.HopfIdeal.IsNormal.weightSpaceOneSubcomodule: the scheme-theoretic invariant representation, admitting nonreduced normal subgroups.

References

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

noncomputable def TauCeti.HopfIdeal.basePointFixedSubmodule {R : Type u} {H : Type v} (M : Type w) [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (I : HopfIdeal R H) : Submodule R M

The submodule fixed by all base-valued points of the closed subgroup cut out by I.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.HopfIdeal.basePointFixedSubmodule_def {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (I : HopfIdeal R H) : basePointFixedSubmodule M I = Representation.invariants ((Comodule.basePointsRepresentation M).comp (CommHopfAlgCat.quotientPointsSubgroup (↧H) I ↧R).subtype)

The base-point-fixed submodule as Mathlib's invariant submodule for the quotient point subgroup.

@[simp]

theorem TauCeti.HopfIdeal.mem_basePointFixedSubmodule {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (I : HopfIdeal R H) (m : M) : m ∈ basePointFixedSubmodule M I ↔ ∀ (n : ↥(CommHopfAlgCat.quotientPointsSubgroup (↧H) I ↧R)), ((Comodule.basePointsRepresentation M) ↑n) m = m

Membership in the base-point-fixed submodule means being fixed by every base-valued point cut out by the Hopf ideal.

theorem TauCeti.HopfIdeal.mem_basePointFixedSubmodule_of_quotient_coact_eq_tmul_one {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (I : HopfIdeal R H) (m : M) (hm : (TensorProduct.map LinearMap.id (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (↧H) I)).toLinearMap) (Comodule.coact m) = m ⊗ₜ[R] 1) : m ∈ basePointFixedSubmodule M I

A vector fixed by the quotient coaction is fixed by every base-valued point of the closed subgroup cut out by I. This direction requires no point-separation hypotheses.

theorem TauCeti.HopfIdeal.mem_basePointFixedSubmodule_iff_quotient_coact_eq_tmul_one {k : Type u} {A : Type v} {M : Type w} [Field k] [CommRing A] [HopfAlgebra k A] [AddCommGroup M] [Module k M] [Comodule k A M] [IsAlgClosed k] (I : HopfIdeal k A) [Algebra.FiniteType k ↑(CommHopfAlgCat.quotient (↧A) I)] [IsReduced ↑(CommHopfAlgCat.quotient (↧A) I)] (m : M) : m ∈ basePointFixedSubmodule M I ↔ (TensorProduct.map LinearMap.id (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (↧A) I)).toLinearMap) (Comodule.coact m) = m ⊗ₜ[k] 1

Over an algebraically closed field, if the quotient coordinate ring is reduced and of finite type, base-point-fixed vectors are exactly the vectors fixed by the restricted coaction of the closed subgroup scheme.

noncomputable def TauCeti.HopfIdeal.IsNormal.weightSpaceOneSubcomodule {k : Type u} {A : Type v} (V : Type w) [Field k] [IsAlgClosed k] [CommRing A] [HopfAlgebra k A] [Algebra.FiniteType k A] [IsReduced A] [AddCommGroup V] [Module k V] [Comodule k A V] {I : HopfIdeal k A} (hI : I.IsNormal) : Subcomodule k A V

Scheme-theoretic invariants of a normal closed subgroup form an ambient subrepresentation. Only the ambient group is required to be reduced; the subgroup can be nonreduced.

Equations

• TauCeti.HopfIdeal.IsNormal.weightSpaceOneSubcomodule V hI = TauCeti.Subcomodule.ofEndOfPointStable (I.weightSpace V 1) ⋯

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.weightSpaceOneSubcomodule_toSubmodule {k : Type u} {A : Type v} {V : Type w} [Field k] [IsAlgClosed k] [CommRing A] [HopfAlgebra k A] [Algebra.FiniteType k A] [IsReduced A] [AddCommGroup V] [Module k V] [Comodule k A V] {I : HopfIdeal k A} (hI : I.IsNormal) : (weightSpaceOneSubcomodule V hI).toSubmodule = I.weightSpace V 1

Normal-subgroup invariants are the weight space of the trivial character.

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.mem_weightSpaceOneSubcomodule {k : Type u} {A : Type v} {V : Type w} [Field k] [IsAlgClosed k] [CommRing A] [HopfAlgebra k A] [Algebra.FiniteType k A] [IsReduced A] [AddCommGroup V] [Module k V] [Comodule k A V] {I : HopfIdeal k A} (hI : I.IsNormal) {v : V} : v ∈ weightSpaceOneSubcomodule V hI ↔ (TensorProduct.map LinearMap.id (Ideal.Quotient.mkₐ k I.toIdeal).toLinearMap) (Comodule.coact v) = v ⊗ₜ[k] 1

An ambient vector belongs to the normal-subgroup invariant representation precisely when its coaction restricts to the trivial coaction on the subgroup.

theorem TauCeti.HopfIdeal.IsNormal.endOfPoint_comp_mkₐ_tmul_of_mem_weightSpaceOneSubcomodule {k : Type u} {A : Type v} {V : Type w} [Field k] [IsAlgClosed k] [CommRing A] [HopfAlgebra k A] [Algebra.FiniteType k A] [IsReduced A] [AddCommGroup V] [Module k V] [Comodule k A V] {I : HopfIdeal k A} (hI : I.IsNormal) {B : Type u_1} [CommSemiring B] [Algebra k B] (g : A ⧸ I.toIdeal →ₐ[k] B) (b : B) {v : V} (hv : v ∈ weightSpaceOneSubcomodule V hI) : (Comodule.endOfPoint V (g.comp (Ideal.Quotient.mkₐ k I.toIdeal))) (b ⊗ₜ[k] v) = b ⊗ₜ[k] v

Every algebra-valued subgroup point fixes the scalar extension of an invariant vector.

theorem TauCeti.HopfIdeal.IsNormal.basePointsRepresentation_mem_basePointFixedSubmodule {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {I : HopfIdeal R H} (hI : I.IsNormal) (g : ↑(HopfAlgebra.points ↧R)) {m : M} (hm : m ∈ basePointFixedSubmodule M I) : ((Comodule.basePointsRepresentation M) g) m ∈ basePointFixedSubmodule M I

Every ambient base-valued point sends a base-point-fixed vector to another base-point-fixed vector.

@[reducible, inline]

noncomputable abbrev TauCeti.HopfIdeal.IsNormal.basePointFixedSubrepresentation {R : Type u} {H : Type v} (M : Type w) [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {I : HopfIdeal R H} (hI : I.IsNormal) : Representation R ↑(HopfAlgebra.points ↧R) ↥(basePointFixedSubmodule M I)

The representation of the full group of base-valued points on the vectors fixed by the point subgroup cut out by the normal Hopf ideal I. Normality makes this submodule ambient-stable.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.HopfIdeal.IsNormal.endOfPoint_le_comap_basePointFixedSubmodule_baseChange {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {I : HopfIdeal R H} (hI : I.IsNormal) (g : ↑(HopfAlgebra.points ↧R)) : Submodule.baseChange R (basePointFixedSubmodule M I) ≤ Submodule.comap (Comodule.endOfPoint M g.ofConv) (Submodule.baseChange R (basePointFixedSubmodule M I))

The scalar extension of the base-point-fixed submodule is stable under every ambient point endomorphism.

theorem TauCeti.HopfIdeal.IsNormal.endOfPoint_one_tmul_mem_basePointFixedSubmodule_baseChange {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] {I : HopfIdeal R H} (hI : I.IsNormal) (g : ↑(HopfAlgebra.points ↧R)) {m : M} (hm : m ∈ basePointFixedSubmodule M I) : (Comodule.endOfPoint M g.ofConv) (1 ⊗ₜ[R] m) ∈ Submodule.baseChange R (basePointFixedSubmodule M I)

Scalar-extension form of the stability of normal-subgroup fixed vectors. This is the shape needed by geometric point-separation criteria for promoting a submodule to a subcomodule.