English
Freiman-homomorphisms are preserved under products: given h1: A1→B1 with f1 and h2: A2→B2 with f2, Prod.map f1 f2 is a Freiman-hom between A1×A2 and B1×B2.
Русский
Сохранение Фримановой гомоморфии под произведением: если h1: A1→B1 с f1 и h2: A2→B2 с f2, то Prod.map f1 f2 задаёт Фриманову гомоморфию между A1×A2 и B1×B2.
LaTeX
$$$\\text{IsMulFreimanHom } n\hspace{-0.1em} \\ A_1\\ B_1 f_1 \\; \\land\\; \\text{IsMulFreimanHom } n\\ A_2\\ B_2 f_2 \\Rightarrow IsMulFreimanHom n (A_1 \\times\\!\\!\\, A_2) (B_1 \\times\\!\\!\\, B_2) (Prod.map f_1 f_2)$$$
Lean4
@[to_additive prodMap]
theorem prodMap (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) :
IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
where
mapsTo := h₁.mapsTo.prodMap h₂.mapsTo
map_prod_eq_map_prod s t hsA htA hs ht
h := by
simp only [mem_prod, forall_and, Prod.forall] at hsA htA
simp only [Prod.ext_iff, fst_prod, snd_prod, map_map, Function.comp_apply, Prod.map_fst, Prod.map_snd] at h ⊢
rw [← Function.comp_def, ← map_map, ← map_map, ← Function.comp_def f₂, ← map_map, ← map_map]
exact
⟨h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa) (by simpa) h.1,
h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) (by simpa [@forall_swap α₁] using htA.2)
(by simpa) (by simpa) h.2⟩
