Presented matrix points over the integers

A subgroup of GLₙ(A) presented by a fixed integral Hopf ideal inherits entrywise maps of value rings and a representing equivalence with points of the quotient coordinate algebra. IntegralPointsPresentation records the subgroup and its presentation. Its API supplies these constructions uniformly, including their functoriality and naturality.

A family of presentations over commutative rings determines a group-valued functor on commutative ℤ-algebras. The quotient coordinate Hopf algebra represents this functor. Presentations over different universes can be used together in the induced maps of points.

The constructions transport the API of TauCeti.Algebra.AlgebraicGroup.GeneralLinear.HopfIdealPoints.Functor along the presentation equalities. The specialization to ℤ allows arbitrary ring homomorphisms as value-ring maps.

Formal provenance

This API is extracted from the functorial-points interfaces of the seven integral carriers:

• TauCeti.SlStd (#5212) and TauCeti.SpStd (#5172);
• TauCeti.TypeBSpinCarrier (#5552) and TauCeti.TypeDSpinCarrier (#5353);
• TauCeti.E6Minuscule (#5265), TauCeti.E6DoubledMinuscule (#5404), and TauCeti.E7Minuscule (#5471).

Those interfaces supplied the declaration order and proof templates consolidated here. The doubled E₆ and E₇ interfaces followed the E₆ minuscule interface; the E₆ minuscule and type-D interfaces followed the type-A and type-C interfaces. The type-B interface followed the type-D spin interface. The earlier type-A and type-C interfaces also drew on TauCeti.DynkinType's pinned Geck-carrier points API. Their Carter and Jantzen references remain in the carrier modules, where they describe the underlying group constructions.

@[reducible, inline]

abbrev TauCeti.GeneralLinear.IntegralPointsPresentation (n : ℕ) (I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)) (A : Type v) [CommRing A] : Type v

A matrix subgroup over a value ring, presented by an integral Hopf ideal.

Equations

• TauCeti.GeneralLinear.IntegralPointsPresentation n I A = { subgroup : Subgroup (GL (Fin n) A) // subgroup = TauCeti.GeneralLinear.hopfIdealPointsSubgroup n I A }

noncomputable def TauCeti.GeneralLinear.IntegralPointsPresentation.map {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} {B : Type w} [CommRing A] [CommRing B] (P : IntegralPointsPresentation n I A) (Q : IntegralPointsPresentation n I B) (f : A →+* B) : ↥↑P →* ↥↑Q

The map of presented points induced by a homomorphism of value rings.

Equations

• P.map Q f = TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr n I ⋯ ⋯ f.toIntAlgHom

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.coe_map {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} {B : Type w} [CommRing A] [CommRing B] (P : IntegralPointsPresentation n I A) (Q : IntegralPointsPresentation n I B) (f : A →+* B) (g : ↥↑P) : ↑((P.map Q f) g) = (Matrix.GeneralLinearGroup.map f) ↑g

The map of presented points is the entrywise matrix map.

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.coe_map_apply {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} {B : Type w} [CommRing A] [CommRing B] (P : IntegralPointsPresentation n I A) (Q : IntegralPointsPresentation n I B) (f : A →+* B) (g : ↥↑P) (i j : Fin n) : ↑↑((P.map Q f) g) i j = f (↑↑g i j)

The induced map applies the value-ring homomorphism to each matrix coefficient.

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.map_id {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} [CommRing A] (P : IntegralPointsPresentation n I A) : P.map P (RingHom.id A) = MonoidHom.id ↥↑P

The identity homomorphism induces the identity on presented points.

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.map_comp {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} {B : Type w} {C : Type z} [CommRing A] [CommRing B] [CommRing C] (P : IntegralPointsPresentation n I A) (Q : IntegralPointsPresentation n I B) (S : IntegralPointsPresentation n I C) (f : A →+* B) (g : B →+* C) : P.map S (g.comp f) = (Q.map S g).comp (P.map Q f)

Maps of presented points compose through any presentation of the intermediate point group.

The intermediate presentation Q occurs only on the right, so simp cannot infer it. Use this theorem explicitly, supplying Q, rather than as a simplification rule.

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.map_injective {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : Type v} {B : Type w} [CommRing A] [CommRing B] (P : IntegralPointsPresentation n I A) (Q : IntegralPointsPresentation n I B) {f : A →+* B} (hf : Function.Injective ⇑f) : Function.Injective ⇑(P.map Q f)

An injective homomorphism of value rings induces an injective map of presented points.

noncomputable def TauCeti.GeneralLinear.IntegralPointsPresentation.mulEquiv {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : CommAlgCat ℤ} (P : IntegralPointsPresentation n I ↑A) : ↑(HopfAlgebra.points A) ≃* ↥↑P

Quotient coordinate-algebra points are the presented matrix points.

Equations

• P.mulEquiv = (TauCeti.GeneralLinear.hopfIdealPointsSubgroupMulEquiv n I A).trans (MulEquiv.subgroupCongr ⋯).symm

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.coe_mulEquiv_apply {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : CommAlgCat ℤ} (P : IntegralPointsPresentation n I ↑A) (q : ↑(HopfAlgebra.points A)) : ↑(P.mulEquiv q) = (pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra ℤ n) I A)) q)

A quotient point is its underlying general-linear point read as a matrix.

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.quotientPointsHom_mulEquiv_symm {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A : CommAlgCat ℤ} (P : IntegralPointsPresentation n I ↑A) (g : ↥↑P) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (coordinateHopfAlgebra ℤ n) I A)) (P.mulEquiv.symm g) = (pointsMulEquiv n).symm ↑g

The inverse representing equivalence recovers the ambient point of the underlying matrix.

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.mulEquiv_mapPoints {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} {A B : CommAlgCat ℤ} (P : IntegralPointsPresentation n I ↑A) (Q : IntegralPointsPresentation n I ↑B) (f : A ⟶ B) (q : ↑(HopfAlgebra.points A)) : Q.mulEquiv ((CategoryTheory.ConcreteCategory.hom (HopfAlgebra.mapPoints f)) q) = (P.map Q ↑(CommAlgCat.Hom.hom f)) (P.mulEquiv q)

The representing equivalence is natural in the value algebra.

The source presentation occurs only on the right, so this is not a simplification rule.

noncomputable def TauCeti.GeneralLinear.IntegralPointsPresentation.functor {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) : CategoryTheory.Functor (CommAlgCat ℤ) GrpCat

A family of presentations gives a group-valued functor on commutative integer algebras.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.functor_obj {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) (A : CommAlgCat ℤ) : (functor P).obj A = ↧↥↑(P ↑A)

The object part is the chosen subgroup of matrices.

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.functor_map {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) {A B : CommAlgCat ℤ} (f : A ⟶ B) : (functor P).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom ((P ↑A).map (P ↑B) ↑(CommAlgCat.Hom.hom f))) (CategoryTheory.eqToHom ⋯))

The morphism part is the map of presented points.

noncomputable def TauCeti.GeneralLinear.IntegralPointsPresentation.natIso {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) : HopfAlgebra.pointsFunctor ≅ functor P

The quotient coordinate Hopf algebra represents a family of presented matrix point groups.

Equations

• TauCeti.GeneralLinear.IntegralPointsPresentation.natIso P = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat ℤ) => (P ↑A).mulEquiv.toGrpIso) ⋯

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.natIso_hom_app_apply {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) (A : CommAlgCat ℤ) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((natIso P).hom.app A)) q) = (P ↑A).mulEquiv q

The forward component of the representing isomorphism is the pointwise equivalence.

@[simp]

theorem TauCeti.GeneralLinear.IntegralPointsPresentation.natIso_inv_app_apply {n : ℕ} {I : HopfIdeal ℤ ↑(coordinateHopfAlgebra ℤ n)} (P : (A : Type v) → [inst : CommRing A] → IntegralPointsPresentation n I A) (A : CommAlgCat ℤ) (g : ↥↑(P ↑A)) : (CategoryTheory.ConcreteCategory.hom ((natIso P).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (P ↑A).mulEquiv.symm g

The inverse component of the representing isomorphism is the inverse pointwise equivalence.