Reductive algebraic groups

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremBorel conjugacy#

Any two Borel subgroups of a finite-type affine group over an algebraically closed field are conjugate by a rational point. The ambient group need not be smooth, reduced, or connected.

TauCeti.HopfIdeal.IsBorelOverAlgClosed.exists_conjugate_eq.{u} {k : Type u} [Field k]
  [IsAlgClosed k] {H : TauCeti.FiniteTypeCommHopfAlgCat k} {I J : TauCeti.HopfIdeal k ↑H.obj}
  (hI : TauCeti.HopfIdeal.IsBorelOverAlgClosed k H I)
  (hJ : TauCeti.HopfIdeal.IsBorelOverAlgClosed k H J) : ∃ g, I.conjugate g = J

Lean

Formalized in Tau Ceti as TauCeti.HopfIdeal.IsBorelOverAlgClosed.exists_conjugate_eq.

Sources

• Tau Ceti documentation: TauCeti.HopfIdeal.IsBorelOverAlgClosed.exists_conjugate_eq
• Source of TauCeti.HopfIdeal.IsBorelOverAlgClosed.exists_conjugate_eq in TauCeti/Algebra/AlgebraicGroup/Borel/Conjugacy/Existence.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.HopfIdeal.IsBorelOverAlgClosed.exists_conjugate_eq

Uses 2

Proof usesBorel fixed-point theorem, orbit form · The Jacobian criterion for étaleness

TheoremExistence of closed orbits#

A nonempty scheme of finite type over an algebraically closed field, acted on by a group scheme of finite type, contains the closed orbit of a rational point.

TauCeti.SchemeAction.exists_isClosed_orbit.{u} {k : Type u} [Field k] [IsAlgClosed k]
  (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))
  {X : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)} [CategoryTheory.GrpObj G]
  [CategoryTheory.ModObj G X] [AlgebraicGeometry.LocallyOfFiniteType G.hom] [CompactSpace ↥G.left]
  [AlgebraicGeometry.LocallyOfFiniteType X.hom] [CompactSpace ↥X.left] [Nonempty ↥X.left] :
  ∃ y, IsClosed (TauCeti.SchemeAction.orbit G y)

Lean

Formalized in Tau Ceti as TauCeti.SchemeAction.exists_isClosed_orbit.

Sources

• Tau Ceti documentation: TauCeti.SchemeAction.exists_isClosed_orbit
• Source of TauCeti.SchemeAction.exists_isClosed_orbit in TauCeti/AlgebraicGeometry/GroupAction/ClosedOrbit.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.SchemeAction.exists_isClosed_orbit

TheoremGLₙ/G is affine for a faithful reductive representation#

Let G be a reductive group over a field of characteristic zero and ρ : G → GLₙ a faithful representation with coordinate morphism ρ* : O(GLₙ) ⟶ O(G). Restriction to the functions on GLₙ invariant under right translation by G identifies the fppf homogeneous quotient GLₙ/G with the sheaf of points of Spec O(GLₙ)^G.

TauCeti.Comodule.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_coordinateBialgHom.{u}
  {k H M : Type u} [Field k] [CharZero k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H]
  [AddCommMonoid M] [_root_.Module k M] [TauCeti.Comodule k H M] {n : ℕ}
  (b : Module.Basis (Fin n) k M) (hM : TauCeti.Comodule.IsFaithful)
  (hH : TauCeti.reductiveCommHopfAlgProperty k (TauCeti.FiniteTypeCommHopfAlgCat.of k H)) :
  CategoryTheory.IsIso
    (TauCeti.HopfIdeal.ker
        (TauCeti.Comodule.coordinateBialgHom b)).fppfHomogeneousQuotientToCoinvariantsPoints

Lean

Formalized in Tau Ceti as TauCeti.Comodule.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_coordinateBialgHom.

Sources

• Tau Ceti documentation: TauCeti.Comodule.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_coordinateBialgHom
• Source of TauCeti.Comodule.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_coordinateBialgHom in TauCeti/Algebra/AlgebraicGroup/Fppf/Quotient/Homogeneous/GeneralLinear.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.Comodule.isIso_fppfHomogeneousQuotientToCoinvariantsPoints_ker_coordinateBialgHom

Uses 1

Proof usesMatsushima's criterion, affine direction, in characteristic zero

TheoremTauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero#

An affine group scheme of finite type over a field of characteristic zero is smooth.

TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero.{u} {k : Type u} [Field k] [CharZero k]
  (G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k)) [CategoryTheory.GrpObj G]
  [AlgebraicGeometry.IsAffine G.left] [AlgebraicGeometry.LocallyOfFiniteType G.hom] :
  AlgebraicGeometry.Smooth G.hom

Lean

Formalized in Tau Ceti as TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero.

Sources

• Tau Ceti documentation: TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero
• Source of TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero in TauCeti/AlgebraicGeometry/Group/Cartier.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero

Uses 1

Proof usesCartier's theorem

DefinitionTauCeti.HopfIdeal.IsParabolic#

A Hopf ideal defines a parabolic subgroup when its base change to an algebraic closure defines a smooth closed subgroup of the geometric fibre containing a Borel subgroup.

The order is contravariant: I ≤ J says that the subgroup cut out by I contains the subgroup cut out by J.

TauCeti.HopfIdeal.IsParabolic.{u, v} (k : Type u) [Field k] (H : CommHopfAlgCat k)
  [Algebra.FiniteType k ↑H] (I : TauCeti.HopfIdeal k ↑H) : Prop

Lean

Formalized in Tau Ceti as TauCeti.HopfIdeal.IsParabolic.

Sources

• Tau Ceti documentation: TauCeti.HopfIdeal.IsParabolic
• Source of TauCeti.HopfIdeal.IsParabolic in TauCeti/Algebra/AlgebraicGroup/Parabolic/Basic.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.HopfIdeal.IsParabolic

DefinitionThe fppf quotient P(λ)/U(λ) is the dynamic Levi Z(λ)#

The subgroup in the quotient is given by its actual defining ideal inside the parabolic coordinate ring.

BialgHom.parabolicLeviFppfQuotientIso.{u} {R H : Type u} [CommRing R] [CommRing H] [HopfAlgebra R H]
  (l : H →ₐc[R] LaurentPolynomial R) :
  TauCeti.CommHopfAlgCat.fppfQuotientSheaf
      ((↧H).quotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l))
      (l.unipotentDefiningHopfIdeal.map
        (CommHopfAlgCat.Hom.hom
          ((↧H).mkQuotient (TauCeti.Cocharacter.parabolicDefiningHopfIdeal l))))
      ⋯ ≅
    TauCeti.CommHopfAlgCat.pointsFppfGroupObject
      ((↧H).quotient (TauCeti.Cocharacter.leviDefiningHopfIdeal l))

Lean

Formalized in Tau Ceti as BialgHom.parabolicLeviFppfQuotientIso.

Sources

• Tau Ceti documentation: BialgHom.parabolicLeviFppfQuotientIso
• Source of BialgHom.parabolicLeviFppfQuotientIso in TauCeti/Algebra/AlgebraicGroup/Dynamic/Levi/Quotient.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanBialgHom.parabolicLeviFppfQuotientIso

TheoremBialgHom.algebraEtale_coinvariants_centralizer_normalizer#

The represented quotient of the scheme normalizer by the scheme centralizer is étale, retaining the full subgroup schemes even when D(X) is nonreduced.

BialgHom.algebraEtale_coinvariants_centralizer_normalizer.{u} {k : Type u} [Field k] [IsAlgClosed k]
  {H : TauCeti.FiniteTypeCommHopfAlgCat k} {X : Type u} [CommGroup X]
  (π : ↑H.obj →ₐc[k] MonoidAlgebra k X) (hπ : Function.Surjective ⇑π)
  [IsReduced ↑(H.quotient (π.normalizerHopfIdeal hπ)).obj] :
  Algebra.Etale k
    ↥(π.centralizerHopfIdeal.map
          (Bialgebra.Quotient.mkBialgHom (π.normalizerHopfIdeal hπ).toIdeal)).coinvariants

Lean

Formalized in Tau Ceti as BialgHom.algebraEtale_coinvariants_centralizer_normalizer.

Sources

• Tau Ceti documentation: BialgHom.algebraEtale_coinvariants_centralizer_normalizer
• Source of BialgHom.algebraEtale_coinvariants_centralizer_normalizer in TauCeti/Algebra/AlgebraicGroup/DiagonalizableGroup/Normalizer/Quotient.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanBialgHom.algebraEtale_coinvariants_centralizer_normalizer

TheoremThe centralizer of a diagonalizable subgroup of a smooth affine group of finite type is smooth, over any base ring#

BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal.{u, v, w} {R : Type u} {X : Type w}
  [CommRing R] [CommGroup X] {H : TauCeti.FiniteTypeCommHopfAlgCat R} [Algebra.Smooth R ↑H.obj]
  (π : ↑H.obj →ₐc[R] MonoidAlgebra R X) :
  TauCeti.smoothCommHopfAlgProperty R (H.quotient π.centralizerHopfIdeal).obj

Lean

Formalized in Tau Ceti as BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal.

Sources

• Tau Ceti documentation: BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal
• Source of BialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal in TauCeti/Algebra/AlgebraicGroup/DiagonalizableGroup/Centralizer/Smooth.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanBialgHom.smoothCommHopfAlgProperty_quotient_centralizerHopfIdeal

DefinitionG₀(K) ≃ G^F#

The K-rational points of H are isomorphic to the points of the base change k ⊗[K] H over a domain k fixed by the geometric Frobenius. The isomorphism sends a rational point g to s ⊗ h ↦ s * g h.

TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius.{u_1, u_2, u_3}
  (K : Type u_1) [Field K] [Fintype K] (k : Type u_2) [CommRing k] [IsDomain k] [Algebra K k]
  (H : Type u_3) [CommSemiring H] [HopfAlgebra K H] :
  WithConv (H →ₐ[K] K) ≃*
    ↥(TauCeti.fixedSubgroup (TauCeti.FiniteField.geometricFrobeniusBialgHom K k H).mapDomain)

Lean

Formalized in Tau Ceti as TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius.

Sources

• Tau Ceti documentation: TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius
• Source of TauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius in TauCeti/Algebra/AlgebraicGroup/Frobenius/FiniteField.lean
• Tau Ceti roadmap status: Reductive algebraic groups

LeanTauCeti.FiniteField.rationalPointsMulEquivFixedSubgroupGeometricFrobenius

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.