Conjugating the toral Kostant closure by a constant matrix

The toral Kostant closure is the smallest closed subgroup scheme of GLₙ over ℤ containing the represented Kostant root subgroups and the represented weight torus. Its points therefore satisfy a universal property with respect to every closed subgroup scheme Z ≤ GLₙ and every automorphism of GLₙ: if an automorphism carries each generator into Z, it carries the whole closure into Z. This file records that property for conjugation by a constant invertible integral matrix P, in its algebra-valued form: if

P xᵢ(t) P⁻¹ ∈ Z(A)    and    P d(s) P⁻¹ ∈ Z(A)

for every root subgroup xᵢ, every torus point d(s), and every ring A, then P g P⁻¹ ∈ Z(A) for every point g of the toral closure over every ring A.

Taking Z to be a second toral Kostant closure compares two explicit carriers built from different representations: a change of basis carrying the generators of one into the other carries all points, and a change of basis matching the generators in both directions identifies the two point groups over every ring. This recognises one explicit carrier as another carrier of the same diagram without passing through any statement about the underlying abstract group.

Main results

• comapOfSurjective_conjCoordinateIso_inv_le_kostantToralDefiningIdeal, kostantToralConjToQuotient, and conj_mem_hopfIdealPointsSubgroup_of_mem_kostantToralPointsSubgroup: the universal property above, for an arbitrary closed subgroup scheme of GLₙ, on defining ideals, schemes, and points. The scheme morphism is a closed immersion and its composite with the target inclusion is the source inclusion followed by conjugation.
• map_conj_kostantToralPointsSubgroup_le: conjugation by P maps the points of one toral closure into those of a second when it maps its generators there.
• map_reindex_conj_kostantToralPointsSubgroup_eq and kostantToralPointsReindexConjMulEquiv: when in addition the inverse operation maps the generators of the second closure into the first, reindexing along finCongr followed by conjugation identifies the two point groups over every ring. The reindexing lets the two carriers have matrix sizes that agree only propositionally.

All of these live in the TauCeti.UniversalEnvelopingAlgebra namespace.

References

The toral closure is the carrier of the Chevalley--Demazure construction assembled from the root subgroups and a split torus; see J. E. Humphreys, Linear Algebraic Groups, §§7.5 and 26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.

theorem TauCeti.UniversalEnvelopingAlgebra.comapOfSurjective_conjCoordinateIso_inv_le_kostantToralDefiningIdeal {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : J.comapOfSurjective (CommHopfAlgCat.Hom.hom (GeneralLinear.conjCoordinateIso P).inv) ⋯ ≤ kostantToralDefiningIdeal e h ρ M hM hnil b wt

Conjugating the generators into a Hopf ideal quotient pulls that ideal into the toral defining ideal. If conjugation by P carries every represented root subgroup point and every represented weight-torus point into the closed subgroup scheme cut out by J, then the image of J under the coordinate automorphism of conjugation by P lies in the defining ideal of the toral closure.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralConjCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) J ⟶ CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)

The coordinate morphism from the quotient cut out by J to the toral-closure quotient, obtained by first transporting along conjugation by P and then applying the quotient map induced by the universal-property containment. Contravariantly, this presents the conjugated toral closure as a closed subgroup of the quotient by J.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mkQuotient_comp_kostantToralConjCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) J) (kostantToralConjCoordinateMap e h ρ M hM hnil b wt J P hroot htorus) = CategoryTheory.CategoryStruct.comp (GeneralLinear.conjCoordinateIso P).hom (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt))

The conjugated quotient coordinate morphism is induced by the ambient conjugation coordinate automorphism.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralConjToQuotient {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : kostantToralGroupScheme e h ρ M hM hnil b wt ⟶ CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ n) J

The closed immersion of the toral Kostant closure into the quotient cut out by J, after conjugation by P. It exists whenever conjugation carries every root-subgroup generator and every weight-torus generator into that quotient.

Equations

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

instance TauCeti.UniversalEnvelopingAlgebra.isClosedImmersion_kostantToralConjToQuotient {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (kostantToralConjToQuotient e h ρ M hM hnil b wt J P hroot htorus).hom.hom)

The conjugated toral closure is a closed subgroup scheme of the quotient cut out by J.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantToralConjToQuotient_comp_quotientSpecι {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) : CategoryTheory.CategoryStruct.comp (kostantToralConjToQuotient e h ρ M hM hnil b wt J P hroot htorus) (CommHopfAlgCat.quotientSpecι (GeneralLinear.coordinateHopfAlgebra ℤ n) J) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (GeneralLinear.coordinateHopfAlgebra ℤ n) (kostantToralDefiningIdeal e h ρ M hM hnil b wt)) ((AlgebraicGeometry.hopfSpec ↧ℤ).map (GeneralLinear.conjCoordinateIso P).hom.op)

The conjugated toral-closure immersion, followed by the target quotient inclusion, is the source quotient inclusion followed by conjugation on the ambient general-linear spectrum.

theorem TauCeti.UniversalEnvelopingAlgebra.conj_mem_hopfIdealPointsSubgroup_of_mem_kostantToralPointsSubgroup {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) (J : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ n)) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A) (A : Type v) [CommRing A] {g : GL (Fin n) A} (hg : g ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) : (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * g * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ GeneralLinear.hopfIdealPointsSubgroup n J A

The toral closure is carried into every closed subgroup scheme into which conjugation by P carries its generators.

theorem TauCeti.UniversalEnvelopingAlgebra.map_conj_kostantToralPointsSubgroup_le {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) {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)))) (b' : Module.Basis (Fin n) ℤ ↥M') (wt' : Fin n → κ' → ℤ) (P : GL (Fin n) ℤ) (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b' wt' A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P * (kostantTorusMatrix M b wt) s * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b' wt' A) (A : Type v) [CommRing A] : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) P))) (kostantToralPointsSubgroup e h ρ M hM hnil b wt A) ≤ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b' wt' A

Conjugation by P maps the points of one toral closure into those of a second as soon as it maps the generating root subgroup and weight-torus points of the first into the second.

Carriers of propositionally equal size

The matrix size of a toral closure is the rank of its lattice, which for a concrete carrier is often a closed-form expression, such as the cardinality of an index set, that equals the size of a second carrier only after computation. The comparison below therefore allows the second carrier to live in GLₙ' for some n' with n = n', and reindexes along finCongr before conjugating.

theorem TauCeti.UniversalEnvelopingAlgebra.map_reindex_conj_kostantToralPointsSubgroup_eq {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) {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' : ℕ} (hn : n = n') (b'' : Module.Basis (Fin n') ℤ ↥M') (wt'' : Fin n' → κ' → ℤ) (Q : GL (Fin n') ℤ) [Fintype κ'] (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantTorusMatrix M b wt) s) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (hroot' : ∀ (A : Type) [inst : CommRing A] (i : I') (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantRootSubgroupMatrix e' h' ρ' M' hM' i ⋯ b'') q * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (htorus' : ∀ (A : Type) [inst : CommRing A] (s : κ' → Aˣ), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantTorusMatrix M' b'' wt'') s * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (A : Type v) [CommRing A] : Subgroup.map ((MulEquiv.toMonoidHom (MulAut.conj ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q))).comp ((finCongr hn).reindexGL A).toMonoidHom) (kostantToralPointsSubgroup e h ρ M hM hnil b wt A) = kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A

Conjugation by Q after reindexing identifies the points of two toral closures when it maps the generators of the first into the second and the inverse operation maps the generators of the second into the first.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantToralPointsReindexConjMulEquiv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) {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' : ℕ} (hn : n = n') (b'' : Module.Basis (Fin n') ℤ ↥M') (wt'' : Fin n' → κ' → ℤ) (Q : GL (Fin n') ℤ) [Fintype κ'] (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantTorusMatrix M b wt) s) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (hroot' : ∀ (A : Type) [inst : CommRing A] (i : I') (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantRootSubgroupMatrix e' h' ρ' M' hM' i ⋯ b'') q * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (htorus' : ∀ (A : Type) [inst : CommRing A] (s : κ' → Aˣ), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantTorusMatrix M' b'' wt'') s * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (A : Type v) [CommRing A] : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A) ≃* ↥(kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A)

The identification of the points of two toral closures by reindexing and conjugating by Q.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantToralPointsReindexConjMulEquiv_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type} [Fintype κ] {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 → κ → ℤ) {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' : ℕ} (hn : n = n') (b'' : Module.Basis (Fin n') ℤ ↥M') (wt'' : Fin n' → κ' → ℤ) (Q : GL (Fin n') ℤ) [Fintype κ'] (hroot : ∀ (A : Type) [inst : CommRing A] (i : I) (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (htorus : ∀ (A : Type) [inst : CommRing A] (s : κ → Aˣ), (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ((kostantTorusMatrix M b wt) s) * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ ∈ kostantToralPointsSubgroup e' h' ρ' M' hM' hnil' b'' wt'' A) (hroot' : ∀ (A : Type) [inst : CommRing A] (i : I') (q : WithConv (↑(AdditiveGroup.coordinateHopfAlgebra ℤ) →ₐ[ℤ] A)), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantRootSubgroupMatrix e' h' ρ' M' hM' i ⋯ b'') q * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (htorus' : ∀ (A : Type) [inst : CommRing A] (s : κ' → Aˣ), ((finCongr hn).symm.reindexGL A) (((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹ * (kostantTorusMatrix M' b'' wt'') s * (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q) ∈ kostantToralPointsSubgroup e h ρ M hM hnil b wt A) (A : Type v) [CommRing A] (g : ↥(kostantToralPointsSubgroup e h ρ M hM hnil b wt A)) : ↑((kostantToralPointsReindexConjMulEquiv e h ρ M hM hnil b wt e' h' ρ' M' hM' hnil' hn b'' wt'' Q hroot htorus hroot' htorus' A) g) = (Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q * ((finCongr hn).reindexGL A) ↑g * ((Matrix.GeneralLinearGroup.map (algebraMap ℤ A)) Q)⁻¹

The identification of two toral closures reindexes and then conjugates by Q.