Base change of the full-weight type-D spin carrier

For 4 ≤ n, TauCeti.TypeDSpinCarrier.groupScheme is the explicit integral affine group scheme obtained by closing the numbered type-Dₙ root subgroups and the full spin weight torus inside GL_(2^n). This file specializes the general base-change construction for Kostant toral closures to that carrier.

For every commutative ring A, TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal is an ideal in O(GL_(2^n)/A) whose quotient is canonically the scalar extension of the integral coordinate Hopf algebra. The transported numbered root-subgroup maps and weight-torus map factor through that quotient. Thus the explicit integral carrier and its distinguished root-subgroup and torus maps 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 the represented weight torus is maximal, or that its root datum is the simply connected type-Dₙ datum.

Main declarations

• TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal: the transported defining ideal in the coordinate ring of GL_(2^n)/A.
• TauCeti.TypeDSpinCarrier.baseChangeCoordinateIso: the quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.TypeDSpinCarrier.coordinateHopfAlgebra and TauCeti.TypeDSpinCarrier.coordinateMap: that quotient, the specialized carrier coordinate algebra, and its ambient quotient map.
• TauCeti.TypeDSpinCarrier.baseChangePointsMulEquiv: the points of that quotient in a commutative A-algebra are the matrix points of the integral carrier over that algebra.
• TauCeti.TypeDSpinCarrier.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.TypeDSpinCarrier.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.
• TauCeti.TypeDSpinCarrier.generatorCoordinateMap: the family of transported numbered root and weight-torus maps into the ambient general linear group.

Main results

• TauCeti.TypeDSpinCarrier.mkQuotient_comp_baseChangeCoordinateIso_hom: the coordinate isomorphism is compatible with the two quotient presentations.
• TauCeti.TypeDSpinCarrier.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap and TauCeti.TypeDSpinCarrier.baseChangeCoordinateIso_hom_comp_weightTorusBaseChangeMap: each factored generator is the scalar extension of its integral coordinate map.
• TauCeti.TypeDSpinCarrier.mkQuotient_comp_rootSubgroupIntegralCoordinateMap and TauCeti.TypeDSpinCarrier.mkQuotient_comp_weightTorusIntegralCoordinateMap: over ℤ, each integral generator map recovers the coordinate map it factors.
• TauCeti.TypeDSpinCarrier.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op and TauCeti.TypeDSpinCarrier.hopfSpec_map_weightTorusIntegralCoordinateMap_op: those integral maps represent the carrier's existing root-subgroup and weight-torus morphisms.
• baseChangePointsMulEquiv_mapPointsFunctor_rootSubgroupToBaseChangeCoordinateMap and baseChangePointsMulEquiv_mapPointsFunctor_weightTorusToBaseChangeCoordinateMap: the transported coordinate maps induce the named root-subgroup and weight-torus points.
• TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated after base change by those maps.

References

• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• B. Conrad, Reductive Group Schemes, §1.

This supplies a prerequisite for the base-change target in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, "Base change along ℤ → k for any commutative ring k, and the compatibility of the pinning with it": it transports the underlying type-D carrier and its distinguished generator maps. It does not provide the pinning compatibility or a specialized pinned carrier. Those require the subsequent proofs that this carrier is reductive, that its torus is maximal with the simply connected type-Dₙ root datum, and that the maps supply a pinning. This file depends only on the already-constructed integral carrier and the generic scalar-extension machinery; those subsequent proofs can consume the declarations here as their underlying scalar-extension data. The declaration structure follows the sibling specialization for the pinned Geck carrier in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.GeckLattice.BaseChange. The ideal and generator-map declarations below specialize the corresponding generic Kostant declarations at this carrier's data; the points equivalences instead use the general Hopf-algebra and general-linear points APIs. The transport reading the generic base-change presentation through a named integral defining ideal is the ...OfEq family of Kostant/RootSubgroup/Scheme/ToralClosure/GeneralLinearBaseChange.lean, so nothing of that calculation is repeated here.

noncomputable def TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : HopfIdeal A ↑(GeneralLinear.coordinateHopfAlgebra A (dimension n))

The Hopf ideal in O(GL_(2^n)/A) obtained by transporting the defining ideal of the integral full-weight type-Dₙ carrier along ℤ → A.

Equations

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

theorem TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal_def (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : baseChangeDefiningIdeal n hn A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) A

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

@[simp]

theorem TauCeti.TypeDSpinCarrier.mem_baseChangeDefiningIdeal_iff (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A (dimension n))} : x ∈ baseChangeDefiningIdeal n hn A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (dimension n)).inv) x ∈ CommHopfAlgCat.baseChangeHopfIdeal (definingIdeal n hn)

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

theorem TauCeti.TypeDSpinCarrier.map_tmul_mem_baseChangeDefiningIdeal_of_mem (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (s : A) {y : ↑(GeneralLinear.coordinateHopfAlgebra ℤ (dimension n))} (hy : y ∈ definingIdeal n hn) : (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (dimension n)).hom) (s ⊗ₜ[ℤ] y) ∈ baseChangeDefiningIdeal n hn A

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

noncomputable def TauCeti.TypeDSpinCarrier.baseChangeCoordinateIso (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) ≅ CommHopfAlgCat.baseChange (CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn))

The coordinate Hopf algebra cut out over A by the transported 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.TypeDSpinCarrier.mkQuotient_comp_baseChangeCoordinateIso_hom (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A)) (baseChangeCoordinateIso n hn A).hom = CategoryTheory.CategoryStruct.comp (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (dimension n)).inv (CommHopfAlgCat.baseChangeMap (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn)))

The base-change coordinate isomorphism is compatible with the quotient presentation inside GL_(2^n).

The specialized coordinate Hopf algebra

@[reducible, inline]

noncomputable abbrev TauCeti.TypeDSpinCarrier.coordinateHopfAlgebra (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : CommHopfAlgCat A

The coordinate Hopf algebra of the full-weight type-Dₙ spin carrier after base change to A.

Equations

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

noncomputable def TauCeti.TypeDSpinCarrier.coordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : GeneralLinear.coordinateHopfAlgebra A (dimension n) ⟶ coordinateHopfAlgebra n hn A

The quotient coordinate morphism O(GL_(2^n)) ⟶ O(carrier), representing the closed immersion of the specialized spin carrier into the ambient general linear group.

Equations

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

theorem TauCeti.TypeDSpinCarrier.coordinateMap_surjective (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap n hn A))

The specialized carrier coordinate morphism is surjective.

@[simp]

theorem TauCeti.TypeDSpinCarrier.coordinateMap_ker (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : RingHom.ker (CommHopfAlgCat.Hom.hom (coordinateMap n hn A)) = (baseChangeDefiningIdeal n hn A).toIdeal

The specialized coordinate morphism kills exactly the defining Hopf ideal.

theorem TauCeti.TypeDSpinCarrier.mapPointsFunctor_coordinateMap_app (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] {B : Type w} [CommRing B] [Algebra A B] (g : ↑(HopfAlgebra.points ↧B)) : (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (coordinateMap n hn A)).app ↧B)) g = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) ↧B)) g

Precomposition with the carrier coordinate morphism is the ambient quotient-points map.

@[reducible, inline]

noncomputable abbrev TauCeti.TypeDSpinCarrier.finiteTypeCoordinateHopfAlgebra (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : FiniteTypeCommHopfAlgCat A

The specialized type-Dₙ spin carrier as a finite-type commutative Hopf algebra.

Equations

• TauCeti.TypeDSpinCarrier.finiteTypeCoordinateHopfAlgebra n hn A = TauCeti.FiniteTypeCommHopfAlgCat.of A ↑(TauCeti.TypeDSpinCarrier.coordinateHopfAlgebra n hn A)

@[simp]

theorem TauCeti.TypeDSpinCarrier.finiteTypeCoordinateHopfAlgebra_obj (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : (finiteTypeCoordinateHopfAlgebra n hn A).obj = coordinateHopfAlgebra n hn A

The underlying Hopf algebra of the finite-type carrier is its coordinate Hopf algebra.

Points of the base-changed carrier

noncomputable def TauCeti.TypeDSpinCarrier.baseChangePointsMulEquiv (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (B : CommAlgCat A) : ↑(HopfAlgebra.points B) ≃* ↥(points n hn ↑B)

The points of the base-changed 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.TypeDSpinCarrier.coe_baseChangePointsMulEquiv_apply (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (B : CommAlgCat A) (q : ↑(HopfAlgebra.points B)) : ↑((baseChangePointsMulEquiv n hn A B) q) = (GeneralLinear.pointsMulEquiv (dimension n)) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) B)) q)

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

@[simp]

theorem TauCeti.TypeDSpinCarrier.quotientPointsHom_baseChangePointsMulEquiv_symm (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (B : CommAlgCat A) (g : ↥(points n hn ↑B)) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) B)) ((baseChangePointsMulEquiv n hn A B).symm g) = (GeneralLinear.pointsMulEquiv (dimension n)).symm ↑g

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

@[simp]

theorem TauCeti.TypeDSpinCarrier.baseChangePointsMulEquiv_mapPoints (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] {B C : CommAlgCat A} (f : B ⟶ C) (q : ↑(HopfAlgebra.points B)) : (baseChangePointsMulEquiv n hn A C) ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) q) = ((pointsPresentation n hn ↑B).map (pointsPresentation n hn ↑C) ↑(CommAlgCat.Hom.hom f)) ((baseChangePointsMulEquiv n hn 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.TypeDSpinCarrier.rootSubgroupIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn) ⟶ AdditiveGroup.coordinateHopfAlgebra ℤ

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

Equations

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

theorem TauCeti.TypeDSpinCarrier.rootSubgroupIntegralCoordinateMap_def (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : rootSubgroupIntegralCoordinateMap n hn k = UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMapOfEq (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯ k

The integral root-subgroup coordinate map is the generic Kostant one, read through the named type-Dₙ defining ideal.

@[simp]

theorem TauCeti.TypeDSpinCarrier.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn)) (rootSubgroupIntegralCoordinateMap n hn k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside GL_(2^n), and so determines it.

@[simp]

theorem TauCeti.TypeDSpinCarrier.mulEquiv_mapPointsFunctor_rootSubgroupIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) (B : CommAlgCat ℤ) (k : Fin n ⊕ Fin n) (q : ↑(HopfAlgebra.points B)) : (pointsPresentation n hn ↑B).mulEquiv ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupIntegralCoordinateMap n hn k)).app B)) q) = (rootSubgroupPoints n hn k ↑B) (AdditiveGroup.gaPointsMulEquiv q)

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

theorem TauCeti.TypeDSpinCarrier.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (n : ℕ) (hn : 4 ≤ n) (k : Fin n ⊕ Fin n) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (rootSubgroupIntegralCoordinateMap n hn k).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rootSubgroup n hn k) (CategoryTheory.eqToHom ⋯))

The integral factored root-subgroup coordinate map represents the carrier's kth numbered root subgroup: its spectrum is TauCeti.TypeDSpinCarrier.rootSubgroup, read through the quotient-spectrum presentation of the carrier.

noncomputable def TauCeti.TypeDSpinCarrier.rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (k : Fin n ⊕ Fin n) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

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

Equations

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

@[simp]

theorem TauCeti.TypeDSpinCarrier.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (k : Fin n ⊕ Fin n) : CategoryTheory.CategoryStruct.comp (coordinateMap n hn A) (rootSubgroupToBaseChangeCoordinateMap n hn A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

The factored root-subgroup map recovers its ambient transported coordinate map after composition with the quotient map.

@[simp]

theorem TauCeti.TypeDSpinCarrier.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap_assoc (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (k : Fin n ⊕ Fin n) {Z : CommHopfAlgCat A} (h : AdditiveGroup.coordinateHopfAlgebra A ⟶ Z) : CategoryTheory.CategoryStruct.comp (coordinateMap n hn A) (CategoryTheory.CategoryStruct.comp (rootSubgroupToBaseChangeCoordinateMap n hn A k) h) = CategoryTheory.CategoryStruct.comp (UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k) h

The factored root-subgroup map recovers its ambient transported coordinate map after composition with the quotient map.

@[simp]

theorem TauCeti.TypeDSpinCarrier.baseChangeCoordinateIso_hom_comp_rootSubgroupBaseChangeMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (k : Fin n ⊕ Fin n) : CategoryTheory.CategoryStruct.comp (baseChangeCoordinateIso n hn A).hom (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap (rootSubgroupIntegralCoordinateMap n hn k)) (CommHopfAlgCat.ofHom ↑AdditiveGroup.gaScalarTensorBialgEquiv)) = rootSubgroupToBaseChangeCoordinateMap n hn 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.TypeDSpinCarrier.baseChangePointsMulEquiv_mapPointsFunctor_rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (B : CommAlgCat A) (k : Fin n ⊕ Fin n) (q : ↑(HopfAlgebra.points B)) : (baseChangePointsMulEquiv n hn A B) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (rootSubgroupToBaseChangeCoordinateMap n hn A k)).app B)) q) = (rootSubgroupPoints n hn 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.TypeDSpinCarrier.weightTorusIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn) ⟶ (DiagonalizableGroup.coordinateRing ℤ (SplitTorus.characterGroup (Fin n))).obj

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

Equations

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

theorem TauCeti.TypeDSpinCarrier.weightTorusIntegralCoordinateMap_def (n : ℕ) (hn : 4 ≤ n) : weightTorusIntegralCoordinateMap n hn = UniversalEnvelopingAlgebra.kostantWeightTorusToralCoordinateMapOfEq (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯

The integral weight-torus coordinate map is the generic Kostant one, read through the named type-Dₙ defining ideal.

@[simp]

theorem TauCeti.TypeDSpinCarrier.mkQuotient_comp_weightTorusIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n hn)) (weightTorusIntegralCoordinateMap n hn) = GeneralLinear.weightTorusCoordinateMap (basisWeight n)

The integral factored weight-torus map recovers the weight-torus coordinate map inside GL_(2^n), and so determines it.

@[simp]

theorem TauCeti.TypeDSpinCarrier.mulEquiv_mapPointsFunctor_weightTorusIntegralCoordinateMap (n : ℕ) (hn : 4 ≤ n) (B : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points B)) : (pointsPresentation n hn ↑B).mulEquiv ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (weightTorusIntegralCoordinateMap n hn)).app B)) q) = (weightTorusPoints n hn ↑B) (SplitTorus.pointsMulEquiv q)

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

theorem TauCeti.TypeDSpinCarrier.hopfSpec_map_weightTorusIntegralCoordinateMap_op (n : ℕ) (hn : 4 ≤ n) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (weightTorusIntegralCoordinateMap n hn).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (weightTorus n hn) (CategoryTheory.eqToHom ⋯))

The integral factored weight-torus coordinate map represents the carrier's weight torus: its spectrum is TauCeti.TypeDSpinCarrier.weightTorus, read through the quotient-spectrum presentation of the carrier.

noncomputable def TauCeti.TypeDSpinCarrier.weightTorusToBaseChangeCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n hn A) ⟶ (DiagonalizableGroup.coordinateRing A (SplitTorus.characterGroup (Fin n))).obj

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

Equations

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

@[simp]

theorem TauCeti.TypeDSpinCarrier.coordinateMap_comp_weightTorusToBaseChangeCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (coordinateMap n hn A) (weightTorusToBaseChangeCoordinateMap n hn A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (basisWeight n)

The factored weight-torus map recovers its ambient transported coordinate map, and so determines it.

@[simp]

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

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

@[simp]

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

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

@[reducible, inline]

noncomputable abbrev TauCeti.TypeDSpinCarrier.generatorCoordinateAlgebra (n : ℕ) (A : Type v) [CommRing A] : (Fin n ⊕ Fin n) ⊕ Unit → CommHopfAlgCat A

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

Equations

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

noncomputable def TauCeti.TypeDSpinCarrier.generatorCoordinateMap (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (j : (Fin n ⊕ Fin n) ⊕ Unit) : GeneralLinear.coordinateHopfAlgebra A (dimension n) ⟶ generatorCoordinateAlgebra n A j

The coordinate maps of the numbered root subgroups and the split weight torus into GL_(2^n).

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.TypeDSpinCarrier.generatorCoordinateMap n hn A (Sum.inr val) = TauCeti.GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (TauCeti.TypeDSpinCarrier.basisWeight n)

@[simp]

theorem TauCeti.TypeDSpinCarrier.generatorCoordinateMap_inl (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] (k : Fin n ⊕ Fin n) : generatorCoordinateMap n hn A (Sum.inl k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap (serreRootGenerator (CartanMatrix.D n)) (serreH ℚ (CartanMatrix.D n)) (rep n hn) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

The root branch of the generator family is the transported root-subgroup map.

@[simp]

theorem TauCeti.TypeDSpinCarrier.generatorCoordinateMap_inr (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : generatorCoordinateMap n hn A (Sum.inr ()) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (basisWeight n)

The torus branch of the generator family is the transported weight-torus map.

theorem TauCeti.TypeDSpinCarrier.baseChangeDefiningIdeal_le_commonKernel (n : ℕ) (hn : 4 ≤ n) (A : Type v) [CommRing A] : baseChangeDefiningIdeal n hn A ≤ CommHopfAlgCat.commonKernelHopfIdeal (generatorCoordinateMap n hn A)

The closed subgroup of GL_(2^n)/A generated by the transported numbered root subgroups and the transported weight torus lies in the base change of the integral type-Dₙ carrier.

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