Functoriality of the diagonalizable group in the abelian group

TauCeti.Algebra.AlgebraicGroup.DiagonalizableGroup.Basic computes the functor of points of the diagonalizable group D(G) = Spec R[G]: for every commutative R-algebra A, the convolution group of R-algebra maps R[G] →ₐ[R] A is the character group G →* Aˣ. This file records the remaining variance, making D into a contravariant functor on commutative groups: a group homomorphism φ : G →* G' induces a homomorphism of group functors D(φ) : D(G') → D(G), and under the character identification this is just precomposition χ ↦ χ ∘ φ of characters.

Concretely φ induces, by MonoidAlgebra.mapDomainBialgHom, the bialgebra map R[G] →ₐc[R] R[G'], which TauCeti.AlgHom.mapDomain turns into a monoid homomorphism WithConv (R[G'] →ₐ[R] A) →* WithConv (R[G] →ₐ[R] A) of convolution groups. The headline calculation pointsMulEquiv_pointsMap says this monoid homomorphism is intertwined by pointsMulEquiv with precomposition by φ on character groups, so the contravariant functor G ↦ D(G) agrees on points with the contravariant functor G ↦ (G →* Aˣ). This is the on-points half of the roadmap's anti-equivalence M ↦ D(M).

This advances the reductive-groups roadmap (Layer 4, "diagonalizable groups and groups of multiplicative type: the anti-equivalence M ↦ D(M)"), building on the diagonalizable-group worked example and the coordinate-Hopf-algebra functoriality AlgHom.mapDomain.

Main declarations

• TauCeti.DiagonalizableGroup.pointsMap: the homomorphism of convolution groups of points induced by a group homomorphism φ : G →* G', contravariantly.
• TauCeti.DiagonalizableGroup.pointsMap_id, TauCeti.DiagonalizableGroup.pointsMap_comp: the contravariant functoriality of pointsMap.
• TauCeti.DiagonalizableGroup.mapValue_pointsMap: pointsMap is natural in the value algebra, commuting with AlgHom.mapValue.
• TauCeti.DiagonalizableGroup.charOfPoint_comp: reading off the character of a precomposed point is precomposition of the character by φ.
• TauCeti.DiagonalizableGroup.pointsMulEquiv_pointsMap: the points homomorphism is intertwined by pointsMulEquiv with precomposition of characters by φ.

References

The group-algebra bialgebra functoriality MonoidAlgebra.mapDomainBialgHom is Mathlib's (Mathlib.RingTheory.Bialgebra.MonoidAlgebra). The convolution-group functoriality in the coordinate Hopf algebra is Tau Ceti's TauCeti.AlgHom.mapDomain (TauCeti.Algebra.AlgebraicGroup.Hopf.Map). This realizes the diagonalizable-group functoriality of the Tau Ceti reductive-groups roadmap (Layer 4).

noncomputable def TauCeti.DiagonalizableGroup.pointsMap {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') : WithConv (MonoidAlgebra R G' →ₐ[R] A) →* WithConv (MonoidAlgebra R G →ₐ[R] A)

The diagonalizable group is contravariant in the abelian group. A group homomorphism φ : G →* G' induces, by pre-composition with the bialgebra map R[G] →ₐc[R] R[G'], a homomorphism of convolution groups of points D(G')(A) → D(G)(A).

Equations

• TauCeti.DiagonalizableGroup.pointsMap φ = TauCeti.AlgHom.mapDomain (MonoidAlgebra.mapDomainBialgHom R φ)

@[simp]

theorem TauCeti.DiagonalizableGroup.pointsMap_apply {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') (f : WithConv (MonoidAlgebra R G' →ₐ[R] A)) : (pointsMap φ) f = WithConv.toConv (f.ofConv.comp ↑(MonoidAlgebra.mapDomainBialgHom R φ))

pointsMap φ acts by pre-composition with the induced bialgebra map.

@[simp]

theorem TauCeti.DiagonalizableGroup.pointsMap_id {R : Type u} {A : Type v} {G : Type w} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] : pointsMap (MonoidHom.id G) = MonoidHom.id (WithConv (MonoidAlgebra R G →ₐ[R] A))

Pre-composition by the identity homomorphism is the identity on points.

theorem TauCeti.DiagonalizableGroup.pointsMap_comp {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} {G'' : Type w''} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] [CommGroup G''] (φ : G →* G') (ψ : G' →* G'') : pointsMap (ψ.comp φ) = (pointsMap φ).comp (pointsMap ψ)

Contravariant functoriality. Pre-composition by a composite homomorphism is the composite of the induced points homomorphisms, in the opposite order.

theorem TauCeti.DiagonalizableGroup.mapValue_pointsMap {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] {B : Type u_1} [CommSemiring B] [Algebra R B] (φ : G →* G') (χ : A →ₐ[R] B) : (pointsMap φ).comp (AlgHom.mapValue χ) = (AlgHom.mapValue χ).comp (pointsMap φ)

Naturality in the value algebra. The contravariant points homomorphism pointsMap φ commutes with the value-algebra functoriality AlgHom.mapValue χ: pre-composition by the induced bialgebra map and post-composition by χ : A →ₐ[R] B may be applied in either order. This makes pointsMap φ a natural transformation of functors of points.

@[simp]

theorem TauCeti.DiagonalizableGroup.charOfPoint_comp {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') (f : MonoidAlgebra R G' →ₐ[R] A) : charOfPoint (f.comp ↑(MonoidAlgebra.mapDomainBialgHom R φ)) = (charOfPoint f).comp φ

Reading off the character of a point pre-composed by the induced bialgebra map is the character of the original point pre-composed by φ.

theorem TauCeti.DiagonalizableGroup.pointsMulEquiv_pointsMap {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') (f : WithConv (MonoidAlgebra R G' →ₐ[R] A)) : pointsMulEquiv ((pointsMap φ) f) = (pointsMulEquiv f).comp φ

The points homomorphism is precomposition of characters. Under the identification of points of D(G) with characters of G, the homomorphism pointsMap φ induced by φ : G →* G' is intertwined with precomposition χ ↦ χ ∘ φ of characters.

theorem TauCeti.DiagonalizableGroup.pointsMap_injective {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') (hφ : Function.Surjective ⇑φ) : Function.Injective ⇑(pointsMap φ)

If φ is surjective, then the induced contravariant map on diagonalizable-group points is injective. Under the character identification this is injectivity of precomposition by a surjective homomorphism.

theorem TauCeti.DiagonalizableGroup.pointsMap_pointsMulEquiv_symm_apply {R : Type u} {A : Type v} {G : Type w} {G' : Type w'} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommGroup G] [CommGroup G'] (φ : G →* G') (χ : G' →* Aˣ) : (pointsMap φ) (pointsMulEquiv.symm χ) = pointsMulEquiv.symm (χ.comp φ)

Mapping the point attached to a character is precomposition of that character by φ.