WordProductsAndClosure.lean

theorem wordProducts_one (X : Set G) :
    wordProducts X 1 = X

theorem wordProducts_mul_wordProducts (X : Set G) :
    ∀ m n, wordProducts X m * wordProducts X n = wordProducts X (m + n)
  | m, 0 => by
      simp only [wordProducts, mul_singleton, mul_one, image_id', add_zero]
  | m, n + 1 => by
      calc
        wordProducts X m * wordProducts X (n + 1)
            = wordProducts X m * (wordProducts X n * X) := by
                rfl
        _ = (wordProducts X m * wordProducts X n) * X := by
              rw [mul_assoc]
        _ = wordProducts X (m + n) * X := by
              rw [wordProducts_mul_wordProducts X m n]
        _ = wordProducts X (m + n + 1) := by
              rfl

theorem one_mem_wordProducts {X : Set G} (h1 : (1 : G) ∈ X) :
    ∀ n, (1 : G) ∈ wordProducts X n
  | 0 => by
      simp only [wordProducts, mem_singleton_iff]
  | n + 1 => by
      exact ⟨1, one_mem_wordProducts h1 n, 1, h1, by simp only [mul_one]⟩

theorem wordProducts_subset_closure (X : Set G) :
    ∀ n, wordProducts X n ⊆ ((Subgroup.closure X : Subgroup G) : Set G)
  | 0 => by
      intro x hx
      simp only [wordProducts, mem_singleton_iff] at hx
      simp only [hx, SetLike.mem_coe, one_mem]
  | n + 1 => by
      intro x hx
      rcases hx with ⟨a, ha, b, hb, rfl⟩
      exact (Subgroup.closure X).mul_mem
        (wordProducts_subset_closure X n ha)
        (Subgroup.subset_closure hb)

theorem wordProducts_inv_mem {X : Set G} (hXinv : X = Inv.inv '' X) :
    ∀ {n : ℕ} {x : G}, x ∈ wordProducts X n → x⁻¹ ∈ wordProducts X n
  | 0, x, hx => by
      simpa [wordProducts] using hx
  | n + 1, x, hx => by
      rcases hx with ⟨a, ha, b, hb, rfl⟩
      have hb' : b⁻¹ ∈ X := by
        rw [hXinv]
        exact ⟨b, hb, by simp only⟩
      have ha' : a⁻¹ ∈ wordProducts X n := wordProducts_inv_mem hXinv ha
      have hmem : b⁻¹ * a⁻¹ ∈ wordProducts X 1 * wordProducts X n := by
        exact ⟨b⁻¹, by
          show b⁻¹ ∈ wordProducts X 1
          simpa [wordProducts_one] using hb', a⁻¹, ha', rfl⟩
      have hEq : wordProducts X 1 * wordProducts X n = wordProducts X (1 + n) := by
        simpa using (wordProducts_mul_wordProducts X 1 n)
      have hmem' : b⁻¹ * a⁻¹ ∈ wordProducts X (1 + n) := by
        exact hEq ▸ hmem
      simpa [Nat.succ_eq_add_one, Nat.add_comm] using hmem'

theorem wordProducts_mono_len {X : Set G} (h1 : (1 : G) ∈ X) {m n : ℕ} (hmn : m ≤ n) :
    wordProducts X m ⊆ wordProducts X n

theorem subgroupClosure_eq_iUnion_wordProducts {X : Set G}
    (hXinv : X = Inv.inv '' X) :
    (((Subgroup.closure X : Subgroup G) : Set G)) = ⋃ n, wordProducts X n

theorem wordProducts_isCompact [CompactSpace G] {X : Set G}
    (hXclosed : IsClosed X) :
    ∀ n, IsCompact (wordProducts X n)
  | 0 => by
      simp only [wordProducts, finite_singleton, Finite.isCompact]
  | n + 1 => by
      have hprev : IsCompact (wordProducts X n) := wordProducts_isCompact hXclosed n
      have hEq :
          wordProducts X (n + 1) =
            (fun p : G × G => p.1 * p.2) '' ((wordProducts X n) ×ˢ X) := by
        ext x
        constructor
        · intro hx
          rcases hx with ⟨a, ha, b, hb, rfl⟩
          exact ⟨(a, b), ⟨ha, hb⟩, rfl⟩
        · intro hx
          rcases hx with ⟨⟨a, b⟩, hab, rfl⟩
          exact ⟨a, hab.1, b, hab.2, rfl⟩
      rw [hEq]
      exact (hprev.prod hXclosed.isCompact).image (continuous_fst.mul continuous_snd)

theorem wordProducts_isClosed [CompactSpace G] [T2Space G] {X : Set G}
    (hXclosed : IsClosed X) (n : ℕ) :
    IsClosed (wordProducts X n)

theorem exists_openNormalSubgroup_inf_eq_bot_of_finite
    [CompactSpace G] [TotallyDisconnectedSpace G]
    (K : Subgroup G) [Finite K] :
    ∃ U : OpenNormalSubgroup G, ((U : Subgroup G) ⊓ K) = ⊥