Linear maps of split-torus character lattices

An integral linear map between finite coordinate character lattices induces, contravariantly, a morphism of the corresponding split tori. On scheme-valued points this morphism is the Laurent monomial map prescribed by the images of the standard basis characters.

Main definitions

• TauCeti.SplitTorus.characterMapOfLinearMap: the homomorphism of character groups induced by an integral linear map between coordinate lattices.
• TauCeti.SplitTorus.ofLinearMap: the resulting contravariant morphism of split tori.
• TauCeti.SplitTorus.powEnd: the coordinatewise integer power endomorphism of a split torus.

Main results

• TauCeti.SplitTorus.schemePointsMulEquiv_ofLinearMap: the induced map on points is the Laurent monomial specified by the image of a basis character.
• TauCeti.SplitTorus.schemePointsMulEquiv_powEnd: powEnd n raises every coordinate to n.

noncomputable def TauCeti.SplitTorus.characterMapOfLinearMap {sigma tau : Type u} [Finite sigma] [Finite tau] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : Multiplicative (sigma →₀ ℤ) →* Multiplicative (tau →₀ ℤ)

Convert an integral linear map between finite coordinate lattices into the corresponding homomorphism of free multiplicative character groups.

Equations

• TauCeti.SplitTorus.characterMapOfLinearMap f = AddMonoidHom.toMultiplicative (↑(Finsupp.linearEquivFunOnFinite ℤ ℤ tau).symm ∘ₗ f ∘ₗ ↑(Finsupp.linearEquivFunOnFinite ℤ ℤ sigma)).toAddMonoidHom

@[simp]

theorem TauCeti.SplitTorus.characterMapOfLinearMap_ofAdd {sigma tau : Type u} [Finite sigma] [Finite tau] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) (x : sigma →₀ ℤ) : (characterMapOfLinearMap f) (Multiplicative.ofAdd x) = Multiplicative.ofAdd ((Finsupp.linearEquivFunOnFinite ℤ ℤ tau).symm (f ((Finsupp.linearEquivFunOnFinite ℤ ℤ sigma) x)))

The additive representative of characterMapOfLinearMap f is obtained by transporting f across the finite-support/function equivalence.

@[simp]

theorem TauCeti.SplitTorus.characterMapOfLinearMap_comp {sigma tau upsilon : Type u} [Finite sigma] [Finite tau] [Finite upsilon] (g : (tau → ℤ) →ₗ[ℤ] upsilon → ℤ) (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : (characterMapOfLinearMap g).comp (characterMapOfLinearMap f) = characterMapOfLinearMap (g ∘ₗ f)

The character-group map associated to a composite integral linear map is the composite of the character-group maps.

@[simp]

theorem TauCeti.SplitTorus.characterMapOfLinearMap_id {sigma : Type u} [Finite sigma] : characterMapOfLinearMap LinearMap.id = MonoidHom.id (Multiplicative (sigma →₀ ℤ))

The identity linear map induces the identity character-group map.

noncomputable def TauCeti.SplitTorus.characterGroupMapOfLinearMap {sigma tau : Type u} [Finite sigma] [Finite tau] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : characterGroup sigma ⟶ characterGroup tau

The character-group morphism associated to an integral linear map between finite coordinate lattices.

Equations

• TauCeti.SplitTorus.characterGroupMapOfLinearMap f = TauCeti.FGCommGrpCat.ofHom (TauCeti.SplitTorus.characterMapOfLinearMap f)

@[simp]

theorem TauCeti.SplitTorus.toMonoidHom_characterGroupMapOfLinearMap {sigma tau : Type u} [Finite sigma] [Finite tau] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : FGCommGrpCat.toMonoidHom (characterGroupMapOfLinearMap f) = characterMapOfLinearMap f

The underlying monoid homomorphism of characterGroupMapOfLinearMap.

@[simp]

theorem TauCeti.SplitTorus.characterGroupMapOfLinearMap_comp {sigma tau upsilon : Type u} [Finite sigma] [Finite tau] [Finite upsilon] (g : (tau → ℤ) →ₗ[ℤ] upsilon → ℤ) (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : CategoryTheory.CategoryStruct.comp (characterGroupMapOfLinearMap f) (characterGroupMapOfLinearMap g) = characterGroupMapOfLinearMap (g ∘ₗ f)

Composition of linear maps becomes composition of the associated character-group morphisms.

@[simp]

theorem TauCeti.SplitTorus.characterGroupMapOfLinearMap_id {sigma : Type u} [Finite sigma] : characterGroupMapOfLinearMap LinearMap.id = CategoryTheory.CategoryStruct.id (characterGroup sigma)

The identity linear map induces the identity character-group morphism.

noncomputable def TauCeti.SplitTorus.ofLinearMap {sigma tau : Type u} [Finite sigma] [Finite tau] (R : Type u) [CommRing R] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : groupScheme R tau ⟶ groupScheme R sigma

The contravariant split-torus morphism induced by an integral map of coordinate character lattices. If f : X^*(T_sigma) → X^*(T_tau), then ofLinearMap R f is the corresponding morphism T_tau → T_sigma.

Equations

• TauCeti.SplitTorus.ofLinearMap R f = TauCeti.DiagonalizableGroup.groupSchemeMap R (TauCeti.SplitTorus.characterGroupMapOfLinearMap f)

@[simp]

theorem TauCeti.SplitTorus.ofLinearMap_comp {R sigma tau upsilon : Type u} [CommRing R] [Finite sigma] [Finite tau] [Finite upsilon] (g : (tau → ℤ) →ₗ[ℤ] upsilon → ℤ) (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) : CategoryTheory.CategoryStruct.comp (ofLinearMap R g) (ofLinearMap R f) = ofLinearMap R (g ∘ₗ f)

Contravariance reverses composition of integral character-lattice maps.

@[simp]

theorem TauCeti.SplitTorus.ofLinearMap_id {R sigma : Type u} [CommRing R] [Finite sigma] : ofLinearMap R LinearMap.id = CategoryTheory.CategoryStruct.id (groupScheme R sigma)

The identity character-lattice map induces the identity split-torus morphism.

@[simp]

theorem TauCeti.SplitTorus.schemePointsMulEquiv_ofLinearMap {R A sigma tau : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] [Finite tau] (f : (sigma → ℤ) →ₗ[ℤ] tau → ℤ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R tau).X) (i : sigma) : schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (ofLinearMap R f).hom.hom) i = ((Finsupp.linearEquivFunOnFinite ℤ ℤ tau).symm (f ((Finsupp.linearEquivFunOnFinite ℤ ℤ sigma) (Finsupp.single i 1)))).prod fun (j : tau) (n : ℤ) => schemePointsMulEquiv p j ^ n

On scheme-valued points, ofLinearMap R f is the Laurent monomial map prescribed by the images under f of the standard basis characters.

noncomputable def TauCeti.SplitTorus.powEnd (R : Type u) [CommRing R] (sigma : Type u) [Finite sigma] (n : ℤ) : groupScheme R sigma ⟶ groupScheme R sigma

The coordinatewise n-th power endomorphism of a split torus.

Equations

• TauCeti.SplitTorus.powEnd R sigma n = TauCeti.SplitTorus.ofLinearMap R (n • LinearMap.id)

theorem TauCeti.SplitTorus.powEnd_def {R sigma : Type u} [CommRing R] [Finite sigma] (n : ℤ) : powEnd R sigma n = ofLinearMap R (n • LinearMap.id)

The character-lattice map defining the coordinatewise power endomorphism.

@[simp]

theorem TauCeti.SplitTorus.powEnd_comp {R sigma : Type u} [CommRing R] [Finite sigma] (m n : ℤ) : CategoryTheory.CategoryStruct.comp (powEnd R sigma m) (powEnd R sigma n) = powEnd R sigma (m * n)

Power endomorphisms multiply their exponents under composition.

@[simp]

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

The first power endomorphism is the identity split-torus morphism.

@[simp]

theorem TauCeti.SplitTorus.schemePointsMulEquiv_powEnd {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (n : ℤ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) (i : sigma) : schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (powEnd R sigma n).hom.hom) i = schemePointsMulEquiv p i ^ n

On scheme-valued points, powEnd n raises every coordinate to the integer power n.