a question by contradiction

Stream: mathlib4

[Move fast]

I want to show if a group has no non-trivial subgroups, then it must be a cyclic group of order $p$. I meet a problem that I don't know how to show the $p$ is prime by contradiction in Lean.

  import Mathlib
open Subgroup Nat

/--
Define variables: Declare the group G with its group structure.
-/
variable {G : Type*} [Group G]

/--
Lemma: If a group G has no nontrivial proper subgroups, then G is cyclic.
-/
lemma no_non_trivial_proper_subgroups_is_cyclic
  {G : Type*} [Group G]
  (h : ∀ H : Subgroup G, H = ⊥ ∨ H = ⊤ ) :
  ∃ (g : G), ∀ (x : G),  ∃ n : ℤ, x =  g ^ n := by
  -- First, check if there exists a non-identity element in G
  by_cases h1 : ∃ g : G, g ≠ 1
  · -- If there is a non-identity element, name it g₁ and prove it generates G
    rcases h1 with ⟨g₁, hg₁⟩
    -- Assume for contradiction that G is not cyclic
    by_contra hep
    push_neg at hep
    -- Prove the subgroup generated by g₁ is nontrivial
    have h2 : ¬ (Subgroup.zpowers g₁ = ⊥) := by exact Subgroup.zpowers_ne_bot.mpr hg₁
    -- This subgroup must equal the entire group due to the assumption
    have h3 : Subgroup.zpowers g₁ = ⊤ := by apply (or_iff_right h2).mp  (h (Subgroup.zpowers g₁))
    -- Use contradiction to find an element not generated by g₁
    rcases hep g₁ with ⟨x₁, hx₁⟩
    -- Show this element must lie in the subgroup, leading to contradiction
    have : x₁ ∉ Subgroup.zpowers g₁ := by
      by_contra heq
      have : ∃ n₁ : ℤ ,  g₁ ^ n₁ = x₁ := by apply Subgroup.mem_zpowers_iff.mp heq
      rcases this with ⟨n₁, hn₁⟩
      have : x₁ ≠ x₁ := by nth_rw 2 [← hn₁]; apply hx₁
      contradiction
    have : x₁ ∈ Subgroup.zpowers g₁ := by rw[h3]; exact trivial
    contradiction
  · -- If G has no non-identity elements, it is trivial and cyclic
    push_neg at h1
    use 1; intro x; use 0
    simp only [zpow_zero]
    apply h1 x

/--
Theorem 1: If a group G has no nontrivial proper subgroups, then its order is either 1 or a prime number.
-/
theorem card_eq_one_or_prime
    (h : ∀ H : Subgroup G, H = ⊥ ∨ H = ⊤) :
    Nat.card G = 1 ∨ ∃ p : ℕ, Nat.Prime p ∧ Nat.card G = p := by
  -- By Lemma, G is cyclic
  have h1 : ∃ (g : G), ∀ (x : G),  ∃ n : ℤ, x =  g ^ n := no_non_trivial_proper_subgroups_is_cyclic h
  rcases h1 with ⟨g, hg⟩
  -- Case 1: G has order 1
  by_cases h2 : Nat.card G = 1
  · exact Or.inl h2
  -- Case 2: Order must be prime
  · right
    use Nat.card G
    constructor
    · -- Proof that the order is prime (omitted as marked with `sorry`)
      apply sorry
    · rfl

/--
Theorem 2: A group of prime order has only trivial subgroups.
-/
theorem p_has_trivial {G : Type*} [Group G] (H : Subgroup G) [hp : Fact (Nat.Prime (Nat.card G))]  : H = ⊥ ∨ H = ⊤ :=by
  -- Use built-in Mathlib lemma for prime-order groups [[9]]
  exact Subgroup.eq_bot_or_eq_top_of_prime_card H

I don't know how to show:

  -- Case 2: Order must be prime
  · right
    use Nat.card G
    constructor
    · -- Proof that the order is prime (omitted as marked with `sorry`)
      apply sorry
    · rfl

[Michał Mrugała]

(deleted)

[Edison Xie]

(deleted)

[Michał Mrugała]

Edison falling for the same trap as me. Do you have a proof of this on paper that you want to formalize? Also, this probably belongs in #new members.

[Aaron Liu]

You can use by_contra h to argue by contradiction.

[Aaron Liu]

This tactic will give you a hypothesis called h which is the negation of your goal, and it will change your goal to be False.

[Aaron Liu]

You can also contrapose! h, to contrapose with an existing hypothesis h.

[Aaron Liu]

In your case, this will change h to say that Nat.card G is not prime, and change your goal to say that there exists a nontrivial proper subgroup of G.

[Kevin Buzzard]

@Move fast can you clarify if your code was written by an LLM? The maintainers are strongly considering insisting on people who post LLM-generated code declare this. You have posted a whole bunch of code but you have got nowhere near actually embarking on the guts of the question, and now you're asking other people to do your work for you without clarifying that you haven't actually done any work yourself on the question.

[Move fast]

It was not from LLM! I just want to know how can I represent Nat.card G in lean, if it is not a prime by contradiction. Maybe I need to give a proof of this question on paper:joy:

[Kevin Buzzard]

Yes that would be good.. Why not write a maths proof first

[Jz Pan]

Aaron Liu said:

In your case, this will change h to say that Nat.card G is not prime, and change your goal to say that there exists a nontrivial proper subgroup of G.

I think this result is not trivial in group theory, as you need Sylow subgroups.

[Jz Pan]

Oh, you can take any non-trivial element in G and it generates a cyclic subgroup. If it is not equal to G then it's done. If it is equal to G but #G is not prime, then it has a proper cyclic subgroup.

[Edison Xie]

I don't know why is it finite

[Edison Xie]

but the rest of the proof is rather trivial

[Edison Xie]

import Mathlib


variable {G : Type*} [Group G]

lemma no_non_trivial_proper_subgroups_is_cyclic
  {G : Type*} [Group G]
  (h : ∀ H : Subgroup G, H = ⊥ ∨ H = ⊤ ) :
  ∃ (g : G), ∀ (x : G),  ∃ n : ℤ, x = g ^ n := by
  by_cases h1 : ∃ g : G, g ≠ 1
  · rcases h1 with ⟨g₁, hg₁⟩
    by_contra hep
    push_neg at hep
    have h2 : ¬ (Subgroup.zpowers g₁ = ⊥) := Subgroup.zpowers_ne_bot.mpr hg₁
    have h3 : Subgroup.zpowers g₁ = ⊤ := by apply (or_iff_right h2).mp  (h (Subgroup.zpowers g₁))
    rcases hep g₁ with ⟨x₁, hx₁⟩
    have : x₁ ∉ Subgroup.zpowers g₁ := by
      by_contra heq
      have : ∃ n₁ : ℤ ,  g₁ ^ n₁ = x₁ := by apply Subgroup.mem_zpowers_iff.mp heq
      rcases this with ⟨n₁, hn₁⟩
      have : x₁ ≠ x₁ := by nth_rw 2 [← hn₁]; apply hx₁
      contradiction
    have : x₁ ∈ Subgroup.zpowers g₁ := by rw[h3]; exact trivial
    contradiction
  · push_neg at h1
    use 1; intro x; use 0
    simp only [zpow_zero]
    apply h1 x

lemma pow_zpow (M : Type*) [Group M] (g : M) (n : ℕ) (m : ℤ): (g^n)^m = g^(n*m) := by
  induction m with
  | hz => simp
  | hp i hi => rw [zpow_add, hi, mul_add, zpow_add, mul_one, zpow_one, (zpow_natCast g n)]
  | hn i hi =>
    rw [zpow_sub, hi, mul_sub, zpow_sub, mul_one, zpow_one, (zpow_natCast g n)]

lemma zpow_eq_self_iff (M : Type*) [Group M] (g : M) (n : ℤ): g^n = g ↔ g^(n-1) = 1 :=
  ⟨fun h ↦ by apply_fun (· * g⁻¹) at h; rwa [mul_inv_cancel, ← zpow_sub_one] at h,
  fun h ↦ by apply_fun (· * g) at h; rwa [one_mul, ← zpow_add_one, sub_add_cancel] at h⟩

open Subgroup Nat in
theorem card_eq_one_or_prime
    (h : ∀ H : Subgroup G, H = ⊥ ∨ H = ⊤) :
    Nat.card G = 1 ∨ ∃ p : ℕ, Nat.Prime p ∧ Nat.card G = p := by
  obtain ⟨g, hg⟩ := no_non_trivial_proper_subgroups_is_cyclic h
  haveI : Nonempty G := ⟨g⟩
  if Nat.card G = 1 then tauto else
  right
  haveI : Finite G := sorry
  haveI := Nat.card_ne_zero (α := G)|>.2 ⟨inferInstance, inferInstance⟩
  simp only [prime_def_lt', exists_eq_right']
  refine ⟨by omega, ?_⟩
  by_contra! hh
  obtain ⟨m, hm1, hm2, hm3⟩ := hh
  specialize h (Subgroup.zpowers (g^m))
  by_contra! hgm
  have h0 : Subgroup.zpowers g = ⊤ := SetLike.ext_iff.2 fun x ↦ by
    simp only [mem_zpowers_iff, mem_top, iff_true]
    exact ⟨hg x|>.choose, hg x|>.choose_spec.symm⟩
  have h1 : Nat.card G = orderOf g := by
    have heq := (card_top (G := G)).symm
    rw [← h0] at heq
    simpa [card_zpowers] using heq
  rw [h1] at hm2 hm3
  refine h.elim (Subgroup.ne_bot_iff_exists_ne_one.2 ⟨⟨g^m, by simp⟩, fun hgm ↦ ?_⟩) fun hgm ↦ ?_
  · simp at hgm
    have ord_le := orderOf_le_of_pow_eq_one (by omega) hgm
    omega
  · simp [Subgroup.eq_top_iff', mem_zpowers_iff] at hgm
    obtain ⟨k, hk⟩ := hgm g
    rw [pow_zpow, zpow_eq_self_iff, ← pow_natAbs_eq_one] at hk
    have := orderOf_dvd_of_pow_eq_one hk
    simp at this
    have div := Nat.dvd_iff_dvd_dvd _ _ |>.1 this m hm3
    have := Int.eq_one_of_dvd_one (by omega) <| Int.dvd_iff_dvd_of_dvd_sub
      (Int.ofNat_dvd_left.2 div)|>.1 <| Int.dvd_mul_right _ _
    omega

[Move fast]

If it is an infinite cyclic group then it will be isomorphic to ℤ , then it has infinite nontrivial subgroups. But I also don't know how to show this.

[Move fast]

Thank you very much. Maybe I need to learn more about Lean. I thought a question about
if n is not equal 1, then n ≥ 2(When n is a natural number). I even can't solve this question by lean :joy:

[Ruben Van de Velde]

Note that zero is a natural number in lean

[Move fast]

How can I solve this question? I want to use the latter part 'g ^ 2 ≠ 1'.

        -- From orderOf_eq_zero_iff we can get ∀ n > 0, g^n ≠ 1
        have hg_inf : ∀ n : ℕ, 0<n → g ^ n ≠ 1 := by
          rw [orderOf_eq_zero_iff'] at h0
          exact h0
        --Let H = <g^2>，show that H is neither 1 nor G.
        have h_ne_bot : Subgroup.zpowers (g ^ 2) ≠ ⊥ :=
          Subgroup.zpowers_ne_bot.mpr (hg_inf 2)--hg_inf 2 is false

image.png

[Aaron Liu]

The error message tells you all you need to know. hg_inf 2 has type 0 < 2 → g ^ 2 ≠ 1, so you need to pass in a proof that 0 < 2.

[Move fast]

Like this?

        -- From orderOf_eq_zero_iff we can get ∀ n > 0, g^n ≠ 1
        have hg_inf : ∀ n : ℕ, 0<n → g ^ n ≠ 1 := by
          rw [orderOf_eq_zero_iff'] at h0
          exact h0
        --Let H = <g^2>，show that H is neither 1 nor G.
        have h_ne_bot : Subgroup.zpowers (g ^ 2) ≠ ⊥ :=
          have : 0 < 2 := by norm_num
          Subgroup.zpowers_ne_bot.mpr (hg_inf 2 this)--hg_inf 2 is false

[Aaron Liu]

like this

        -- From orderOf_eq_zero_iff we can get ∀ n > 0, g^n ≠ 1
        have hg_inf : ∀ n : ℕ, 0<n → g ^ n ≠ 1 := by
          rw [orderOf_eq_zero_iff'] at h0
          exact h0
        --Let H = <g^2>，show that H is neither 1 nor G.
        have h_ne_bot : Subgroup.zpowers (g ^ 2) ≠ ⊥ :=
          have h_zero_lt_two : 0 < 2 := by norm_num
          Subgroup.zpowers_ne_bot.mpr (hg_inf 2 h_zero_lt_two)--hg_inf 2 is false

or like this

        -- From orderOf_eq_zero_iff we can get ∀ n > 0, g^n ≠ 1
        have hg_inf : ∀ n : ℕ, 0<n → g ^ n ≠ 1 := by
          rw [orderOf_eq_zero_iff'] at h0
          exact h0
        --Let H = <g^2>，show that H is neither 1 nor G.
        have h_ne_bot : Subgroup.zpowers (g ^ 2) ≠ ⊥ :=
          Subgroup.zpowers_ne_bot.mpr (hg_inf 2 (by norm_num))--hg_inf 2 is false

[Edison Xie]

open Subgroup Nat in
@[simps]
noncomputable def infiniteCyclicEquivZ [Infinite G] (g : G) (hg : ∀ (x : G), ∃ (n : ℤ), x = g ^ n):
    G ≃* Multiplicative ℤ :=
  have h0 : Subgroup.zpowers g = ⊤ := SetLike.ext_iff.2 fun x ↦ by
    simp only [mem_zpowers_iff, mem_top, iff_true]
    exact ⟨hg x|>.choose, hg x|>.choose_spec.symm⟩
  have h1 : Nat.card G = orderOf g := by
    simpa [← h0, card_zpowers] using card_top (G := G)|>.symm
  {
  toFun g' := hg g'|>.choose
  invFun m := g^(Multiplicative.toAdd m)
  left_inv _ := hg _|>.choose_spec.symm
  right_inv m := by
    simp only
    by_contra! ne
    have := @Exists.choose_spec ℤ (fun n ↦ g ^ Multiplicative.toAdd m = g ^ n)
      (hg (g ^ Multiplicative.toAdd m))
    set n := @Exists.choose ℤ (fun n ↦ g ^ Multiplicative.toAdd m = g ^ n)
      (hg (g ^ Multiplicative.toAdd m)) with n_eq
    apply_fun (· * g^(-n)) at this
    rw [← zpow_add, ← zpow_add, add_neg_cancel, zpow_zero, Int.add_neg_eq_sub,
      ← pow_natAbs_eq_one] at this
    have := orderOf_dvd_of_pow_eq_one this
    simp [← h1, sub_eq_zero] at this
    exact ne this.symm
  map_mul' g1 g2 := by
    have eq1 := hg (g1 * g2)|>.choose_spec
    set mm := hg (g1 * g2)|>.choose
    have eq2 := hg g1|>.choose_spec
    have eq3 := hg g2|>.choose_spec
    set m1 := hg g1|>.choose
    set m2 := hg g2|>.choose
    simp [eq2, eq3, ← zpow_add] at eq1
    change mm = m1 + m2
    by_contra! ne
    apply_fun (· * g^(-mm)) at eq1
    rw [← zpow_add, ← zpow_add, add_neg_cancel, zpow_zero, Int.add_neg_eq_sub,
      ← pow_natAbs_eq_one] at eq1
    have := orderOf_dvd_of_pow_eq_one eq1
    simp [← h1, sub_eq_zero] at this
    exact ne this.symm
  }

Is this the equivalence you have in mind? @Move fast

[Edison Xie]

this is terrible code though :(

[Move fast]

Yes, you are so cool. In mathematical language, it is easy to understand, but in Lean, it is very difficult for me to type the code to prove it. @Edison Xie

[Maja Kądziołka]

btw instead of choose and choose spec, I usually do obtain \<a, ha> := Classical.indefiniteDescription hexists

[Move fast]

(deleted)

[Move fast]

-- H' ≠ ⊤

    have H'_ne_top : H' ≠ ⊤ := by

      intro h0

  --  H = 2ℤ , 1 ∉ H

      have one_not_mem : (Multiplicative.ofAdd 1) ∉ H := by

        intro h1

        -- If 1 ∈ 2ℤ，then ∃ n such that 2 * n = 1, contradiction

        rcases Subgroup.mem_zpowers_iff.mp h1 with ⟨n, hn⟩

        -- rw Multiplicative.ofAdd

        rw [← Int.ofAdd_mul 2 n,] at hn

        have con:2 * n = 1 := by

  -- use Multiplicative.ofAdd

          exact Multiplicative.ofAdd.injective hn

        have :2 ∣ 1 := by

          use n.toNat

          nth_rw 2[con]

image.png

I want to make

1=2*n.toNat \iff  2*n=1

but "type mismatch", what can I do?

[Robin Arnez]

you can try

apply_fun (· % 2) at con
simp at con

instead of what you're doing

[Maja Kądziołka]

(is omega not able to conclude here already?)