The canonical map over the coinvariants of a Hopf ideal

For a Hopf ideal I in a commutative Hopf algebra H, put B = I.coinvariants. The canonical map

H ⊗[B] H → H ⊗[R] (H / I),    a ⊗ b ↦ (a ⊗ 1) (id ⊗ π)(Δ b)

is an H-algebra homomorphism and is surjective. Geometrically, this says that (g, n) ↦ (g, gn) is a closed immersion from G × N into G ×_{Spec B} G. This supplies the surjectivity part of the canonical-map criterion for a quotient torsor; injectivity and faithful flatness are separate questions. Neither normality of I nor flatness over the base is needed here.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.

noncomputable def TauCeti.HopfIdeal.canonicalMap {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : TensorProduct (↥I.coinvariants) H H →ₐ[H] TensorProduct R H (H ⧸ I.toIdeal)

The canonical map for a Hopf quotient, with the tensor product balanced over the coinvariant subalgebra. It is linear over the first copy of H.

Equations

• I.canonicalMap = Algebra.TensorProduct.lift (Algebra.ofId H (TensorProduct R H (H ⧸ I.toIdeal))) (TauCeti.HopfIdeal.coinvariantCoaction✝ I) ⋯

@[simp]

theorem TauCeti.HopfIdeal.canonicalMap_tmul {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) (a b : H) : I.canonicalMap (a ⊗ₜ[↥I.coinvariants] b) = a ⊗ₜ[R] 1 * (Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I.toIdeal)) (CoalgebraStruct.comul b)

On pure tensors the canonical map multiplies the left factor by the quotient coaction of the right factor.

theorem TauCeti.HopfIdeal.canonicalMap_comp_mapOfCompatibleSMul {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : (AlgHom.restrictScalars R I.canonicalMap).comp (Algebra.TensorProduct.mapOfCompatibleSMul (↥I.coinvariants) R R H H) = (Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I.toIdeal)).comp ↑HopfAlgebra.tensorShearMulRight

The absolute tensor-square map factors through balancing over the coinvariants. Its other factorization is the tensor shear followed by the quotient in the second factor.

theorem TauCeti.HopfIdeal.canonicalMap_surjective {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : Function.Surjective ⇑I.canonicalMap

The canonical map over the coinvariants of any Hopf ideal is surjective. No normality or flatness hypothesis is required.