English
If there is a Freiman 2-homomorphism from A to B, then R(B) ≤ R(A) under suitable bijection assumptions.
Русский
Если существует Фриман 2-гомоморфизм от A к B, то при надлежащих биекцияx R(B) ≤ R(A).
LaTeX
$$$IsMulFreimanHom_2\ A\ B\ f \land BijOn(f,A,B) \Rightarrow mulRothNumber(B) \le mulRothNumber(A)$$$
Lean4
/-- Arithmetic progressions can be pushed forward along bijective 2-Freiman homs. -/
@[to_additive /-- Arithmetic progressions can be pushed forward along bijective 2-Freiman homs. -/
]
theorem mulRothNumber_mono (hf : IsMulFreimanHom 2 A B f) (hf' : Set.BijOn f A B) : mulRothNumber B ≤ mulRothNumber A :=
by
obtain ⟨s, hsB, hcard, hs⟩ := mulRothNumber_spec B
have hsA : invFunOn f A '' s ⊆ A := (hf'.surjOn.mapsTo_invFunOn.mono (coe_subset.2 hsB) Subset.rfl).image_subset
have hfsA : Set.SurjOn f A s := hf'.surjOn.mono Subset.rfl (coe_subset.2 hsB)
rw [← hcard, ← s.card_image_of_injOn ((invFunOn_injOn_image f _).mono hfsA)]
refine ThreeGPFree.le_mulRothNumber ?_ (mod_cast hsA)
rw [coe_image]
simpa using (hf.subset hsA hfsA.bijOn_subset.mapsTo).threeGPFree (hf'.injOn.mono hsA) hs
