Erdős Problem 274

References: erdosproblems.com/274 Wikipedia

theorem erdos_274 : (∀ (G : Type u_1) [inst : CommGroup G], ∃ (P : Partition ⊤), 1 < P.parts.ncard ∧ (∀ A ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑A) ∧ P.parts.Pairwise fun (A B : Subgroup G) => Cardinal.mk ↥A ≠ Cardinal.mk ↥B) ↔ sorry

If G is an abelian group then can there exist an exact covering of G by more than one cosets of different sizes? (i.e. each element is contained in exactly one of the cosets.)

theorem erdos_274.variants.nonabelian : (∀ (G : Type u_1) [inst : Group G] [inst_1 : Fintype G], ∃ (P : Partition ⊤), 1 < P.parts.ncard ∧ (∀ A ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑A) ∧ P.parts.Pairwise fun (A B : Subgroup G) => Cardinal.mk ↥A ≠ Cardinal.mk ↥B) ↔ sorry

In [Er97c] Erdős asks this for finite (not necessarily abelian) groups.

[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erd\H{o}s, I (1997), 47-67.

theorem herzog_schonheim (G : Type u_1) [Group G] (P : Partition ⊤) : 1 < P.parts.ncard → (∀ B ∈ P.parts, ∃ (s : G) (H : Subgroup G), s • ↑H = ↑B) → ∃ A ∈ P.parts, ∃ B ∈ P.parts, A ≠ B ∧ A.index = B.index

Let $G$ be a group, and let $A = \{a_1G_1, \dots, a_kG_k\}$ be a finite system of left cosets of subgroups $G_1, \dots, G_k$ of $G$.

Herzog and Schönheim conjectured that if $A$ forms a partition of $G$ with $k > 1$, then the indices $[G:G_1], \dots, [G:G_k]$ cannot be distinct.