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^{\prime }$ when $G,G^{\prime }$ are elementary abelian 2-groups.
• homomorphism_pfr : If $f:G\to G^{\prime }$ 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 $\varphi :G\to G^{\prime }$ such that $f(x)-\varphi (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 $\varphi :H_0\to G^{\prime }$ can be extended to a homomorphism $\tilde{\varphi }:G\to G^{\prime }$.

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^{\prime }$. Then there exists a subgroup $H_0$ of $G$, a subgroup $H_1$ of $G^{\prime }$, and a homomorphism $\varphi :G\to G^{\prime }$ such that $$H:=\{(x,\varphi (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^{\prime }$ 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 $\varphi :G\to G^{\prime }$ such that $$|\{f(x)-\varphi (x)\}|\le |S{|}^{10}.$$