The points of the tripled type-D4 carrier, functorially

TauCeti.D4Tripled.groupScheme is the explicit tripled type-D₄ carrier over ℤ, and TauCeti.D4Tripled.points A realizes its A-valued points as a subgroup of GL₂₄(A). This file supplies the homomorphism induced by an arbitrary homomorphism of value rings and assembles these point groups into a functor on commutative ℤ-algebras.

The induced map is entrywise and preserves the two pinned families:

f (x_i(u)) = x_i(f(u)),        f (t(s)) = t(Units.map f ∘ s).

The coordinates of a weight-torus point are unit-valued, so the map induced on them is the map Units.map f of unit groups rather than f itself.

The quotient of the ambient general-linear coordinate Hopf algebra by the tripled carrier's defining ideal represents this functor. Nothing here asserts reductivity, maximality of the weight torus, or an identification of the carrier with the pinned simply connected group scheme of type D₄.

Main declarations

• TauCeti.D4Tripled.pointsMap: the map on carrier points induced by a ring homomorphism.
• TauCeti.D4Tripled.pointsFunctor: the group-valued functor of points.
• TauCeti.D4Tripled.pointsMulEquiv: the pointwise representing isomorphism.
• TauCeti.D4Tripled.pointsFunctorNatIso: the natural representing isomorphism.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, Sections 1.15 and 1.17.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• The carrier-independent functor this interface specializes is TauCeti.Algebra.AlgebraicGroup.GeneralLinear.HopfIdealPoints.Functor.

noncomputable def TauCeti.D4Tripled.pointsMap {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) : ↥(points A) →* ↥(points B)

The map on the points of the tripled type-D₄ carrier induced by a homomorphism of value rings. It is the entrywise map on GL₂₄, restricted to the subgroup cut out by the carrier's defining ideal.

Equations

• TauCeti.D4Tripled.pointsMap f = TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr 24 TauCeti.D4Tripled.definingIdeal ⋯ ⋯ f.toIntAlgHom

@[simp]

theorem TauCeti.D4Tripled.coe_pointsMap {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (g : ↥(points A)) : ↑((pointsMap f) g) = (Matrix.GeneralLinearGroup.map f) ↑g

The induced map on tripled carrier points is the entrywise map.

@[simp]

theorem TauCeti.D4Tripled.pointsMap_id {A : Type v} [CommRing A] : pointsMap (RingHom.id A) = MonoidHom.id ↥(points A)

The identity homomorphism induces the identity on tripled carrier points.

@[simp]

theorem TauCeti.D4Tripled.pointsMap_comp {A : Type v} {B : Type v'} [CommRing A] [CommRing B] {C : Type u_1} [CommRing C] (f : A →+* B) (g : B →+* C) : pointsMap (g.comp f) = (pointsMap g).comp (pointsMap f)

The induced maps on tripled carrier points compose.

theorem TauCeti.D4Tripled.pointsMap_injective {A : Type v} {B : Type v'} [CommRing A] [CommRing B] {f : A →+* B} (hf : Function.Injective ⇑f) : Function.Injective ⇑(pointsMap f)

An injective homomorphism of value rings induces an injective map on tripled carrier points.

@[simp]

theorem TauCeti.D4Tripled.pointsMap_rootSubgroupPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (k : Fin 4 ⊕ Fin 4) (u : Multiplicative A) : (pointsMap f) ((rootSubgroupPoints k A) u) = (rootSubgroupPoints k B) (Multiplicative.ofAdd (f (Multiplicative.toAdd u)))

The induced map carries a numbered root-subgroup parameter along the homomorphism of value rings.

@[simp]

theorem TauCeti.D4Tripled.pointsMap_weightTorusPoints {A : Type v} {B : Type v'} [CommRing A] [CommRing B] (f : A →+* B) (s : Fin 4 → Aˣ) : (pointsMap f) ((weightTorusPoints A) s) = (weightTorusPoints B) fun (i : Fin 4) => (Units.map ↑f) (s i)

The induced map carries a point of the pinned split weight torus coordinatewise along the homomorphism of value rings.

The functor of points

noncomputable def TauCeti.D4Tripled.pointsFunctor : CategoryTheory.Functor (CommAlgCat ℤ) GrpCat

The group-valued functor of points of the tripled type-D₄ carrier.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.pointsFunctor_obj (A : CommAlgCat ℤ) : pointsFunctor.obj A = ↧↥(points ↑A)

The object part of the tripled carrier's points functor is its named point group.

@[simp]

theorem TauCeti.D4Tripled.pointsFunctor_map {A B : CommAlgCat ℤ} (f : A ⟶ B) : pointsFunctor.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (pointsMap ↑(CommAlgCat.Hom.hom f))) (CategoryTheory.eqToHom ⋯))

The morphism part of the tripled carrier's points functor is the induced entrywise map.

noncomputable def TauCeti.D4Tripled.pointsMulEquiv (A : CommAlgCat ℤ) : ↑(HopfAlgebra.points A) ≃* ↥(points ↑A)

The points of the quotient coordinate Hopf algebra are the named tripled carrier points.

Equations

• TauCeti.D4Tripled.pointsMulEquiv A = (TauCeti.GeneralLinear.hopfIdealPointsSubgroupMulEquiv 24 TauCeti.D4Tripled.definingIdeal A).trans (MulEquiv.subgroupCongr ⋯).symm

@[simp]

theorem TauCeti.D4Tripled.coe_pointsMulEquiv_apply (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : ↑((pointsMulEquiv A) q) = (GeneralLinear.pointsMulEquiv 24) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal A)) q)

A quotient point, read through pointsMulEquiv, is its ambient point viewed as an invertible matrix.

@[simp]

theorem TauCeti.D4Tripled.quotientPointsHom_pointsMulEquiv_symm (A : CommAlgCat ℤ) (g : ↥(points ↑A)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal A)) ((pointsMulEquiv A).symm g) = (GeneralLinear.pointsMulEquiv 24).symm ↑g

Including the ambient Hopf-algebra point underlying the inverse of pointsMulEquiv recovers the point corresponding to the underlying matrix.

@[simp]

theorem TauCeti.D4Tripled.pointsMulEquiv_mapPoints {A B : CommAlgCat ℤ} (f : A ⟶ B) (q : ↑(HopfAlgebra.points A)) : (pointsMulEquiv B) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) q) = (pointsMap ↑(CommAlgCat.Hom.hom f)) ((pointsMulEquiv A) q)

The pointwise identification with quotient Hopf-algebra points is natural in the value algebra.

noncomputable def TauCeti.D4Tripled.pointsFunctorNatIso : HopfAlgebra.pointsFunctor ≅ pointsFunctor

The quotient coordinate Hopf algebra represents the points functor of the tripled type-D₄ carrier.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.pointsFunctorNatIso_hom_app_apply (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom (pointsFunctorNatIso.hom.app A)) q) = (pointsMulEquiv A) q

The forward component of the representing natural isomorphism is the pointwise identification.

@[simp]

theorem TauCeti.D4Tripled.pointsFunctorNatIso_inv_app_apply (A : CommAlgCat ℤ) (g : ↥(points ↑A)) : (CategoryTheory.ConcreteCategory.hom (pointsFunctorNatIso.inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (pointsMulEquiv A).symm g

The inverse component of the representing natural isomorphism is the inverse pointwise identification.