The general linear group scheme

For a commutative ring R and a natural number n, the coordinate Hopf algebra of the general linear group is the determinant localization

R[Xᵢⱼ][det(X)⁻¹].

Applying relative spectrum to the bundled coordinate Hopf algebra gives an affine group scheme over Spec R. This file presents its underlying scheme canonically as the spectrum of the raw determinant localization. Under that presentation, the structural morphism, unit, multiplication, and inversion are induced contravariantly by the algebra structure map, counit, comultiplication, and antipode, respectively. The multiplication source is identified with the spectrum of the tensor square of the raw coordinate ring.

For a same-universe commutative R-algebra A, Mathlib's spectrum-points equivalence followed by GeneralLinear.pointsMulEquiv identifies scheme-valued points with invertible matrices over A. The resulting identification computes entries by evaluation on the bundled matrix coordinates and is covariantly natural in A.

The construction includes rank zero and the zero ring. Mathlib's current hopfSpec construction and spectrum-points equivalence require the base ring, Hopf-algebra carrier, and value algebra to lie in the same universe, so this file uses that same-universe setting.

Main declarations

• TauCeti.GeneralLinear.groupScheme: the general linear group scheme over Spec R.
• TauCeti.GeneralLinear.hopfIdealInclusion: the generic closed immersion into GL_n cut out by a Hopf ideal.
• TauCeti.GeneralLinear.groupSchemeSpecIso: its canonical raw-coordinate presentation.
• TauCeti.GeneralLinear.groupSchemeMulSourceIso: the tensor-coordinate presentation of the multiplication source.
• TauCeti.GeneralLinear.groupScheme_one_left, TauCeti.GeneralLinear.groupScheme_mul_left, and TauCeti.GeneralLinear.groupScheme_inv_left: the raw-coordinate formulas for the group operations.
• TauCeti.GeneralLinear.isAffine_groupScheme and TauCeti.GeneralLinear.locallyOfFiniteType_groupScheme: affineness and local finite type over the base.
• TauCeti.GeneralLinear.groupSchemePointMulEquiv: the canonical passage between algebra points and scheme-valued points.
• TauCeti.GeneralLinear.schemePointsMulEquiv and TauCeti.GeneralLinear.schemePointsMulEquiv_apply: scheme-valued points are invertible matrices over the value algebra, with an entrywise coordinate formula.
• TauCeti.GeneralLinear.schemePointsMulEquiv_mapValue: covariance in the value algebra.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter IV, section 1.8, and Algebraic Groups (2017), sections 2.8 and 3.3--3.6.
• The Stacks Project, Tags 022W, 022X, and 00CM.

The scheme-valued-points interface follows the spectrum-retyping and value-algebra naturality pattern in TauCetiProject/TauCeti, revision 1f55a87ca0ca0c64550c374d78dfe8e701a4ccfc, TauCeti/Algebra/AlgebraicGroup/AdditiveGroup/Scheme.lean (Apache 2.0).

noncomputable def TauCeti.GeneralLinear.groupScheme (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The general linear group scheme obtained by applying relative spectrum to its coordinate Hopf algebra.

The same-universe restriction is imposed by Mathlib's current hopfSpec construction.

Equations

• TauCeti.GeneralLinear.groupScheme R n = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (TauCeti.GeneralLinear.coordinateHopfAlgebra R n))

theorem TauCeti.GeneralLinear.groupScheme_def (R : Type u) [CommRing R] (n : ℕ) : groupScheme R n = (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op (coordinateHopfAlgebra R n))

The general linear group scheme is the relative spectrum of its coordinate Hopf algebra.

noncomputable def TauCeti.GeneralLinear.hopfIdealInclusion (R : Type u) [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) : CommHopfAlgCat.quotientSpec (coordinateHopfAlgebra R n) I ⟶ groupScheme R n

The closed subgroup inclusion into GL_n cut out by a Hopf ideal of its coordinate algebra.

Equations

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

theorem TauCeti.GeneralLinear.hopfIdealInclusion_def (R : Type u) [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) : hopfIdealInclusion R n I = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.quotientSpecι (coordinateHopfAlgebra R n) I) (CategoryTheory.eqToIso ⋯).hom

A Hopf-ideal inclusion is the quotient-spectrum inclusion followed by the named identification with GL_n.

instance TauCeti.GeneralLinear.isClosedImmersion_hopfIdealInclusion (R : Type u) [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (hopfIdealInclusion R n I).hom.hom)

Every subgroup of GL_n cut out by a Hopf ideal is closed.

instance TauCeti.GeneralLinear.locallyOfFiniteType_hopfIdealQuotientSpec (R : Type u) [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) : AlgebraicGeometry.LocallyOfFiniteType (CommHopfAlgCat.quotientSpec (coordinateHopfAlgebra R n) I).X.hom

A subgroup of GL_n cut out by a Hopf ideal is locally of finite type over the base.

theorem TauCeti.GeneralLinear.groupScheme_X_left (R : Type u) [CommRing R] (n : ℕ) : (groupScheme R n).X.left = AlgebraicGeometry.Spec ↧↑(coordinateHopfAlgebra R n)

The scheme underlying the general linear group scheme is the spectrum of its bundled coordinate Hopf algebra.

noncomputable def TauCeti.GeneralLinear.groupSchemeSpecIso (R : Type u) [CommRing R] (n : ℕ) : (groupScheme R n).X.left ≅ AlgebraicGeometry.Spec ↧(CoordinateRing R n)

The scheme underlying the general linear group scheme is canonically isomorphic to the spectrum of the determinant localization.

Equations

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

theorem TauCeti.GeneralLinear.groupScheme_X_hom (R : Type u) [CommRing R] (n : ℕ) : (groupScheme R n).X.hom = CategoryTheory.CategoryStruct.comp (groupSchemeSpecIso R n).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R (CoordinateRing R n))))

The structural morphism of the general linear group scheme is induced by the algebra structure map on the determinant localization.

noncomputable def TauCeti.GeneralLinear.groupSchemeMulSourceIso (R : Type u) [CommRing R] (n : ℕ) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (groupScheme R n).X (groupScheme R n).X).left ≅ AlgebraicGeometry.Spec ↧(TensorProduct R (CoordinateRing R n) (CoordinateRing R n))

The multiplication source is canonically the spectrum of the tensor square of the raw determinant-localization coordinate ring. This combines the fibre-product presentation of the product over Spec R, the standard affine pullback isomorphism, and the coordinate equivalence on both tensor factors.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.groupScheme_one_left (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(counit R n))) (groupSchemeSpecIso R n).inv

The unit of the general linear group scheme is induced by the raw coordinate counit.

@[simp]

theorem TauCeti.GeneralLinear.groupScheme_mul_left (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Over.Hom.left CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (groupSchemeMulSourceIso R n).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(comul R n))) (groupSchemeSpecIso R n).inv)

Multiplication on the general linear group scheme is induced by the raw matrix-multiplication comultiplication. The source presentation fixes the tensor-factor order representing ordinary matrix multiplication.

@[simp]

theorem TauCeti.GeneralLinear.groupScheme_inv_left (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Over.Hom.left CategoryTheory.GrpObj.inv = CategoryTheory.CategoryStruct.comp (groupSchemeSpecIso R n).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(antipode R n))) (groupSchemeSpecIso R n).inv)

Inversion on the general linear group scheme is induced by the raw inverse-matrix antipode.

instance TauCeti.GeneralLinear.isAffine_groupScheme (R : Type u) [CommRing R] (n : ℕ) : AlgebraicGeometry.IsAffine (groupScheme R n).X.left

The general linear group scheme is affine.

instance TauCeti.GeneralLinear.locallyOfFiniteType_groupScheme (R : Type u) [CommRing R] (n : ℕ) : AlgebraicGeometry.LocallyOfFiniteType (groupScheme R n).X.hom

The structural morphism of the general linear group scheme is locally of finite type.

noncomputable def TauCeti.GeneralLinear.groupSchemePointMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A) ≃* ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X)

Mathlib's spectrum-points equivalence, with its target presented as the underlying object of the general linear group scheme. It sends an algebra point to its contravariant spectrum morphism.

The retyping makes the equivalence usable without unfolding the opaque definition of groupScheme.

Equations

• TauCeti.GeneralLinear.groupSchemePointMulEquiv n A = TauCeti.CommHopfAlgCat.mapMulEquivOfPresentation (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) A ⋯

@[simp]

theorem TauCeti.GeneralLinear.groupSchemePointMulEquiv_apply_left {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (f : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : CategoryTheory.Over.Hom.left ((groupSchemePointMulEquiv n A) f) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑f.ofConv)) (CategoryTheory.eqToHom ⋯)

The underlying map of the spectrum point associated to an algebra point.

noncomputable def TauCeti.GeneralLinear.schemePointsMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) ≃* GL (Fin n) A

The group of scheme-valued points of the general linear group scheme is the ordinary general linear group over the value algebra.

The source consists of morphisms over Spec R from Spec A to the underlying object of groupScheme R n; its multiplication is the pointwise group law induced by that group object.

Equations

• TauCeti.GeneralLinear.schemePointsMulEquiv n A = (TauCeti.GeneralLinear.groupSchemePointMulEquiv n A).symm.trans (TauCeti.GeneralLinear.pointsMulEquiv n)

@[simp]

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_apply {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) (i j : Fin n) : ↑((schemePointsMulEquiv n A) p) i j = ((groupSchemePointMulEquiv n A).symm p).ofConv ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))))

A scheme-valued point corresponds entrywise to evaluation of its canonical algebra point on the bundled matrix coordinates.

@[simp]

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_groupSchemePointMulEquiv {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (q : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : (schemePointsMulEquiv n A) ((groupSchemePointMulEquiv n A) q) = (pointsMulEquiv n) q

Evaluating the scheme-points equivalence on a point presented by groupSchemePointMulEquiv recovers the canonical algebra point.

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_symm_apply {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] (g : GL (Fin n) A) : (schemePointsMulEquiv n A).symm g = (groupSchemePointMulEquiv n A) ((pointsMulEquiv n).symm g)

The inverse scheme-points equivalence sends an invertible matrix to the spectrum map induced by its canonical coordinate-algebra point.

theorem TauCeti.GeneralLinear.schemePointsMulEquiv_mapValue {R : Type u} [CommRing R] (n : ℕ) (A : Type u) [CommRing A] [Algebra R A] {B : Type u} [CommRing B] [Algebra R B] (φ : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) : (schemePointsMulEquiv n B) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = (Matrix.GeneralLinearGroup.map φ.toRingHom) ((schemePointsMulEquiv n A) p)

The scheme-valued point identification is covariantly natural in the value algebra. An R-algebra map A → B becomes precomposition by the reversed spectrum map and acts entrywise on the corresponding invertible matrix.