Assignment6.lean

import Mathlib.Algebra.CharP.Lemmas
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Nat.Choose.Dvd
import Mathlib.GroupTheory.Index
import Mathlib.GroupTheory.OrderOfElement
import Mathlib.Tactic.Group

/-! # Exercises to practice -/

variable {G H K : Type*} [Group G] [Group H] [Group K]
open Subgroup

-- Prove that the trivial subgroup of the integers has index zero.
example : (⊥ : AddSubgroup ℤ).index = 0 := by
  unfold AddSubgroup.index
  refine Nat.card_eq_zero.mpr ?_
  right
  rw??



/- State and prove that the preimage of `U` under the composition of `φ` and `ψ` is a preimage
of a preimage of `U`. This should be an equality of subgroups! -/
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) : sorry := sorry

/- State and prove that the image of `S` under the composition of `φ` and `ψ`
is a image of an image of `S`. -/
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) : sorry := sorry


/- A ring has characteristic `p` if `1 + ⋯ + 1 = 0`, where we add `1` `p` times to itself.
This is written `CharP` in Lean.
In a module over a ring with characteristic 2, for every element `m` we have `m + m = 0`. -/
example {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [CharP R 2] (m : M) :
    m + m = 0 := by
  sorry
  done

section Frobenius
variable (p : ℕ) [hp : Fact p.Prime] (R : Type*) [CommRing R] [CharP R p]
/- Let's define the Frobenius morphism `x ↦ x ^ p`.
You can use lemmas from the library.
We state that `p` is prime using `Fact p.Prime`.
This allows type-class inference to see that this is true.
You can access the fact that `p` is prime using `hp.out`. -/

def frobeniusMorphism (p : ℕ) [hp : Fact p.Prime] (R : Type*) [CommRing R] [CharP R p] :
  R →+* R := sorry

@[simp] lemma frobeniusMorphism_def (x : R) : frobeniusMorphism p R x = x ^ p := sorry

/- Prove the following equality for iterating the frobenius morphism. -/
lemma iterate_frobeniusMorphism (n : ℕ) (x : R) : (frobeniusMorphism p R)^[n] x = x ^ p ^ n := by
  sorry
  done

/- Show that the Frobenius morphism is injective on a domain. -/
lemma frobeniusMorphism_injective [IsDomain R] :
    Function.Injective (frobeniusMorphism p R) := by
  sorry
  done

/- Show that the Frobenius morphism is bijective on a finite domain. -/
lemma frobeniusMorphism_bijective [IsDomain R] [Finite R] :
    Function.Bijective (frobeniusMorphism p R) := by
  sorry
  done

example [IsDomain R] [Finite R] (k : ℕ) (x : R) : x ^ p ^ k = 1 ↔ x = 1 := by
  sorry
  done

example {R : Type*} [CommRing R] [IsDomain R] [Finite R] [CharP R 2] (x : R) : IsSquare x := by
  sorry
  done

end Frobenius

section Ring
variable {R : Type*} [CommRing R]


/- Let's define ourselves what it means to be a unit in a ring and then
prove that the units of a ring form a group.
Hint: I recommend that you first prove that the product of two units is again a unit,
and that you define the inverse of a unit separately using `Exists.choose`.
Hint 2: to prove associativity, use something like `intros; ext; apply mul_assoc`
(`rw` doesn't work well because of the casts) -/

#check Exists.choose
#check Exists.choose_spec
def IsAUnit (x : R) : Prop := ∃ y, y * x = 1

def IsAUnit.mul {x y : R} (hx : IsAUnit x) (hy : IsAUnit y) : IsAUnit (x * y) := by
  sorry
  done

instance groupUnits : Group {x : R // IsAUnit x} := sorry

-- you have the correct group structure if this is true by `rfl`
example (x y : {x : R // IsAUnit x}) : (↑(x * y) : R) = ↑x * ↑y := by sorry

end Ring


/-! # Exercises to hand in -/

section conjugate

/- Define the conjugate of a subgroup, as the elements of the form `xhx⁻¹` for `h ∈ H`. -/
def conjugate (x : G) (H : Subgroup G) : Subgroup G where
  carrier := { x * h * x⁻¹ | h ∈ H }
  mul_mem' := by
    intro a b ha hb
    simp at *
    obtain ⟨ h1 , ha1, ha2 ⟩ := ha
    obtain ⟨ h2 , hb1, hb2 ⟩ := hb
    use h1 * h2
    rw [← hb2]
    rw [← ha2]
    constructor
    · exact (Subgroup.mul_mem_cancel_right H hb1).mpr ha1
    · simp
    done
  one_mem' := by
    simp
  inv_mem' := by
    intro x₁ hx
    simp at *
    obtain ⟨hex₁ , he_H, he_h⟩ := hx
    use hex₁⁻¹
    constructor
    · exact (Subgroup.inv_mem_iff H).mpr he_H
    · rw [← he_h]
      group
    done


-- Characterise normal subgroups in terms of your definition.
example {H : Subgroup G} : H.Normal ↔ ∀ x : G, conjugate x H = H := by
  constructor
  · intro h
    intro x
    unfold conjugate
    ext y
    simp
    constructor
    · intro ⟨a, haH, ha⟩
      have h' :  (x⁻¹)⁻¹ * a * x⁻¹ ∈ H := Subgroup.Normal.conj_mem' h a haH x⁻¹
      simp at h'
      rw [ha] at h'
      assumption
    · intro hy
      have h' : x⁻¹ * y * x ∈ H := Subgroup.Normal.conj_mem' h y hy x
      use x⁻¹ * y * x
      constructor
      · assumption
      · group
  · intro h
    apply Subgroup.Normal.mk
    intro n hnH
    intro g
    specialize h g
    have hn: g * n * g⁻¹ ∈ conjugate g H := by
      unfold conjugate
      simp
      assumption
    rw [h] at hn
    assumption
  done





/- Prove the following lemmas. In the language of group action (next Tuesday), they prove that
a group acts on its own subgroups by conjugation. -/

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  unfold conjugate
  ext x
  constructor
  · simp
  · simp
  done

lemma conjugate_mul (x y : G) (H : Subgroup G) :
    conjugate (x * y) H = conjugate x (conjugate y H) := by
  ext g
  unfold conjugate
  simp
  constructor
  · intro ⟨a, haH, ha⟩
    use a
    constructor
    · assumption
    · rw [← ha]
      group
  · intro ⟨a, haH, ha⟩
    use a
    constructor
    · assumption
    · rw [← ha]
      group
  done

end conjugate

section finite

section

variable {G : AddSubgroup ℚ}

-- In this section, you will prove a nice group theory fact: `(ℚ, +)` has no non-trivial subgroup
-- of finite index: any finite index subgroup must be `⊤`. Follow the steps below.

-- In the proof we will consider the following subgroup, consisting of all `n`-fold multiples
-- of rational numbers.
def multiple (n : ℕ) : AddSubgroup ℚ where
  carrier := { q | ∃ r : ℚ, n * r = q}
  add_mem' := by
    intro a b
    simp
    intro x hx y hy
    use x + y
    linarith
  zero_mem' := by
    simp
  neg_mem' := by
    simp
    intro a
    use -a
    simp

-- If your definition above is correct, this proof is true by rfl.
lemma mem_multiple_iff (n : ℕ) (q : ℚ) : q ∈ multiple n ↔ ∃ r, n * r = q := by rfl

-- The next lemma is a general fact from group theory: use mathlib to find the right lemma.
-- Hint: it's similar to `Subgroup.pow_index_mem`.

lemma step1 {n : ℕ} (hG : G.index = n) (q : ℚ) : n • q ∈ G := by
  rw [← hG]
  exact AddSubgroup.nsmul_index_mem G q
  done

lemma step2 {n : ℕ} (hG : G.index = n) : multiple n ≤ G := by
  sorry

lemma step3 {n : ℕ} (hn : n ≠ 0) : multiple n = ⊤ := by
  sorry

-- The goal of this exercise: (ℚ, +) has no non-trivial subgroups of finite index.
example (hG : G.index ≠ 0) : G = ⊤ := by
  sorry

end

end finite

section frobenius

/- The Frobenius morphism in a domain of characteristic `p` is the map `x ↦ x ^ p`.
Let's prove that the Frobenius morphism is additive, without using that
fact from the library. A proof sketch is given, and the following results will be useful. -/

#check add_pow
#check CharP.cast_eq_zero_iff

variable (p : ℕ) [hp : Fact p.Prime] (R : Type*) [CommRing R] [IsDomain R] [CharP R p] in
open Nat Finset in
lemma add_pow_eq_pow_add_pow (x y : R) : (x + y) ^ p = x ^ p + y ^ p := by
  have hp' : p.Prime := hp.out
  have range_eq_insert_Ioo : range p = insert 0 (Ioo 0 p) := by
    ext a
    constructor
    · intro h
      simp at *
      by_cases ha : a=0
      · left
        assumption
      · push_neg at ha
        right
        constructor
        · exact zero_lt_of_ne_zero ha
        · assumption
    · intro h
      simp at *
      obtain h1 | h2 := h
      · rw [h1]
        exact pos_of_neZero p
      · obtain ⟨ha1, ha2⟩ := h2
        assumption
  have dvd_choose : ∀ i ∈ Ioo 0 p, p ∣ Nat.choose p i := by
    simp
    intro i hi_0 hi_p
    refine Prime.dvd_choose_self hp' ?_ hi_p
    linarith
  have h6 : ∑ i ∈ Ioo 0 p, x ^ i * y ^ (p - i) * Nat.choose p i = 0 :=
    calc
     _ =  ∑ i ∈ Ioo 0 p, x ^ i * y ^ (p - i) * 0 := by
      have h_help (i : Ioo 0 p) : (Nat.choose p i  : R)= 0 := by
        specialize dvd_choose i
        simp at dvd_choose
        rw [CharP.cast_eq_zero_iff R p]
        assumption
      rw [sum_congr]
      rfl
      intro i hi
      specialize dvd_choose i
      simp at dvd_choose
      simp
      right
      rw [CharP.cast_eq_zero_iff R p ↑(p.choose i)]
      simp at hi
      obtain ⟨hi1, hi2⟩ := hi
      specialize dvd_choose hi1 hi2
      assumption
     _ = 0 := by
      simp
  rw [@add_pow_expChar]
  done

end frobenius