Documentation

TauCeti.Algebra.AlgebraicGroup.Connected.ComponentGroup.Group

The group structure on connected components of an affine group #

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. Every connected component of Spec H contains a rational point, and two rational points lie in the same component exactly when they differ by a point of the identity component. Thus the canonical equivalence

H(k) / H⁰(k) ≃ ConnectedComponents (Spec H)

transports the quotient-group structure to the connected components. This file records that structure and its characteristic API: the component of a product is the product of the components, and the component map from rational points is a surjective group homomorphism whose kernel is exactly H⁰(k).

This is the group-theoretic input for representing π₀(H) by the finite constant group scheme on the connected components. The coordinate-algebra comparison additionally needs the orthogonal component-idempotent decomposition.

Main declarations #

References #

This advances Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap.

source
@[instance_reducible]
noncomputable instance TauCeti.FiniteTypeCommHopfAlgCat.instGroupConnectedComponents {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
Group (ConnectedComponents (PrimeSpectrum ↑H.obj))

The group structure on the connected components of the spectrum of a finite-type affine group. It is characterized by the requirement that the canonical bijection from H(k) / H⁰(k) be multiplicative.

Equations
source
noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsMulEquivConnectedComponents {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
↑H.componentGroupPoints ≃* ConnectedComponents (PrimeSpectrum ↑H.obj)

The canonical equivalence from the rational pointwise component group to the connected components of the spectrum, as a multiplicative equivalence.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsMulEquivConnectedComponents_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (q : ↑H.componentGroupPoints) :
    H.componentGroupPointsMulEquivConnectedComponents q = H.componentGroupPointsToConnectedComponents q

    The multiplicative component-group equivalence is the canonical component map on elements.

    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsToConnectedComponents_one {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
    H.componentGroupPointsToConnectedComponents 1 = 1

    The canonical bijection from the rational pointwise quotient to connected components sends the identity to the identity component.

    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsToConnectedComponents_mul {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (q r : ↑H.componentGroupPoints) :
    H.componentGroupPointsToConnectedComponents (q * r) = H.componentGroupPointsToConnectedComponents q * H.componentGroupPointsToConnectedComponents r

    The canonical bijection from the rational pointwise quotient to connected components preserves multiplication.

    source
    @[simp]
    theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsToConnectedComponents_inv {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (q : ↑H.componentGroupPoints) :
    H.componentGroupPointsToConnectedComponents q⁻¹ = (H.componentGroupPointsToConnectedComponents q)⁻¹

    The canonical bijection from the rational pointwise quotient to connected components preserves inverses.

    source
    noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.rationalComponentMap {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
    ↑(HopfAlgebra.points ↧k) →* ConnectedComponents (PrimeSpectrum ↑H.obj)

    Send a rational point of a finite-type affine group to the connected component containing its kernel point.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalComponentMap_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) :
      H.rationalComponentMap g = ConnectedComponents.mk (H.rationalKernelPoint g)

      The rational component map sends a point to the component containing its kernel point.

      source
      @[simp]
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalKernelPoint_one_component {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
      ConnectedComponents.mk (Bialgebra.augmentationPoint k ↑H.obj) = 1

      The component containing the identity rational point is the identity of the component group.

      source
      @[simp]
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalKernelPoint_mul_component {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g h : ↑(HopfAlgebra.points ↧k)) :
      ConnectedComponents.mk (H.rationalKernelPoint (g * h)) = ConnectedComponents.mk (H.rationalKernelPoint g) * ConnectedComponents.mk (H.rationalKernelPoint h)

      The component of a product of rational points is the product of their components.

      source
      @[simp]
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalKernelPoint_inv_component {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) :
      ConnectedComponents.mk (H.rationalKernelPoint g⁻¹) = (ConnectedComponents.mk (H.rationalKernelPoint g))⁻¹

      The component of the inverse of a rational point is the inverse component.

      source
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalComponentMap_surjective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
      Function.Surjective ⇑H.rationalComponentMap

      Every connected component of the spectrum contains the kernel point of a rational point.

      source
      @[simp]
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalComponentMap_eq_one_iff {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) :
      H.rationalComponentMap g = 1 ↔ g ∈ CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal ↧k

      A rational point maps to the identity component exactly when it belongs to the rational points of H⁰.

      source
      theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalComponentMap_ker {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) :
      H.rationalComponentMap.ker = CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal ↧k

      The kernel of the rational component map is the rational-point subgroup of the identity component.