English
Under a 2-Freiman isomorphism, the Roth number is preserved: mulRothNumber A = mulRothNumber B.
Русский
При 2-Freiman изоморфизме число Рота сохраняется: mulRothNumber A = mulRothNumber B.
LaTeX
$$$IsMulFreimanIso(2, A, B, f) \Rightarrow mulRothNumber(A) = mulRothNumber(B)$$$
Lean4
/-- Arithmetic progressions are preserved under 2-Freiman isos. -/
@[to_additive /-- Arithmetic progressions are preserved under 2-Freiman isos. -/
]
theorem mulRothNumber_congr (hf : IsMulFreimanIso 2 A B f) : mulRothNumber A = mulRothNumber B :=
by
refine le_antisymm ?_ (hf.isMulFreimanHom.mulRothNumber_mono hf.bijOn)
obtain ⟨s, hsA, hcard, hs⟩ := mulRothNumber_spec A
rw [← coe_subset] at hsA
have hfs : Set.InjOn f s := hf.bijOn.injOn.mono hsA
have := (hf.subset hsA hfs.bijOn_image).threeGPFree_congr.1 hs
rw [← coe_image] at this
rw [← hcard, ← Finset.card_image_of_injOn hfs]
refine this.le_mulRothNumber ?_
rw [← coe_subset, coe_image]
exact (hf.bijOn.mapsTo.mono hsA Subset.rfl).image_subset
