Base change of Hopf ideals

A closed subgroup scheme of Spec H is cut out by a Hopf ideal J of the coordinate Hopf algebra H. This file base-changes that description along a ring map k → K: the ideal of K ⊗[k] H generated by 1 ⊗ J is again a Hopf ideal, and quotienting by it produces the base change K ⊗[k] (H ⧸ J) of the original quotient. Geometrically, the closed subgroup scheme base-changes to a closed subgroup scheme of the base-changed ambient group, and its points over a K-algebra are the original points over the same algebra viewed over k.

The Hopf-ideal structure is obtained without checking the comultiplication condition again: the base-changed ideal is realized as the kernel of the base change of the quotient morphism, which is surjective, and the kernel of a surjective morphism of commutative Hopf algebras is a Hopf ideal (TauCeti.HopfIdeal.kerOfSurjective). Right exactness of the tensor product (Algebra.TensorProduct.lTensor_ker) then identifies that kernel with the extension of J along h ↦ 1 ⊗ h.

Main declarations

• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal: the base change J_K of a Hopf ideal J.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_toIdeal: J_K is generated by 1 ⊗ J.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_le_iff: along an injective scalar map, base change reflects containment of Hopf ideals when the larger quotient is flat over the base.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_toIdeal_le_ker_baseChangeMap: base-changing a morphism that kills J gives a morphism that kills J_K.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_augmentation: base change preserves the augmentation ideal, so the identity section base-changes to the identity section.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_le_iff_of_faithfullyFlat: faithfully flat base change reflects containment of Hopf ideals.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_injective: faithfully flat base change reflects equality of Hopf ideals.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_comapOfIso: base change commutes with pulling a Hopf ideal back along an ambient isomorphism.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal_le: the subgroup generated by a base-changed family sits inside the base change of the subgroup it generates.
• Module.Basis.mem_baseChangeHopfIdeal_iff: over a basis of K, an element lies in J_K exactly when all its coefficients lie in J.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal: when K is free over k, for instance a field extension, the two subgroups agree, so generation commutes with base change.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_baseChangeHopfIdeal: base change of Hopf ideals along a tower k → E → K agrees with one-step base change across the tower comparison.
• TauCeti.CommHopfAlgCat.quotientBaseChangeIso: the identification (K ⊗[k] H) ⧸ J_K ≅ K ⊗[k] (H ⧸ J).
• TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_of_quotientIso: an ambient base-change isomorphism carries a base-changed Hopf ideal onto a target ideal presented as the kernel of the base change of the quotient morphism.
• TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_kerOfSurjective: the specialization to kernels of surjective morphisms matched by base change.
• TauCeti.CommHopfAlgCat.quotientBaseChangeIsoOfMapEq: transport of this identification across an ambient base-change isomorphism carrying the base-changed ideal to a target ideal.
• TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientBaseChangeIso_hom: the identification is compatible with the two quotient morphisms.
• TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_baseChangeHopfIdeal_iff: a point of the base change lies in the base-changed closed subgroup exactly when its restriction lies in the original one.
• TauCeti.CommHopfAlgCat.isCentral_baseChangeHopfIdeal: base change preserves central Hopf ideals.

References

This supplies the Hopf-ideal infrastructure for the Layer 9 milestone "base change along ℤ → k for any commutative ring k" of TauCetiRoadmap/ReductiveGroups/README.md, transporting a Chevalley--Demazure carrier presented as a Hopf-ideal quotient. See J. S. Milne, Algebraic Groups (2017), §§1.d, 2.a, and W. C. Waterhouse, Introduction to Affine Group Schemes, §16.

noncomputable def TauCeti.CommHopfAlgCat.baseChangeHopfIdeal {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) : HopfIdeal K ↑(baseChange H)

The base change of a Hopf ideal J of H along k → K, as a Hopf ideal of K ⊗[k] H.

It is defined as the kernel of the base change of the quotient morphism H ⟶ H ⧸ J, which is surjective, so no Hopf-ideal condition has to be rechecked; TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_toIdeal identifies the underlying ideal with the one generated by 1 ⊗ J.

Equations

• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal J = TauCeti.HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom (TauCeti.CommHopfAlgCat.baseChangeMap (TauCeti.CommHopfAlgCat.mkQuotient H J))) ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_baseChangeHopfIdeal_iff {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) (y : ↑(baseChange H)) : y ∈ baseChangeHopfIdeal J ↔ (CommHopfAlgCat.Hom.hom (baseChangeMap (mkQuotient H J))) y = 0

Membership in the base-changed Hopf ideal is vanishing under the base-changed quotient morphism.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_toIdeal {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) : (baseChangeHopfIdeal J).toIdeal = Ideal.map Algebra.TensorProduct.includeRight J.toIdeal

The base change of a Hopf ideal is the ideal generated by 1 ⊗ J, that is, the extension of J along h ↦ 1 ⊗ h.

theorem TauCeti.CommHopfAlgCat.tmul_mem_baseChangeHopfIdeal {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {J : HopfIdeal k ↑H} (s : K) {h : ↑H} (hh : h ∈ J) : s ⊗ₜ[k] h ∈ baseChangeHopfIdeal J

A scalar multiple of a base-changed element of a Hopf ideal lies in its base change.

theorem TauCeti.CommHopfAlgCat.one_tmul_mem_baseChangeHopfIdeal {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {J : HopfIdeal k ↑H} {h : ↑H} (hh : h ∈ J) : 1 ⊗ₜ[k] h ∈ baseChangeHopfIdeal J

An element of a Hopf ideal lies in its base change, viewed through h ↦ 1 ⊗ h.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_mono {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {J J' : HopfIdeal k ↑H} (hJ : J ≤ J') : baseChangeHopfIdeal J ≤ baseChangeHopfIdeal J'

Base change of Hopf ideals is monotone.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_comapOfIso {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H L : CommHopfAlgCat k} (J : HopfIdeal k ↑L) (e : H ≅ L) : baseChangeHopfIdeal (J.comapOfSurjective (CommHopfAlgCat.Hom.hom e.hom) ⋯) = (baseChangeHopfIdeal J).comapOfSurjective (CommHopfAlgCat.Hom.hom (baseChangeMap e.hom)) ⋯

Base change commutes with pulling a Hopf ideal back along an ambient Hopf-algebra isomorphism.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_le_iff {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (halg : Function.Injective ⇑(algebraMap k K)) {J J' : HopfIdeal k ↑H} [Module.Flat k ↑(quotient H J')] : baseChangeHopfIdeal J ≤ baseChangeHopfIdeal J' ↔ J ≤ J'

Along an injective scalar map, base change reflects containment of Hopf ideals when the quotient by the larger ideal is flat over the base. In particular, this applies to every field extension.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_le_iff_of_faithfullyFlat {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} [Module.FaithfullyFlat k K] (J J' : HopfIdeal k ↑H) : baseChangeHopfIdeal J ≤ baseChangeHopfIdeal J' ↔ J ≤ J'

Faithfully flat base change preserves and reflects containment of Hopf ideals.

Contravariantly, one closed subgroup scheme is contained in another exactly when the same is true after base change.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_injective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} [Module.FaithfullyFlat k K] : Function.Injective baseChangeHopfIdeal

Faithfully flat base change reflects equality of Hopf ideals.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_toIdeal_le_ker_baseChangeMap {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H N : CommHopfAlgCat k} (J : HopfIdeal k ↑H) (f : H ⟶ N) (hJ : J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom) : (baseChangeHopfIdeal J).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (baseChangeMap f))).toRingHom

If a Hopf ideal is killed by a morphism, its base change is killed by the base change of that morphism. This is the ideal-theoretic form of compatibility between closed subgroup factorizations and base change.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_bot {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} : baseChangeHopfIdeal ⊥ = ⊥

The base change of the trivial Hopf ideal is trivial.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_augmentation {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} : baseChangeHopfIdeal (HopfIdeal.augmentation k ↑H) = HopfIdeal.augmentation K ↑(baseChange H)

Base change preserves the augmentation ideal: the identity section of a base-changed affine group scheme is the base change of the identity section.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal_le {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {ι : Type y} {N : ι → CommHopfAlgCat k} (f : (i : ι) → H ⟶ N i) : baseChangeHopfIdeal (commonKernelHopfIdeal f) ≤ commonKernelHopfIdeal fun (i : ι) => baseChangeMap (f i)

The base change of the largest Hopf ideal killed by a family of morphisms is killed by the base change of that family.

Contravariantly: the closed subgroup scheme generated by a base-changed family of morphisms is a closed subgroup scheme of the base change of the one generated by the original family. The reverse containment holds when K is free over k: see TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal.

Free base change

When K is free as a k-module, an element of K ⊗[k] H is determined by its coefficients in a basis of K. Taking coefficients of the elements of a Hopf ideal of K ⊗[k] H produces a Hopf ideal of H, which gives the reverse of baseChangeHopfIdeal_commonKernelHopfIdeal_le.

theorem Module.Basis.mem_baseChangeHopfIdeal_iff {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {κ : Type u_1} [DecidableEq κ] (b : Basis κ k K) (J : TauCeti.HopfIdeal k ↑H) (y : ↑(TauCeti.CommHopfAlgCat.baseChange H)) : y ∈ TauCeti.CommHopfAlgCat.baseChangeHopfIdeal J ↔ ∀ (j : κ), ((TensorProduct.equivFinsuppOfBasisLeft b) y) j ∈ J

Over a basis of K, membership in a base-changed Hopf ideal J_K is membership of every coefficient in J.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {ι : Type y} {N : ι → CommHopfAlgCat k} [Module.Free k K] (f : (i : ι) → H ⟶ N i) : baseChangeHopfIdeal (commonKernelHopfIdeal f) = commonKernelHopfIdeal fun (i : ι) => baseChangeMap (f i)

Generation commutes with free base change. If K is free as a k-module, for instance a field extension, then the base change of the largest Hopf ideal killed by a family of morphisms is the largest Hopf ideal killed by the base-changed family.

Contravariantly: the closed subgroup scheme generated by a family of morphisms base-changes to the closed subgroup scheme generated by the base-changed family.

noncomputable def TauCeti.CommHopfAlgCat.quotientBaseChangeIso {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) : quotient (baseChange H) (baseChangeHopfIdeal J) ≅ baseChange (quotient H J)

The quotient of a base change by a base-changed Hopf ideal is the base change of the quotient: (K ⊗[k] H) ⧸ J_K ≅ K ⊗[k] (H ⧸ J).

Geometrically, the closed subgroup scheme cut out by J base-changes to the closed subgroup scheme cut out by J_K.

Equations

• TauCeti.CommHopfAlgCat.quotientBaseChangeIso J = TauCeti.CommHopfAlgCat.quotientKerOfSurjectiveIso (TauCeti.CommHopfAlgCat.baseChangeMap (TauCeti.CommHopfAlgCat.mkQuotient H J)) ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_quotientBaseChangeIso_hom {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) : CategoryTheory.CategoryStruct.comp (mkQuotient (baseChange H) (baseChangeHopfIdeal J)) (quotientBaseChangeIso J).hom = baseChangeMap (mkQuotient H J)

The identification of the base-changed quotient is compatible with the quotient morphisms: quotienting K ⊗[k] H by J_K and then identifying is base-changing H ⟶ H ⧸ J.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientBaseChangeIso_hom_apply {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (J : HopfIdeal k ↑H) (y : ↑(baseChange H)) : (CategoryTheory.ConcreteCategory.hom (quotientBaseChangeIso J).hom) ((Ideal.Quotient.mk (baseChangeHopfIdeal J).toIdeal) y) = (CommHopfAlgCat.Hom.hom (baseChangeMap (mkQuotient H J))) y

The identification of the base-changed quotient reads a quotient class through the base-changed quotient morphism.

theorem TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_of_toIdeal_eq_span {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {H' : CommHopfAlgCat K} {S : Set ↑H} {S' : Set ↑H'} (J : HopfIdeal k ↑H) (J' : HopfIdeal K ↑H') (e : baseChange H ≅ H') (hJ : J.toIdeal = Ideal.span S) (hJ' : J'.toIdeal = Ideal.span S') (h : (fun (x : ↑H) => (CommHopfAlgCat.Hom.hom e.hom) (1 ⊗ₜ[k] x)) '' S = S') : (baseChangeHopfIdeal J).map (CommHopfAlgCat.Hom.hom e.hom) = J'

An ambient base-change isomorphism carries a base-changed Hopf ideal generated by a set to the target Hopf ideal when it carries the generating set onto the target generating set.

theorem TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_of_quotientIso {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H T : CommHopfAlgCat k} {H' T' : CommHopfAlgCat K} (J : HopfIdeal k ↑H) (J' : HopfIdeal K ↑H') (e : baseChange H ≅ H') (t : baseChange T ≅ T') (q : quotient H J ≅ T) {f : H ⟶ T} {f' : H' ⟶ T'} (hq : CategoryTheory.CategoryStruct.comp (mkQuotient H J) q.hom = f) (hf' : CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp (baseChangeMap f) t.hom) = f') (hJ' : ∀ (x : ↑H'), x ∈ J' ↔ (CommHopfAlgCat.Hom.hom f') x = 0) : (baseChangeHopfIdeal J).map (CommHopfAlgCat.Hom.hom e.hom) = J'

An ambient base-change isomorphism carries a base-changed Hopf ideal onto a target Hopf ideal, when both are presented as vanishing ideals of morphisms matched by base change: J is the kernel of f, which factors through the quotient by J via the isomorphism q, and f' is the base change of f read through e and t.

This is the kernel-presented companion of TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_of_toIdeal_eq_span, for ideals that come with a quotient presentation rather than with generating sets.

theorem TauCeti.CommHopfAlgCat.map_baseChangeHopfIdeal_kerOfSurjective {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H T : CommHopfAlgCat k} {H' T' : CommHopfAlgCat K} (e : baseChange H ≅ H') (t : baseChange T ≅ T') {f : H ⟶ T} (hf : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)) {f' : H' ⟶ T'} (hf' : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f')) (hbase : CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp (baseChangeMap f) t.hom) = f') : (baseChangeHopfIdeal (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f) hf)).map (CommHopfAlgCat.Hom.hom e.hom) = HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom f') hf'

An ambient base-change isomorphism carries the base change of the kernel of a surjective morphism f onto the kernel of a surjective morphism f', when f' is the base change of f read through e and t.

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_baseChangeHopfIdeal (k : Type u) (K : Type w) [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {E : Type v} [CommRing E] [Algebra k E] [Algebra E K] [IsScalarTower k E K] (J : HopfIdeal k ↑H) : baseChangeHopfIdeal (baseChangeHopfIdeal J) = (baseChangeHopfIdeal J).comapOfSurjective (CommHopfAlgCat.Hom.hom (baseChangeTowerIso k K H).hom) ⋯

Base change of Hopf ideals composes in stages. For a tower k → E → K, base-changing a Hopf ideal to E and then to K gives the pullback of its one-step base change along the tower comparison K ⊗[E] (E ⊗[k] H) ≅ K ⊗[k] H.

noncomputable def TauCeti.CommHopfAlgCat.quotientBaseChangeIsoOfMapEq {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {H' : CommHopfAlgCat K} (J : HopfIdeal k ↑H) (J' : HopfIdeal K ↑H') (e : baseChange H ≅ H') (hJ : (baseChangeHopfIdeal J).map (CommHopfAlgCat.Hom.hom e.hom) = J') : baseChange (quotient H J) ≅ quotient H' J'

Transport the base change of a Hopf-ideal quotient across an isomorphism of the ambient base-changed Hopf algebra which carries the base-changed ideal to a target Hopf ideal.

Equations

• TauCeti.CommHopfAlgCat.quotientBaseChangeIsoOfMapEq J J' e hJ = (TauCeti.CommHopfAlgCat.quotientBaseChangeIso J).symm ≪≫ TauCeti.CommHopfAlgCat.quotientIsoOfComapEq e J' ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeMap_mkQuotient_comp_quotientBaseChangeIsoOfMapEq_hom {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {H' : CommHopfAlgCat K} (J : HopfIdeal k ↑H) (J' : HopfIdeal K ↑H') (e : baseChange H ≅ H') (hJ : (baseChangeHopfIdeal J).map (CommHopfAlgCat.Hom.hom e.hom) = J') : CategoryTheory.CategoryStruct.comp (baseChangeMap (mkQuotient H J)) (quotientBaseChangeIsoOfMapEq J J' e hJ).hom = CategoryTheory.CategoryStruct.comp e.hom (mkQuotient H' J')

The transported quotient base-change isomorphism commutes with the quotient morphisms.

theorem TauCeti.CommHopfAlgCat.mem_quotientPointsSubgroup_baseChangeHopfIdeal_iff {k : Type u} {K : Type w} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} (A : CommAlgCat K) (J : HopfIdeal k ↑H) (g : ↑(HopfAlgebra.points A)) : g ∈ quotientPointsSubgroup (baseChange H) (baseChangeHopfIdeal J) A ↔ (baseChangePointsMulEquiv A H) g ∈ quotientPointsSubgroup H J (CommAlgCat.restrictScalarsObj (algebraMap k K) A)

A point of the base change lies in the closed subgroup cut out by the base-changed Hopf ideal exactly when its restriction along h ↦ 1 ⊗ h lies in the closed subgroup cut out by the original one. On points, base change changes nothing but the base ring the algebra is viewed over.

theorem TauCeti.CommHopfAlgCat.isCentral_baseChangeHopfIdeal {k : Type u} {K : Type v} [CommRing k] [CommRing K] [Algebra k K] {H : CommHopfAlgCat k} {J : HopfIdeal k ↑H} (hJ : J.IsCentral) : (baseChangeHopfIdeal J).IsCentral

Base change preserves central Hopf ideals, or equivalently central closed subgroup schemes.