Flat base change of coinvariant algebras

For a closed subgroup N of an affine group G, the algebra of functions invariant under right translation by N commutes with flat extension of scalars. No normality, finite-type, or smoothness assumption is needed. This compares the candidate coordinate algebra of G/N with the corresponding candidate after extending the ground field.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §16.3.
• Mathlib's AlgHom.tensorEqualizerEquiv.

noncomputable def TauCeti.CommHopfAlgCat.coinvariantsBaseChangeEquiv {R : Type u} {S : Type w} [CommRing R] [CommRing S] [Algebra R S] {H : CommHopfAlgCat R} [Module.Flat R S] (I : HopfIdeal R ↑H) : TensorProduct R S ↥I.coinvariants ≃ₐ[S] ↥(baseChangeHopfIdeal I).coinvariants

Flat scalar extension commutes with taking functions invariant under a closed subgroup: S ⊗[R] H^{co H/I} ≃ (S ⊗[R] H)^{co (S ⊗[R] H)/I_S}.

Equations

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

@[simp]

theorem TauCeti.CommHopfAlgCat.coe_coinvariantsBaseChangeEquiv {R : Type u} {S : Type w} [CommRing R] [CommRing S] [Algebra R S] {H : CommHopfAlgCat R} [Module.Flat R S] (I : HopfIdeal R ↑H) (z : TensorProduct R S ↥I.coinvariants) : ↑((coinvariantsBaseChangeEquiv I) z) = (Algebra.TensorProduct.map (AlgHom.id S S) I.coinvariants.val) z

The comparison sends a tensor of invariant functions to the same tensor in the ambient coordinate algebra.

@[simp]

theorem TauCeti.CommHopfAlgCat.map_coinvariantsBaseChangeEquiv_symm {R : Type u} {S : Type w} [CommRing R] [CommRing S] [Algebra R S] {H : CommHopfAlgCat R} [Module.Flat R S] (I : HopfIdeal R ↑H) (z : ↥(baseChangeHopfIdeal I).coinvariants) : (Algebra.TensorProduct.map (AlgHom.id S S) I.coinvariants.val) ((coinvariantsBaseChangeEquiv I).symm z) = ↑z

Including the inverse image of an invariant function recovers that function in the ambient scalar-extended coordinate algebra.

@[simp]

theorem TauCeti.CommHopfAlgCat.coinvariants_baseChangeHopfIdeal {R : Type u} {S : Type w} [CommRing R] [CommRing S] [Algebra R S] {H : CommHopfAlgCat R} [Module.Flat R S] (I : HopfIdeal R ↑H) : (baseChangeHopfIdeal I).coinvariants = Subalgebra.baseChange S I.coinvariants

As subalgebras of the scalar-extended coordinate ring, coinvariants commute with flat base change.