English
Let f: M → N be a monoid homomorphism between commutative monoids, and suppose f(x) = 1 implies x = 1 for all x in M. Then for any family g : α → M, the finitary product commutes with f:
f(∏ᶠ i, g(i)) = ∏ᶠ i, f(g(i)).
Русский
Пусть f: M → N — гомоморфизм моноидов между коммутативными моноидами, и выполняется свойство: f(x) = 1 ⇒ x = 1 для всех x ∈ M. Тогда для любого семейства g: α → M выполняется:
f(∏ᶠ i, g(i)) = ∏ᶠ i, f(g(i)).
LaTeX
$$$$ f\left(\prod^{\mathrm{fin}}_{i} g(i)\right) = \prod^{\mathrm{fin}}_{i} f\bigl(g(i)\bigr). $$$$
Lean4
@[to_additive]
theorem map_finprod_of_preimage_one (f : M →* N) (hf : ∀ x, f x = 1 → x = 1) (g : α → M) :
f (∏ᶠ i, g i) = ∏ᶠ i, f (g i) :=
by
by_cases hg : (mulSupport <| g ∘ PLift.down).Finite; · exact f.map_finprod_plift g hg
rw [finprod, dif_neg, f.map_one, finprod, dif_neg]
exacts [Infinite.mono (fun x hx => mt (hf (g x.down)) hx) hg, hg]
