Documentation

TauCeti.Algebra.AlgebraicGroup.SplitTorus.Scheme

The finite-rank split torus as a group scheme #

For a finite index type sigma, the split torus with character lattice sigma →₀ ℤ is the diagonalizable group scheme D(Multiplicative (sigma →₀ ℤ)). This file synchronizes that scheme presentation with the existing functor-of-points and character--cocharacter APIs:

The scheme-valued point comparison uses the same-universe diagonalizable-group bridge from DiagonalizableGroup.Scheme.Points; this is why both the base ring and finite index type live in the same universe. Ordinary character and cocharacter exponents remain in ℤ.

This advances Layer 4 of the reductive-groups roadmap (TauCetiRoadmap/ReductiveGroups/README.md): the finite-rank split torus, its character and cocharacter lattices, and their perfect pairing now have a synchronized group-scheme realization.

Main declarations #

References #

Milne, Algebraic Groups, Definition 12.7 and Theorems 12.8--12.9, describes split tori through diagonalizable groups. The coordinate computations reuse Tau Ceti's freeAbelianCharEquiv, SplitTorus.cocharEquiv, and SplitTorus.latticePairing.

source
@[reducible, inline]
noncomputable abbrev TauCeti.SplitTorus.groupScheme (R sigma : Type u) [CommRing R] [Finite sigma] :
CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The finite-rank split torus with character lattice sigma →₀ ℤ, as a group scheme over Spec R.

Equations
Instances For
    source
    noncomputable def TauCeti.SplitTorus.schemePointsMulEquiv {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] :
    ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) ≃* (sigma → Aˣ)

    Scheme-valued points of the finite-rank split torus are coordinate families of units.

    Equations
    Instances For
      source
      theorem TauCeti.SplitTorus.schemePointsMulEquiv_eq_freeAbelianCharEquiv {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) :
      schemePointsMulEquiv p = freeAbelianCharEquiv ((DiagonalizableGroup.schemePointsMulEquiv (characterGroup sigma)) p)

      The split-torus scheme-points equivalence is the free-abelian character equivalence applied to the underlying diagonalizable-group character.

      source
      @[simp]
      theorem TauCeti.SplitTorus.schemePointsMulEquiv_apply_coe {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) (i : sigma) :
      ↑(schemePointsMulEquiv p i) = ((DiagonalizableGroup.groupSchemePointsMulEquiv (characterGroup sigma)) p).ofConv (MonoidAlgebra.single (Multiplicative.ofAdd (Finsupp.single i 1)) 1)

      The i-th coordinate of a scheme-valued point is its value on the group-algebra monomial for the i-th standard character.

      source
      theorem TauCeti.SplitTorus.schemePointsMulEquiv_symm_apply {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (c : sigma → Aˣ) :
      schemePointsMulEquiv.symm c = (DiagonalizableGroup.groupSchemePointsMulEquiv (characterGroup sigma)).symm (pointsMulEquiv.symm c)

      The inverse coordinate equivalence is the spectrum morphism extending the free-abelian character determined by the coordinate family.

      source
      theorem TauCeti.SplitTorus.schemePointsMulEquiv_mapValue {R A B sigma : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Finite sigma] (phi : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) :
      schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom phi.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = fun (i : sigma) => (Units.map ↑phi.toRingHom) (schemePointsMulEquiv p i)

      The split-torus scheme-points equivalence is natural in the value algebra.

      Characters and cocharacters as group-scheme morphisms #

      source
      noncomputable def TauCeti.SplitTorus.characterGroupSchemeMap {R sigma : Type u} [CommRing R] [Finite sigma] (m : sigma →₀ ℤ) :
      groupScheme R sigma ⟶ DiagonalizableGroup.multiplicativeGroupScheme R

      A character in the split torus character lattice gives a group-scheme morphism to the multiplicative group scheme.

      Equations
      Instances For
        source
        theorem TauCeti.SplitTorus.characterGroupSchemeMap_def {R sigma : Type u} [CommRing R] [Finite sigma] (m : sigma →₀ ℤ) :
        characterGroupSchemeMap m = DiagonalizableGroup.characterGroupSchemeMap (characterGroup sigma) (Multiplicative.ofAdd m)

        A split-torus scheme-level character is the diagonalizable-group character associated to its multiplicative character-lattice element.

        source
        @[simp]
        theorem TauCeti.SplitTorus.multiplicativeGroupSchemePointsMulEquiv_characterGroupSchemeMap {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (m : sigma →₀ ℤ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R sigma).X) :
        DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (characterGroupSchemeMap m).hom.hom) = m.prod fun (i : sigma) (n : ℤ) => schemePointsMulEquiv p i ^ n

        On scheme-valued points, a split-torus character is the Laurent monomial with exponent vector m.

        source
        noncomputable def TauCeti.SplitTorus.cocharacterGroupSchemeMap {R sigma : Type u} [CommRing R] [Finite sigma] (psi : Multiplicative (sigma →₀ ℤ) →* Multiplicative ℤ) :
        DiagonalizableGroup.multiplicativeGroupScheme R ⟶ groupScheme R sigma

        A split-torus cocharacter gives a group-scheme morphism from the multiplicative group scheme.

        Equations
        Instances For
          source
          theorem TauCeti.SplitTorus.cocharacterGroupSchemeMap_def {R sigma : Type u} [CommRing R] [Finite sigma] (psi : Multiplicative (sigma →₀ ℤ) →* Multiplicative ℤ) :
          cocharacterGroupSchemeMap psi = DiagonalizableGroup.cocharacterGroupSchemeMap (characterGroup sigma) psi

          A split-torus scheme-level cocharacter is the corresponding diagonalizable-group cocharacter of its multiplicative character lattice.

          source
          @[simp]
          theorem TauCeti.SplitTorus.schemePointsMulEquiv_cocharacterGroupSchemeMap {R A sigma : Type u} [CommRing R] [CommRing A] [Algebra R A] [Finite sigma] (psi : Multiplicative (sigma →₀ ℤ) →* Multiplicative ℤ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (DiagonalizableGroup.multiplicativeGroupScheme R).X) (i : sigma) :
          schemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (cocharacterGroupSchemeMap psi).hom.hom) i = DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv p ^ cocharEquiv psi i

          On scheme-valued points, a split-torus cocharacter raises the input unit to the integer specified by each cocharacter coordinate.

          source
          theorem TauCeti.SplitTorus.cocharacterGroupSchemeMap_comp_characterGroupSchemeMap {R sigma : Type u} [CommRing R] [Finite sigma] (m : sigma →₀ ℤ) (psi : Multiplicative (sigma →₀ ℤ) →* Multiplicative ℤ) :
          CategoryTheory.CategoryStruct.comp (cocharacterGroupSchemeMap psi) (characterGroupSchemeMap m) = DiagonalizableGroup.powEndGroupSchemeMap ((latticePairing m) (Additive.ofMul psi))

          Composing a split-torus cocharacter with a character is the power map whose exponent is their perfect lattice pairing.