Geometric normal-subgroup-freeness properties

This file packages the common construction behind the reductive and semisimple predicates. Given an isomorphism-invariant property P of finite-type commutative Hopf algebras over an algebraic closure, geometricNormalSubgroupFreeCommHopfAlgProperty k P says that the ambient group is smooth and geometrically connected and that every connected normal closed subgroup satisfying P is trivial.

The construction is invariant under isomorphism and can be established using an isomorphic coordinate model of the geometric fibre. Its shared API also shows that, when the whole geometric fibre satisfies P, its zero Hopf ideal is the augmentation ideal and its coordinate algebra is bialgebra-equivalent to the algebraic closure via the counit.

Main declarations

• TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty: the generic normal-subgroup-freeness property.
• TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty_of_geometricFiber_iso: establish the property using an isomorphic coordinate model of the geometric fibre.
• TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.eq_augmentation: candidate normal subgroups are trivial.
• TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.geometricFiberCounitBialgEquiv: a geometric fibre satisfying the candidate property is trivial.

This is shared infrastructure for the reductive and semisimple definitions in Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap.

def TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty (k : Type u) [Field k] (P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))) : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat k)

The object property selecting smooth geometrically connected finite-type affine groups whose connected normal geometric subgroups satisfying P are all trivial.

The candidate property P is imposed on the coordinate Hopf algebra of the subgroup, represented contravariantly as a quotient by a normal Hopf ideal.

Equations

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

@[simp]

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty_iff (k : Type u) [Field k] (P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))) (H : FiniteTypeCommHopfAlgCat k) : geometricNormalSubgroupFreeCommHopfAlgProperty k P H ↔ Algebra.Smooth k ↑H.obj ∧ geometricallyConnectedCommHopfAlgProperty k H.obj ∧ ∀ (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj), I.IsNormal → geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj → P (H.baseChange.quotient I) → I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

Membership in the generic geometric normal-subgroup-freeness property.

instance TauCeti.instIsClosedUnderIsomorphismsFiniteTypeCommHopfAlgCatGeometricNormalSubgroupFreeCommHopfAlgPropertyOfAlgebraicClosure (k : Type u) [Field k] (P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))) [P.IsClosedUnderIsomorphisms] : (geometricNormalSubgroupFreeCommHopfAlgProperty k P).IsClosedUnderIsomorphisms

Geometric normal-subgroup-freeness is invariant under isomorphism when the candidate subgroup property is invariant under isomorphism.

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty_of_geometricFiber_iso (k : Type u) [Field k] (P : CategoryTheory.ObjectProperty (CommHopfAlgCat (AlgebraicClosure k))) [P.IsClosedUnderIsomorphisms] (H : FiniteTypeCommHopfAlgCat k) (G : CommHopfAlgCat (AlgebraicClosure k)) (hsmooth : Algebra.Smooth k ↑H.obj) (hconnected : geometricallyConnectedCommHopfAlgProperty k H.obj) (e : H.baseChange.obj ≅ G) (htrivial : ∀ (I : HopfIdeal (AlgebraicClosure k) ↑G), I.IsNormal → geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (CommHopfAlgCat.quotient G I) → P (CommHopfAlgCat.quotient G I) → I = HopfIdeal.augmentation (AlgebraicClosure k) ↑G) : geometricNormalSubgroupFreeCommHopfAlgProperty k (P.inverseImage (CategoryTheory.forget₂ (FiniteTypeCommHopfAlgCat (AlgebraicClosure k)) (CommHopfAlgCat (AlgebraicClosure k)))) H

Establish geometric normal-subgroup-freeness using an isomorphic coordinate model of the geometric fibre and an isomorphism-invariant candidate property on commutative Hopf algebras.

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.smooth {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) : Algebra.Smooth k ↑H.obj

A group satisfying a geometric normal-subgroup-freeness property is smooth.

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.geometricallyConnected {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) : geometricallyConnectedCommHopfAlgProperty k H.obj

A group satisfying a geometric normal-subgroup-freeness property is geometrically connected.

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.eq_augmentation {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) (I : HopfIdeal (AlgebraicClosure k) ↑H.baseChange.obj) (hI : I.IsNormal) (hconnected : geometricallyConnectedCommHopfAlgProperty (AlgebraicClosure k) (H.baseChange.quotient I).obj) (hP : P (H.baseChange.quotient I)) : I = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

Every connected normal closed subgroup of the geometric fibre satisfying P is trivial.

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.bot_eq_augmentation {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} [P.IsClosedUnderIsomorphisms] (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) (hP : P H.baseChange) : ⊥ = HopfIdeal.augmentation (AlgebraicClosure k) ↑H.baseChange.obj

If the whole geometric fibre satisfies P, its zero Hopf ideal is the augmentation ideal.

noncomputable def TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.geometricFiberCounitBialgEquiv {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} [P.IsClosedUnderIsomorphisms] (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) (hP : P H.baseChange) : ↑H.baseChange.obj ≃ₐc[AlgebraicClosure k] AlgebraicClosure k

If the whole geometric fibre satisfies P, its coordinate algebra is bialgebra-equivalent to the algebraic closure via the counit.

Equations

• hH.geometricFiberCounitBialgEquiv hP = TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot ⋯

@[simp]

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.geometricFiberCounitBialgEquiv_apply {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} [P.IsClosedUnderIsomorphisms] (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) (hP : P H.baseChange) (x : ↑H.baseChange.obj) : (hH.geometricFiberCounitBialgEquiv hP) x = (Bialgebra.counitBialgHom (AlgebraicClosure k) ↑H.baseChange.obj) x

The generic trivial-geometric-fibre equivalence is the counit.

@[simp]

theorem TauCeti.geometricNormalSubgroupFreeCommHopfAlgProperty.geometricFiberCounitBialgEquiv_symm_apply {k : Type u} [Field k] {P : CategoryTheory.ObjectProperty (FiniteTypeCommHopfAlgCat (AlgebraicClosure k))} {H : FiniteTypeCommHopfAlgCat k} [P.IsClosedUnderIsomorphisms] (hH : geometricNormalSubgroupFreeCommHopfAlgProperty k P H) (hP : P H.baseChange) (r : AlgebraicClosure k) : (hH.geometricFiberCounitBialgEquiv hP).symm r = (algebraMap (AlgebraicClosure k) ↑H.baseChange.obj) r

The inverse of the generic trivial-geometric-fibre equivalence is the structure map.