Relabelling the coordinates of a split torus

A permutation τ of the index set of the rank-sigma split torus permutes its coordinates, hence acts on its character lattice sigma →₀ ℤ, on its coordinate Hopf algebra, and on the group scheme itself. This file records that action at all three levels, together with its two structural identities: it is multiplicative in τ and trivial at the identity permutation.

The character-lattice map sends a character χ to χ ∘ τ⁻¹. On points, a character is precomposed with this map, so a coordinate tuple d becomes d ∘ τ. A consumer that has to check a finite-order relation for a relabelling — the graph automorphism of a Chevalley group is the case this file was written for — gets it from the two identities below and the order of τ in Equiv.Perm sigma, with no further computation.

Main declarations

• TauCeti.SplitTorus.characterRelabel: the induced automorphism of the character lattice.
• TauCeti.SplitTorus.characterRelabelHom: the same map, read in FGCommGrpCat.
• TauCeti.SplitTorus.relabelCoordinateMap: the induced automorphism of the coordinate Hopf algebra.
• TauCeti.SplitTorus.relabel: the induced automorphism of the split-torus group scheme.
• TauCeti.SplitTorus.relabelIso: the same automorphism as a bundled isomorphism.
• TauCeti.SplitTorus.schemePointsMulEquiv_relabel: its action on coordinate tuples.

Universes

The character lattice and the coordinate Hopf algebra are relabelled for a base ring in an arbitrary universe. From relabel onwards the base ring and the index set must share a universe: TauCeti.SplitTorus.groupScheme takes (R sigma : Type u), and its scheme-valued points take the value algebra in that same universe, because Mathlib's hopfSpec and Spec.mapMulEquiv are same-universe.

References

• J. S. Milne, Algebraic Groups (2017), §12.

noncomputable def TauCeti.SplitTorus.characterRelabel {sigma : Type u} (τ : Equiv.Perm sigma) : Multiplicative (sigma →₀ ℤ) ≃* Multiplicative (sigma →₀ ℤ)

Relabelling the characters of the rank-sigma split torus along a permutation of sigma. It sends the character χ to χ ∘ τ⁻¹.

Equations

• TauCeti.SplitTorus.characterRelabel τ = AddEquiv.toMultiplicative (Finsupp.domCongr τ)

@[simp]

theorem TauCeti.SplitTorus.characterRelabel_apply {sigma : Type u} (τ : Equiv.Perm sigma) (x : Multiplicative (sigma →₀ ℤ)) : (characterRelabel τ) x = Multiplicative.ofAdd (Finsupp.equivMapDomain τ (Multiplicative.toAdd x))

Relabelling a character reindexes its coordinate function.

theorem TauCeti.SplitTorus.characterRelabel_ofAdd {sigma : Type u} (τ : Equiv.Perm sigma) (f : sigma →₀ ℤ) : (characterRelabel τ) (Multiplicative.ofAdd f) = Multiplicative.ofAdd (Finsupp.equivMapDomain τ f)

Relabelling an additively written character.

@[simp]

theorem TauCeti.SplitTorus.characterRelabel_comp {sigma : Type u} (τ ν : Equiv.Perm sigma) : (↑(characterRelabel τ)).comp ↑(characterRelabel ν) = ↑(characterRelabel (τ * ν))

Relabelling is multiplicative in the permutation.

@[simp]

theorem TauCeti.SplitTorus.characterRelabel_one {sigma : Type u} : ↑(characterRelabel 1) = MonoidHom.id (Multiplicative (sigma →₀ ℤ))

Relabelling by the identity permutation is the identity.

noncomputable def TauCeti.SplitTorus.characterRelabelHom {sigma : Type u} [Finite sigma] (τ : Equiv.Perm sigma) : characterGroup sigma ⟶ characterGroup sigma

The relabelling of the character group, read as a morphism of finitely generated commutative groups.

Equations

• TauCeti.SplitTorus.characterRelabelHom τ = TauCeti.FGCommGrpCat.ofHom ↑(TauCeti.SplitTorus.characterRelabel τ)

@[simp]

theorem TauCeti.SplitTorus.toMonoidHom_characterRelabelHom {sigma : Type u} [Finite sigma] (τ : Equiv.Perm sigma) : FGCommGrpCat.toMonoidHom (characterRelabelHom τ) = ↑(characterRelabel τ)

The underlying monoid homomorphism of characterRelabelHom.

@[simp]

theorem TauCeti.SplitTorus.characterRelabelHom_comp {sigma : Type u} [Finite sigma] (τ ν : Equiv.Perm sigma) : CategoryTheory.CategoryStruct.comp (characterRelabelHom ν) (characterRelabelHom τ) = characterRelabelHom (τ * ν)

Relabelling of character groups is multiplicative in the permutation.

@[simp]

theorem TauCeti.SplitTorus.characterRelabelHom_one {sigma : Type u} [Finite sigma] : characterRelabelHom 1 = CategoryTheory.CategoryStruct.id (characterGroup sigma)

Relabelling of character groups by the identity permutation is the identity.

noncomputable def TauCeti.SplitTorus.relabelCoordinateMap {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] (τ : Equiv.Perm sigma) : (DiagonalizableGroup.coordinateRing R (characterGroup sigma)).obj ⟶ (DiagonalizableGroup.coordinateRing R (characterGroup sigma)).obj

The relabelling automorphism of the coordinate Hopf algebra of the split torus.

Equations

• TauCeti.SplitTorus.relabelCoordinateMap R τ = (TauCeti.DiagonalizableGroup.coordinateMap R (TauCeti.SplitTorus.characterRelabelHom τ)).hom

theorem TauCeti.SplitTorus.hom_relabelCoordinateMap {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] (τ : Equiv.Perm sigma) : CommHopfAlgCat.Hom.hom (relabelCoordinateMap R τ) = MonoidAlgebra.mapDomainBialgHom R ↑(characterRelabel τ)

The bialgebra morphism underlying the coordinate relabelling.

@[simp]

theorem TauCeti.SplitTorus.relabelCoordinateMap_comp {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] (τ ν : Equiv.Perm sigma) : CategoryTheory.CategoryStruct.comp (relabelCoordinateMap R τ) (relabelCoordinateMap R ν) = relabelCoordinateMap R (ν * τ)

Coordinate relabelling is multiplicative in the permutation.

@[simp]

theorem TauCeti.SplitTorus.relabelCoordinateMap_one {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] : relabelCoordinateMap R 1 = CategoryTheory.CategoryStruct.id (DiagonalizableGroup.coordinateRing R (characterGroup sigma)).obj

Coordinate relabelling by the identity permutation is the identity.

instance TauCeti.SplitTorus.isIso_relabelCoordinateMap {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] (τ : Equiv.Perm sigma) : CategoryTheory.IsIso (relabelCoordinateMap R τ)

theorem TauCeti.SplitTorus.relabelCoordinateMap_injective {sigma : Type u} [Finite sigma] (R : Type v) [CommRing R] (τ : Equiv.Perm sigma) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (relabelCoordinateMap R τ))

Coordinate relabelling is injective, as the underlying map of an isomorphism.

noncomputable def TauCeti.SplitTorus.relabel {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : groupScheme R sigma ⟶ groupScheme R sigma

The relabelling automorphism of the split-torus group scheme. On points a character is precomposed with characterRelabel τ, so the coordinate tuple d becomes d ∘ τ.

Equations

• TauCeti.SplitTorus.relabel R τ = TauCeti.DiagonalizableGroup.groupSchemeMap R (TauCeti.SplitTorus.characterRelabelHom τ)

@[simp]

theorem TauCeti.SplitTorus.relabel_comp {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ ν : Equiv.Perm sigma) : CategoryTheory.CategoryStruct.comp (relabel R τ) (relabel R ν) = relabel R (τ * ν)

Relabelling of group schemes is multiplicative in the permutation.

@[simp]

theorem TauCeti.SplitTorus.relabel_one {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] : relabel R 1 = CategoryTheory.CategoryStruct.id (groupScheme R sigma)

Relabelling by the identity permutation is the identity.

instance TauCeti.SplitTorus.isIso_relabel {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : CategoryTheory.IsIso (relabel R τ)

noncomputable def TauCeti.SplitTorus.relabelIso {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : CategoryTheory.Aut (groupScheme R sigma)

The relabelling automorphism of the split torus, bundled as an isomorphism.

Equations

• TauCeti.SplitTorus.relabelIso R τ = CategoryTheory.asIso (TauCeti.SplitTorus.relabel R τ)

@[simp]

theorem TauCeti.SplitTorus.relabelIso_hom {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : (relabelIso R τ).hom = relabel R τ

@[simp]

theorem TauCeti.SplitTorus.relabelIso_inv {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : (relabelIso R τ).inv = relabel R τ⁻¹

The inverse of the bundled relabelling is relabelling by the inverse permutation.

@[simp]

theorem TauCeti.SplitTorus.relabelIso_mul {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ ν : Equiv.Perm sigma) : relabelIso R (τ * ν) = relabelIso R ν * relabelIso R τ

Bundled relabelling is multiplicative, with the order reversed by categorical composition.

@[simp]

theorem TauCeti.SplitTorus.relabelIso_one {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] : relabelIso R 1 = 1

Bundled relabelling by the identity permutation is the identity automorphism.

@[simp]

theorem TauCeti.SplitTorus.relabelIso_pow_hom {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) (m : ℕ) : (relabelIso R τ ^ m).hom = relabel R (τ ^ m)

The forward morphism of a power of a relabelling is relabelling by the corresponding permutation power.

@[simp]

theorem TauCeti.SplitTorus.schemePointsMulEquiv_relabel {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] {A : Type u} [CommRing A] [Algebra R A] (τ : Equiv.Perm sigma) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R sigma).X) (i : sigma) : schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (relabel R τ).hom.hom) i = schemePointsMulEquiv p (τ i)

On scheme-valued points, relabelling sends a coordinate tuple d to d ∘ τ.

theorem TauCeti.SplitTorus.relabel_def {sigma : Type u} [Finite sigma] (R : Type u) [CommRing R] (τ : Equiv.Perm sigma) : relabel R τ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.hopfSpec (CommRingCat.of R)).map (relabelCoordinateMap R τ).op) (CategoryTheory.eqToHom ⋯))

The group-scheme relabelling is the spectrum of the coordinate relabelling, read across the canonical presentation of the split torus.