Coinvariants of a Hopf ideal

Let H be a commutative Hopf algebra over R and let I be a Hopf ideal, cutting out a closed subgroup N of the affine group G represented by H. The coinvariants of I are the elements h with

(id ⊗ π) (Δ h) = h ⊗ 1   in H ⊗[R] (H ⧸ I),

where π : H → H ⧸ I is the quotient map. Equivalently Δ h - h ⊗ 1 ∈ H ⊗ I. They form a subalgebra H^{co H/I} of H: geometrically, the functions f on G that are invariant under right translation by N, f (g n) = f g. Over a field, when N is normal, this subalgebra is the coordinate ring of the quotient G / N (Waterhouse, §16.3; Takeuchi); that identification, which rests on faithful flatness of H over its Hopf subalgebras, is not proved here. The coinvariants are therefore the candidate representing object for the fppf quotient sheaf TauCeti.CommHopfAlgCat.fppfQuotientSheaf.

This file sets up that candidate and proves its Hopf-algebraic closure properties:

• the functor-of-points characterization: h is a coinvariant exactly when (g * n)(h) = g(h) for all points g of G and n of N over every value algebra;
• every coinvariant is congruent to its counit modulo I, so the augmentation ideal of the coinvariants is contained in I: N lies in the kernel of G → G / N;
• the coinvariants of the zero ideal are the scalars and those of the augmentation ideal are everything;
• when H is flat, comultiplication maps the coinvariants into H ⊗ H^{co H/I}, so they form a left coideal subalgebra;
• when I is normal, the antipode preserves the coinvariants, and comultiplication maps them into H^{co H/I} ⊗ H^{co H/I} as soon as H and H ⧸ H^{co H/I} are flat (for instance over a field). So the coinvariants of a normal Hopf ideal are a Hopf subalgebra.

Main declarations

• TauCeti.HopfIdeal.coinvariants: the subalgebra of right N-invariant functions.
• TauCeti.HopfIdeal.mem_coinvariants_iff and TauCeti.HopfIdeal.mem_coinvariants_iff_comul_sub_mem_rightTensorIdeal: membership criteria.
• TauCeti.HopfIdeal.ofConv_mul_apply_of_mem_coinvariants and TauCeti.HopfIdeal.mem_coinvariants_iff_forall_mul: the functor-of-points characterization.
• TauCeti.HopfIdeal.sub_algebraMap_counit_mem_of_mem_coinvariants: coinvariants are constant on N.
• TauCeti.HopfIdeal.coinvariants_mono, TauCeti.HopfIdeal.coinvariants_bot and TauCeti.HopfIdeal.coinvariants_augmentation: dependence on the Hopf ideal.
• TauCeti.HopfIdeal.comul_mem_range_lTensor_of_mem_coinvariants: the left coideal property.
• TauCeti.HopfIdeal.IsNormal.antipode_mem_coinvariants: stability under the antipode.
• TauCeti.HopfIdeal.IsNormal.comul_mem_range_rTensor_of_mem_coinvariants: the right coideal property for a normal Hopf ideal.
• TauCeti.HopfIdeal.IsNormal.coinvariantsSubcoalgebra: the coinvariants of a normal Hopf ideal as a subcoalgebra.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• M. Takeuchi, A correspondence between Hopf ideals and sub-Hopf algebras, Manuscripta Math. 7 (1972), 251–270.
• J. S. Milne, Algebraic Groups (2017), §5.c.

noncomputable def TauCeti.HopfIdeal.coinvariants {R : Type u} {H : Type v} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : Subalgebra R H

The coinvariants of a Hopf ideal I: the elements h with (id ⊗ π) (Δ h) = h ⊗ 1, where π : H → H ⧸ I is the quotient map. Geometrically these are the functions on the affine group that are invariant under right translation by the closed subgroup cut out by I.

Equations

• I.coinvariants = ((Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I.toIdeal)).comp (Bialgebra.comulAlgHom R H)).equalizer Algebra.TensorProduct.includeLeft

theorem TauCeti.HopfIdeal.coinvariants_eq_equalizer {R : Type u} {H : Type v} [CommSemiring R] [CommRing H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.coinvariants = ((Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I.toIdeal)).comp (Bialgebra.comulAlgHom R H)).equalizer Algebra.TensorProduct.includeLeft

Coinvariants are the equalizer of the subgroup coaction and the trivial coaction.

@[simp]

theorem TauCeti.HopfIdeal.mem_coinvariants_iff {R : Type u} {H : Type v} [CommSemiring R] [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {h : H} : h ∈ I.coinvariants ↔ (Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I.toIdeal)) (CoalgebraStruct.comul h) = h ⊗ₜ[R] 1

Membership in the coinvariants: (id ⊗ π) (Δ h) = h ⊗ 1.

theorem TauCeti.HopfIdeal.mk_eq_algebraMap_counit_of_mem_coinvariants {R : Type u} {H : Type v} [CommSemiring R] [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {h : H} (hh : h ∈ I.coinvariants) : (Ideal.Quotient.mk I.toIdeal) h = (algebraMap R (H ⧸ I.toIdeal)) (CoalgebraStruct.counit h)

A coinvariant is congruent modulo I to the scalar given by its counit: the functions invariant under the subgroup cut out by I are constant on that subgroup.

theorem TauCeti.HopfIdeal.coinvariants_mono {R : Type u} {H : Type v} [CommSemiring R] [CommRing H] [HopfAlgebra R H] {I J : HopfIdeal R H} (hIJ : I ≤ J) : I.coinvariants ≤ J.coinvariants

Enlarging the Hopf ideal shrinks the subgroup it cuts out, so enlarges the coinvariants.

theorem TauCeti.HopfIdeal.mem_coinvariants_iff_comul_sub_mem_rightTensorIdeal {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {h : H} : h ∈ I.coinvariants ↔ CoalgebraStruct.comul h - h ⊗ₜ[R] 1 ∈ rightTensorIdeal R H I.toIdeal

Membership in the coinvariants: Δ h - h ⊗ 1 lies in H ⊗ I.

theorem TauCeti.HopfIdeal.sub_algebraMap_counit_mem_of_mem_coinvariants {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {h : H} (hh : h ∈ I.coinvariants) : h - (algebraMap R H) (CoalgebraStruct.counit h) ∈ I

A coinvariant minus its counit lies in the Hopf ideal: the augmentation ideal of the coinvariants is contained in I.

@[simp]

theorem TauCeti.HopfIdeal.coinvariants_bot {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] : ⊥.coinvariants = ⊥

The zero Hopf ideal cuts out the whole group, whose right-invariant functions are the constants.

theorem TauCeti.HopfIdeal.comul_mem_range_lTensor_of_mem_coinvariants {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {I : HopfIdeal R H} {h : H} [Module.Flat R H] (hh : h ∈ I.coinvariants) : CoalgebraStruct.comul h ∈ (LinearMap.lTensor H (Subalgebra.toSubmodule I.coinvariants).subtype).range

Coinvariants form a left coideal. Over a flat Hopf algebra, comultiplication maps the coinvariants of I into H ⊗ H^{co H/I}: if f is right N-invariant then so is y ↦ f (x y) for every x.

theorem TauCeti.HopfIdeal.ofConv_mul_apply_of_mem_coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {h : ↑H} (hh : h ∈ I.coinvariants) {A : CommAlgCat R} (g : ↑(HopfAlgebra.points A)) {n : ↑(HopfAlgebra.points A)} (hn : n ∈ CommHopfAlgCat.quotientPointsSubgroup H I A) : (g * n).ofConv h = g.ofConv h

A coinvariant is invariant under right translation by the points of the subgroup cut out by I: (g * n)(h) = g(h).

theorem TauCeti.HopfIdeal.mem_coinvariants_iff_forall_mul {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {h : ↑H} : h ∈ I.coinvariants ↔ ∀ (A : CommAlgCat R) (g n : ↑(HopfAlgebra.points A)), n ∈ CommHopfAlgCat.quotientPointsSubgroup H I A → (g * n).ofConv h = g.ofConv h

Functor-of-points characterization of the coinvariants. An element is a coinvariant exactly when it is invariant under right translation by the points of the subgroup cut out by I, over every commutative value algebra.

@[simp]

theorem TauCeti.HopfIdeal.coinvariants_augmentation {R : Type u} [CommRing R] {H : CommHopfAlgCat R} : (augmentation R ↑H).coinvariants = ⊤

The augmentation ideal cuts out the trivial subgroup, so every function is invariant.

theorem TauCeti.HopfIdeal.IsNormal.antipode_mem_coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {h : ↑H} (hI : I.IsNormal) (hh : h ∈ I.coinvariants) : (HopfAlgebraStruct.antipode R) h ∈ I.coinvariants

The antipode preserves the coinvariants of a normal Hopf ideal. If f is invariant under right translation by a normal subgroup N, so is g ↦ f (g⁻¹), because (g n)⁻¹ = g⁻¹ (g n⁻¹ g⁻¹) and g n⁻¹ g⁻¹ ∈ N.

theorem TauCeti.HopfIdeal.IsNormal.comul_mem_range_rTensor_of_mem_coinvariants {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {h : ↑H} [Module.Flat R ↑H] (hI : I.IsNormal) (hh : h ∈ I.coinvariants) : CoalgebraStruct.comul h ∈ (LinearMap.rTensor (↑H) (Subalgebra.toSubmodule I.coinvariants).subtype).range

Coinvariants of a normal Hopf ideal form a right coideal. Over a flat Hopf algebra, comultiplication maps the coinvariants of a normal Hopf ideal into H^{co H/I} ⊗ H.

noncomputable def TauCeti.HopfIdeal.IsNormal.coinvariantsSubcoalgebra {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : Subcoalgebra R ↑H

The coinvariants of a normal Hopf ideal form a subcoalgebra, when H and H ⧸ H^{co H/I} are flat, for instance over a field. Together with TauCeti.HopfIdeal.IsNormal.antipode_mem_coinvariants, this makes the coinvariants a Hopf subalgebra of H.

Equations

• hI.coinvariantsSubcoalgebra = TauCeti.Subcoalgebra.ofSubmodule (Subalgebra.toSubmodule I.coinvariants) ⋯

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.coinvariantsSubcoalgebra_carrier {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} [Module.Flat R ↑H] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : hI.coinvariantsSubcoalgebra.carrier = Subalgebra.toSubmodule I.coinvariants

The underlying submodule of the coinvariant subcoalgebra is the coinvariant subalgebra.

@[simp]

theorem TauCeti.HopfIdeal.IsNormal.mem_coinvariantsSubcoalgebra {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {I : HopfIdeal R ↑H} {h : ↑H} [Module.Flat R ↑H] [Module.Flat R (↑H ⧸ Subalgebra.toSubmodule I.coinvariants)] (hI : I.IsNormal) : h ∈ hI.coinvariantsSubcoalgebra ↔ h ∈ I.coinvariants

The subcoalgebra of coinvariants has the coinvariants as its elements.