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.
• TauCeti.CommHopfAlgCat.quotientBaseChangeIso: the identification (K ⊗[k] H) ⧸ J_K ≅ K ⊗[k] (H ⧸ J).
• 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 does not follow from generation alone.

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

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

@[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.

@[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.

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.

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 ≪≫ CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.CommHopfAlgCat.quotientIsoOfIso 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.