Documentation

TauCeti.Algebra.AlgebraicGroup.Connected.CommHopfAlgCat

Geometric connectedness of commutative Hopf algebras #

For a commutative Hopf algebra H over a field k, geometric connectedness means that after every extension K / k of the base field, the base-changed coordinate ring H ⊗[k] K has connected prime spectrum. This is equivalent to saying that every such base change has no idempotents other than zero and one.

The condition is exposed as an ObjectProperty on the ambient Hopf-algebra category; consumers can impose it without introducing a separate bundled category of connected objects.

Main declarations #

References #

This is the geometric-connectedness prerequisite for Layer 3, "Identity component and component group", of the ReductiveGroups roadmap.

source
def TauCeti.geometricallyConnectedCommHopfAlgProperty (k : Type u) [Field k] :
CategoryTheory.ObjectProperty (CommHopfAlgCat k)

A commutative Hopf algebra over a field is geometrically connected when the spectrum of its coordinate ring remains connected after every extension of the base field.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty_iff (k : Type u) [Field k] (H : CommHopfAlgCat k) :
    geometricallyConnectedCommHopfAlgProperty k H ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K], ConnectedSpace (PrimeSpectrum (TensorProduct k (↑H) K))

    Membership in the geometrically connected commutative-Hopf-algebra object property.

    source
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.connectedSpace (k : Type u) [Field k] (H : CommHopfAlgCat k) (h : geometricallyConnectedCommHopfAlgProperty k H) :
    ConnectedSpace (PrimeSpectrum ↑H)

    A geometrically connected commutative Hopf algebra has connected prime spectrum.

    source
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.connectedSpace_algebraicClosureBaseChange {k : Type u} [Field k] {H : CommHopfAlgCat k} (h : geometricallyConnectedCommHopfAlgProperty k H) :
    ConnectedSpace (PrimeSpectrum (TensorProduct k (AlgebraicClosure k) ↑H))

    The geometric fibre of a geometrically connected commutative Hopf algebra has connected prime spectrum, written with the algebraic closure on the left. This is the orientation used by the geometric character group.

    source
    instance TauCeti.instIsClosedUnderIsomorphismsCommHopfAlgCatGeometricallyConnectedCommHopfAlgProperty (k : Type u) [Field k] :
    (geometricallyConnectedCommHopfAlgProperty k).IsClosedUnderIsomorphisms

    Geometric connectedness is invariant under isomorphisms of commutative Hopf algebras.

    source
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty_iff_idempotent_eq_zero_or_one (k : Type u) [Field k] (H : CommHopfAlgCat k) :
    geometricallyConnectedCommHopfAlgProperty k H ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] (e : TensorProduct k (↑H) K), IsIdempotentElem e → e = 0 ∨ e = 1

    A commutative Hopf algebra is geometrically connected exactly when, after every extension K / k of the base field, every idempotent of H ⊗[k] K is zero or one.

    source
    theorem TauCeti.geometricallyConnectedCommHopfAlgProperty.of_injective {k : Type u} [Field k] {H : CommHopfAlgCat k} {H' : CommHopfAlgCat k} (f : ↑H →ₐ[k] ↑H') (hf : Function.Injective ⇑f) (h : geometricallyConnectedCommHopfAlgProperty k H') :
    geometricallyConnectedCommHopfAlgProperty k H

    Geometric connectedness descends along injective algebra homomorphisms. If the coordinate ring of H embeds, as a k-algebra, into that of a geometrically connected H', then H is geometrically connected. The embedding need not respect the Hopf structures: geometrically, the connected spectrum of H' maps dominantly onto that of H after every extension of the base field.