English
Let G,H be semigroups with Multiplication, and f: H →* G a monoid homomorphism that preserves the unique-products structure via a suitable compatibility hf. If G has UniqueProds, then H has UniqueProds.
Русский
Пусть G и H — полугруппы с умножением, а f: H →* G моноидный гомоморфизм, сохраняющий структуру уникальных произведений по совместимости hf. Если G имеет UniqueProds, то и H имеет UniqueProds.
LaTeX
$$$ \\forall G,H\\,[\\text{Mul }G][\\text{Mul }H]\\ (f: H \\to_* G)\\ (hf: \\forall a,b,c,d, a b=c d \\Rightarrow f a=f c \\land f b=f d \\Rightarrow a=c \\land b=d)\\ [\\mathrm{UniqueProds }G] \\Rightarrow \\mathrm{UniqueProds }H.$$$
Lean4
@[to_additive]
theorem of_mulHom (f : H →ₙ* G) (hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d)
[UniqueProds G] : UniqueProds H where
uniqueMul_of_nonempty {A B} A0
B0 := by
classical
obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩
