The subgroup scheme of GLₙ preserving a constant bilinear multiplication

For a commutative ring R, a natural number n, and a family of constant structure matrices C : Fin n → Matrix (Fin n) (Fin n) R, read Cₖ as the matrix of left multiplication by the kth basis vector of Rⁿ, so that the bilinear multiplication is the one with structure constants eₖ * eⱼ = ∑ᵢ (Cₖ)ᵢⱼ eᵢ. A matrix M is multiplicative for that product exactly when

M Cₖ = (∑ₐ Mₐₖ Cₐ) M

for every k: the left-hand side sends x to M (eₖ * x), the right-hand side sends x to (M eₖ) * (M x), and linearity in the first argument reduces multiplicativity to the basis vectors. The entries of the relation matrices X Cₖ − (∑ₐ Xₐₖ Cₐ) X — X the localized generic matrix of GL n, the Cₐ read in the coordinate Hopf algebra through the structure morphism — generate a Hopf ideal in the coordinate Hopf algebra of GL n. Its quotient represents the closed subgroup scheme of GL n preserving the multiplication, whose points over a commutative R-algebra A are the invertible matrices multiplicative for the transported product.

Nothing is assumed of C: the multiplication is an arbitrary bilinear map Rⁿ × Rⁿ → Rⁿ, not required to be associative, commutative, alternating, or unital, and the construction includes n = 0 and the zero ring. Multiplication by a fixed constant matrix, composition algebras, and Lie brackets are all instances.

The three Hopf-ideal closure conditions are proved by matrix algebra rather than coordinate by coordinate, from three identities satisfied by the relation matrices f_k(M) := M Cₖ − (∑ₐ Mₐₖ Cₐ) M of an arbitrary matrix M over an arbitrary commutative R-algebra:

• f_k(1) = 0, so the counit, which sends X to the identity matrix, kills every generator;
• f_k(M N) = M f_k(N) + (∑ₐ Nₐₖ f_a(M)) N, so the comultiplication, which sends X to Y Z for Y and Z the two tensor inclusions of X, sends a generator into the sum of the right and left tensor ideals of the generators;
• f_k(N) = −N (∑ₐ Nₐₖ f_a(M)) N whenever M N = N M = 1, so the antipode, which sends X to its inverse matrix, sends a generator into the span of the generators.

The middle identity also says that the matrices preserving the multiplication are closed under multiplication, and the last that they are closed under inversion.

Main declarations

• TauCeti.ConstantMultiplication.imageStructureMatrix and TauCeti.ConstantMultiplication.relationMatrix: the matrix ∑ₐ Mₐₖ Cₐ of left multiplication by M eₖ, and the matrix of defining relations M Cₖ − (∑ₐ Mₐₖ Cₐ) M, with TauCeti.ConstantMultiplication.imageStructureMatrix_map and TauCeti.ConstantMultiplication.relationMatrix_map transporting both along an algebra morphism of value rings.
• TauCeti.ConstantMultiplication.Preserves: multiplicativity of a matrix for the product, with TauCeti.ConstantMultiplication.preserves_one, TauCeti.ConstantMultiplication.Preserves.mul, TauCeti.ConstantMultiplication.Preserves.of_mul_eq_one, and TauCeti.ConstantMultiplication.Preserves.map.
• TauCeti.ConstantMultiplication.preserves_toMatrix_iff: when C consists of the structure matrices of an algebra in a basis, a matrix preserves the multiplication exactly when the linear endomorphism it represents is multiplicative.
• TauCeti.ConstantMultiplication.definingHopfIdeal: the Hopf ideal generated by the entries of the relation matrices of the generic matrix.
• TauCeti.ConstantMultiplication.definingHopfIdeal_toIdeal_le_ker_of_preserves_map_genericMatrix: a coordinate morphism whose generic matrix preserves the multiplication kills the defining ideal.
• TauCeti.ConstantMultiplication.coordinateHopfAlgebra and TauCeti.ConstantMultiplication.coordinateMap: the quotient coordinate Hopf algebra and the quotient morphism onto it, with TauCeti.ConstantMultiplication.preserves_map_genericMatrix_coordinateMap saying that the transported generic matrix preserves the multiplication.
• TauCeti.ConstantMultiplication.groupScheme and TauCeti.ConstantMultiplication.inclusion: the subgroup scheme preserving the multiplication and its closed immersion into the general linear group scheme.
• TauCeti.ConstantMultiplication.mem_definingPointsSubgroup_iff: an ambient point is cut out exactly when its matrix preserves the multiplication.

References

• J. S. Milne, Algebraic Groups (2017), §2.3, where subgroups of GLₙ are cut out by the entries of a matrix relation, and §24, where automorphism group schemes of algebras appear.
• W. C. Waterhouse, Introduction to Affine Group Schemes (1979), Chapter 1, for such groups as representable functors on commutative rings.
• The Stacks Project, Tag 022W, for the ambient general linear group scheme.

The declaration order and the shape of the closure proofs follow TauCeti.ConstantForm, which carries out the same programme for the relation X C Xᵀ − C of a single constant matrix; the three identities above and the reduction of the closure conditions to them are specific to this file.

def TauCeti.ConstantMultiplication.imageStructureMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) (k : Fin n) : Matrix (Fin n) (Fin n) S

The structure matrix of the image of the kth basis vector under M: the combination ∑ₐ Mₐₖ Cₐ, which is the matrix of left multiplication by M eₖ.

Equations

• TauCeti.ConstantMultiplication.imageStructureMatrix R n C M k = ∑ a : Fin n, M a k • (C a).map ⇑(algebraMap R S)

theorem TauCeti.ConstantMultiplication.imageStructureMatrix_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) (k : Fin n) : imageStructureMatrix R n C M k = ∑ a : Fin n, M a k • (C a).map ⇑(algebraMap R S)

The image structure matrix is the combination of the structure matrices weighted by the kth column of M.

def TauCeti.ConstantMultiplication.relationMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) (k : Fin n) : Matrix (Fin n) (Fin n) S

The matrix of defining relations of M at the index k: M Cₖ − (∑ₐ Mₐₖ Cₐ) M.

Equations

• TauCeti.ConstantMultiplication.relationMatrix R n C M k = M * (C k).map ⇑(algebraMap R S) - TauCeti.ConstantMultiplication.imageStructureMatrix R n C M k * M

theorem TauCeti.ConstantMultiplication.relationMatrix_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) (k : Fin n) : relationMatrix R n C M k = M * (C k).map ⇑(algebraMap R S) - imageStructureMatrix R n C M k * M

The relation matrix compares left multiplication by eₖ transported by M with left multiplication by the image of eₖ.

def TauCeti.ConstantMultiplication.Preserves (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) : Prop

A matrix preserves the multiplication given by the structure matrices C when it is multiplicative for it, M (x * y) = (M x) * (M y), written as one matrix identity for each basis vector of the first argument.

Equations

• TauCeti.ConstantMultiplication.Preserves R n C M = ∀ (k : Fin n), M * (C k).map ⇑(algebraMap R S) = TauCeti.ConstantMultiplication.imageStructureMatrix R n C M k * M

theorem TauCeti.ConstantMultiplication.preserves_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) : Preserves R n C M ↔ ∀ (k : Fin n), M * (C k).map ⇑(algebraMap R S) = imageStructureMatrix R n C M k * M

Preserving the multiplication is one matrix identity per basis vector.

theorem TauCeti.ConstantMultiplication.preserves_iff_relationMatrix_eq_zero (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M : Matrix (Fin n) (Fin n) S) : Preserves R n C M ↔ ∀ (k : Fin n), relationMatrix R n C M k = 0

Preserving the multiplication is the vanishing of every relation matrix.

Behaviour of the relation matrices under the group operations

@[simp]

theorem TauCeti.ConstantMultiplication.imageStructureMatrix_one (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (k : Fin n) : imageStructureMatrix R n C 1 k = (C k).map ⇑(algebraMap R S)

The image structure matrix of the identity is the structure matrix itself.

@[simp]

theorem TauCeti.ConstantMultiplication.relationMatrix_one (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (k : Fin n) : relationMatrix R n C 1 k = 0

The identity matrix satisfies every defining relation.

theorem TauCeti.ConstantMultiplication.sum_smul_imageStructureMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M N : Matrix (Fin n) (Fin n) S) (k : Fin n) : ∑ a : Fin n, N a k • imageStructureMatrix R n C M a = imageStructureMatrix R n C (M * N) k

The image structure matrices of a product are recombined from those of the left factor by the column of the right factor.

theorem TauCeti.ConstantMultiplication.mul_imageStructureMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M N : Matrix (Fin n) (Fin n) S) (k : Fin n) : M * imageStructureMatrix R n C N k = ∑ a : Fin n, N a k • (M * (C a).map ⇑(algebraMap R S))

Left multiplication distributes across the image structure matrix: framing imageStructureMatrix N k on the left by M frames each structure matrix separately, M * imageStructureMatrix N k = ∑ₐ Nₐₖ • (M Cₐ), the structure matrices read in the value ring through its structure morphism.

theorem TauCeti.ConstantMultiplication.relationMatrix_mul (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] (M N : Matrix (Fin n) (Fin n) S) (k : Fin n) : relationMatrix R n C (M * N) k = M * relationMatrix R n C N k + (∑ a : Fin n, N a k • relationMatrix R n C M a) * N

The relation matrices of a product decompose into the relations of the two factors: f_k(M N) = M f_k(N) + (∑ₐ Nₐₖ f_a(M)) N.

theorem TauCeti.ConstantMultiplication.relationMatrix_of_mul_eq_one (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {M N : Matrix (Fin n) (Fin n) S} (h₁ : M * N = 1) (k : Fin n) : relationMatrix R n C N k = -((N * ∑ a : Fin n, N a k • relationMatrix R n C M a) * N)

The relation matrices of an inverse: f_k(N) = −N (∑ₐ Nₐₖ f_a(M)) N whenever M N = 1. For square matrices over a commutative ring that identity already makes N a two-sided inverse.

@[simp]

theorem TauCeti.ConstantMultiplication.imageStructureMatrix_map (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {T : Type w} [CommRing T] [Algebra R T] (φ : S →ₐ[R] T) (M : Matrix (Fin n) (Fin n) S) (l : Fin n) : (imageStructureMatrix R n C M l).map ⇑φ = imageStructureMatrix R n C (M.map ⇑φ) l

Mapping an image structure matrix through an algebra morphism gives the image structure matrix of the image matrix: the combination is taken with the entries of the matrix, which map along, and the structure matrices are constant.

@[simp]

theorem TauCeti.ConstantMultiplication.relationMatrix_map (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {T : Type w} [CommRing T] [Algebra R T] (φ : S →ₐ[R] T) (M : Matrix (Fin n) (Fin n) S) (k : Fin n) : (relationMatrix R n C M k).map ⇑φ = relationMatrix R n C (M.map ⇑φ) k

Mapping a relation matrix through an algebra morphism gives the relation matrix of the image matrix: the structure matrices are constant, so they map to themselves.

The matrices preserving the multiplication

@[simp]

theorem TauCeti.ConstantMultiplication.preserves_one (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] : Preserves R n C 1

The identity matrix preserves the multiplication.

theorem TauCeti.ConstantMultiplication.Preserves.mul (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {M N : Matrix (Fin n) (Fin n) S} (hM : Preserves R n C M) (hN : Preserves R n C N) : Preserves R n C (M * N)

A product of matrices preserving the multiplication preserves it.

theorem TauCeti.ConstantMultiplication.Preserves.of_mul_eq_one (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {M N : Matrix (Fin n) (Fin n) S} (hM : Preserves R n C M) (h₁ : M * N = 1) : Preserves R n C N

An inverse of a matrix preserving the multiplication preserves it. Only one of the two inverse identities is needed: for square matrices over a commutative ring it implies the other.

theorem TauCeti.ConstantMultiplication.Preserves.map (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {T : Type w} [CommRing T] [Algebra R T] {M : Matrix (Fin n) (Fin n) S} (hM : Preserves R n C M) (φ : S →ₐ[R] T) : Preserves R n C (M.map ⇑φ)

Preserving the multiplication is stable under an algebra morphism of value rings.

Structure matrices of an algebra with a basis

When the structure matrices C k are those of an actual algebra B over S with a basis b, that is, when C k read in S is the matrix in b of left multiplication by b k, preserving the multiplication is exactly multiplicativity of the linear endomorphism of B that the matrix represents in b.

theorem TauCeti.ConstantMultiplication.imageStructureMatrix_toMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {B : Type w} [NonUnitalNonAssocSemiring B] [Module S B] [IsScalarTower S B B] [SMulCommClass S B B] (b : Module.Basis (Fin n) S B) (hC : ∀ (k : Fin n), (LinearMap.toMatrix b b) (LinearMap.mulLeft S (b k)) = (C k).map ⇑(algebraMap R S)) (f : B →ₗ[S] B) (k : Fin n) : imageStructureMatrix R n C ((LinearMap.toMatrix b b) f) k = (LinearMap.toMatrix b b) (LinearMap.mulLeft S (f (b k)))

If the structure matrices of a basis b are the C k, then the image structure matrix at k of the matrix of a linear endomorphism f is the matrix of left multiplication by f (b k).

theorem TauCeti.ConstantMultiplication.preserves_toMatrix_iff (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {S : Type v} [CommRing S] [Algebra R S] {B : Type w} [NonUnitalNonAssocSemiring B] [Module S B] [IsScalarTower S B B] [SMulCommClass S B B] (b : Module.Basis (Fin n) S B) (hC : ∀ (k : Fin n), (LinearMap.toMatrix b b) (LinearMap.mulLeft S (b k)) = (C k).map ⇑(algebraMap R S)) (f : B →ₗ[S] B) : Preserves R n C ((LinearMap.toMatrix b b) f) ↔ ∀ (x y : B), f (x * y) = f x * f y

Preserving the multiplication is multiplicativity. If the structure matrices of a basis b of a non-unital, non-associative S-algebra B are the C k, then the matrix in b of a linear endomorphism f of B preserves the multiplication exactly when f is multiplicative.

The defining relations over the coordinate Hopf algebra of GLₙ

def TauCeti.ConstantMultiplication.relationSet (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : Set ↑(GeneralLinear.coordinateHopfAlgebra R n)

The set of defining relations: the entries of the relation matrices of the generic matrix.

Equations

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

theorem TauCeti.ConstantMultiplication.relationMatrix_genericMatrix_mem_relationSet (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) (k i j : Fin n) : relationMatrix R n C (GeneralLinear.genericMatrix R n) k i j ∈ relationSet R n C

Every entry of every relation matrix of the generic matrix is a defining relation.

@[simp]

theorem TauCeti.ConstantMultiplication.mem_relationSet_iff (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {x : ↑(GeneralLinear.coordinateHopfAlgebra R n)} : x ∈ relationSet R n C ↔ ∃ (k : Fin n) (i : Fin n) (j : Fin n), relationMatrix R n C (GeneralLinear.genericMatrix R n) k i j = x

An element is a defining relation exactly when it is an entry of a relation matrix of the generic matrix.

The three Hopf-ideal closure conditions

The defining Hopf ideal and quotient

noncomputable def TauCeti.ConstantMultiplication.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R n)

The Hopf ideal preserving the multiplication: the ideal of the coordinate Hopf algebra of GL n generated by the entries of the relation matrices X Cₖ − (∑ₐ Xₐₖ Cₐ) X, with the three closure conditions extended from the generators across the span.

Equations

• TauCeti.ConstantMultiplication.definingHopfIdeal R n C = TauCeti.HopfIdeal.ofSpan (TauCeti.ConstantMultiplication.relationSet R n C) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.ConstantMultiplication.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : (definingHopfIdeal R n C).toIdeal = Ideal.span (relationSet R n C)

The underlying ideal of the defining Hopf ideal is the span of the defining relations.

theorem TauCeti.ConstantMultiplication.definingHopfIdeal_toIdeal_le_ker_of_preserves_map_genericMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {T : Type w} [CommRing T] [Algebra R T] (φ : ↑(GeneralLinear.coordinateHopfAlgebra R n) →ₐ[R] T) (hφ : Preserves R n C ((GeneralLinear.genericMatrix R n).map ⇑φ)) : (definingHopfIdeal R n C).toIdeal ≤ RingHom.ker ↑φ

A coordinate morphism whose generic matrix preserves the multiplication kills the defining ideal. This is the criterion by which a subgroup of GL n given by generating morphisms is shown to lie in the subgroup scheme preserving the multiplication: it suffices to evaluate the relations on the generic matrix of each generator.

@[reducible, inline]

noncomputable abbrev TauCeti.ConstantMultiplication.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : CommHopfAlgCat R

The coordinate Hopf algebra of the subgroup scheme of GL n preserving the multiplication.

Equations

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

noncomputable def TauCeti.ConstantMultiplication.coordinateMap (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n C

The quotient coordinate morphism from O(GL n) to the coordinate Hopf algebra of the subgroup scheme preserving the multiplication.

Equations

• TauCeti.ConstantMultiplication.coordinateMap R n C = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.ConstantMultiplication.definingHopfIdeal R n C)

theorem TauCeti.ConstantMultiplication.coordinateMap_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : coordinateMap R n C = CommHopfAlgCat.mkQuotient (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C)

The coordinate map is the canonical quotient morphism by the defining Hopf ideal.

@[simp]

theorem TauCeti.ConstantMultiplication.coordinateMap_relationMatrix (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) (k i j : Fin n) : (CommHopfAlgCat.Hom.hom (coordinateMap R n C)) (relationMatrix R n C (GeneralLinear.genericMatrix R n) k i j) = 0

Every defining relation vanishes in the quotient coordinate Hopf algebra.

@[simp]

theorem TauCeti.ConstantMultiplication.preserves_map_genericMatrix_coordinateMap (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : Preserves R n C ((GeneralLinear.genericMatrix R n).map ⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n C)))

The generic matrix of the quotient preserves the multiplication: transporting the generic matrix of GL n along the quotient coordinate morphism gives a matrix over the quotient coordinate Hopf algebra that is multiplicative for the product, since exactly the entries of its relation matrices were divided out.

The group scheme and its closed immersion

@[reducible, inline]

noncomputable abbrev TauCeti.ConstantMultiplication.groupScheme (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The subgroup scheme of GL n preserving the multiplication.

Equations

• TauCeti.ConstantMultiplication.groupScheme R n C = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.ConstantMultiplication.definingHopfIdeal R n C)

theorem TauCeti.ConstantMultiplication.groupScheme_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : groupScheme R n C = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C)

The subgroup scheme preserving the multiplication is the quotient spectrum of its coordinate Hopf algebra.

noncomputable def TauCeti.ConstantMultiplication.inclusion (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : groupScheme R n C ⟶ GeneralLinear.groupScheme R n

The closed-subgroup inclusion into the named general linear group scheme: the generic Hopf-ideal closed immersion GeneralLinear.hopfIdealInclusion at the defining Hopf ideal.

Equations

• TauCeti.ConstantMultiplication.inclusion R n C = TauCeti.GeneralLinear.hopfIdealInclusion R n (TauCeti.ConstantMultiplication.definingHopfIdeal R n C)

theorem TauCeti.ConstantMultiplication.inclusion_def (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : inclusion R n C = GeneralLinear.hopfIdealInclusion R n (definingHopfIdeal R n C)

The inclusion is the generic Hopf-ideal closed immersion at the defining Hopf ideal.

instance TauCeti.ConstantMultiplication.isClosedImmersion_inclusion (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (inclusion R n C).hom.hom)

The inclusion into the named general linear group scheme is a closed immersion.

Algebra-valued points

theorem TauCeti.ConstantMultiplication.mem_definingPointsSubgroup_iff (R : Type u) [CommRing R] (n : ℕ) (C : Fin n → Matrix (Fin n) (Fin n) R) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n C) ↧A ↔ Preserves R n C ↑((GeneralLinear.pointsMulEquiv n) g)

The ambient membership criterion: an ambient point belongs to the subgroup cut out by the defining Hopf ideal exactly when its matrix preserves the multiplication.