Scheme-valued points and morphisms of diagonalizable group schemes

For a commutative ring R and a finitely generated commutative group G, the diagonalizable group scheme D(G) is represented by the group algebra R[G]. This file synchronizes its group-scheme and functor-of-points presentations. A scheme-valued point Spec A ⟶ D(G) over Spec R is identified multiplicatively with a character G →* Aˣ. Under this identification, the group-scheme morphism induced contravariantly by G ⟶ H acts by precomposition on characters, and the equivalence is natural in A.

The same bridge realizes characters, cocharacters, and integer power maps as actual group-scheme morphisms. Their composite is the power map whose exponent is the established character--cocharacter pairing. No classification of arbitrary group-scheme morphisms is asserted; such a classification requires additional hypotheses on the base.

The scheme-facing constructions are same-universe because Mathlib's current hopfSpec and Spec.mapMulEquiv interfaces are same-universe. Consequently the character group used for 𝔾ₘ over R : Type u is the canonical same-universe copy ULift.{u} (Multiplicative ℤ). The local character equivalence combines Mathlib's zpowersMulHom with MulEquiv.ulift; public exponents and cocharacters remain expressed using ordinary integers.

Main declarations

• TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv: the typed comparison between scheme-valued points of D(G) and algebra points of R[G].
• TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_symm_apply_left: the underlying spectrum map of the inverse comparison.
• TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_mapValue and TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_groupSchemeMap: its naturality in the value algebra and the character group.
• TauCeti.DiagonalizableGroup.schemePointsMulEquiv: scheme-valued points of D(G) are characters G →* Aˣ.
• TauCeti.DiagonalizableGroup.schemePointsMulEquiv_eq_pointsMulEquiv_groupSchemePointsMulEquiv: this character comparison factors through the convolution-point comparison.
• TauCeti.DiagonalizableGroup.schemePointsMulEquiv_mapValue: this identification is natural in the value algebra.
• TauCeti.DiagonalizableGroup.schemePointsMulEquiv_groupSchemeMap: a diagonalizable group-scheme morphism acts on points by precomposition on characters.
• TauCeti.DiagonalizableGroup.multiplicativeGroupScheme: the same-universe presentation of 𝔾ₘ.
• TauCeti.DiagonalizableGroup.characterGroupSchemeMap and TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap: scheme-level characters and cocharacters.
• TauCeti.DiagonalizableGroup.powEndGroupSchemeMap: the scheme-level integer power map of 𝔾ₘ.
• TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap_comp_characterGroupSchemeMap: the character--cocharacter pairing as an equality of group-scheme morphisms.

References

Milne, Algebraic Groups, Definition 12.7 and Theorems 12.8--12.9, describes the contravariant diagonalizable-group construction. The scheme-points bridge combines Mathlib's AlgebraicGeometry.Spec.mapMulEquiv with Tau Ceti's DiagonalizableGroup.pointsMulEquiv, CommHopfAlgCat.mapMulEquiv_mapValue, and CommHopfAlgCat.mapMulEquiv_mapDomain.

noncomputable def TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) : ((AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) ≃* WithConv (MonoidAlgebra R ↑G →ₐ[R] A)

Scheme-valued points of D(G) are the convolution group of algebra maps out of its coordinate ring. This typed wrapper keeps the defining identification of groupScheme with Spec R[G] local to this module.

Equations

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

theorem TauCeti.DiagonalizableGroup.eqToHom_hom_hom_left {R : Type u} [CommRing R] {G₁ G₂ : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of R)))} (h : G₁ = G₂) : CategoryTheory.Over.Hom.left (CategoryTheory.eqToHom h).hom.hom = CategoryTheory.eqToHom ⋯

The underlying scheme morphism of an equality transport between group objects over Spec R is the equality transport between their underlying schemes.

theorem TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_apply_left_comp {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left p) (CategoryTheory.eqToHom ⋯) = CategoryTheory.Over.Hom.left (AlgebraicGeometry.Spec.mapMulEquiv ((groupSchemePointsMulEquiv G) p))

The underlying map of a scheme point under the typed comparison.

theorem TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_symm_apply_left {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (f : WithConv (MonoidAlgebra R ↑G →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((groupSchemePointsMulEquiv G).symm f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.ofConv.toRingHom)) (CategoryTheory.eqToHom ⋯)

The inverse typed point comparison is the spectrum morphism induced by the algebra point, transported to the named diagonalizable group scheme.

theorem TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_mapValue {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (G : FGCommGrpCat) (phi : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) : (groupSchemePointsMulEquiv G) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom phi.toRingHom)) (AlgebraicGeometry.Spec (CommRingCat.of R))) p) = (AlgHom.mapValue phi) ((groupSchemePointsMulEquiv G) p)

The typed scheme-point comparison is natural in the value algebra.

theorem TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv_groupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {G H : FGCommGrpCat} (f : G ⟶ H) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R H).X) : (groupSchemePointsMulEquiv G) (CategoryTheory.CategoryStruct.comp p (groupSchemeMap R f).hom.hom) = (pointsMap (FGCommGrpCat.toMonoidHom f)) ((groupSchemePointsMulEquiv H) p)

The typed scheme-point comparison sends postcomposition by groupSchemeMap f to the existing contravariant algebra-point map induced by the underlying homomorphism f.

noncomputable def TauCeti.DiagonalizableGroup.schemePointsMulEquiv {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) : ((AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) ≃* (↑G →* Aˣ)

Scheme-valued points of D(G) over Spec R are multiplicative characters G →* Aˣ.

The equivalence reverses the spectrum morphism into an algebra point through groupSchemePointsMulEquiv, then applies the diagonalizable-group points equivalence.

Equations

• TauCeti.DiagonalizableGroup.schemePointsMulEquiv G = (TauCeti.DiagonalizableGroup.groupSchemePointsMulEquiv G).trans TauCeti.DiagonalizableGroup.pointsMulEquiv

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_eq_pointsMulEquiv_groupSchemePointsMulEquiv {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) : (schemePointsMulEquiv G) p = pointsMulEquiv ((groupSchemePointsMulEquiv G) p)

The diagonalizable-group scheme-points character is obtained by first passing to its convolution point and then applying the algebra-valued points equivalence.

@[simp]

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_apply_coe {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) (g : ↑G) : ↑(((schemePointsMulEquiv G) p) g) = ((groupSchemePointsMulEquiv G) p).ofConv (MonoidAlgebra.single g 1)

A scheme-valued point, viewed as a character, evaluates a group element on the corresponding group-algebra basis monomial.

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_symm_apply {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (chi : ↑G →* Aˣ) : (schemePointsMulEquiv G).symm chi = (groupSchemePointsMulEquiv G).symm (pointsMulEquiv.symm chi)

The inverse scheme-points equivalence is the spectrum morphism associated to the algebra point extending a character.

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_groupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {G H : FGCommGrpCat} (f : G ⟶ H) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R H).X) : (schemePointsMulEquiv G) (CategoryTheory.CategoryStruct.comp p (groupSchemeMap R f).hom.hom) = ((schemePointsMulEquiv H) p).comp (FGCommGrpCat.toMonoidHom f)

The scheme-points equivalence intertwines groupSchemeMap f with precomposition by the underlying homomorphism f on characters.

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_mapValue {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (G : FGCommGrpCat) (phi : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) : (schemePointsMulEquiv G) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom phi.toRingHom)) (AlgebraicGeometry.Spec (CommRingCat.of R))) p) = (Units.map ↑phi.toRingHom).comp ((schemePointsMulEquiv G) p)

The scheme-points equivalence is natural in the value algebra. For phi : A →ₐ[R] B, precomposing by Spec B ⟶ Spec A applies phi to the values of the corresponding character.

The multiplicative group and scheme-level characters

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.multiplicativeCharacterGroup : FGCommGrpCat

The character group of the multiplicative group scheme, in the universe of the base. It is the canonical universe lift of Multiplicative ℤ.

Equations

• TauCeti.DiagonalizableGroup.multiplicativeCharacterGroup = TauCeti.FGCommGrpCat.of (ULift.{?u.1, 0} (Multiplicative ℤ))

@[reducible, inline]

noncomputable abbrev TauCeti.DiagonalizableGroup.multiplicativeGroupScheme (R : Type u) [CommRing R] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of R)))

The multiplicative group scheme, presented in the base universe as D(ULift (Multiplicative ℤ)).

Equations

• TauCeti.DiagonalizableGroup.multiplicativeGroupScheme R = TauCeti.DiagonalizableGroup.groupScheme R TauCeti.DiagonalizableGroup.multiplicativeCharacterGroup

noncomputable def TauCeti.DiagonalizableGroup.uliftZPowersMulEquiv (M : Type u) [CommGroup M] : M ≃* (ULift.{u, 0} (Multiplicative ℤ) →* M)

Evaluation at the lifted standard generator identifies characters of ULift (Multiplicative ℤ) with elements of a commutative group.

Equations

• TauCeti.DiagonalizableGroup.uliftZPowersMulEquiv M = (zpowersMulHom M).trans MulEquiv.ulift.symm.monoidHomCongrLeft

@[simp]

theorem TauCeti.DiagonalizableGroup.uliftZPowersMulEquiv_apply (M : Type u) [CommGroup M] (m : M) (n : Multiplicative ℤ) : ((uliftZPowersMulEquiv M) m) { down := n } = m ^ Multiplicative.toAdd n

The character corresponding to m evaluates on a lifted integer n as m ^ n.

@[simp]

theorem TauCeti.DiagonalizableGroup.uliftZPowersMulEquiv_symm_apply (M : Type u) [CommGroup M] (f : ULift.{u, 0} (Multiplicative ℤ) →* M) : (uliftZPowersMulEquiv M).symm f = f { down := Multiplicative.ofAdd 1 }

The inverse equivalence evaluates a lifted-integer character at the standard generator.

noncomputable def TauCeti.DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : ((AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) ≃* Aˣ

Scheme-valued points of the multiplicative group scheme are units of the value algebra, read off on the lifted standard generator.

Equations

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

@[simp]

theorem TauCeti.DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv_apply {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) : multiplicativeGroupSchemePointsMulEquiv p = ((schemePointsMulEquiv multiplicativeCharacterGroup) p) { down := Multiplicative.ofAdd 1 }

The scheme-points equivalence for 𝔾ₘ evaluates the corresponding character on the lifted generator Multiplicative.ofAdd 1.

theorem TauCeti.DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv_mapValue {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (phi : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) : multiplicativeGroupSchemePointsMulEquiv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom phi.toRingHom)) (AlgebraicGeometry.Spec (CommRingCat.of R))) p) = (Units.map ↑phi.toRingHom) (multiplicativeGroupSchemePointsMulEquiv p)

The multiplicative-group scheme-points equivalence is natural in the value algebra.

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_multiplicativeCharacterGroup_apply {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) (n : Multiplicative ℤ) : ((schemePointsMulEquiv multiplicativeCharacterGroup) p) { down := n } = multiplicativeGroupSchemePointsMulEquiv p ^ Multiplicative.toAdd n

A character of the lifted integer group evaluates at ULift.up n as the corresponding unit raised to the ordinary integer exponent n.toAdd.

Scheme-level characters, cocharacters, and power maps

noncomputable def TauCeti.DiagonalizableGroup.characterGroupSchemeMap {R : Type u} [CommRing R] (G : FGCommGrpCat) (g : ↑G) : groupScheme R G ⟶ multiplicativeGroupScheme R

A group element g : G, viewed as a character of D(G), gives the group-scheme morphism D(G) ⟶ 𝔾ₘ induced contravariantly by the homomorphism from the lifted integer group that sends its standard generator to g.

Equations

• TauCeti.DiagonalizableGroup.characterGroupSchemeMap G g = TauCeti.DiagonalizableGroup.groupSchemeMap R (TauCeti.FGCommGrpCat.ofHom ((TauCeti.DiagonalizableGroup.uliftZPowersMulEquiv ↑G) g))

theorem TauCeti.DiagonalizableGroup.characterGroupSchemeMap_def {R : Type u} [CommRing R] (G : FGCommGrpCat) (g : ↑G) : characterGroupSchemeMap G g = groupSchemeMap R (FGCommGrpCat.ofHom ((uliftZPowersMulEquiv ↑G) g))

A scheme-level character is the contravariant diagonalizable-group morphism induced by the corresponding homomorphism from the lifted integer group.

@[simp]

theorem TauCeti.DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv_characterGroupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (g : ↑G) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (groupScheme R G).X) : multiplicativeGroupSchemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (characterGroupSchemeMap G g).hom.hom) = ((schemePointsMulEquiv G) p) g

On scheme-valued points, the group-scheme character associated to g evaluates the corresponding G-character at g.

noncomputable def TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap {R : Type u} [CommRing R] (G : FGCommGrpCat) (psi : ↑G →* Multiplicative ℤ) : multiplicativeGroupScheme R ⟶ groupScheme R G

A cocharacter psi : G →* Multiplicative ℤ gives a group-scheme morphism 𝔾ₘ ⟶ D(G). The target character lattice is universe-lifted only at this scheme boundary.

Equations

• TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap G psi = TauCeti.DiagonalizableGroup.groupSchemeMap R (TauCeti.FGCommGrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp psi))

theorem TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap_def {R : Type u} [CommRing R] (G : FGCommGrpCat) (psi : ↑G →* Multiplicative ℤ) : cocharacterGroupSchemeMap G psi = groupSchemeMap R (FGCommGrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp psi))

A scheme-level cocharacter is the contravariant diagonalizable-group morphism induced by the universe-lifted cocharacter lattice homomorphism.

@[simp]

theorem TauCeti.DiagonalizableGroup.schemePointsMulEquiv_cocharacterGroupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (G : FGCommGrpCat) (psi : ↑G →* Multiplicative ℤ) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) (g : ↑G) : ((schemePointsMulEquiv G) (CategoryTheory.CategoryStruct.comp p (cocharacterGroupSchemeMap G psi).hom.hom)) g = multiplicativeGroupSchemePointsMulEquiv p ^ Multiplicative.toAdd (psi g)

On scheme-valued points, a cocharacter raises the multiplicative-group unit to the ordinary integer obtained by evaluating the cocharacter.

noncomputable def TauCeti.DiagonalizableGroup.powEndGroupSchemeMap {R : Type u} [CommRing R] (n : ℤ) : multiplicativeGroupScheme R ⟶ multiplicativeGroupScheme R

The n-th power endomorphism of the multiplicative group scheme. Its character-lattice map sends the lifted standard generator to the lift of Multiplicative.ofAdd n.

Equations

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

theorem TauCeti.DiagonalizableGroup.powEndGroupSchemeMap_def {R : Type u} [CommRing R] (n : ℤ) : powEndGroupSchemeMap n = characterGroupSchemeMap multiplicativeCharacterGroup { down := Multiplicative.ofAdd n }

The scheme-level power endomorphism is the character associated to the lifted integer exponent.

@[simp]

theorem TauCeti.DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv_powEndGroupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℤ) (p : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶ (multiplicativeGroupScheme R).X) : multiplicativeGroupSchemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (powEndGroupSchemeMap n).hom.hom) = multiplicativeGroupSchemePointsMulEquiv p ^ n

The scheme-level n-th power endomorphism raises every scheme-valued point to the ordinary integer power n.

theorem TauCeti.DiagonalizableGroup.cocharacterGroupSchemeMap_comp_characterGroupSchemeMap {R : Type u} [CommRing R] (G : FGCommGrpCat) (g : ↑G) (psi : ↑G →* Multiplicative ℤ) : CategoryTheory.CategoryStruct.comp (cocharacterGroupSchemeMap G psi) (characterGroupSchemeMap G g) = powEndGroupSchemeMap (pairing g psi)

Composing a cocharacter with a character is the multiplicative-group power map whose exponent is their established character--cocharacter pairing.