Disjoint coset systems

DefinitionG-harmonic tuples#✓fully proved

Let \(G\) be a group and \(a = (a_1, \dots, a_n)\) a tuple of natural numbers. The tuple \(a\) is \(G\)-harmonic if every \(a_i\) is positive and there exist subgroups \(U_1, \dots, U_n\) of \(G\) and elements \(g_1, \dots, g_n \in G\) such that \(U_i\) has index \(a_i\) in \(G\) for every \(i\) and the left cosets \(g_1 U_1, \dots, g_n U_n\) are pairwise disjoint.

def IsGHarmonic (G : Type*) [Group G] {n : ℕ} (a : Fin n → ℕ) : Prop :=
  (∀ i, 0 < a i) ∧
    ∃ (U : Fin n → Subgroup G) (g : Fin n → G),
      (∀ i, (U i).index = a i) ∧
        Set.PairwiseDisjoint Set.univ (fun i => g i • (↑(U i) : Set G))

Used by 7

Used byConstructing a G-harmonic tuple · The empty tuple is G-harmonic · Characterization of G-harmonic tuples · The tuple (1) is G-harmonic · Tuples with a zero entry are not G-harmonic · Entries of a G-harmonic tuple are positive · Witnesses for a G-harmonic tuple

TheoremConstructing a G-harmonic tuple#✓fully proved

Let \(G\) be a group and \(a = (a_1, \dots, a_n)\) a tuple of natural numbers with every \(a_i\) positive. If \(U_1, \dots, U_n\) are subgroups of \(G\) such that \(U_i\) has index \(a_i\) in \(G\) for every \(i\), and \(g_1, \dots, g_n \in G\) are elements such that the left cosets \(g_1 U_1, \dots, g_n U_n\) are pairwise disjoint, then \(a\) is \(G\)-harmonic.

theorem IsGHarmonic.intro {G : Type*} [Group G] {n : ℕ} {a : Fin n → ℕ}
    (hpos : ∀ i, 0 < a i) (U : Fin n → Subgroup G) (g : Fin n → G)
    (hidx : ∀ i, (U i).index = a i)
    (hdisj : Set.PairwiseDisjoint Set.univ (fun i => g i • (↑(U i) : Set G))) :
    IsGHarmonic G a

Uses 1

Statement usesG-harmonic tuples

TheoremEntries of a G-harmonic tuple are positive#✓fully proved

Let \(G\) be a group. If a tuple \(a = (a_1, \dots, a_n)\) of natural numbers is \(G\)-harmonic, then \(a_i > 0\) for every \(i\).

theorem IsGHarmonic.pos {G : Type*} [Group G] {n : ℕ} {a : Fin n → ℕ}
    (h : IsGHarmonic G a) (i : Fin n) : 0 < a i

Uses 1 · Used by 1

Statement usesG-harmonic tuples

Used byTuples with a zero entry are not G-harmonic

TheoremWitnesses for a G-harmonic tuple#✓fully proved

Let \(G\) be a group. If a tuple \(a = (a_1, \dots, a_n)\) of natural numbers is \(G\)-harmonic, then there exist subgroups \(U_1, \dots, U_n\) of \(G\) and elements \(g_1, \dots, g_n \in G\) such that \(U_i\) has index \(a_i\) in \(G\) for every \(i\) and the left cosets \(g_1 U_1, \dots, g_n U_n\) are pairwise disjoint.

theorem IsGHarmonic.witnesses {G : Type*} [Group G] {n : ℕ} {a : Fin n → ℕ}
    (h : IsGHarmonic G a) :
    ∃ (U : Fin n → Subgroup G) (g : Fin n → G),
      (∀ i, (U i).index = a i) ∧
        Set.PairwiseDisjoint Set.univ (fun i => g i • (↑(U i) : Set G))

Uses 1

Statement usesG-harmonic tuples

TheoremCharacterization of G-harmonic tuples#✓fully proved

Let \(G\) be a group and \(a = (a_1, \dots, a_n)\) a tuple of natural numbers. Then \(a\) is \(G\)-harmonic if and only if every \(a_i\) is positive and there are subgroups \(U_1, \dots, U_n\) of \(G\) and elements \(g_1, \dots, g_n \in G\) such that \(U_i\) has index \(a_i\) in \(G\) for every \(i\) and the left cosets \(g_1 U_1, \dots, g_n U_n\) are pairwise disjoint.

theorem isGHarmonic_iff {G : Type*} [Group G] {n : ℕ} (a : Fin n → ℕ) :
    IsGHarmonic G a ↔
      (∀ i, 0 < a i) ∧
        ∃ (U : Fin n → Subgroup G) (g : Fin n → G),
          (∀ i, (U i).index = a i) ∧
            Set.PairwiseDisjoint Set.univ (fun i => g i • (↑(U i) : Set G))

Uses 1

Statement usesG-harmonic tuples

TheoremThe empty tuple is G-harmonic#✓fully proved

For every group \(G\), the empty tuple of natural numbers is (vacuously) \(G\)-harmonic.

theorem isGHarmonic_empty {G : Type*} [Group G] :
    IsGHarmonic G (n := 0) Fin.elim0

Uses 1

Statement usesG-harmonic tuples

TheoremThe tuple (1) is G-harmonic#✓fully proved

For every group \(G\), the one-entry tuple \((1)\) is \(G\)-harmonic; the subgroup \(G\) itself, of index \(1\), with coset representative \(1\) witnesses this.

theorem isGHarmonic_singleton_one {G : Type*} [Group G] :
    IsGHarmonic G (n := 1) (fun _ => 1)

Uses 1

Statement usesG-harmonic tuples

TheoremTuples with a zero entry are not G-harmonic#✓fully proved

Let \(G\) be a group. If a tuple \(a = (a_1, \dots, a_n)\) of natural numbers has \(a_i = 0\) for some \(i\), then \(a\) is not \(G\)-harmonic.

theorem not_isGHarmonic_of_zero {G : Type*} [Group G] {n : ℕ} {a : Fin n → ℕ}
    (i : Fin n) (h0 : a i = 0) : ¬ IsGHarmonic G a

Uses 2

Statement usesG-harmonic tuples

Proof usesEntries of a G-harmonic tuple are positive

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.