Documentation

TauCeti.Algebra.AlgebraicGroup.ConstantGroup.Points

Rational points of finite constant groups #

Let G be a finite group and k a field. The k-valued points of the constant group attached to G are canonically G itself. Indeed, every k-algebra homomorphism from the function algebra k^G to k is evaluation at a unique element of G.

This identification turns a coordinate bialgebra morphism k^G \to H into a group homomorphism from the k-valued points of Spec H to G. If Spec H is connected, that homomorphism is trivial by ConstantGroup.point_comp_eq_one_of_connected.

The point-level formulation is the interface needed by the Lie--Kolchin argument. Its finite permutation action is naturally stated as a homomorphism to a finite symmetric group, whereas connectedness applies to the corresponding morphism of affine group schemes.

Main declarations #

References #

This advances the "Lie--Kolchin; solvable groups" milestone in Layer 5 of the ReductiveGroups roadmap.

source
noncomputable def TauCeti.ConstantGroup.pointsMulEquiv (k : Type u) [Field k] (G : Type v) [Group G] [Finite G] :
G ≃* WithConv (coordinateRing k G →ₐ[k] k)

The base-valued points of the constant group attached to a finite group G are canonically G itself.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ConstantGroup.pointsMulEquiv_apply {k : Type u} [Field k] (G : Type v) [Group G] [Finite G] (g : G) :
    (pointsMulEquiv k G) g = WithConv.toConv (eval k G g)

    The canonical equivalence from a finite group to its constant-group points is evaluation.

    source
    noncomputable def TauCeti.ConstantGroup.pointHom {k : Type u} [Field k] {H : Type w} [CommRing H] [Bialgebra k H] {G : Type v} [Group G] [Finite G] (f : coordinateRing k G →ₐc[k] H) :
    WithConv (H →ₐ[k] k) →* G

    A coordinate bialgebra morphism from the function algebra of a finite group to H induces a homomorphism from the base-valued points of Spec H to that finite group.

    Equations
    Instances For
      source
      theorem TauCeti.ConstantGroup.pointsMulEquiv_pointHom {k : Type u} [Field k] {H : Type w} [CommRing H] [Bialgebra k H] {G : Type v} [Group G] [Finite G] (f : coordinateRing k G →ₐc[k] H) (p : WithConv (H →ₐ[k] k)) :
      (pointsMulEquiv k G) ((pointHom f) p) = (AlgHom.mapDomain f) p

      The point homomorphism induced by f is characterized by evaluation after precomposition with f.

      source
      @[simp]
      theorem TauCeti.ConstantGroup.eval_pointHom {k : Type u} [Field k] {H : Type w} [CommRing H] [Bialgebra k H] {G : Type v} [Group G] [Finite G] (f : coordinateRing k G →ₐc[k] H) (p : WithConv (H →ₐ[k] k)) :
      eval k G ((pointHom f) p) = p.ofConv.comp ↑f

      Pointwise, the coordinate map induced by pointHom f p is precomposition with f.

      source
      @[simp]
      theorem TauCeti.ConstantGroup.pointHom_coordinateBialgHom {k : Type u} [Field k] {G : Type v} [Group G] [Finite G] {F : Type w} [Group F] [Finite F] (q : F →* G) :
      (pointHom (coordinateBialgHom k F G q)).comp ↑(pointsMulEquiv k F) = q

      A coordinate morphism induced contravariantly by a homomorphism of finite groups recovers that homomorphism on base-valued points.

      source
      @[simp]
      theorem TauCeti.ConstantGroup.pointHom_coordinateBialgHom_apply {k : Type u} [Field k] {G : Type v} [Group G] [Finite G] {F : Type w} [Group F] [Finite F] (q : F →* G) (x : F) :
      (pointHom (coordinateBialgHom k F G q)) (WithConv.toConv (eval k F x)) = q x

      Pointwise, the morphism on points induced by a finite-group homomorphism is that homomorphism.

      source
      theorem TauCeti.ConstantGroup.pointHom_eq_one_of_connected {k : Type u} [Field k] {H : Type w} [CommRing H] [Bialgebra k H] {G : Type v} [Group G] [Finite G] (hconnected : ConnectedSpace (PrimeSpectrum H)) (f : coordinateRing k G →ₐc[k] H) :
      pointHom f = 1

      A connected affine group's homomorphism to a finite constant group is trivial on base-valued points.