The kernel criterion for a quotient by normal coinvariants

Let I be a normal Hopf ideal of a commutative Hopf algebra H over a field, let B = H^{co H/I} be its algebra of coinvariants, and let J be the scheme-theoretic kernel of the inclusion B → H. There are two natural maps out of H ⊗[B] H:

• the kernel-pair equivalence identifies it with H ⊗ H/J;
• the canonical map of the proposed quotient has target H ⊗ H/I.

This file proves that the second map is the first followed by the quotient H/J → H/I. Consequently the canonical map is injective exactly when J = I. Since the canonical map is always surjective, this is also exactly when it is an isomorphism. Thus the missing equality in the Hopf ideal--Hopf subalgebra correspondence is reduced to the injectivity part of the usual canonical-map criterion.

References

• M. Takeuchi, A correspondence between Hopf ideals and sub-Hopf algebras, Manuscripta Math. 7 (1972), 251--270.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.coinvariantsKernelQuotientMap {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : quotient H (kernelHopfIdeal (coinvariantsι hI)) ⟶ quotient H I

The quotient from the scheme-theoretic kernel of the coinvariant projection to the proposed normal subgroup. It is induced by the always-valid inclusion kernelHopfIdeal (coinvariantsι hI) ≤ I.

Equations

• TauCeti.CommHopfAlgCat.coinvariantsKernelQuotientMap hI = TauCeti.CommHopfAlgCat.quotientMapOfLe H ⋯

noncomputable def TauCeti.CommHopfAlgCat.coinvariantsKernelTensorMap {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : TensorProduct k (↑H) (↑H ⧸ (kernelHopfIdeal (coinvariantsι hI)).toIdeal) →ₐ[↑H] TensorProduct k (↑H) (↑H ⧸ I.toIdeal)

Tensoring the quotient from the scheme-theoretic kernel with the ambient coordinate algebra, regarded as a map of H-algebras through the left tensor factors.

Equations

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

theorem TauCeti.CommHopfAlgCat.coe_coinvariantsKernelTensorMap {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : ⇑(coinvariantsKernelTensorMap hI) = ⇑(Algebra.TensorProduct.map (AlgHom.id k ↑H) ↑(CommHopfAlgCat.Hom.hom (coinvariantsKernelQuotientMap hI)))

The tensor quotient is the tensor product of the identity with the quotient-to-quotient map.

@[simp]

theorem TauCeti.CommHopfAlgCat.coinvariantsKernelTensorMap_tmul {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) (x : ↑H) (y : ↑H ⧸ (kernelHopfIdeal (coinvariantsι hI)).toIdeal) : (coinvariantsKernelTensorMap hI) (x ⊗ₜ[k] y) = x ⊗ₜ[k] (CommHopfAlgCat.Hom.hom (coinvariantsKernelQuotientMap hI)) y

The tensor quotient acts as the identity on the ambient factor and by the quotient-to-quotient map on the kernel factor.

noncomputable def TauCeti.CommHopfAlgCat.coinvariantsKernelPairTensorEquiv {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : TensorProduct ↥I.coinvariants ↑H ↑H ≃ₐ[↑H] TensorProduct k (↑H) (↑H ⧸ (kernelHopfIdeal (coinvariantsι hI)).toIdeal)

The kernel-pair equivalence for the coinvariant projection, expressed using the canonical subalgebra action of the coinvariants on H.

Equations

• TauCeti.CommHopfAlgCat.coinvariantsKernelPairTensorEquiv hI = TauCeti.CommHopfAlgCat.kernelPairTensorEquiv (TauCeti.CommHopfAlgCat.coinvariantsι hI)

@[simp]

theorem TauCeti.CommHopfAlgCat.coinvariantsKernelPairTensorEquiv_tmul {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) (x y : ↑H) : (coinvariantsKernelPairTensorEquiv hI) (x ⊗ₜ[↥I.coinvariants] y) = x ⊗ₜ[k] 1 * (Algebra.TensorProduct.map (AlgHom.id k ↑H) (Ideal.Quotient.mkₐ k (kernelHopfIdeal (coinvariantsι hI)).toIdeal)) (CoalgebraStruct.comul y)

On pure tensors, the specialized kernel-pair equivalence multiplies the first factor by the comultiplication of the second and projects its right leg to the kernel coordinates.

theorem TauCeti.CommHopfAlgCat.canonicalMap_eq_tensorMap_comp_kernelPairTensorEquiv {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : I.canonicalMap = (coinvariantsKernelTensorMap hI).comp ↑(coinvariantsKernelPairTensorEquiv hI)

The canonical map for I factors as the kernel-pair equivalence of the coinvariant projection, followed by the quotient from its scheme-theoretic kernel to I.

theorem TauCeti.CommHopfAlgCat.coinvariantsKernelQuotientMap_injective_iff {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : Function.Injective ⇑(CommHopfAlgCat.Hom.hom (coinvariantsKernelQuotientMap hI)) ↔ kernelHopfIdeal (coinvariantsι hI) = I

The quotient from the scheme-theoretic kernel of the coinvariant projection to I is injective exactly when that kernel is I.

theorem TauCeti.CommHopfAlgCat.canonicalMap_injective_iff_kernelHopfIdeal_coinvariantsι_eq {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : Function.Injective ⇑I.canonicalMap ↔ kernelHopfIdeal (coinvariantsι hI) = I

Kernel criterion for normal coinvariants. The canonical map H ⊗[H^{co H/I}] H → H ⊗ H/I is injective exactly when the scheme-theoretic kernel of the corresponding quotient projection is the original normal subgroup I.

theorem TauCeti.CommHopfAlgCat.canonicalMap_bijective_iff_kernelHopfIdeal_coinvariantsι_eq {k : Type u} [Field k] {H : CommHopfAlgCat k} {I : HopfIdeal k ↑H} (hI : I.IsNormal) : Function.Bijective ⇑I.canonicalMap ↔ kernelHopfIdeal (coinvariantsι hI) = I

The canonical map over normal coinvariants is bijective exactly when the proposed subgroup is the scheme-theoretic kernel of the quotient projection. Surjectivity holds for every Hopf ideal, so only the injectivity criterion contributes to this equivalence.