Base change of scheme-theoretic kernels

The coordinate ring of the kernel of an affine group-scheme morphism is the quotient by the kernel Hopf ideal K·f(H⁺). This file identifies it with the base change K ⊗[H] R, where K is an H-algebra through f and R an H-algebra through the counit: this is Milne's description of the kernel as the fiber of Spec K → Spec H over the identity point, O(ker) = O(G) ⊗_{O(G')} R, over an arbitrary commutative base ring and with no flatness hypotheses.

The identification is assembled from Mathlib's Algebra.TensorProduct.quotIdealMapEquivTensorQuot (right exactness of the tensor product) and the first isomorphism theorem for the counit (Ideal.quotientKerAlgEquivOfSurjective); the two canonical algebra structures are introduced with letI in the statement, as they are determined by f and the counit rather than by instance search.

Two consequences of the identification are recorded here: the kernel coordinate ring is finite over the base as soon as the coordinate morphism is finite, and faithfully flat over the base as soon as the coordinate morphism is faithfully flat. Both are the corresponding base-change stability results transported across the identification.

Formation of the kernel Hopf ideal also commutes with extension of the base ring, including its infinitesimal structure.

Main declarations

• TauCeti.CommHopfAlgCat.quotientKernelHopfIdealAlgEquiv: the K-algebra equivalence from the kernel coordinate ring to K ⊗[H] R.
• TauCeti.CommHopfAlgCat.moduleFinite_quotient_kernelHopfIdeal: the kernel coordinate ring is finite over the base.
• TauCeti.CommHopfAlgCat.moduleFaithfullyFlat_quotient_kernelHopfIdeal: the kernel coordinate ring is faithfully flat over the base.
• TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_kernelHopfIdeal: the kernel Hopf ideal commutes with scalar extension.

noncomputable def TauCeti.CommHopfAlgCat.quotientKernelHopfIdealAlgEquiv {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) : (↑K ⧸ (kernelHopfIdeal f).toIdeal) ≃ₐ[↑K] TensorProduct (↑H) (↑K) R

The coordinate ring of the kernel of an affine group-scheme morphism is the base change of the identity point: K ⧸ K·f(H⁺) ≃ₐ[K] K ⊗[H] R, with K an H-algebra through f and R an H-algebra through the counit.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientKernelHopfIdealAlgEquiv_mk {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (k : ↑K) : (quotientKernelHopfIdealAlgEquiv f) ((Ideal.Quotient.mk (kernelHopfIdeal f).toIdeal) k) = k ⊗ₜ[↑H] 1

The identification sends a quotient representative to its pure tensor against 1.

@[simp]

theorem TauCeti.CommHopfAlgCat.quotientKernelHopfIdealAlgEquiv_symm_tmul {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (k : ↑K) (r : R) : (quotientKernelHopfIdealAlgEquiv f).symm (k ⊗ₜ[↑H] r) = (Ideal.Quotient.mk (kernelHopfIdeal f).toIdeal) ((algebraMap R ↑K) r * k)

The inverse of the identification sends k ⊗ₜ r to the class of r-scaled k.

theorem TauCeti.CommHopfAlgCat.moduleFinite_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : (↑(CommHopfAlgCat.Hom.hom f)).Finite) : Module.Finite R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

The coordinate ring of the kernel is finite as a module over the base when the coordinate map is finite.

theorem TauCeti.CommHopfAlgCat.moduleFaithfullyFlat_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat) : Module.FaithfullyFlat R (↑K ⧸ (kernelHopfIdeal f).toIdeal)

The coordinate ring of the kernel is faithfully flat over the base when the coordinate map is faithfully flat.

@[simp]

theorem TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {S : Type w} [CommRing S] [Algebra R S] (f : H ⟶ K) : baseChangeHopfIdeal (kernelHopfIdeal f) = kernelHopfIdeal (baseChangeMap f)

Formation of the kernel Hopf ideal commutes with extension of the base ring.