Endomorphisms of a generated subgroup scheme of GLₙ on matrix points

Let G be the closed subgroup scheme of GLₙ over R generated by a family of coordinate morphisms f i : O(GLₙ/R) ⟶ K i, and let ψ : O(GLₙ/R) ⟶ O(G) be a morphism of commutative Hopf algebras, that is, a homomorphism G → GLₙ. When ψ is killed by the defining Hopf ideal of G — which the generator criteria of TauCeti.Algebra.AlgebraicGroup.HopfIdeal.CommonKernel.Endomorphism supply — the homomorphism maps G into G, and this file records the resulting endomorphism of the group of matrix points of G over every R-algebra.

The defining property below reads a coordinate of the image matrix: it is the value at the argument point of any representative of the transported coordinate. Together with the generic matrix of ψ this determines the image matrix entrywise.

Main declarations

In the namespace TauCeti.GeneralLinear:

• pointsMulEquiv_mapPointsFunctor_mem_generatedPointsSubgroup_of_le_ker: the image of a point of the generated subgroup scheme is again one of its points.
• generatedPointsEndomorphism: the induced endomorphism of the matrix points.
• ofConv_pointsMulEquiv_symm_generatedPointsEndomorphism: its defining property.

References

• R. W. Carter, Simple Groups of Lie Type, §§7.1 and 12.2.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_mem_generatedPointsSubgroup_of_le_ker {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (hψ : (CommHopfAlgCat.commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (A : Type w) [CommRing A] [Algebra R A] (p : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor ψ).app ↧A)) p) ∈ generatedPointsSubgroup n f A

A point of the generated subgroup scheme is carried by ψ to a point of it.

noncomputable def TauCeti.GeneralLinear.generatedPointsUnderlyingMap {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (A : Type w) [CommRing A] [Algebra R A] : ↥(generatedPointsSubgroup n f A) →* GL (Fin n) A

The ambient matrix map underlying the endomorphism represented by ψ, restricted in its domain to the generated point subgroup.

Equations

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

theorem TauCeti.GeneralLinear.generatedPointsUnderlyingMap_apply {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (A : Type w) [CommRing A] [Algebra R A] (g : ↥(generatedPointsSubgroup n f A)) : (generatedPointsUnderlyingMap n ψ A) g = (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor ψ).app ↧A)) ((hopfIdealPointsSubgroupMulEquiv n (CommHopfAlgCat.commonKernelHopfIdeal f) ↧A).symm ((MulEquiv.subgroupCongr ⋯) g)))

The underlying matrix map evaluates ψ on the quotient point corresponding to its argument.

theorem TauCeti.GeneralLinear.generatedPointsUnderlyingMap_mem {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (hψ : (CommHopfAlgCat.commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (A : Type w) [CommRing A] [Algebra R A] (g : ↥(generatedPointsSubgroup n f A)) : (generatedPointsUnderlyingMap n ψ A) g ∈ generatedPointsSubgroup n f A

The underlying matrix map lands in the generated point subgroup.

noncomputable def TauCeti.GeneralLinear.generatedPointsEndomorphism {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (hψ : (CommHopfAlgCat.commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (A : Type w) [CommRing A] [Algebra R A] : ↥(generatedPointsSubgroup n f A) →* ↥(generatedPointsSubgroup n f A)

The endomorphism of the matrix points of a generated subgroup scheme of GLₙ restricting the homomorphism to GLₙ represented by ψ.

Equations

• TauCeti.GeneralLinear.generatedPointsEndomorphism n ψ hψ A = (TauCeti.GeneralLinear.generatedPointsUnderlyingMap n ψ A).codRestrict (TauCeti.GeneralLinear.generatedPointsSubgroup n f A) ⋯

theorem TauCeti.GeneralLinear.coe_generatedPointsEndomorphism {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (hψ : (CommHopfAlgCat.commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (A : Type w) [CommRing A] [Algebra R A] (g : ↥(generatedPointsSubgroup n f A)) : ↑((generatedPointsEndomorphism n ψ hψ A) g) = (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor ψ).app ↧A)) ((hopfIdealPointsSubgroupMulEquiv n (CommHopfAlgCat.commonKernelHopfIdeal f) ↧A).symm ((MulEquiv.subgroupCongr ⋯) g)))

The underlying matrix of the generated point endomorphism is obtained by applying the represented point map to the corresponding quotient point.

theorem TauCeti.GeneralLinear.ofConv_pointsMulEquiv_symm_generatedPointsEndomorphism {R : Type u} [CommRing R] (n : ℕ) {ι : Type v} {K : ι → CommHopfAlgCat R} {f : (i : ι) → coordinateHopfAlgebra R n ⟶ K i} (ψ : coordinateHopfAlgebra R n ⟶ CommHopfAlgCat.quotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f)) (hψ : (CommHopfAlgCat.commonKernelHopfIdeal f).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom ψ)).toRingHom) (A : Type w) [CommRing A] [Algebra R A] (g : ↥(generatedPointsSubgroup n f A)) (x y : ↑(coordinateHopfAlgebra R n)) (hxy : (CommHopfAlgCat.Hom.hom (CommHopfAlgCat.mkQuotient (coordinateHopfAlgebra R n) (CommHopfAlgCat.commonKernelHopfIdeal f))) y = (CommHopfAlgCat.Hom.hom ψ) x) : ((pointsMulEquiv n).symm ↑((generatedPointsEndomorphism n ψ hψ A) g)).ofConv x = ((pointsMulEquiv n).symm ↑g).ofConv y

The defining property of the point endomorphism: the point of the image matrix evaluates an ambient coordinate at the point of the argument, after transporting that coordinate along ψ and choosing any representative of the result.