Documentation

TauCeti.Algebra.AlgebraicGroup.Tangent.Zero

Connected affine groups with zero tangent space #

Let H be the coordinate Hopf algebra of an affine group over a field. If its tangent Lie algebra at the identity is zero, then the augmentation ideal m satisfies m / m ^ 2 = 0. When m is finitely generated, this equality upgrades to m ^ 2 = m, so m is generated by an idempotent. Connectedness of Spec H forces that idempotent to be zero or one. It cannot be one because the counit has nonzero codomain, and hence m = 0.

Thus a connected affine group of finite type with zero Lie algebra is trivial: its counit is an equivalence by HopfIdeal.counitBialgEquivOfAugmentationEqBot. The result is formulated first with the exact connectedness and finite-generation assumptions used in the proof, then specialized to geometrically connected finite-type commutative Hopf algebras.

This is the zero-dimensional quotient input for the equal-dimension containment argument in Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

Main declarations #

References #

source
theorem TauCeti.HopfIdeal.augmentation_eq_bot_iff_finrank_lie_eq_zero {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [ConnectedSpace (PrimeSpectrum H)] (hfg : (Bialgebra.AugmentationIdeal k H).FG) :
augmentation k H = ⊥ ↔ Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)) = 0

A connected affine group with finitely generated augmentation ideal has zero augmentation ideal exactly when its tangent Lie algebra has dimension zero.

source
theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.augmentation_eq_bot_of_finrank_lie_eq_zero {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hconnected : geometricallyConnectedCommHopfAlgProperty k ↧H) (hlie : Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)) = 0) :
HopfIdeal.augmentation k H = ⊥

A geometrically connected affine group of finite type whose tangent Lie algebra has dimension zero has zero augmentation ideal, and is therefore trivial via the counit.

This is the coordinate-ring form of the fact that a connected zero-dimensional algebraic group is trivial.

source
noncomputable def TauCeti.geometricallyConnectedCommHopfAlgProperty.counitBialgEquivOfFinrankLieEqZero {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hconnected : geometricallyConnectedCommHopfAlgProperty k ↧H) (hlie : Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)) = 0) :
H ≃ₐc[k] k

A geometrically connected affine group of finite type with zero-dimensional tangent Lie algebra is bialgebra-equivalent to the base field via the counit.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.counitBialgEquivOfFinrankLieEqZero_apply {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hconnected : geometricallyConnectedCommHopfAlgProperty k ↧H) (hlie : Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)) = 0) (x : H) :
    (hconnected.counitBialgEquivOfFinrankLieEqZero hlie) x = (Bialgebra.counitBialgHom k H) x

    The zero-tangent equivalence from the coordinate algebra to the base field is the counit.

    source
    @[simp]
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.counitBialgEquivOfFinrankLieEqZero_symm_apply {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] (hconnected : geometricallyConnectedCommHopfAlgProperty k ↧H) (hlie : Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k)) = 0) (r : k) :
    (hconnected.counitBialgEquivOfFinrankLieEqZero hlie).symm r = (algebraMap k H) r

    The inverse zero-tangent equivalence from the base field is the structure map.