Union of chain of subgroups is a subgroup?

Stream: Is there code for X?

[Terence Tao]

I'm finding my Lean skills have become a little rusty after a few months of disuse, and am struggling to prove something simple, namely that every subgroup H of a group G contains a subgroup K of cardinality at most k that is maximal (in the subgroup order) amongst all such subgroups, if k ≠ 0. I got as far as invoking Zorn's lemma:

import Mathlib

lemma exists_max_subgroup {G : Type*} [AddCommGroup G] (H: AddSubgroup G) {k:ℕ} (hk: k ≠ 0) : ∃ K :
{K: AddSubgroup G // K ≤ H ∧ (K: Set G).ncard ≤ k }, IsMax K := by
  let S := {K: AddSubgroup G // K ≤ H ∧ (K: Set G).ncard ≤ k }
  have : Nonempty S := Nonempty.intro {
      val := ⊥,
      property := by
        simp
        exact Nat.one_le_iff_ne_zero.mpr hk
      }
  refine zorn_le_nonempty ?_
  intro h hc hcnon
  sorry

But now I need to verify that every chain of subgroups of cardinality at most k, is bounded by another subgroup of cardinality at most k.

What I would like to invoke at this point is that the union of a chain of subgroups is again a subgroup, but I wasn't able to find this in lemma in Mathlib. Is it in here somewhere?

Also, I suspect that perhaps my spelling of the above lemma is not ideal (one reason for this is that the subtype used above is not automatically acquiring useful instances such as SetLike or AddSubgroupClass). What I actually want to prove ultimately is this result:

-- Every subgroup H of a finite m-torsion abelian group G contains a subgroup H' of order between k and mk, if 0 < k < |H|.

lemma torsion_exists_subgroup_subset_card_le {G : Type*} {m : ℕ} (hm : m ≥ 2)
    [AddCommGroup G] [Fintype G] (htorsion: ∀ x:G, m • x = 0)
    {k : ℕ} (H : AddSubgroup G) (hk : k ≤ Nat.card H) (h'k : k ≠ 0) :
    ∃ (H' : AddSubgroup G), k ≤ Nat.card H'   ∧ Nat.card H' < m*k ∧ H' ≤ H := by
    sorry

My plan is to first create the maximal subgroup K from the previous lemma, and then add one more element to it to generate H'.

[Kim Morrison]

We have docs#isSubgroup_iUnion_of_directed. Despite it being in a Deprecated folder you can use it. I'm sure someone will provide a non-deprecated version for you!

[Terence Tao]

OK, this was enough for a hint for me to find the non-deprecated method docs#AddSubgroup.coe_iSup_of_directed , which is close enough I guess.

[Terence Tao]

but now what I am missing is the claim that the cardinality of the union of a chain of sets is the supremum of the cardinality of the individual sets. So something like

import Mathlib

example {G: Type*} {S: Set (Set G)} (hchain: IsChain (fun A B ↦ (A ⊆ B)) S) (hnon: Set.Nonempty S) : Set.encard (Set.sUnion S) = sSup (Set.encard '' S) := by
  sorry

Is there something like this in Mathlib already?

[Violeta Hernández]

I've never worked with encard so I'm not sure if what you're describing exists, but I'd like to mention that this result isn't true for Cardinal.mk

[Violeta Hernández]

Intervals Iio x ⊆ ω₁ are all countable, so the supremum of their cardinalities is ℵ₀, but the cardinality of the union is ℵ₁

[Violeta Hernández]

(saying this before anyone gets any ideas of adding it)

[Terence Tao]

Ah, good point. The encard version should still be OK though.

[Terence Tao]

For the record, I did manage to prove the result I wanted:

import Mathlib

-- A silly little set lemma
lemma set_avoid {G:Type*} {A B : Set G} (hA: A ⊆ B) (hneq: A ≠ B) : ∃ a:G, a ∈ B ∧ a ∉ A := by
  contrapose! hneq
  exact Set.Subset.antisymm hA hneq

open Pointwise

/-- Every subgroup H of a finite m-torsion abelian group G contains a subgroup H' of order between k and mk, if 0 < k < |H|. -/
lemma torsion_exists_subgroup_subset_card_le {G : Type*} {m : ℕ} (hm : m ≥ 2)
    [AddCommGroup G] [Fintype G] (htorsion: ∀ x:G, m • x = 0)
    {k : ℕ} (H : AddSubgroup G) (hk : k ≤ Nat.card H) (h'k : k ≠ 0) :
    ∃ (K : AddSubgroup G), Nat.card K ≤ k ∧ k < m * Nat.card K ∧ K ≤ H := by
    let S := {K: AddSubgroup G | K ≤ H ∧ Nat.card K ≤ k }
    have hnon : S.Nonempty := by
      use ⊥
      simp only [Set.mem_setOf_eq, bot_le, AddSubgroup.mem_bot, Nat.card_eq_fintype_card,
        Fintype.card_ofSubsingleton, true_and, S]
      exact Nat.one_le_iff_ne_zero.mpr h'k
    obtain ⟨ K, ⟨ hK, hK' ⟩ ⟩ := Set.Finite.exists_maximal_wrt (fun K:AddSubgroup G ↦ Nat.card K) S (Set.toFinite S) hnon
    simp only [ge_iff_le, Set.mem_setOf_eq, S] at hK
    use K
    refine ⟨ hK.2, ?_, hK.1 ⟩
    rcases LE.le.lt_or_eq hK.1 with heq | heq
    . have hneq : (K:Set G) ≠ (H:Set G) := by
        contrapose! heq
        simp only [SetLike.coe_set_eq] at heq
        simp only [heq, lt_self_iff_false, not_false_eq_true]
      obtain ⟨ a, ⟨ ha, ha' ⟩⟩ := set_avoid hK.1 hneq
      let Z := AddSubgroup.zmultiples a
      let H' := K ⊔ Z
      contrapose! ha'
      have hcard : Nat.card H' ≤ k := by
        apply le_trans _ ha'
        rw [<-SetLike.coe_sort_coe, <-SetLike.coe_sort_coe, AddSubgroup.normal_add K Z, Nat.mul_comm]
        calc
          _ ≤ (Nat.card (K:Set G)) * (Nat.card (Z:Set G)) := Set.card_add_le
          _ ≤ _ := by
            gcongr
            rw [SetLike.coe_sort_coe, Nat.card_zmultiples a]
            apply addOrderOf_le_of_nsmul_eq_zero (Nat.zero_lt_of_lt hm) (htorsion a)
      have hH' : H' ≤ H := by
        simpa only [sup_le_iff, hK.1, AddSubgroup.zmultiples_le, true_and, H', Z]
      have hsub : (K:Set G) ⊆ (H':Set G) := SetLike.coe_subset_coe.mpr le_sup_left
      have hcard' : Nat.card K ≤ Nat.card H' := by
          rw [<-SetLike.coe_sort_coe, <-SetLike.coe_sort_coe, Set.Nat.card_coe_set_eq (K:Set G), Set.Nat.card_coe_set_eq (H':Set G)]
          exact Set.ncard_le_ncard hsub (Set.toFinite H')
      have : (K:Set G) = (H':Set G) := by
          apply (Set.subset_iff_eq_of_ncard_le ?_ ?_).mp hsub
          . apply Eq.le
            rw [<-Set.Nat.card_coe_set_eq (H':Set G), <-Set.Nat.card_coe_set_eq (K:Set G)]
            exact ((hK' H' ⟨ hH', hcard ⟩) hcard').symm
          exact Set.toFinite (H':Set G)
      rw [this]
      exact (le_sup_right : AddSubgroup.zmultiples a ≤ H') (AddSubgroup.mem_zmultiples a)
    rw [heq]
    exact lt_of_le_of_lt hk ((Nat.lt_mul_iff_one_lt_left Nat.card_pos).mpr hm)

I only needed the result for finite groups, so I could use docs#Set.Finite.exists_maximal_wrt without having to mess around with Zorn's lemma after all. But thanks for the help anyways!