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

TauCeti.TypeBSpinCarrier.groupScheme n is the explicit integral affine group scheme obtained by closing the numbered type-Bₙ₊₁ root subgroups and the full spin weight torus inside GL_(2^(n+1)). This file specializes the base-change construction for a general Kostant toral closure to that carrier.

For every commutative ring A, TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal is an ideal in the coordinate ring of the ambient general linear group over A; its quotient is canonically the scalar extension of the integral carrier coordinate Hopf algebra. The transported numbered root-subgroup maps and weight-torus map factor through this quotient. Thus the carrier and its distinguished generators base-change together, rather than being chosen anew over A.

The transported defining ideal is contained in the common kernel of the transported generators. Equality is not asserted over an arbitrary, possibly non-flat, base, where specialization can introduce additional equations. This file also makes no claim that the carrier is reductive, that its torus is maximal, or that its root datum is the simply connected type-Bₙ₊₁ datum.

Main declarations

• TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal: the transported defining ideal.
• TauCeti.TypeBSpinCarrier.baseChangeCoordinateIso: its quotient is the scalar extension of the integral carrier coordinate Hopf algebra.
• TauCeti.TypeBSpinCarrier.coordinateHopfAlgebra and TauCeti.TypeBSpinCarrier.coordinateMap: that quotient, the specialized carrier coordinate algebra, and its ambient quotient map; TauCeti.TypeBSpinCarrier.finiteTypeCoordinateHopfAlgebra bundles it with its finite-type property.
• TauCeti.TypeBSpinCarrier.baseChangePointsMulEquiv: the points of that quotient in a commutative A-algebra are the matrix points of the integral carrier over that algebra.
• TauCeti.TypeBSpinCarrier.rootSubgroupToBaseChangeCoordinateMap: the transported numbered root subgroup factored through the specialized carrier.
• TauCeti.TypeBSpinCarrier.weightTorusToBaseChangeCoordinateMap: the transported weight torus factored through the specialized carrier.
• TauCeti.TypeBSpinCarrier.generatorCoordinateMap: the family of transported numbered root-subgroup and weight-torus maps into the ambient general linear group.
• TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal_le_commonKernel: the transported carrier contains the subgroup generated by the transported maps.

Main results

• TauCeti.TypeBSpinCarrier.coe_baseChangePointsMulEquiv_apply and TauCeti.TypeBSpinCarrier.baseChangePointsMulEquiv_mapPoints: the point equivalence preserves ambient matrices and is natural in the value algebra.
• baseChangePointsMulEquiv_mapPointsFunctor_rootSubgroupToBaseChangeCoordinateMap and baseChangePointsMulEquiv_mapPointsFunctor_weightTorusToBaseChangeCoordinateMap: the transported coordinate maps induce the named root-subgroup and weight-torus points.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. E. Humphreys, Linear Algebraic Groups, §§26--27.
• B. Conrad, Reductive Group Schemes, §1.
• TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.BaseChange, for the corresponding full-weight type-D specialization. All constructions below use the generic Kostant base-change API rather than repeating its coordinate-ring calculations.

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

The Hopf ideal in the coordinate ring of GL_(2^(n+1))/A obtained by transporting the defining ideal of the integral full-weight type-Bₙ₊₁ spin carrier along ℤ → A.

Equations

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

theorem TauCeti.TypeBSpinCarrier.baseChangeDefiningIdeal_def (n : ℕ) (A : Type v) [CommRing A] : baseChangeDefiningIdeal n A = UniversalEnvelopingAlgebra.kostantToralBaseChangePresentationIdeal typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (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.TypeBSpinCarrier.mem_baseChangeDefiningIdeal_iff (n : ℕ) (A : Type v) [CommRing A] {x : ↑(GeneralLinear.coordinateHopfAlgebra A (dimension n))} : x ∈ baseChangeDefiningIdeal n A ↔ (CommHopfAlgCat.Hom.hom (GeneralLinear.coordinateHopfAlgebraBaseChangeIso ℤ A (dimension n)).inv) x ∈ CommHopfAlgCat.baseChangeHopfIdeal (definingIdeal n)

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

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

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

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

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

The base-change coordinate isomorphism is compatible with the quotient presentation inside the ambient general linear group.

The specialized coordinate Hopf algebra

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.coordinateHopfAlgebra (n : ℕ) (A : Type v) [CommRing A] : CommHopfAlgCat A

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

Equations

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

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

The quotient coordinate morphism O(GL_(2^(n+1))) ⟶ 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.TypeBSpinCarrier.coordinateMap_surjective (n : ℕ) (A : Type v) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (coordinateMap n A))

The specialized carrier coordinate morphism is surjective.

@[simp]

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

The specialized coordinate morphism kills exactly the defining Hopf ideal.

theorem TauCeti.TypeBSpinCarrier.mapPointsFunctor_coordinateMap_app (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 A)).app ↧B)) g = (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n A) ↧B)) g

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

@[reducible, inline]

noncomputable abbrev TauCeti.TypeBSpinCarrier.finiteTypeCoordinateHopfAlgebra (n : ℕ) (A : Type v) [CommRing A] : FiniteTypeCommHopfAlgCat A

The specialized type-Bₙ₊₁ spin carrier as a finite-type commutative Hopf algebra.

Equations

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

@[simp]

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

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

Points of the base-changed carrier

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

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

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

@[simp]

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

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

Equations

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

theorem TauCeti.TypeBSpinCarrier.rootSubgroupIntegralCoordinateMap_def (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : rootSubgroupIntegralCoordinateMap n k = UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMapOfEq typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯ k

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.mkQuotient_comp_rootSubgroupIntegralCoordinateMap (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra ℤ (dimension n)) (definingIdeal n)) (rootSubgroupIntegralCoordinateMap n k) = UniversalEnvelopingAlgebra.kostantRootSubgroupCoordinateMap typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ k ⋯ (latticeBasis n)

The integral factored root-subgroup map recovers the represented kth root-subgroup coordinate map inside the ambient general linear group.

@[simp]

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

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

theorem TauCeti.TypeBSpinCarrier.hopfSpec_map_rootSubgroupIntegralCoordinateMap_op (n : ℕ) (k : Fin (n + 1) ⊕ Fin (n + 1)) : (AlgebraicGeometry.hopfSpec ↧ℤ).map (rootSubgroupIntegralCoordinateMap n k).op = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rootSubgroup n k) (CategoryTheory.eqToHom ⋯))

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

noncomputable def TauCeti.TypeBSpinCarrier.rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n A) ⟶ AdditiveGroup.coordinateHopfAlgebra A

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

Equations

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.mkQuotient_comp_rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n A)) (rootSubgroupToBaseChangeCoordinateMap n A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.coordinateMap_comp_rootSubgroupToBaseChangeCoordinateMap (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : CategoryTheory.CategoryStruct.comp (coordinateMap n A) (rootSubgroupToBaseChangeCoordinateMap n A k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

The factored kth root-subgroup map composed with the carrier coordinate morphism recovers its ambient transported coordinate map.

@[simp]

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

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

Equations

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

theorem TauCeti.TypeBSpinCarrier.weightTorusIntegralCoordinateMap_def (n : ℕ) : weightTorusIntegralCoordinateMap n = UniversalEnvelopingAlgebra.kostantWeightTorusToralCoordinateMapOfEq typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) (basisWeight n) ⋯

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

@[simp]

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

The integral factored weight-torus map recovers the represented weight-torus coordinate map inside the ambient general linear group.

@[simp]

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

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

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

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

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

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

Equations

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.mkQuotient_comp_weightTorusToBaseChangeCoordinateMap (n : ℕ) (A : Type v) [CommRing A] : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra A (dimension n)) (baseChangeDefiningIdeal n A)) (weightTorusToBaseChangeCoordinateMap n A) = GeneralLinear.weightTorusBaseChangeCoordinateMap ℤ A (basisWeight n)

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[reducible, inline]

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

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

Equations

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

noncomputable def TauCeti.TypeBSpinCarrier.generatorCoordinateMap (n : ℕ) (A : Type v) [CommRing A] (j : (Fin (n + 1) ⊕ Fin (n + 1)) ⊕ 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+1)).

Equations

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

@[simp]

theorem TauCeti.TypeBSpinCarrier.generatorCoordinateMap_inl (n : ℕ) (A : Type v) [CommRing A] (k : Fin (n + 1) ⊕ Fin (n + 1)) : generatorCoordinateMap n A (Sum.inl k) = UniversalEnvelopingAlgebra.kostantRootSubgroupBaseChangePresentationCoordinateMap typeBSimpleRootGeneratorFamily typeBSimpleCorootGenerator (rep n) (lattice n).toAddSubgroup ⋯ ⋯ (latticeBasis n) A k

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

@[simp]

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

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

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

The closed subgroup of the ambient general linear group generated by the transported numbered root subgroups and weight torus lies in the base change of the integral type-Bₙ₊₁ carrier.

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