MathAdv_10.lean

import Mathlib

open scoped BigOperators
open scoped Real
open scoped Nat
open scoped Classical
open scoped Pointwise

set_option maxHeartbeats 8000000
set_option maxRecDepth 4000
set_option synthInstance.maxHeartbeats 20000
set_option synthInstance.maxSize 128

set_option relaxedAutoImplicit false
set_option autoImplicit false

set_option pp.fullNames true
set_option pp.structureInstances true
set_option pp.coercions.types true
set_option pp.funBinderTypes true
set_option pp.letVarTypes true
set_option pp.piBinderTypes true

set_option grind.warning false

/-- A subgroup has index three. -/
def HasIndexThree {G : Type*} [Group G] [Fintype G] (H : Subgroup G) : Prop :=
  H.index = 3

/-- Every integer power of an involution is either the identity or the element itself. -/
lemma zpow_involution_eq_one_or_self {G : Type*} [Group G] (g : G) (hg : g ^ 2 = 1) (n : ℤ) :
    g ^ n = 1 ∨ g ^ n = g := by
  have h2 : g ^ (2 : ℤ) = 1 := by rw [zpow_two, ← pow_two, hg]
  rcases Int.even_or_odd n with ⟨k, hk⟩ | ⟨k, hk⟩
  · left
    subst hk
    rw [show k + k = 2 * k by ring, zpow_mul, h2, one_zpow]
  · right
    subst hk
    rw [zpow_add_one, zpow_mul, h2, one_zpow, one_mul]

/-- The transposition `(0 1)` in `S₃` has order two. -/
lemma orderOf_swap01 : orderOf (Equiv.swap (0 : Fin 3) 1) = 2 := by
  apply orderOf_eq_prime
  · rw [pow_two, Equiv.swap_mul_self]
  · intro h
    exact absurd (congrArg (fun f => f 0) h) (by decide)

/-- The subgroup of `S₃` generated by the transposition `(0 1)`. -/
noncomputable def H01 : Subgroup (Equiv.Perm (Fin 3)) :=
  Subgroup.zpowers (Equiv.swap (0 : Fin 3) 1)

lemma H01_index : HasIndexThree H01 := by
  have hcard : Nat.card (Equiv.Perm (Fin 3)) = 6 := by
    rw [Nat.card_eq_fintype_card, Fintype.card_perm]
    decide
  have h := Subgroup.index_mul_card H01
  rw [hcard, H01, Nat.card_zpowers, orderOf_swap01] at h
  simpa [HasIndexThree, H01] using (by omega : (Subgroup.zpowers (Equiv.swap (0 : Fin 3) 1)).index = 3)

lemma H01_not_normal : ¬ H01.Normal := by
  intro hN
  have hmem : Equiv.swap (0 : Fin 3) 1 ∈ H01 := Subgroup.mem_zpowers _
  have hconj := hN.conj_mem _ hmem (Equiv.swap (1 : Fin 3) 2)
  obtain ⟨n, hn⟩ := hconj
  simp only [] at hn
  have hsq : (Equiv.swap (0 : Fin 3) 1) ^ 2 = 1 := by rw [pow_two, Equiv.swap_mul_self]
  rcases zpow_involution_eq_one_or_self (Equiv.swap (0 : Fin 3) 1) hsq n with h | h <;>
    rw [h] at hn <;> revert hn <;> decide

/-- The statement "a subgroup of index 3 is normal" is false:
`S₃` has a subgroup of index `3` (generated by a transposition) that is not normal. -/
theorem Gallian_11 :
    ∃ H : Subgroup (Equiv.Perm (Fin 3)),
      HasIndexThree (G := Equiv.Perm (Fin 3)) H ∧ ¬ H.Normal :=
  ⟨H01, H01_index, H01_not_normal⟩