Base change of the general linear coordinate Hopf algebra

For a morphism of commutative rings R → K, this file identifies scalar extension of the coordinate ring of GLₙ with the coordinate ring constructed directly over K:

K ⊗[R] R[Xᵢⱼ, det(X)⁻¹] ≃ K[Xᵢⱼ, det(X)⁻¹].

The equivalence first commutes tensor product with localization, then uses Mathlib's scalar extension equivalence for multivariate polynomial rings. It preserves the generic matrix, comultiplication, and counit, and is therefore bundled as an isomorphism of commutative Hopf algebras. In particular, this is an identification of the chosen coordinate Hopf structures, not only an abstract algebra isomorphism.

This is the general-linear compatibility needed by the base-change part of the explicit Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.GeneralLinear.coordinateRingBaseChangeAlgEquiv: the coordinate-ring equivalence.
• TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv: the bialgebra equivalence.
• TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso: its bundled commutative-Hopf-algebra form, when the extension ring's universe contains the base ring's.
• TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_hom_determinantGroupLike: scalar extension carries the generic determinant to the generic determinant.
• TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso: the corresponding isomorphism of finite-type commutative Hopf algebras.
• TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeMap_X: the value on a generic matrix entry after transporting the base change of any coordinate morphism.
• TauCeti.GeneralLinear.pointToGeneralLinear_baseChangeMap: scalar extension of a coordinate morphism preserves the matrix read from a point.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter IV, §1.8.
• The Stacks Project, Tags 01JO and 022W.
• The underlying formal equivalences are Mathlib's IsLocalization.Away.tensorProductEquivTMulRight and MvPolynomial.algebraTensorAlgEquiv; the bundled base-changed Hopf structure is Tau Ceti's CommHopfAlgCat.baseChange.

noncomputable def TauCeti.GeneralLinear.coordinateRingBaseChangeAlgEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : TensorProduct R K (CoordinateRing R n) ≃ₐ[K] CoordinateRing K n

Scalar extension of the general-linear coordinate algebra is canonically the general-linear coordinate algebra over the new base.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.coordinateRingBaseChangeAlgEquiv_tmul_coordinateRingMap (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (p : MatrixMonoid.CoordinateRing R n) : (coordinateRingBaseChangeAlgEquiv R K n) (s ⊗ₜ[R] (coordinateRingMap R n) p) = s • (coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p)

Base change sends a scalar tensored with a polynomial coordinate to that scalar times the same polynomial with its coefficients extended to the new base.

theorem TauCeti.GeneralLinear.coordinateRingBaseChangeAlgEquiv_one_tmul_X (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (i j : Fin n) : (coordinateRingBaseChangeAlgEquiv R K n) (1 ⊗ₜ[R] (coordinateRingMap R n) (MvPolynomial.X (i, j))) = (coordinateRingMap K n) (MvPolynomial.X (i, j))

Base change carries each localized generic matrix entry to the corresponding generic entry over the new base.

@[simp]

theorem TauCeti.GeneralLinear.coordinateRingBaseChangeAlgEquiv_symm_coordinateRingMap (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (p : MatrixMonoid.CoordinateRing R n) : (coordinateRingBaseChangeAlgEquiv R K n).symm ((coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p)) = 1 ⊗ₜ[R] (coordinateRingMap R n) p

The inverse coordinate-ring base-change equivalence sends a polynomial coordinate with extended coefficients back to the corresponding pure tensor.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebra_baseChange_algHom_ext (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) {C : Type u_1} [CommRing C] [Algebra R C] [Algebra K C] [IsScalarTower R K C] {f g : TensorProduct R K ↑(coordinateHopfAlgebra R n) →ₐ[K] C} (h : ∀ (i j : Fin n), f (1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = g (1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))))) : f = g

Two K-algebra maps out of the base-changed coordinate Hopf algebra of GLₙ are equal if they agree on the pure tensors of localized generic entries.

noncomputable def TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : ↑(CommHopfAlgCat.baseChange (coordinateHopfAlgebra R n)) ≃ₐc[K] ↑(coordinateHopfAlgebra K n)

The coordinate Hopf algebra of GLₙ commutes with base change.

Equations

• TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv R K n = BialgEquiv.ofAlgEquiv (TauCeti.GeneralLinear.bundledCoordinateBaseChangeAlgEquiv✝ R K n) ⋯ ⋯

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv_tmul (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (x : ↑(coordinateHopfAlgebra R n)) : (coordinateHopfAlgebraBaseChangeBialgEquiv R K n) (s ⊗ₜ[R] x) = (coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingBaseChangeAlgEquiv R K n) (s ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n).symm x))

The Hopf-algebra base-change equivalence on an arbitrary pure tensor, expressed through the coordinate-ring equivalence.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv_tmul_coordinateRingMap (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (p : MatrixMonoid.CoordinateRing R n) : (coordinateHopfAlgebraBaseChangeBialgEquiv R K n) (s ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) p)) = (coordinateHopfAlgebraAlgEquiv K n) (s • (coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p))

On polynomial coordinates, the Hopf-algebra base-change equivalence extends coefficients and multiplies by the scalar in the new base.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv_symm_coordinateRingMap (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (p : MatrixMonoid.CoordinateRing R n) : (coordinateHopfAlgebraBaseChangeBialgEquiv R K n).symm ((coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p))) = 1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) p)

The inverse Hopf-algebra base-change equivalence sends a polynomial coordinate with extended coefficients back to the corresponding pure tensor.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv_one_tmul_X (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (i j : Fin n) : (coordinateHopfAlgebraBaseChangeBialgEquiv R K n) (1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))) = (coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingMap K n) (MvPolynomial.X (i, j)))

Base change carries each bundled generic matrix entry to the corresponding entry over the new base.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeBialgEquiv_one_tmul_localizedGenericMatrix_inv_apply (R : Type u) (K : Type v) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (i j : Fin n) : (coordinateHopfAlgebraBaseChangeBialgEquiv R K n) (1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((localizedGenericMatrix R n)⁻¹ i j)) = (coordinateHopfAlgebraAlgEquiv K n) ((localizedGenericMatrix K n)⁻¹ i j)

Base change carries each inverse localized generic matrix entry to the corresponding inverse entry over the new base.

noncomputable def TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : CommHopfAlgCat.baseChange (coordinateHopfAlgebra R n) ≅ coordinateHopfAlgebra K n

Base change of the bundled general-linear coordinate Hopf algebra is canonically the general-linear coordinate Hopf algebra over the new base. The extension ring's carrier universe must contain the base ring's carrier universe; in particular, this covers ℤ → K for K in any universe. The unbundled algebra and bialgebra equivalences have no such restriction.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_hom_apply (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (p : MatrixMonoid.CoordinateRing R n) : (CategoryTheory.ConcreteCategory.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom) (s ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) p)) = (coordinateHopfAlgebraAlgEquiv K n) (s • (coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p))

The categorical base-change isomorphism has the same action on polynomial coordinates as the underlying bialgebra equivalence.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_hom_determinantGroupLike (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom) (1 ⊗ₜ[R] ↑(determinantGroupLike R n)) = ↑(determinantGroupLike K n)

The general-linear base-change isomorphism sends the scalar extension of the generic determinant to the generic determinant over the new base.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_hom_genericMatrix (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : let x := Algebra.compHom (↑(coordinateHopfAlgebra K n)) (algebraMap R K); have x_1 := ⋯; (genericMatrix R n).map ⇑((AlgHom.restrictScalars R ↑(CommHopfAlgCat.Hom.hom (coordinateHopfAlgebraBaseChangeIso R K n).hom)).comp Algebra.TensorProduct.includeRight) = genericMatrix K n

The general-linear base-change isomorphism sends the scalar extension of the bundled generic matrix to the bundled generic matrix over the new base.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_inv_apply (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (s : K) (p : MatrixMonoid.CoordinateRing R n) : s • (CategoryTheory.ConcreteCategory.hom (coordinateHopfAlgebraBaseChangeIso R K n).inv) ((coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingMap K n) ((MvPolynomial.map (algebraMap R K)) p))) = s ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) p)

The inverse categorical base-change isomorphism sends an extended polynomial coordinate back to its scalar pure tensor.

@[simp]

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeIso_inv_X (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (i j : Fin n) : (CategoryTheory.ConcreteCategory.hom (coordinateHopfAlgebraBaseChangeIso R K n).inv) ((coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingMap K n) (MvPolynomial.X (i, j)))) = 1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))

The inverse categorical base-change isomorphism sends a generic matrix entry to the corresponding scalar pure tensor.

theorem TauCeti.GeneralLinear.coordinateHopfAlgebraBaseChangeMap_X (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (H : CommHopfAlgCat R) (L : CommHopfAlgCat K) (f : coordinateHopfAlgebra R n ⟶ H) (e : CommHopfAlgCat.baseChange H ≅ L) (i j : Fin n) : (CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K n).inv (CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.baseChangeMap f) e.hom))) ((coordinateHopfAlgebraAlgEquiv K n) ((coordinateRingMap K n) (MvPolynomial.X (i, j)))) = (CommHopfAlgCat.Hom.hom e.hom) (1 ⊗ₜ[R] (CommHopfAlgCat.Hom.hom f) ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))))

Transporting the base change of a coordinate morphism sends a generic matrix entry to the target base-change isomorphism applied to the pure tensor of its original value.

theorem TauCeti.GeneralLinear.pointToGeneralLinear_baseChangeMap (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) (H : CommHopfAlgCat R) (f : coordinateHopfAlgebra R n ⟶ H) {A : Type u_1} [CommRing A] [Algebra K A] [Algebra R A] [IsScalarTower R K A] (q : WithConv (↑(CommHopfAlgCat.baseChange H) →ₐ[K] A)) : pointToGeneralLinear n (WithConv.toConv (q.ofConv.comp ↑(CommHopfAlgCat.Hom.hom (CategoryTheory.CategoryStruct.comp (coordinateHopfAlgebraBaseChangeIso R K n).inv (CommHopfAlgCat.baseChangeMap f))))) = pointToGeneralLinear n (WithConv.toConv ((AlgHom.baseChangePointsMulEquiv.symm q).ofConv.comp ↑(CommHopfAlgCat.Hom.hom f)))

Transporting a scalar-extended coordinate morphism to O(GLₙ/K) and reading its matrix agrees with reading the matrix of the original morphism on the restricted point.

noncomputable def TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).baseChange ≅ finiteTypeCoordinateHopfAlgebra K n

The canonical isomorphism baseChange K (finiteTypeCoordinateHopfAlgebra R n) ≅ finiteTypeCoordinateHopfAlgebra K n induced by coordinateHopfAlgebraBaseChangeIso.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.finiteTypeCoordinateHopfAlgebraBaseChangeIso_hom (R : Type u) (K : Type (max u v)) [CommRing R] [CommRing K] [Algebra R K] (n : ℕ) : (finiteTypeCoordinateHopfAlgebraBaseChangeIso R K n).hom.hom = (CategoryTheory.eqToIso ⋯ ≪≫ coordinateHopfAlgebraBaseChangeIso R K n ≪≫ CategoryTheory.eqToIso ⋯).hom

The underlying commutative-Hopf-algebra morphism of the finite-type base-change isomorphism is the canonical coordinate-Hopf-algebra base-change isomorphism, with the definitional object equalities made explicit.