Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Scheme.ToralClosure.RootSubgroupPoints

Root subgroups on points of the toral Kostant closure #

The toral Kostant closure has a coordinate Hopf algebra obtained by quotienting the coordinate algebra of GLβ‚™, and each represented root subgroup factors through this quotient. This file records the resulting map on algebra-valued points. Thus, for every commutative ring A and root index i, it supplies the intrinsic homomorphism

𝔾ₐ(A) β†’ kostantToralGroupScheme(A).

Composing this homomorphism with the quotient-points inclusion recovers the previously constructed matrix-valued root subgroup. The construction is natural in A; in particular, iterated Frobenius raises its root parameter to the corresponding prime-power exponent. These are the point-level root-subgroup and field-endomorphism interfaces required when the generic Kostant carrier is specialized to a pinned Chevalley--Demazure group.

Main declarations #

References #

This advances the β€œChevalley--Demazure construction” and β€œpoints over an algebraically closed field” targets in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. The resulting intrinsic root-subgroup map and Frobenius law are inputs to milestones L0 and L1 of the CFSGStatement roadmap.

source
noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralPoints {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : CommAlgCat β„€) :
↑(HopfAlgebra.points A) β†’* ↑(HopfAlgebra.points A)

The ith represented root subgroup on algebra-valued points of the toral Kostant closure.

Its coordinate morphism is kostantRootSubgroupToralCoordinateMap; contravariance of the functor of points turns that morphism into a homomorphism from the additive-group points to the intrinsic points of the quotient coordinate Hopf algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralPoints_apply {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : CommAlgCat β„€) (q : ↑(HopfAlgebra.points A)) :
    (kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i A) q = (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantRootSubgroupToralCoordinateMap e h ρ M hM hnil b wt i)).app A)) q

    The intrinsic root-subgroup point map is precomposition by its factored coordinate map.

    source
    @[simp]
    theorem TauCeti.UniversalEnvelopingAlgebra.quotientPointsHom_kostantRootSubgroupToralPoints {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : CommAlgCat β„€) (q : ↑(HopfAlgebra.points A)) :
    (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra β„€ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt) A)) ((kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i A) q) = (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantRootSubgroupCoordinateMap e h ρ M hM i β‹― b)).app A)) q

    Including an intrinsic toral-closure root point into the ambient general linear group recovers the original represented root-subgroup point.

    source
    theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_quotientPointsHom_kostantRootSubgroupToralPoints {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : Type v) [CommRing A] (q : ↑(HopfAlgebra.points ↧A)) :
    (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra β„€ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt) ↧A)) ((kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i ↧A) q)) = (kostantRootSubgroupMatrix e h ρ M hM i β‹― b) q

    In general-linear coordinates, the intrinsic root point is the divided-power exponential matrix previously attached to the represented Kostant root subgroup.

    This is not a simp lemma because GeneralLinear.pointsMulEquiv_apply first normalizes its left-hand side to GeneralLinear.pointToGeneralLinear; use it explicitly when that matrix form is needed.

    source
    noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralParam {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : CommAlgCat β„€) :
    Multiplicative ↑A β†’* ↑(HopfAlgebra.points A)

    The intrinsic toral-closure root subgroup with its parameter read in the value ring through the canonical identification 𝔾ₐ(A) ≃ A⁺.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupToralParam_apply {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (A : CommAlgCat β„€) (t : Multiplicative ↑A) :
      (kostantRootSubgroupToralParam e h ρ M hM hnil b wt i A) t = (kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i A) (AdditiveGroup.gaPointsMulEquiv.symm t)

      The parametrized intrinsic root subgroup is the point map evaluated on the corresponding point of 𝔾ₐ.

      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.mapPoints_kostantRootSubgroupToralPoints {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) {A B : CommAlgCat β„€} (Ο† : A ⟢ B) (q : ↑(HopfAlgebra.points A)) :
      (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints Ο†)) ((kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i A) q) = (kostantRootSubgroupToralPoints e h ρ M hM hnil b wt i B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints Ο†)) q)

      The intrinsic root-subgroup point map is natural in the value algebra.

      source
      @[simp]
      theorem TauCeti.UniversalEnvelopingAlgebra.mapPoints_kostantRootSubgroupToralParam {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) {A B : CommAlgCat β„€} (Ο† : A ⟢ B) (t : Multiplicative ↑A) :
      (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints Ο†)) ((kostantRootSubgroupToralParam e h ρ M hM hnil b wt i A) t) = (kostantRootSubgroupToralParam e h ρ M hM hnil b wt i B) (Multiplicative.ofAdd ((CommAlgCat.Hom.hom Ο†) (Multiplicative.toAdd t)))

      Base change sends the intrinsic root element with parameter t to the root element whose parameter is the image of t.

      source
      theorem TauCeti.UniversalEnvelopingAlgebra.mapPoints_iterateFrobeniusValueHom_kostantRootSubgroupToralParam {L : Type u} [LieRing L] [LieAlgebra β„š L] {I : Type w} {ΞΊ : Type} [Finite ΞΊ] {V : Type} [AddCommGroup V] [Module β„š V] (e : I β†’ L) (h : ΞΊ β†’ L) (ρ : UniversalEnvelopingAlgebra β„š L →ₐ[β„š] Module.End β„š V) (M : AddSubgroup V) (hM : βˆ€ u ∈ kostantForm e h, βˆ€ m ∈ M, (ρ u) m ∈ M) (hnil : βˆ€ (i : I), IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ΞΉ β„š) (e i)))) {n : β„•} (b : Module.Basis (Fin n) β„€ β†₯M) (wt : Fin n β†’ ΞΊ β†’ β„€) (i : I) (p m : β„•) (A : CommAlgCat β„€) [ExpChar (↑A) p] (t : Multiplicative ↑A) :
      (CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints (iterateFrobeniusValueHom p m A))) ((kostantRootSubgroupToralParam e h ρ M hM hnil b wt i A) t) = (kostantRootSubgroupToralParam e h ρ M hM hnil b wt i A) (Multiplicative.ofAdd (Multiplicative.toAdd t ^ p ^ m))

      Iterated Frobenius preserves each intrinsic root subgroup and raises its parameter to the p ^ m-th power. Over an algebraic closure of 𝔽_p, this is the root-subgroup compatibility of the standard q-power Frobenius. The general simp lemma mapPoints_kostantRootSubgroupToralParam already normalizes this specialization.