The homomorphism form of PFR

Here we apply (improved) PFR to show that approximate homomorphisms f from a 2-group to a 2-group are close to actual homomorphisms. Here, approximate is in the sense that f(x+y)-f(x)-f(y) takes few values.

Main results

• goursat: A convenient description of the subspaces of $G \times G'$ when $G, G'$ are elementary abelian 2-groups.
• homomorphism_pfr : If $f : G → G'$ is a map between finite abelian elementary 2-groups such that $f(x+y)-f(x)-f(y)$ takes at most $K$ values, then there is a homomorphism $\phi: G \to G'$ such that $f(x)-\phi(x)$ takes at most $K^{10}$ values.

theorem hahn_banach {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [AddCommGroup G'] [Module (ZMod 2) G] [Module (ZMod 2) G'] (H₀ : AddSubgroup G) (φ : ↥H₀ →+ G') : ∃ (φ' : G →+ G'), ∀ (x : ↥H₀), φ x = φ' ↑x

Let $H_0$ be a subgroup of $G$. Then every homomorphism $\phi: H_0 \to G'$ can be extended to a homomorphism $\tilde \phi: G \to G'$.

theorem goursat {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [AddCommGroup G'] [Module (ZMod 2) G] [Module (ZMod 2) G'] (H : Submodule (ZMod 2) (G × G')) : ∃ (H₀ : Submodule (ZMod 2) G) (H₁ : Submodule (ZMod 2) G') (φ : G →+ G'), (∀ (x : G × G'), x ∈ H ↔ x.1 ∈ H₀ ∧ x.2 - φ x.1 ∈ H₁) ∧ Nat.card ↥H = Nat.card ↥H₀ * Nat.card ↥H₁

Let $H$ be a subgroup of $G \times G'$. Then there exists a subgroup $H_0$ of $G$, a subgroup $H_1$ of $G'$, and a homomorphism $\phi: G \to G'$ such that $$ H := \{ (x, \phi(x) + y): x \in H_0, y \in H_1 \}.$$ In particular, $|H| = |H_0| |H_1|$.

theorem homomorphism_pfr {G : Type u_1} {G' : Type u_2} [AddCommGroup G] [AddCommGroup G'] [Module (ZMod 2) G] [Module (ZMod 2) G'] [Fintype G] [Fintype G'] (f : G → G') (S : Set G') (hS : ∀ (x y : G), f (x + y) - f x - f y ∈ S) : ∃ (φ : G →+ G') (T : Set G'), Nat.card ↑T ≤ Nat.card ↑S ^ 10 ∧ ∀ (x : G), f x - φ x ∈ T

Let $f: G \to G'$ be a function, and let $S$ denote the set $$ S := \{ f(x+y)-f(x)-f(y): x,y \in G \}.$$ Then there exists a homomorphism $\phi: G \to G'$ such that $$ |\{f(x) - \phi(x)\}| \leq |S|^{10}. $$