Documentation

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

Points of the toral Kostant closure #

The closed group scheme kostantToralGroupScheme is generated inside GLₙ by the represented Kostant root subgroups together with the represented weight torus. This file identifies the corresponding formal inclusion on algebra-valued points. Its point subgroup contains both the pointwise elementary group and the represented torus, and hence contains their join.

For an arbitrary set S of root indices, write B_S(A) for the subgroup generated by the root subgroups indexed by S and the torus. After passing from automorphisms of the base-changed lattice to matrices in its chosen basis, the main theorem gives

B_S(A) ≤ kostantToralPointsSubgroup(A).

Taking S = Set.univ places the full torus--elementary subgroup assembled in TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.RootSubgroup.Borel inside the points of the assembled scheme carrier. Equality over an algebraically closed field is a separate generation theorem and is not asserted here.

Main declarations #

TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsSubgroup: the algebra-valued points of the toral closure, viewed in GLₙ.
TauCeti.UniversalEnvelopingAlgebra.kostantToralSchemePointMulEquiv: quotient-coordinate points of the toral closure identified with its scheme-valued points.
TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedPointsSubgroup_le_toralPoints: the root-generated point subgroup is contained in the toral point subgroup.
TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix_mem_toralPoints: every represented weight-torus point lies in the toral closure.
TauCeti.UniversalEnvelopingAlgebra.kostantToralRootSubgroupPoints and TauCeti.UniversalEnvelopingAlgebra.kostantToralWeightTorusPoints: the canonical root-subgroup and weight-torus homomorphisms into the toral-closure points.
TauCeti.UniversalEnvelopingAlgebra.kostantToralWeightTorusPoints_conj_rootSubgroupPoints: the pinning equation in those matrix-valued points.
TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusSubsystemSubgroup_le_toralPoints: every pointwise torus--root-subgroup join lies in the assembled scheme's points.

References #

The construction is the pointwise face of the split torus and root-subgroup carrier in the Chevalley--Demazure construction; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type v) [CommRing A] :

Subgroup (GL (Fin n) A)

The algebra-valued points of the toral Kostant closure, embedded in GLₙ through its Hopf-ideal quotient presentation.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsSubgroup_def {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type v) [CommRing A] :

kostantToralPointsSubgroup e h ρ M hM hnil b wt A = GeneralLinear.hopfIdealPointsSubgroup n (kostantToralDefiningIdeal e h ρ M hM hnil b wt) A

The toral-closure points are the general-linear point subgroup cut out by the toral defining Hopf ideal.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantToralPointsSubgroup_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type v) [CommRing A] (g : GL (Fin n) A) :

g ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A ↔ ∀ x ∈ kostantToralDefiningIdeal e h ρ M hM hnil b wt, ((GeneralLinear.pointsMulEquiv n).symm g).ofConv x = 0

Membership in the points of the toral closure is vanishing on its defining Hopf ideal.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantGeneratedPointsSubgroup_le_toralPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type v) [CommRing A] :

kostantGeneratedPointsSubgroup e h ρ M hM hnil b A ≤ kostantToralPointsSubgroup e h ρ M hM hnil b wt A

The algebra-valued point subgroup of the toral closure contains the root-generated point subgroup: adjoining the weight torus to the generators enlarges the represented point subgroup (by shrinking the defining ideal).

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTorusMatrix_mem_toralPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (A : Type v) [CommRing A] (s : κ → Aˣ) :

(kostantTorusMatrix M b wt) s ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A

Every represented weight-torus matrix is a point of the toral closure.

The canonical subgroups of the toral-closure points #

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralRootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (i : I) (A : Type v) [CommRing A] :

Multiplicative A →* ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)

The canonical root-subgroup homomorphism into the matrix-valued points of the toral Kostant closure. The parameter is read through the multiplicative copy of the additive group.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralRootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (i : I) (A : Type v) [CommRing A] (u : Multiplicative A) :

↑((kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i A) u) = (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) (AdditiveGroup.gaPointsMulEquiv.symm u)

The canonical toral-closure root-subgroup point is its represented divided-power exponential matrix.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralWeightTorusPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (A : Type v) [CommRing A] :

(κ → Aˣ) →* ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)

The canonical weight-torus homomorphism into the matrix-valued points of the toral Kostant closure.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralWeightTorusPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (A : Type v) [CommRing A] (s : κ → Aˣ) :

↑((kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) s) = (kostantTorusMatrix M b wt) s

The canonical toral-closure weight-torus point is its diagonal weight matrix.

@[reducible, inline]

noncomputable abbrev TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsPresentation {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (A : Type v) [CommRing A] :

GeneralLinear.IntegralPointsPresentation n (kostantToralDefiningIdeal e h ρ M hM hnil b wt) A

The integral-points presentation of the toral Kostant closure.

Equations

TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsPresentation e h ρ M hM hnil b wt A = ⟨TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsSubgroup e h ρ M hM hnil b wt A, ⋯⟩

Instances For

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantToralRootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (i : I) (u : Multiplicative A) :

((kostantToralPointsPresentation e h ρ M hM hnil b wt A).map (kostantToralPointsPresentation e h ρ M hM hnil b wt B) f) ((kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i A) u) = (kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i B) (Multiplicative.ofAdd (f (Multiplicative.toAdd u)))

The presented toral-closure root point is natural in the value ring.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantToralWeightTorusPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : κ → Aˣ) :

((kostantToralPointsPresentation e h ρ M hM hnil b wt A).map (kostantToralPointsPresentation e h ρ M hM hnil b wt B) f) ((kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) s) = (kostantToralWeightTorusPoints e h ρ M hM hnil b wt B) fun (i : κ) => (Units.map ↑f) (s i)

The presented toral-closure weight-torus point is natural in the value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralWeightTorusPoints_conj_rootSubgroupPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (hwt : ∀ (x : Fin n), IsCartanWeightVector h ρ (wt x) ↑(b x)) {i : I} {α : κ → ℤ} (hα : ∀ (j : κ), ⁅h j, e i⁆ = ↑(α j) • e i) (A : Type v) [CommRing A] (s : κ → Aˣ) (u : Multiplicative A) :

(kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) s * (kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i A) u * ((kostantToralWeightTorusPoints e h ρ M hM hnil b wt A) s)⁻¹ = (kostantToralRootSubgroupPoints e h ρ M hM hnil b wt i A) (Multiplicative.ofAdd (↑(torusCharacter s α) * Multiplicative.toAdd u))

The pinning equation in the matrix-valued points of the toral Kostant closure. If e i has Cartan weight α, conjugation by the weight-torus point s rescales the root-subgroup parameter by α(s). This is not a simp lemma: the weight α is pinned only by the hypothesis hα, so simp could never infer it from the left-hand side.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantTorusSubsystemSubgroup_le_toralPoints {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Fintype κ] (S : Set I) (A : Type v) [CommRing A] :

Subgroup.map (Units.map ↑(LinearMap.toMatrixAlgEquiv (Module.Basis.baseChange A b)).toMulEquiv) (kostantTorusSubsystemSubgroup e h ρ M hM hnil b wt S ↧A) ≤ kostantToralPointsSubgroup e h ρ M hM hnil b wt A

After writing automorphisms in the basis b, every subgroup generated by a set of represented root subgroups together with the weight torus lies in the points of the toral closure.

Scheme-valued points #

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_eq_hopfSpec {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] :

kostantToralGroupScheme e h ρ M hM hnil b wt = (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)))

The toral closure is represented by its quotient coordinate Hopf algebra.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralGroupScheme_X_left {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] :

(kostantToralGroupScheme e h ρ M hM hnil b wt).X.left = AlgebraicGeometry.Spec ↧↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt))

The underlying scheme of the toral closure is the spectrum of its coordinate ring.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralSchemePointMulEquiv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type) [CommRing A] :

WithConv (↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) →ₐ[ℤ ] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (kostantToralGroupScheme e h ρ M hM hnil b wt).X)

Algebra-valued points of the toral closure, transported to scheme-valued points.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralSchemePointMulEquiv_apply_left {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ 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 → κ → ℤ) [Finite κ] (A : Type) [CommRing A] (q : WithConv (↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) →ₐ[ℤ ] A)) :

CategoryTheory.Over.Hom.left ((kostantToralSchemePointMulEquiv e h ρ M hM hnil b wt A) q) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑q.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying spectrum map of a quotient point of the toral closure.