Theorems · Theorem · group theory

MonoidHom.restrict_surjective

Deprecated since 2026-07-19Use MonoidHom.domRestrict_surjective instead.

∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G),
  Function.Surjective ⇑(MonoidHom.domRestrictHom H Mˣ)

Alias of MonoidHom.domRestrict_surjective. Let G be a finite commutative group and let H be a subgroup. If M is a commutative monoid such that G →* Mˣ and H →* Mˣ are both finite (this is the case for example if M is a commutative domain) and with enough nth roots of unity, where n is the exponent of G, then any homomorphism H →* Mˣ can be extended to an homomorphism G →* Mˣ.

Defined in

Mathlib.GroupTheory.FiniteAbelian.Duality

Cited by

0 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupFiniteCommMonoidHasEnoughRootsOfUnity