Erdős Problem 274

References: erdosproblems.com/274 Wikipedia

structure Erdos274.Group.ExactCovering (G : Type u_1) [Group G] (ι : Type u_2) [Fintype ι] : Type (max u_1 u_2)

An exact covering of a group G is a finite collection of subgroups {H_1, ..., H_k} and representative {g_1, ..., g_k} such that the cosets g_iH_i are pairwise disjoint and their union covers G.

Note that this differs from Partition (α := Subgroup G) because the covering condition there invokes Subgroup.sup which is subgroup generation and thus stronger than union. This definition is easier to use in this contect than the alternative Partition (α := Set G), which lacks subgroup definitions such as Subgroup.index.

• parts : ι → Subgroup G
• reps : ι → G
• nonempty (i : ι) : (↑(self.parts i)).Nonempty
• disjoint : Set.univ.PairwiseDisjoint fun (i : ι) => self.reps i • ↑(self.parts i)
• covers : ⋃ (i : ι), self.reps i • ↑(self.parts i) = Set.univ

theorem Erdos274.erdos_274 : sorry ↔ ∀ (G : Type u_1) (h : Group G), 1 < ENat.card G → ∃ (ι : Type u_2) (x : Fintype ι) (P : Group.ExactCovering G ι), 1 < Fintype.card ι ∧ (Set.range P.parts).Pairwise fun (A B : Subgroup G) => Cardinal.mk ↥A ≠ Cardinal.mk ↥B

If G is a 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 Erdos274.erdos_274.variants.abelian {G : Type u_1} [Fintype G] [CommGroup G] (hG : 1 < Fintype.card G) {ι : Type u_2} [Fintype ι] (P : Group.ExactCovering G ι) (hι : 1 < Fintype.card ι) : ∃ (i : ι) (j : ι), i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)

If G is a finite abelian group then there cannot 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 Erdos274.herzog_schonheim {G : Type u_1} [Group G] (hG : 1 < ENat.card G) {ι : Type u_2} [Fintype ι] (hι : 1 < Fintype.card ι) (P : Group.ExactCovering G ι) : ∃ (i : ι) (j : ι), i ≠ j ∧ (P.parts i).index = (P.parts j).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.