Faithful flatness of maps of group algebras

An injective homomorphism of commutative groups induces a faithfully flat map of group algebras over any commutative ring. Over a nonzero commutative ring, the induced ring map is faithfully flat exactly when the homomorphism is injective. This is the coordinate-algebra criterion for faithful flatness of morphisms of diagonalizable groups.

theorem TauCeti.MonoidAlgebra.faithfullyFlat_mapDomainRingHom_of_injective {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (k : Type u_3) [CommRing k] (p : G →* H) (hp : Function.Injective ⇑p) : (MonoidAlgebra.mapDomainRingHom k p).FaithfullyFlat

An injective homomorphism of commutative groups induces a faithfully flat group-algebra map, including over the zero ring.

@[simp]

theorem TauCeti.MonoidAlgebra.faithfullyFlat_mapDomainRingHom_iff {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (k : Type u_3) [CommRing k] [Nontrivial k] (p : G →* H) : (MonoidAlgebra.mapDomainRingHom k p).FaithfullyFlat ↔ Function.Injective ⇑p

Over a nonzero commutative ring, the group-algebra map is faithfully flat exactly when the homomorphism of character groups is injective.