English
If m ≤ n and f is an n-Freiman-hom between A and B, then f is also an m-Freiman-hom between A and B.
Русский
Если m ≤ n и f является n‑Фримановой гомоморфией между A и B, то она является и m‑Фримановой гомоморфией.
LaTeX
$$$m \\le n \\Rightarrow IsMulFreimanHom n A B f \\Rightarrow IsMulFreimanHom m A B f$$$
Lean4
@[to_additive]
theorem mono (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom m A B f
where
mapsTo := hf.mapsTo
map_prod_eq_map_prod s t hsA htA hs ht
h := by
obtain rfl | hm := m.eq_zero_or_pos
· rw [card_eq_zero] at hs ht
rw [hs, ht]
simp only [← hs, card_pos_iff_exists_mem] at hm
obtain ⟨a, ha⟩ := hm
suffices ((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod
by
simp_rw [Multiset.map_add, prod_add] at this
exact mul_right_cancel this
replace ha := hsA ha
refine hf.map_prod_eq_map_prod (fun a ha ↦ ?_) (fun a ha ↦ ?_) ?_ ?_ ?_
· rw [Multiset.mem_add] at ha
obtain ha | ha := ha
· exact hsA ha
· rwa [eq_of_mem_replicate ha]
· rw [Multiset.mem_add] at ha
obtain ha | ha := ha
· exact htA ha
· rwa [eq_of_mem_replicate ha]
· rw [card_add, card_replicate, hs, Nat.add_sub_cancel' hmn]
· rw [card_add, card_replicate, ht, Nat.add_sub_cancel' hmn]
· rw [prod_add, prod_add, h]
