Finite morphisms of group algebras

For a homomorphism p : M →* N of commutative groups, R[N] is finite over R[M] through mapDomainRingHom R p if the cokernel of p is finite. Over a nonzero coefficient ring the converse holds as well. No injectivity or finite generation of the groups is needed.

Coset representatives span the target as a module over the source. Conversely, the group algebra of the cokernel is a quotient of the target on which the source acts through its augmentation, so finiteness forces its standard basis to be finite.

This is the coordinate-ring finiteness criterion for morphisms of diagonalizable groups; it supplies the finiteness condition in the character description of their isogenies.

Without commutativity, R[N] is still a finitely generated R[M]-module through any monoid homomorphism p : M →* N into a finite monoid, since it is already finitely generated over R (TauCeti.MonoidAlgebra.mapDomainRingHom_moduleFinite_of_finite). This is the finiteness behind restricting representations of a finite group along a homomorphism.

theorem TauCeti.MonoidAlgebra.span_range_single_quotient_eq_top (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommGroup M] [CommGroup N] [CommSemiring R] (p : M →* N) (s : N ⧸ p.range → N) (hs : Function.RightInverse s ⇑(QuotientGroup.mk' p.range)) : have this := (MonoidAlgebra.mapDomainRingHom R p).toAlgebra; Submodule.span (MonoidAlgebra R M) (Set.range fun (q : N ⧸ p.range) => MonoidAlgebra.single (s q) 1) = ⊤

Monomials indexed by representatives of the cokernel span the target group algebra as a module over the source group algebra.

theorem TauCeti.MonoidAlgebra.mapDomainRingHom_finite_of_finite_quotient (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommGroup M] [CommGroup N] [CommRing R] (p : M →* N) [Finite (N ⧸ p.range)] : (MonoidAlgebra.mapDomainRingHom R p).Finite

A homomorphism of commutative groups with finite cokernel induces a finite morphism of group algebras, over any commutative coefficient ring.

@[simp]

theorem TauCeti.MonoidAlgebra.mapDomainRingHom_finite_iff_finite_quotient (R : Type u_1) {M : Type u_2} {N : Type u_3} [CommGroup M] [CommGroup N] [CommRing R] [Nontrivial R] (p : M →* N) : (MonoidAlgebra.mapDomainRingHom R p).Finite ↔ Finite (N ⧸ p.range)

Over a nonzero commutative ring, the group-algebra map induced by a homomorphism of commutative groups is finite exactly when its cokernel is finite.

theorem TauCeti.MonoidAlgebra.mapDomainRingHom_moduleFinite_of_finite {R : Type u_4} [Semiring R] {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] [Finite N] (p : M →* N) : Module.Finite (MonoidAlgebra R M) (MonoidAlgebra R N)

Finiteness over the algebra of any monoid mapping to a finite one. For a monoid homomorphism p : M →* N with N finite, R[N] is a finitely generated R[M]-module through mapDomainRingHom R p, because it is already finitely generated over R. Neither monoid need be commutative, so the algebras need not be, and the statement uses the module structure RingHom.toModule rather than RingHom.Finite.