English
If there is a multiplicative hom f: H → G with a compatibility condition, and G has TwoUniqueProds, then H has TwoUniqueProds.
Русский
Если имеется мультипликативный гомоморфизм f: H → G с условием совместимости, и G имеет TwoUniqueProds, то H имеет TwoUniqueProds.
LaTeX
$$$ \\forall G,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) \\Rightarrow \\mathrm{TwoUniqueProds}(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)
[TwoUniqueProds G] : TwoUniqueProds H where
uniqueMul_of_one_lt_card {A B}
hc := by
classical
obtain hc' | hc' := lt_or_ge 1 (#(A.image f) * #(B.image f))
· obtain ⟨⟨a1, b1⟩, h1, ⟨a2, b2⟩, h2, hne, hu1, hu2⟩ := uniqueMul_of_one_lt_card hc'
simp_rw [mem_product, mem_image] at h1 h2 ⊢
obtain ⟨⟨a1, ha1, rfl⟩, b1, hb1, rfl⟩ := h1
obtain ⟨⟨a2, ha2, rfl⟩, b2, hb2, rfl⟩ := h2
exact
⟨(a1, b1), ⟨ha1, hb1⟩, (a2, b2), ⟨ha2, hb2⟩, mt (congr_arg (Prod.map f f)) hne,
UniqueMul.of_mulHom_image f hf hu1, UniqueMul.of_mulHom_image f hf hu2⟩
rw [← card_product] at hc hc'
obtain ⟨p1, h1, p2, h2, hne⟩ := one_lt_card_iff_nontrivial.mp hc
refine ⟨p1, h1, p2, h2, hne, ?_⟩
cases mem_product.mp h1; cases mem_product.mp h2
constructor <;>
refine
UniqueMul.of_mulHom_image f hf ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc') <;>
apply mem_image_of_mem <;>
assumption
