Linearly reductive affine group schemes

This file transports linear reductivity from commutative Hopf algebras to affine group schemes over a field. The coordinate-ring predicate tests finite-dimensional comodules whose carriers lie in Type u, the universe of the base field and coordinate ring; transport to a finite standard basis shows that this implies complete reducibility in every carrier universe. The affine Hopf/group-scheme anti-equivalence makes this an intrinsic, isomorphism-invariant property of the represented group scheme.

The resulting full subcategories remain anti-equivalent. The compatibility isomorphism with hopfSpec is provided so later comparison theorems can compute on coordinate rings without unfolding either restricted equivalence.

Main declarations

• TauCeti.linearlyReductiveAffineGroupSchemeProperty: linear reductivity of affine group schemes over a field.
• TauCeti.LinearlyReductiveAffineGroupSchemeCat: the corresponding full subcategory.
• TauCeti.linearlyReductiveAffineGroupSchemeProperty_hopfSpec_iff: the characterization on a canonical Hopf spectrum.
• TauCeti.linearlyReductiveCommHopfAlgCatOpEquivLinearlyReductiveAffineGroupSchemeCat: the restricted Hopf-algebra/group-scheme anti-equivalence.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.
• J. S. Milne, Algebraic Groups (2017), Theorem 12.12.

This synchronizes the coordinate-ring and group-scheme views for the complete-reducibility characterization in Layer 6 of the ReductiveGroups roadmap.

The organization follows TauCeti/AlgebraicGeometry/AffineGroupScheme/Unipotent.lean.

def TauCeti.linearlyReductiveAffineGroupSchemeProperty (k : Type u) [Field k] : CategoryTheory.ObjectProperty (AffineGroupSchemeCat ↧k)

The object property selecting affine group schemes whose finite-dimensional coordinate-ring comodules with carriers in Type u are completely reducible.

The property is transported through the affine Hopf/group-scheme anti-equivalence and therefore does not add smoothness, connectedness, or finite type to the ambient affine group.

Equations

• TauCeti.linearlyReductiveAffineGroupSchemeProperty k = (TauCeti.linearlyReductiveCommHopfAlgProperty k).op.inverseImage (TauCeti.commHopfAlgCatOpEquivAffineGroupSchemeCat ↧k).inverse

@[simp]

theorem TauCeti.linearlyReductiveAffineGroupSchemeProperty_iff (k : Type u) [Field k] (G : AffineGroupSchemeCat ↧k) : linearlyReductiveAffineGroupSchemeProperty k G ↔ Coalgebra.IsLinearlyReductive k ↑(Opposite.unop ((commHopfAlgCatOpEquivAffineGroupSchemeCat ↧k).inverse.obj G))

An affine group scheme is linearly reductive exactly when finite-dimensional comodules over the coordinate Hopf algebra recovered by the affine anti-equivalence, with carriers in Type u, are completely reducible.

instance TauCeti.instIsClosedUnderIsomorphismsAffineGroupSchemeCatOfLinearlyReductiveAffineGroupSchemeProperty (k : Type u) [Field k] : (linearlyReductiveAffineGroupSchemeProperty k).IsClosedUnderIsomorphisms

Linear reductivity of affine group schemes is invariant under isomorphism.

@[reducible, inline]

abbrev TauCeti.LinearlyReductiveAffineGroupSchemeCat (k : Type u) [Field k] : Type (u + 1)

The category of linearly reductive affine group schemes over a field.

Equations

• TauCeti.LinearlyReductiveAffineGroupSchemeCat k = (TauCeti.linearlyReductiveAffineGroupSchemeProperty k).FullSubcategory

theorem TauCeti.linearlyReductiveAffineGroupSchemeProperty_inverseImage (k : Type u) [Field k] : (linearlyReductiveAffineGroupSchemeProperty k).inverseImage (commHopfAlgCatOpEquivAffineGroupSchemeCat ↧k).functor = (linearlyReductiveCommHopfAlgProperty k).op

Under the affine Hopf/group-scheme anti-equivalence, the inverse image of linear reductivity on group schemes is linear reductivity of coordinate Hopf algebras.

theorem TauCeti.linearlyReductiveAffineGroupSchemeProperty_hopfSpec_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) : linearlyReductiveAffineGroupSchemeProperty k { obj := (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op H), property := ⋯ } ↔ Coalgebra.IsLinearlyReductive k ↑H

A canonical Hopf spectrum is linearly reductive exactly when its coordinate Hopf algebra is linearly reductive for finite-dimensional comodules with carriers in Type u.

noncomputable def TauCeti.linearlyReductiveCommHopfAlgCatOpEquivLinearlyReductiveAffineGroupSchemeCat (k : Type u) [Field k] : (LinearlyReductiveCommHopfAlgCat k)ᵒᵖ ≌ LinearlyReductiveAffineGroupSchemeCat k

Spec restricts to an anti-equivalence from linearly reductive commutative Hopf algebras to linearly reductive affine group schemes.

Equations

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

noncomputable def TauCeti.linearlyReductiveCommHopfAlgCatOpEquivLinearlyReductiveAffineGroupSchemeCat.functorCompιIso (k : Type u) [Field k] : (linearlyReductiveCommHopfAlgCatOpEquivLinearlyReductiveAffineGroupSchemeCat k).functor.comp ((linearlyReductiveAffineGroupSchemeProperty k).ι.comp (affineGroupSchemeProperty ↧k).ι) ≅ (CategoryTheory.forget₂ (LinearlyReductiveCommHopfAlgCat k) (CommHopfAlgCat k)).op.comp (AlgebraicGeometry.hopfSpec ↧k)

The restricted anti-equivalence followed by the inclusions into affine group schemes is hopfSpec after forgetting the proof of linear reductivity.

Equations

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