Base change of the tripled type-D4 carrier

TauCeti.D4Tripled.groupScheme is the explicit integral affine group scheme obtained by closing the eight numbered type-D₄ root subgroups and the rank-four weight torus of V(ϖ₁) ⊕ V(ϖ₃) ⊕ V(ϖ₄) inside GL₂₄. This file specializes the base-change construction for a general Kostant toral closure to that carrier.

For every commutative ring A, TauCeti.D4Tripled.baseChangeDefiningIdeal is an ideal in O(GL₂₄/A) whose quotient is canonically the scalar extension of the integral coordinate Hopf algebra, and whose points in a commutative A-algebra B are the integral carrier's matrix points over B. The transported numbered root-subgroup maps and weight-torus map factor through that quotient, and on points they are the carrier's named root-subgroup and weight-torus points. Thus the integral carrier and its numbered generators base-change together; none of the data is chosen anew over A.

The defining ideal transported from ℤ is contained in the common kernel of the transported generators. Equality is not asserted over an arbitrary, possibly non-flat, base: additional equations can appear after specialization. Nor does this file assert that the carrier is reductive, that its torus is maximal, or that it is isomorphic to an independently defined pinned group scheme of type D₄.

Main declarations

• TauCeti.D4Tripled.baseChangeDefiningIdeal: the transported defining ideal in O(GL₂₄/A).
• TauCeti.D4Tripled.baseChangeDefiningIdeal_def: its unfolding to the generic construction.
• TauCeti.D4Tripled.coordinateHopfAlgebra and TauCeti.D4Tripled.coordinateMap: the specialized coordinate Hopf algebra and its quotient map from O(GL₂₄/A).
• TauCeti.D4Tripled.finiteTypeCoordinateHopfAlgebra: the same coordinate algebra bundled with its finite-type property.
• TauCeti.D4Tripled.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.D4Tripled.baseChangePointsMulEquiv: the points of that quotient in a commutative A-algebra are the matrix points of the integral carrier over that algebra.
• TauCeti.D4Tripled.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.D4Tripled.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.
• TauCeti.D4Tripled.generatorCoordinateMap: the family of transported numbered root and weight-torus maps into the ambient general linear group.

Main results

• TauCeti.D4Tripled.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the quotient presentations.
• TauCeti.D4Tripled.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.D4Tripled.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: the numbered generators are the scalar extensions of their integral coordinate maps.
• TauCeti.D4Tripled.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.D4Tripled.hopfSpec_map_weightTorusIntegralCoordinateMap_op: the integral coordinate maps represent the existing root-subgroup and weight-torus morphisms.
• pointsMulEquiv_mapPointsFunctor_rootSubgroupIntegralCoordinateMap and pointsMulEquiv_mapPointsFunctor_weightTorusIntegralCoordinateMap: over ℤ, the integral coordinate maps induce the named root-subgroup and weight-torus points.
• baseChangePointsMulEquiv_mapPointsFunctor_rootSubgroupToBaseChangeCoordinateMap and baseChangePointsMulEquiv_mapPointsFunctor_weightTorusToBaseChangeCoordinateMap: the transported coordinate maps induce the named root-subgroup and weight-torus points.
• TauCeti.D4Tripled.baseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated after base change by the transported maps.

References

• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 12.2.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• B. Conrad, Reductive Group Schemes, §1.
• Analogous base-change APIs for other explicit carriers are provided by TauCeti.Algebra.Lie.E6.DoubledMinuscule.BaseChange and TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.BaseChange.

@[reducible, inline]

noncomputable abbrev TauCeti.D4Tripled.generatorCoordinateAlgebra (A : Type v) [CommRing A] : (Fin 4 ⊕ Fin 4) ⊕ Unit → CommHopfAlgCat A

The coordinate Hopf algebras of the numbered root groups and the split weight torus.

Equations

• TauCeti.D4Tripled.generatorCoordinateAlgebra A (Sum.inl val) = TauCeti.AdditiveGroup.coordinateHopfAlgebra A
• TauCeti.D4Tripled.generatorCoordinateAlgebra A (Sum.inr val) = (TauCeti.DiagonalizableGroup.coordinateRing A (TauCeti.SplitTorus.characterGroup (Fin 4))).obj

noncomputable def TauCeti.D4Tripled.generatorCoordinateMap (A : Type v) [CommRing A] (j : (Fin 4 ⊕ Fin 4) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra A 24 ⟶ generatorCoordinateAlgebra A j

The coordinate maps of the numbered root subgroups and split weight torus into GL₂₄.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.D4Tripled.generatorCoordinateMap A (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A TauCeti.DynkinType.d4TripledWeight

@[simp]

theorem TauCeti.D4Tripled.generatorCoordinateMap_inl (A : Type v) [CommRing A] (i : Fin 4 ⊕ Fin 4) : generatorCoordinateMap A (Sum.inl i) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis A i

The numbered branches of the generator family are the transported root maps.

@[simp]

theorem TauCeti.D4Tripled.generatorCoordinateMap_inr (A : Type v) [CommRing A] : generatorCoordinateMap A (Sum.inr ()) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A DynkinType.d4TripledWeight

The final branch of the generator family is the transported weight torus.

noncomputable def TauCeti.D4Tripled.baseChangeDefiningIdeal (A : Type v) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A 24)

The Hopf ideal in O(GL₂₄/A) obtained by transporting the defining ideal of the integral tripled type-D₄ carrier along ℤ → A.

Equations

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

theorem TauCeti.D4Tripled.baseChangeDefiningIdeal_def (A : Type v) [CommRing A] : baseChangeDefiningIdeal A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight A

The transported defining ideal is the ideal supplied by the generic Kostant toral-closure base change.

@[reducible, inline]

noncomputable abbrev TauCeti.D4Tripled.coordinateHopfAlgebra (A : Type v) [CommRing A] : CommHopfAlgCat A

The coordinate Hopf algebra of the tripled type-D₄ carrier after base change to A.

Equations

• TauCeti.D4Tripled.coordinateHopfAlgebra A = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 24) (TauCeti.D4Tripled.baseChangeDefiningIdeal A)

noncomputable def TauCeti.D4Tripled.coordinateMap (A : Type v) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A 24 ⟶ coordinateHopfAlgebra A

The quotient coordinate morphism O(GL₂₄) ⟶ O(carrier), representing the closed immersion of the specialized tripled type-D₄ carrier into GL₂₄.

Equations

• TauCeti.D4Tripled.coordinateMap A = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra A 24) (TauCeti.D4Tripled.baseChangeDefiningIdeal A)

theorem TauCeti.D4Tripled.coordinateMap_surjective (A : Type v) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap A))

The specialized carrier coordinate morphism is surjective.

@[simp]

theorem TauCeti.D4Tripled.coordinateMap_ker (A : Type v) [CommRing A] : RingHom.ker (CommHopfAlgCat.Hom.hom (coordinateMap A)) = (baseChangeDefiningIdeal A).toIdeal

The kernel of the specialized carrier coordinate morphism is its transported defining ideal.

@[reducible, inline]

noncomputable abbrev TauCeti.D4Tripled.finiteTypeCoordinateHopfAlgebra (A : Type v) [CommRing A] : FiniteTypeCommHopfAlgCat A

The specialized tripled type-D₄ carrier as a finite-type commutative Hopf algebra.

Equations

• TauCeti.D4Tripled.finiteTypeCoordinateHopfAlgebra A = TauCeti.FiniteTypeCommHopfAlgCat.of A ↑(TauCeti.D4Tripled.coordinateHopfAlgebra A)

@[simp]

theorem TauCeti.D4Tripled.finiteTypeCoordinateHopfAlgebra_obj (A : Type v) [CommRing A] : (finiteTypeCoordinateHopfAlgebra A).obj = coordinateHopfAlgebra A

The finite-type package has the specialized carrier coordinate Hopf algebra as its underlying object.

@[simp]

theorem TauCeti.D4Tripled.mapPointsFunctor_coordinateMap_app (A : Type v) [CommRing A] {B : Type w} [CommRing B] [Algebra A B] (g : ↑(HopfAlgebra.points ↧B)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (coordinateMap A)).app ↧B)) g = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) ↧B)) g

Mapping a carrier point along the coordinate morphism gives the corresponding quotient point of the ambient general linear group.

@[simp]

theorem TauCeti.D4Tripled.mem_baseChangeDefiningIdeal_iff (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A 24)} : x ∈ baseChangeDefiningIdeal A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 24).inv) x ∈ CommHopfAlgCat.baseChangeHopfIdeal definingIdeal

Membership in the transported defining ideal is membership of the corresponding element in the base change of the named integral defining ideal.

theorem TauCeti.D4Tripled.map_tmul_mem_baseChangeDefiningIdeal_of_mem (A : Type v) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ 24)} (hy : y ∈ definingIdeal) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 24).hom) (s ⊗ₜ[ℤ] y) ∈ baseChangeDefiningIdeal A

Transporting a pure tensor of a scalar and an integral defining equation produces an equation in the transported defining ideal.

noncomputable def TauCeti.D4Tripled.baseChangeCoordinateIso (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal)

The coordinate Hopf algebra cut out over A by the transported tripled type-D₄ defining ideal is canonically the scalar extension of the integral coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.mkQuotient_comp_baseChangeCoordinateIso_hom (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A)) (baseChangeCoordinateIso A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A 24).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal))

The base-change coordinate isomorphism is compatible with the quotient presentation inside GL₂₄.

Points of the base-changed carrier

noncomputable def TauCeti.D4Tripled.baseChangePointsMulEquiv (A : Type v) [CommRing A] (B : CommAlgCat A) : ↑(HopfAlgebra.points B) ≃* ↥(points ↑B)

The points of the base-changed tripled type-D₄ carrier over a commutative A-algebra are its matrix-valued carrier points over that algebra.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.coe_baseChangePointsMulEquiv_apply (A : Type v) [CommRing A] (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : ↑((baseChangePointsMulEquiv A B) q) = (GeneralLinear.pointsMulEquiv 24) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) B)) q)

The base-change points equivalence preserves the ambient invertible matrix.

@[simp]

theorem TauCeti.D4Tripled.quotientPointsHom_baseChangePointsMulEquiv_symm (A : Type v) [CommRing A] (B : CommAlgCat A) (g : ↥(points ↑B)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) B)) ((baseChangePointsMulEquiv A B).symm g) = (GeneralLinear.pointsMulEquiv 24).symm ↑g

The quotient point underlying the inverse base-change equivalence is the point determined by the ambient invertible matrix.

@[simp]

theorem TauCeti.D4Tripled.baseChangePointsMulEquiv_mapPoints (A : Type v) [CommRing A] {B C : CommAlgCat A} (f : B ⟶ C) (q : ↑(HopfAlgebra.points B)) : (baseChangePointsMulEquiv A C) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) q) = (pointsMap ↑(CommAlgCat.Hom.hom f)) ((baseChangePointsMulEquiv A B) q)

The identification of the base-changed carrier's points is natural in the value algebra.

The transported root subgroups

noncomputable def TauCeti.D4Tripled.rootSubgroupIntegralCoordinateMap (k : Fin 4 ⊕ Fin 4) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

The integral kth root-subgroup coordinate map, with source expressed using the named tripled type-D₄ defining ideal.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal) (rootSubgroupIntegralCoordinateMap k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside GL₂₄.

@[simp]

theorem TauCeti.D4Tripled.pointsMulEquiv_mapPointsFunctor_rootSubgroupIntegralCoordinateMap (B : CommAlgCat ℤ) (k : Fin 4 ⊕ Fin 4) (q : ↑(HopfAlgebra.points B)) : (pointsMulEquiv B) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupIntegralCoordinateMap k)).app B)) q) = (rootSubgroupPoints k ↑B) (AdditiveGroup.gaPointsMulEquiv q)

On points, the integral factored coordinate map is the named numbered root subgroup.

theorem TauCeti.D4Tripled.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (k : Fin 4 ⊕ Fin 4) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (rootSubgroupIntegralCoordinateMap k).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rootSubgroup k) (CategoryTheory.eqToHom groupScheme_def))

The integral factored root-subgroup coordinate map represents the carrier's kth numbered root subgroup.

noncomputable def TauCeti.D4Tripled.rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 4 ⊕ Fin 4) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

The base-changed kth root-subgroup coordinate map factored through the transported tripled type-D₄ carrier.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.mkQuotient_comp_rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A)) (rootSubgroupToBaseChangeCoordinateMap A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis A k

The factored root-subgroup map recovers its ambient transported coordinate map.

@[simp]

theorem TauCeti.D4Tripled.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (A : Type v) [CommRing A] (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupIntegralCoordinateMap k)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = rootSubgroupToBaseChangeCoordinateMap A k

Under the base-change coordinate isomorphism, the factored kth root-subgroup map is the scalar extension of its integral coordinate map.

@[simp]

theorem TauCeti.D4Tripled.baseChangePointsMulEquiv_mapPointsFunctor_rootSubgroupToBaseChangeCoordinateMap (A : Type v) [CommRing A] (B : CommAlgCat A) (k : Fin 4 ⊕ Fin 4) (q : ↑(HopfAlgebra.points B)) : (baseChangePointsMulEquiv A B) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupToBaseChangeCoordinateMap A k)).app B)) q) = (rootSubgroupPoints k ↑B) (AdditiveGroup.gaPointsMulEquiv q)

On points, the transported factored coordinate map is the named numbered root subgroup.

The transported weight torus

noncomputable def TauCeti.D4Tripled.weightTorusIntegralCoordinateMap : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin 4))).obj

The integral weight-torus coordinate map, with source expressed using the named tripled type-D₄ defining ideal.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.mkQuotient_comp_weightTorusIntegralCoordinateMap : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal) weightTorusIntegralCoordinateMap = GeneralLinear.weightTorusCoordinateMap DynkinType.d4TripledWeight

The integral factored weight-torus map recovers the represented weight-torus coordinate map inside GL₂₄.

@[simp]

theorem TauCeti.D4Tripled.pointsMulEquiv_mapPointsFunctor_weightTorusIntegralCoordinateMap (B : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points B)) : (pointsMulEquiv B) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor weightTorusIntegralCoordinateMap).app B)) q) = (weightTorusPoints ↑B) (SplitTorus.pointsMulEquiv q)

On points, the integral factored coordinate map is the named weight torus.

theorem TauCeti.D4Tripled.hopfSpec_map_weightTorusIntegralCoordinateMap_op : (AlgebraicGeometry.hopfSpec ↧ℤ).map weightTorusIntegralCoordinateMap.op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp weightTorus (CategoryTheory.eqToHom groupScheme_def))

The integral factored weight-torus coordinate map represents the carrier's weight torus.

noncomputable def TauCeti.D4Tripled.weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin 4))).obj

The base-changed weight-torus coordinate map factored through the transported tripled type-D₄ carrier.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.mkQuotient_comp_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A 24) (baseChangeDefiningIdeal A)) (weightTorusToBaseChangeCoordinateMap A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A DynkinType.d4TripledWeight

The factored weight-torus map recovers its ambient transported coordinate map.

@[simp]

theorem TauCeti.D4Tripled.coordinateMap_comp_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (coordinateMap A) (weightTorusToBaseChangeCoordinateMap A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A DynkinType.d4TripledWeight

The factored weight-torus map composed with the carrier coordinate morphism recovers its ambient transported coordinate map.

@[simp]

theorem TauCeti.D4Tripled.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap weightTorusIntegralCoordinateMap) (CommHopfAlgCat.ofHom ↑(MonoidAlgebra.scalarTensorBialgEquiv ℤ A))) = weightTorusToBaseChangeCoordinateMap A

Under the base-change coordinate isomorphism, the factored weight-torus map is the scalar extension of its integral coordinate map.

@[simp]

theorem TauCeti.D4Tripled.baseChangePointsMulEquiv_mapPointsFunctor_weightTorusToBaseChangeCoordinateMap (A : Type v) [CommRing A] (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : (baseChangePointsMulEquiv A B) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightTorusToBaseChangeCoordinateMap A)).app B)) q) = (weightTorusPoints ↑B) (SplitTorus.pointsMulEquiv q)

On points, the transported factored weight-torus map is the named weight torus.

theorem TauCeti.D4Tripled.baseChangeDefiningIdeal_le_commonKernel (A : Type v) [CommRing A] : baseChangeDefiningIdeal A ≤ CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap A)

The closed subgroup of GL₂₄/A generated by the transported numbered root subgroups and weight torus lies in the base change of the integral tripled type-D₄ carrier.

The reverse inclusion is not asserted over an arbitrary base ring.