English
A distributive action of a monoid M on a finite cyclic group G of order n factors through an action on ZMod n.
Русский
Дистрибутивное действие моноида M на конечной циклической группе G порядка n факторизуется через действие на ZMod n.
LaTeX
$$Let M be a monoid with a distributive action on a cyclic group G of order n, with Nat.card G = n; then there exists a monoid hom φ: M →* ZMod n describing the action.$$
Lean4
/-- A distributive action of a monoid on a finite cyclic group of order `n` factors through an
action on `ZMod n`. -/
noncomputable def toMonoidHomZModOfIsCyclic (M : Type*) [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ}
(hn : Nat.card G = n) : M →* ZMod n
where
toFun m := (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose
map_one' := by
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq, zpow_one, ←
(MulDistribMulAction.toMonoidHom G 1).map_cyclic.choose_spec, MulDistribMulAction.toMonoidHom_apply, one_smul]
map_mul' m
n := by
obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq, zpow_mul', ←
(MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec, ←
(MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec, ←
(MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec, MulDistribMulAction.toMonoidHom_apply,
MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply, mul_smul]
