The ambient coordinate automorphism of a numbered Kostant symmetry

A symmetry of numbered Kostant data is a self-map σ of the index set together with a rational automorphism θ of the representation which preserves the integral lattice M and carries the action of eᵢ to the action of e_{σ i}. Conjugating by the scalar extension of θ is then an automorphism of the general linear group of A ⊗[ℤ] M, natural in the value ring A.

This file turns that natural automorphism into an automorphism of the coordinate Hopf algebra of GLₙ itself, and records the two compositional identities a closed subgroup scheme of GLₙ needs in order to inherit it:

γ ≫ xᵢ = x_{σ i},        γ ≫ (weight torus of wt) = weight torus of (wt ∘ π⁻¹).

The first says that conjugation permutes the represented Kostant root subgroups without touching their additive parameters. The second says that when θ acts monomially on the chosen lattice basis, with coordinate permutation π and integral scaling coefficients, conjugation carries the represented weight torus of a weight family to the weight torus of the relabelled family. The scaling coefficients cancel from diagonal conjugation. Preserving a subgroup scheme cut out by both families additionally requires weight equivariance identifying that family with the original one, through a permutation of the torus index and GeneralLinear.weightTorusCoordinateMap_reindex.

Neither identity is available from the construction of the coordinate automorphism, which goes through the functor of points: full faithfulness of the functor of points on commutative Hopf algebras recovers the coordinate morphism from the natural conjugation, and each identity is then proved by evaluating both sides at the generic point of the relevant codomain.

Nothing here assumes that σ comes from a Dynkin-diagram symmetry, that θ is unique, or that the weights are the weights of an admissible lattice: all of that is supplied by the caller.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix: the matrix of the base-changed lattice symmetry in the chosen basis.
• TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryCoordinateIso: the resulting automorphism of the coordinate Hopf algebra of GLₙ.
• TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryPoints: conjugation by that matrix, as an automorphism of any subgroup of GLₙ it normalizes, together with its coordinate formula, its naturality in the value ring, and its order relation.

Main results

• pointsMulEquiv_mapPointsFunctor_kostantNumberedSymmetryCoordinateIso: on algebra-valued points the coordinate automorphism is conjugation by the base-changed matrix.
• pointsMulEquiv_toConv_comp_kostantNumberedSymmetryCoordinateIso: the explicit precomposition form of the same statement.
• kostantNumberedSymmetryCoordinateIso_hom_comp_rootSubgroupCoordinateMap: the pinning equation γ ≫ xᵢ = x_{σ i} on coordinate algebras.
• kostantNumberedSymmetryCoordinateIso_hom_comp_weightTorusCoordinateMap: a monomial-basis symmetry carries the represented weight torus to the relabelled weight torus.

All of these live in the TauCeti.UniversalEnvelopingAlgebra namespace.

References

• R. W. Carter, Simple Groups of Lie Type, §12.2.
• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.
• J. E. Humphreys, Linear Algebraic Groups, §27.

This advances the pinnings and pinned-isomorphism targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md; the automorphisms it produces are required by milestone L1 of TauCetiRoadmap/CFSGStatement/README.md.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] : GL (Fin n) A

The matrix of the base-changed lattice symmetry in the chosen basis.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantNumberedSymmetryMatrix {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (φ : A →+* B) : (Matrix.GeneralLinearGroup.map φ) (kostantNumberedSymmetryMatrix M b θ hθM A) = kostantNumberedSymmetryMatrix M b θ hθM B

The matrix of the numbered symmetry commutes with extension of the value ring.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix_pow_eq_one {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] {m : ℕ} (hm : ∀ (x : V), (θ ^ m) x = x) : kostantNumberedSymmetryMatrix M b θ hθM A ^ m = 1

The matrix of a numbered symmetry satisfies every order relation satisfied by the underlying rational linear equivalence.

The symmetry on a normalized group of matrix-valued points

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryPoints {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (P : Subgroup (GL (Fin n) A)) (hP : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) P = P) : MulAut ↥P

The automorphism of a group of matrix-valued points induced by a numbered symmetry, given by conjugation by the symmetry's matrix on any subgroup P of GLₙ that matrix normalizes. A carrier cut out inside GLₙ supplies P and the normalization hypothesis; everything the conjugation satisfies is then read off the matrix.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryPoints M b θ hθM A P hP = P.normalizerMonoidHom ⟨TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix M b θ hθM A, ⋯⟩

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantNumberedSymmetryPoints {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (P : Subgroup (GL (Fin n) A)) (hP : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) P = P) (g : ↥P) : ↑((kostantNumberedSymmetryPoints M b θ hθM A P hP) g) = kostantNumberedSymmetryMatrix M b θ hθM A * ↑g * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹

On matrices, the numbered symmetry acts on points by conjugation by its matrix.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantNumberedSymmetryPoints_symm {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (P : Subgroup (GL (Fin n) A)) (hP : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) P = P) (g : ↥P) : ↑((MulEquiv.symm (kostantNumberedSymmetryPoints M b θ hθM A P hP)) g) = (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹ * ↑g * kostantNumberedSymmetryMatrix M b θ hθM A

On matrices, the inverse of the numbered symmetry on points is conjugation by the inverse of its matrix.

theorem TauCeti.UniversalEnvelopingAlgebra.comp_kostantNumberedSymmetryPoints {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (P : Subgroup (GL (Fin n) A)) (hP : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) P = P) (Q : Subgroup (GL (Fin n) B)) (hQ : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM B))) Q = Q) (φ : A →+* B) (F : ↥P →* ↥Q) (hF : ∀ (g : ↥P), ↑(F g) = (Matrix.GeneralLinearGroup.map φ) ↑g) : F.comp (MulEquiv.toMonoidHom (kostantNumberedSymmetryPoints M b θ hθM A P hP)) = (MulEquiv.toMonoidHom (kostantNumberedSymmetryPoints M b θ hθM B Q hQ)).comp F

The numbered symmetry on points is natural in the value ring. The naturality is stated against any homomorphism F of point groups which is the entrywise map on matrices, which is what a carrier's own base-change map on points is; in particular the symmetry commutes with every Frobenius map.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryPoints_pow_eq_one {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (P : Subgroup (GL (Fin n) A)) (hP : Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (kostantNumberedSymmetryMatrix M b θ hθM A))) P = P) {m : ℕ} (hm : kostantNumberedSymmetryMatrix M b θ hθM A ^ m = 1) : kostantNumberedSymmetryPoints M b θ hθM A P hP ^ m = 1

The numbered symmetry on points inherits every order relation its matrix satisfies.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryCoordinateIso {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) : GeneralLinear.coordinateHopfAlgebra ℤ n ≅ GeneralLinear.coordinateHopfAlgebra ℤ n

The coordinate Hopf-algebra automorphism recovered from conjugation on points: conjugation by the integral numbered-symmetry matrix.

Equations

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

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_mapPointsFunctor_kostantNumberedSymmetryCoordinateIso {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : CommAlgCat ℤ) (f : ↑(HopfAlgebra.points A)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (kostantNumberedSymmetryCoordinateIso M b θ hθM).hom).app A)) f) = kostantNumberedSymmetryMatrix M b θ hθM ↑A * (GeneralLinear.pointsMulEquiv n) f * (kostantNumberedSymmetryMatrix M b θ hθM ↑A)⁻¹

On algebra-valued points, the recovered coordinate automorphism is conjugation by the base-changed numbered-symmetry matrix.

theorem TauCeti.UniversalEnvelopingAlgebra.pointsMulEquiv_toConv_comp_kostantNumberedSymmetryCoordinateIso {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (f : WithConv (↑(GeneralLinear.coordinateHopfAlgebra ℤ n) →ₐ[ℤ] A)) : (GeneralLinear.pointsMulEquiv n) (WithConv.toConv (f.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (kostantNumberedSymmetryCoordinateIso M b θ hθM).hom))) = kostantNumberedSymmetryMatrix M b θ hθM A * (GeneralLinear.pointsMulEquiv n) f * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹

On points over a value ring in any universe, precomposition with the coordinate automorphism is conjugation by the base-changed numbered-symmetry matrix.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix_conj_kostantRootSubgroupMatrix {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (A : Type v) [CommRing A] (i : I) (q : WithConv (SymmetricAlgebra ℤ ℤ →ₐ[ℤ] A)) : kostantNumberedSymmetryMatrix M b θ hθM A * (kostantRootSubgroupMatrix e h ρ M hM i ⋯ b) q * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹ = (kostantRootSubgroupMatrix e h ρ M hM (σ i) ⋯ b) q

Matrix-coordinate form of the pinning equation.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryCoordinateIso_hom_comp_rootSubgroupCoordinateMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {I : Type w} {κ : Type z} {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) (σ : I → I) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (hθe : ∀ (i : I) (v : V), θ ((ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) v) = (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e (σ i)))) (θ v)) (i : I) : CategoryTheory.CategoryStruct.comp (kostantNumberedSymmetryCoordinateIso M b θ hθM).hom (kostantRootSubgroupCoordinateMap e h ρ M hM i ⋯ b) = kostantRootSubgroupCoordinateMap e h ρ M hM (σ i) ⋯ b

The ambient coordinate automorphism permutes the Kostant root-subgroup coordinate maps.

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantNumberedSymmetryMatrix_apply {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (A : Type v) [CommRing A] (i j : Fin n) : ↑(kostantNumberedSymmetryMatrix M b θ hθM A) i j = ((Module.Basis.baseChange A b).repr (↑(θ.toAddEquiv.baseChangeInvariantRestrictUnit M hθM) ((Module.Basis.baseChange A b) j))) i

The entries of the numbered-symmetry matrix are the coordinates of the images of the basis vectors.

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantNumberedSymmetryMatrix_apply_of_monomial {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (A : Type v) [CommRing A] (i j : Fin n) : ↑(kostantNumberedSymmetryMatrix M b θ hθM A) i j = if i = basisPerm j then (algebraMap ℤ A) (basisScale j) else 0

The matrix of a symmetry acting monomially on the chosen lattice basis. Its jth column has the integral scaling coefficient at row basisPerm j and is zero elsewhere. This is the hypothesis under which conjugation normalizes the diagonal torus of GLₙ; allowing the coefficient is necessary for graph symmetries whose pinned lift is a signed coordinate permutation.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryMatrix_conj_diagGL {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) (A : Type v) [CommRing A] (d : Fin n → Aˣ) : kostantNumberedSymmetryMatrix M b θ hθM A * diagGL d * (kostantNumberedSymmetryMatrix M b θ hθM A)⁻¹ = diagGL fun (i : Fin n) => d (basisPerm⁻¹ i)

Conjugating a diagonal matrix by a monomial basis symmetry relabels its entries by the inverse permutation. The integral scaling coefficients cancel from the conjugation, so in particular every signed permutation normalizes the diagonal torus of GLₙ.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantNumberedSymmetryCoordinateIso_hom_comp_weightTorusCoordinateMap {V : Type} [AddCommGroup V] [Module ℚ V] (M : AddSubgroup V) {n : ℕ} (b : Module.Basis (Fin n) ℤ ↥M) (θ : V ≃ₗ[ℚ] V) (hθM : ∀ (v : V), θ v ∈ M ↔ v ∈ M) {ι : Type} [Finite ι] (wt : Fin n → ι → ℤ) (basisPerm : Equiv.Perm (Fin n)) (basisScale : Fin n → ℤ) (hbasis : ∀ (i : Fin n), θ ↑(b i) = ↑(basisScale i • b (basisPerm i))) : CategoryTheory.CategoryStruct.comp (kostantNumberedSymmetryCoordinateIso M b θ hθM).hom (GeneralLinear.weightTorusCoordinateMap wt) = GeneralLinear.weightTorusCoordinateMap fun (i : Fin n) => wt (basisPerm⁻¹ i)

A monomial-basis numbered symmetry carries the represented weight torus of a weight family to the weight torus of the relabelled family. The scalar coefficients do not affect diagonal conjugation. Stability of a closed subgroup scheme cut out by the root subgroups and a weight torus additionally requires identifying this relabelled family with the original one, via weight equivariance and GeneralLinear.weightTorusCoordinateMap_reindex.