General-linear points cut out by Hopf ideals

This file transports the algebra-valued points of a quotient of the coordinate Hopf algebra of GLₙ through GeneralLinear.pointsMulEquiv. The resulting matrix subgroup is characterized by vanishing on the Hopf ideal and is functorial in the value algebra.

Main declarations

• TauCeti.GeneralLinear.hopfIdealPointsSubgroup: the matrix subgroup cut out by a Hopf ideal in the general-linear coordinate ring.
• TauCeti.GeneralLinear.mem_hopfIdealPointsSubgroup_iff: membership is characterized by vanishing on the Hopf ideal, with TauCeti.GeneralLinear.pointToGeneralLinear_mem_hopfIdealPointsSubgroup_iff_toIdeal_le_ker reading it as a kernel containment for an algebra-valued point.
• TauCeti.GeneralLinear.hopfIdealPointsSubgroup_le_of_le: larger Hopf ideals cut out smaller point subgroups.
• TauCeti.GeneralLinear.hopfIdealPointsSubgroup_sup: a join of Hopf ideals cuts out the intersection of the point subgroups.
• TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup: functoriality of that subgroup in the value algebra.
• TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup_injective: an injective homomorphism of value algebras induces an injective map of point subgroups.
• TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_subalgebra: the points valued in a subalgebra are the ambient points that descend to it.
• TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr: that functoriality read through presentations of two subgroups as point subgroups, so that a carrier defined by a Hopf ideal states its induced map in its own named API.

noncomputable def TauCeti.GeneralLinear.hopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] : Subgroup (GL (Fin n) A)

The subgroup of GLₙ(A) cut out by a Hopf ideal in the general-linear coordinate Hopf algebra.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.mem_hopfIdealPointsSubgroup_iff {R : Type u} [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] (g : GL (Fin n) A) : g ∈ hopfIdealPointsSubgroup n I A ↔ ∀ x ∈ I, ((pointsMulEquiv n).symm g).ofConv x = 0

Membership in the general-linear point subgroup cut out by a Hopf ideal is vanishing on that ideal.

theorem TauCeti.GeneralLinear.pointsMulEquiv_mem_hopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] (q : ↑(HopfAlgebra.points ↧A)) (hq : q ∈ CommHopfAlgCat.quotientPointsSubgroup (coordinateHopfAlgebra R n) I ↧A) : (pointsMulEquiv n) q ∈ hopfIdealPointsSubgroup n I A

A general-linear point lying in the subgroup cut out by a Hopf ideal remains in that subgroup after transport to its matrix representation.

theorem TauCeti.GeneralLinear.pointsMulEquiv_mapPointsFunctor_mem_hopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {H : CommHopfAlgCat R} (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (φ : coordinateHopfAlgebra R n ⟶ H) (hφ : I.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) ∈ hopfIdealPointsSubgroup n I A

A point pulled back along a coordinate morphism that kills a Hopf ideal lies in the general-linear subgroup cut out by that ideal.

theorem TauCeti.GeneralLinear.pointToGeneralLinear_mem_hopfIdealPointsSubgroup_iff_toIdeal_le_ker {R : Type u} [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] (chi : ↑(coordinateHopfAlgebra R n) →ₐ[R] A) : pointToGeneralLinear n (WithConv.toConv chi) ∈ hopfIdealPointsSubgroup n I A ↔ I.toIdeal ≤ RingHom.ker chi.toRingHom

An A-valued point lies in the subgroup cut out by a Hopf ideal exactly when its algebra homomorphism kills that ideal.

theorem TauCeti.GeneralLinear.map_mem_hopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (φ : A →ₐ[R] B) {g : GL (Fin n) A} (hg : g ∈ hopfIdealPointsSubgroup n I A) : (Matrix.GeneralLinearGroup.map ↑φ) g ∈ hopfIdealPointsSubgroup n I B

Applying a value-algebra homomorphism entrywise preserves the general-linear point subgroup cut out by a Hopf ideal.

noncomputable def TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (φ : A →ₐ[R] B) : ↥(hopfIdealPointsSubgroup n I A) →* ↥(hopfIdealPointsSubgroup n I B)

The map between general-linear point subgroups cut out by the same Hopf ideal, induced by a homomorphism of value algebras.

Equations

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

@[simp]

theorem TauCeti.GeneralLinear.coe_mapHopfIdealPointsSubgroup {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (φ : A →ₐ[R] B) (g : ↥(hopfIdealPointsSubgroup n I A)) : ↑((mapHopfIdealPointsSubgroup n I φ) g) = (Matrix.GeneralLinearGroup.map ↑φ) ↑g

The induced map on a general-linear Hopf-ideal point subgroup applies the value-algebra homomorphism entrywise.

@[simp]

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup_id {R : Type u} [CommRing R] (n : ℕ) (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] : mapHopfIdealPointsSubgroup n I (AlgHom.id R A) = MonoidHom.id ↥(hopfIdealPointsSubgroup n I A)

The identity value-algebra homomorphism induces the identity on a general-linear Hopf-ideal point subgroup.

@[simp]

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup_comp {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {C : Type u_1} [CommRing C] [Algebra R C] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (φ : A →ₐ[R] B) (ψ : B →ₐ[R] C) : mapHopfIdealPointsSubgroup n I (ψ.comp φ) = (mapHopfIdealPointsSubgroup n I ψ).comp (mapHopfIdealPointsSubgroup n I φ)

Maps between general-linear Hopf-ideal point subgroups preserve composition of value-algebra homomorphisms.

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup_injective {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {φ : A →ₐ[R] B} (hφ : Function.Injective ⇑φ) : Function.Injective ⇑(mapHopfIdealPointsSubgroup n I φ)

An injective homomorphism of value algebras induces an injective map of general-linear Hopf-ideal point subgroups: reading a matrix point over a subalgebra as a point over the ambient algebra loses no information.

theorem TauCeti.GeneralLinear.map_hopfIdealPointsSubgroup_subalgebra {R : Type u} [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (S : Subalgebra R A) : Subgroup.map (Matrix.GeneralLinearGroup.map ↑S.val) (hopfIdealPointsSubgroup n I ↥S) = hopfIdealPointsSubgroup n I A ⊓ (Matrix.GeneralLinearGroup.map ↑S.val).range

The matrix points valued in a subalgebra, read in the ambient general linear group. They are exactly the A-valued points that are entrywise images of invertible matrices over the subalgebra: such a matrix kills the Hopf ideal over the subalgebra as soon as its image does over A, because the inclusion is injective.

Transport along a presentation of the point subgroup

A carrier cut out by a Hopf ideal typically carries its own points A together with a lemma points_def : points A = hopfIdealPointsSubgroup n I A. The declarations below read the functoriality above through two such presentations, so that a carrier states its induced map in its own named API rather than in the presentation that API is defined by.

noncomputable def TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {PA : Subgroup (GL (Fin n) A)} {PB : Subgroup (GL (Fin n) B)} (hA : PA = hopfIdealPointsSubgroup n I A) (hB : PB = hopfIdealPointsSubgroup n I B) (φ : A →ₐ[R] B) : ↥PA →* ↥PB

TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup read through presentations of two subgroups as Hopf-ideal point subgroups of the general linear group.

Equations

• TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr n I hA hB φ = MonoidHom.subgroupCongr hA hB (TauCeti.GeneralLinear.mapHopfIdealPointsSubgroup n I φ)

@[simp]

theorem TauCeti.GeneralLinear.coe_mapHopfIdealPointsSubgroupCongr {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {PA : Subgroup (GL (Fin n) A)} {PB : Subgroup (GL (Fin n) B)} (hA : PA = hopfIdealPointsSubgroup n I A) (hB : PB = hopfIdealPointsSubgroup n I B) (φ : A →ₐ[R] B) (g : ↥PA) : ↑((mapHopfIdealPointsSubgroupCongr n I hA hB φ) g) = (Matrix.GeneralLinearGroup.map ↑φ) ↑g

The transported map applies the value-algebra homomorphism entrywise.

@[simp]

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr_id {R : Type u} [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {PA : Subgroup (GL (Fin n) A)} (hA : PA = hopfIdealPointsSubgroup n I A) : mapHopfIdealPointsSubgroupCongr n I hA hA (AlgHom.id R A) = MonoidHom.id ↥PA

The identity value-algebra homomorphism induces the identity on a presented point subgroup.

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr_comp {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {C : Type u_1} [CommRing C] [Algebra R C] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {PA : Subgroup (GL (Fin n) A)} {PB : Subgroup (GL (Fin n) B)} {PC : Subgroup (GL (Fin n) C)} (hA : PA = hopfIdealPointsSubgroup n I A) (hB : PB = hopfIdealPointsSubgroup n I B) (hC : PC = hopfIdealPointsSubgroup n I C) (φ : A →ₐ[R] B) (ψ : B →ₐ[R] C) : mapHopfIdealPointsSubgroupCongr n I hA hC (ψ.comp φ) = (mapHopfIdealPointsSubgroupCongr n I hB hC ψ).comp (mapHopfIdealPointsSubgroupCongr n I hA hB φ)

The maps induced on presented point subgroups compose.

Not a simp lemma: the middle subgroup and its presentation appear only on the right-hand side, so simp would have to invent them and would rewrite into an unrelated instantiation. Rewrite pointwise through TauCeti.GeneralLinear.coe_mapHopfIdealPointsSubgroupCongr instead.

theorem TauCeti.GeneralLinear.mapHopfIdealPointsSubgroupCongr_injective {R : Type u} [CommRing R] (n : ℕ) {A : Type w} {B : Type w'} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (I : HopfIdeal R ↑(coordinateHopfAlgebra R n)) {PA : Subgroup (GL (Fin n) A)} {PB : Subgroup (GL (Fin n) B)} (hA : PA = hopfIdealPointsSubgroup n I A) (hB : PB = hopfIdealPointsSubgroup n I B) {φ : A →ₐ[R] B} (hφ : Function.Injective ⇑φ) : Function.Injective ⇑(mapHopfIdealPointsSubgroupCongr n I hA hB φ)

An injective value-algebra homomorphism induces an injective map of presented point subgroups.

theorem TauCeti.GeneralLinear.hopfIdealPointsSubgroup_le_of_le {R : Type u} [CommRing R] (n : ℕ) {I J : HopfIdeal R ↑(coordinateHopfAlgebra R n)} (hIJ : I ≤ J) (A : Type w) [CommRing A] [Algebra R A] : hopfIdealPointsSubgroup n J A ≤ hopfIdealPointsSubgroup n I A

Larger Hopf ideals cut out smaller general-linear point subgroups.

theorem TauCeti.GeneralLinear.hopfIdealPointsSubgroup_sup {R : Type u} [CommRing R] (n : ℕ) (I J : HopfIdeal R ↑(coordinateHopfAlgebra R n)) (A : Type w) [CommRing A] [Algebra R A] : hopfIdealPointsSubgroup n (I ⊔ J) A = hopfIdealPointsSubgroup n I A ⊓ hopfIdealPointsSubgroup n J A

A join of Hopf ideals cuts out the intersection of the point subgroups. Scheme-theoretic intersection of two closed subgroup schemes of GLₙ is intersection of their matrix points.