/CoxeterAristotle.lean at 1668fbcd6f2bfaa6a93c4a73f6dbb1ce9a1b9cb2

/-
This file was edited by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid: eedeabe9-b440-4963-9d51-df6cf6bda648

The following was proved by Aristotle:

- lemma A2_weyl_group_card : Nat.card (CoxeterMatrix.Aₙ 2).Group = 6
-/

import Mathlib


noncomputable section AristotleLemmas

#check PresentedGroup.toGroup
#check (CoxeterMatrix.Aₙ 2).Group
#synth Group (DihedralGroup 3)

/-
Homomorphism from A2 to D3.
-/
def f_A2_to_D3 (i : Fin 2) : DihedralGroup 3 :=
  if i.val = 0 then DihedralGroup.sr 0 else DihedralGroup.sr 1

theorem f_A2_to_D3_rels : ∀ r ∈ (CoxeterMatrix.Aₙ 2).relationsSet,
    (FreeGroup.lift f_A2_to_D3) r = 1 := by
      intro r;
      intro hr;
      cases hr ; aesop;
      fin_cases fst <;> fin_cases snd <;> simp +decide [ CoxeterMatrix.Aₙ ]

def hom_A2_to_D3 : (CoxeterMatrix.Aₙ 2).Group →* DihedralGroup 3 :=
  PresentedGroup.toGroup f_A2_to_D3_rels

#check CoxeterMatrix.simple
#check CoxeterMatrix.Group
#print CoxeterMatrix.simple

/-
Generators and relations for A2.
-/
def s0 : (CoxeterMatrix.Aₙ 2).Group := @CoxeterMatrix.simple (Fin 2) (CoxeterMatrix.Aₙ 2) 0
def s1 : (CoxeterMatrix.Aₙ 2).Group := @CoxeterMatrix.simple (Fin 2) (CoxeterMatrix.Aₙ 2) 1

lemma s0_sq : s0 * s0 = 1 := by
  convert QuotientGroup.eq.mpr _;
  convert Subgroup.normalClosure_mono _ _;
  exact { ( FreeGroup.of 0 ) * ( FreeGroup.of 0 ) };
  · simp +decide [ CoxeterMatrix.relationsSet ];
  · exact Subgroup.inv_mem _ ( Subgroup.subset_normalClosure ( Set.mem_singleton _ ) )
lemma s1_sq : s1 * s1 = 1 := by
  erw [ QuotientGroup.eq_one_iff ];
  refine' Subgroup.subset_normalClosure _;
  exact ⟨ 1, by simp +decide ⟩
lemma s0s1_pow3 : (s0 * s1) ^ 3 = 1 := by
  apply QuotientGroup.eq.mpr;
  norm_num +zetaDelta at *;
  exact Subgroup.subset_normalClosure ( Set.mem_setOf.mpr <| by exact ⟨ ( 0, 1 ), by simp +decide [ pow_succ ] ⟩ )

/-
Braid relation for A2.
-/
lemma braid_rel : s0 * s1 * s0 = s1 * s0 * s1 := by
  -- From $(s_0 s_1)^3 = 1$, we have $s_0 s_1 s_0 s_1 s_0 s_1 = 1$.
  have h_braid : s0 * s1 * s0 * s1 * s0 * s1 = 1 := by
    convert s0s1_pow3 using 1;
  -- From $(s_0 s_1)^3 = 1$, we have $s_0 s_1 s_0 = (s_1 s_0 s_1)^{-1}$.
  have h_inv : s0 * s1 * s0 = (s1 * s0 * s1)⁻¹ := by
    exact eq_inv_of_mul_eq_one_left ( by simpa [ mul_assoc ] using h_braid );
  -- Since $s_0^2 = 1$ and $s_1^2 = 1$, they are their own inverses.
  have h_inv_self : s0⁻¹ = s0 ∧ s1⁻¹ = s1 := by
    exact ⟨ inv_eq_of_mul_eq_one_right ( by simpa [ mul_assoc ] using s0_sq ), inv_eq_of_mul_eq_one_right ( by simpa [ mul_assoc ] using s1_sq ) ⟩;
  aesop

/-
Commutation lemmas for s0 and s0s1.
-/
lemma s0s1_inv : (s0 * s1)⁻¹ = s1 * s0 := by
  -- Since $s0$ and $s1$ are involutions, we have $s0⁻¹ = s0$ and $s1⁻¹ = s1$.
  have h_inv : s0⁻¹ = s0 ∧ s1⁻¹ = s1 := by
    simp ( config := { decide := Bool.true } ) [ inv_eq_iff_mul_eq_one, s0_sq, s1_sq ];
  rw [ mul_inv_rev, h_inv.1, h_inv.2 ]

lemma s0s1_mul_s0 : (s0 * s1) * s0 = s0 * (s0 * s1)⁻¹ := by
  have h_inv : s0⁻¹ = s0 ∧ s1⁻¹ = s1 := by
    simp ( config := { decide := Bool.true } ) [ inv_eq_iff_mul_eq_one, s0_sq, s1_sq ];
  simp ( config := { decide := Bool.true } ) [ h_inv, mul_assoc ]

lemma s0s1_pow_mul_s0 (n : ℕ) : (s0 * s1) ^ n * s0 = s0 * (s0 * s1)⁻¹ ^ n := by
  induction n <;> simp_all ( config := { decide := Bool.true } ) [ pow_succ, mul_assoc ];
  simp_all ( config := { decide := Bool.true } ) [ ← mul_assoc ];
  simp_all ( config := { decide := Bool.true } ) [ mul_assoc, inv_eq_of_mul_eq_one_right ( show s0 * s0 = 1 from s0_sq ), inv_eq_of_mul_eq_one_right ( show s1 * s1 = 1 from s1_sq ) ]

lemma s0s1_zpow_mul_s0 (z : ℤ) : (s0 * s1) ^ z * s0 = s0 * (s0 * s1)⁻¹ ^ z := by
  induction z using Int.induction_on <;> aesop;
  · simp_all ( config := { decide := Bool.true } ) [ zpow_add, mul_assoc ];
    simp_all ( config := { decide := Bool.true } ) [ ← mul_assoc ];
    -- Using the fact that $s0$ and $s1$ are inverses of themselves, we can simplify the expression.
    have h_inv : s0⁻¹ = s0 ∧ s1⁻¹ = s1 := by
      exact ⟨ inv_eq_of_mul_eq_one_right ( by simpa [ mul_assoc ] using s0_sq ), inv_eq_of_mul_eq_one_right ( by simpa [ mul_assoc ] using s1_sq ) ⟩;
    simp_all ( config := { decide := Bool.true } ) [ mul_assoc ];
  · simp_all +decide [ zpow_sub, mul_assoc ];
    simp_all +decide [ ← mul_assoc ];
    simp +decide [ ← a, mul_assoc ];
    simp_all +decide [ ← mul_assoc, s0_sq, s1_sq ];
    exact inv_eq_of_mul_eq_one_right ( by rw [ s1_sq ] )

/-
Powers of s0s1 depend only on exponent mod 3.
-/
lemma s0s1_pow_eq_pow_mod_3 (n : ℕ) : (s0 * s1) ^ n = (s0 * s1) ^ (n % 3) := by
  rw [ ← Nat.mod_add_div n 3, pow_add, pow_mul ] ; aesop;
  -- Since $(s0 * s1)^3 = 1$, raising both sides to the power of $(n / 3)$ gives us $((s0 * s1)^3)^{n / 3} = 1^{n / 3} = 1$.
  have h_s0s1_pow3 : (s0 * s1) ^ 3 = 1 := by
    exact?
  rw [h_s0s1_pow3]
  simp

lemma s0s1_zpow_eq_zpow_mod_3 (z : ℤ) : (s0 * s1) ^ z = (s0 * s1) ^ (z % 3) := by
  -- Since $(s0 * s1)^3 = 1$, we can reduce any exponent modulo 3.
  have h_exp_mod : (s0 * s1) ^ 3 = 1 := by
    exact?;
  exact?

/-
Powers of s0s1 depend only on exponent mod 3.
-/
lemma s0s1_pow_mod_3 (n : ℕ) : (s0 * s1) ^ n = (s0 * s1) ^ (n % 3) := by
  exact?

lemma s0s1_zpow_mod_3 (z : ℤ) : (s0 * s1) ^ z = (s0 * s1) ^ (z % 3) := by
  exact?

#print s0s1_pow_eq_pow_mod_3
#print s0s1_zpow_eq_zpow_mod_3

/-
Map definition and commutation lemma.
-/
def map_D3_to_A2_fun : DihedralGroup 3 → (CoxeterMatrix.Aₙ 2).Group
| DihedralGroup.r k => (s0 * s1) ^ (k.val : ℤ)
| DihedralGroup.sr k => s0 * (s0 * s1) ^ (k.val : ℤ)

lemma s0_comm_zpow (z : ℤ) : s0 * (s0 * s1) ^ z * s0 = (s0 * s1) ^ (-z) := by
  rw [mul_assoc, s0s1_zpow_mul_s0, ← mul_assoc, s0_sq, one_mul]
  rw [inv_zpow, zpow_neg]

/-
Arithmetic lemmas for ZMod 3 values.
-/
lemma zmod3_add_val (i j : ZMod 3) : ((i.val : ℤ) + (j.val : ℤ)) % 3 = ((i + j).val : ℤ) % 3 := by
  fin_cases i <;> fin_cases j <;> simp [ZMod.val, Fin.val] <;> rfl

lemma zmod3_sub_val (i j : ZMod 3) : ((j.val : ℤ) - (i.val : ℤ)) % 3 = ((j - i).val : ℤ) % 3 := by
  fin_cases i <;> fin_cases j <;> simp [ZMod.val, Fin.val] <;> rfl

/-
Helper lemma for D3 to A2 map multiplication.
-/
lemma s0s1_zpow_val_eq_zpow_val_sub (i j : ZMod 3) :
  (s0 * s1) ^ (j.val : ℤ) * (s0 * s1) ^ (-(i.val : ℤ)) = (s0 * s1) ^ ((j - i).val : ℤ) := by
    -- By combining the exponents, we get $(s0 * s1)^{j.val - i.val}$.
    have h_combined : (s0 * s1) ^ (j.val : ℤ) * (s0 * s1) ^ (-(i.val : ℤ)) = (s0 * s1) ^ ((j.val - i.val) : ℤ) := by
      group;
    -- By definition of exponentiation, we can rewrite the exponents as integers modulo 3.
    have h_mod3 : (j.val - i.val : ℤ) % 3 = (j - i : ZMod 3).val := by
      fin_cases i <;> fin_cases j <;> trivial;
    rw [ h_combined, ← h_mod3, ← Int.emod_add_ediv ( ( j.val : ℤ ) - i.val ) 3 ] ; norm_num [ zpow_add, zpow_mul ] ;
    erw [ s0s1_pow3 ] ; norm_num;

/-
Map from D3 to A2 is a homomorphism.
-/
lemma map_D3_to_A2_map_one : map_D3_to_A2_fun 1 = 1 := by
  aesop

lemma map_D3_to_A2_map_mul (x y : DihedralGroup 3) :
  map_D3_to_A2_fun (x * y) = map_D3_to_A2_fun x * map_D3_to_A2_fun y := by
    cases' x with x x <;> cases' y with y y <;> simp ( config := { decide := Bool.true } ) [ * ];
    · -- Using the properties of exponents in the group, we can combine the terms.
      have h_exp : (s0 * s1) ^ (x.val : ℤ) * (s0 * s1) ^ (y.val : ℤ) = (s0 * s1) ^ ((x.val + y.val) : ℤ) := by
        rw [ zpow_add ];
      norm_num +zetaDelta at *;
      convert h_exp.symm using 1;
      exact s0s1_zpow_eq_zpow_mod_3 _ ▸ by fin_cases x <;> fin_cases y <;> rfl;
    · -- Using the commutation relation, we can simplify the expression.
      have h_comm : (s0 * s1) ^ (x.val : ℤ) * s0 = s0 * (s0 * s1) ^ (-(x.val : ℤ)) := by
        have h_comm : s0 * (s0 * s1) ^ (x.val : ℤ) * s0 = (s0 * s1) ^ (-(x.val : ℤ)) := by
          convert s0_comm_zpow x.val using 1;
        rw [ ← h_comm, mul_assoc ];
        simp ( config := { decide := Bool.true } ) [ ← mul_assoc, s0_sq ];
      -- Using the commutation relation, we can simplify the expression further.
      have h_comm_simplified : s0 * (s0 * s1) ^ (-(x.val : ℤ)) * (s0 * s1) ^ (y.val : ℤ) = s0 * (s0 * s1) ^ ((y - x).val : ℤ) := by
        rw [ mul_assoc, ← zpow_add ];
        rw [ show ( - ( x.val : ℤ ) + y.val : ℤ ) = ( y - x : ZMod 3 ).val + 3 * ( ( - ( x.val : ℤ ) + y.val : ℤ ) / 3 ) by linarith [ Int.emod_add_ediv ( - ( x.val : ℤ ) + y.val ) 3, show ( y - x : ZMod 3 ).val = ( - ( x.val : ℤ ) + y.val : ℤ ) % 3 by fin_cases x <;> fin_cases y <;> trivial ] ] ; norm_num [ zpow_add, zpow_mul ];
        erw [ s0s1_pow3 ] ; norm_num;
      unfold map_D3_to_A2_fun; aesop;
      grind;
    · -- By definition of multiplication in the group, we have:
      have h_mul : s0 * (s0 * s1) ^ (x.val + y.val : ℤ) = s0 * (s0 * s1) ^ (x.val : ℤ) * (s0 * s1) ^ (y.val : ℤ) := by
        group;
      aesop;
      convert h_mul using 1;
      convert rfl;
      exact congr_arg _ ( s0s1_zpow_eq_zpow_mod_3 _ );
    · -- Using the lemma s0_comm_zpow, we can rewrite the left-hand side.
      have h_lhs : s0 * (s0 * s1) ^ (x.val : ℤ) * (s0 * (s0 * s1) ^ (y.val : ℤ)) = (s0 * s1) ^ (-(x.val : ℤ)) * (s0 * s1) ^ (y.val : ℤ) := by
        have := s0_comm_zpow x.val; simp_all ( config := { decide := Bool.true } ) [ mul_assoc, mul_left_comm ] ;
        simp ( config := { decide := Bool.true } ) [ ← this, mul_assoc ];
      convert h_lhs.symm using 1;
      convert s0s1_zpow_val_eq_zpow_val_sub x y |> Eq.symm using 1;
      group

#check hom_A2_to_D3
#check map_D3_to_A2_map_mul

/-
Inverse homomorphism and verification on generators.
-/
def hom_D3_to_A2 : DihedralGroup 3 →* (CoxeterMatrix.Aₙ 2).Group where
  toFun := map_D3_to_A2_fun
  map_one' := map_D3_to_A2_map_one
  map_mul' := map_D3_to_A2_map_mul

lemma hom_comp_r1 : hom_A2_to_D3 (hom_D3_to_A2 (DihedralGroup.r 1)) = DihedralGroup.r 1 := by
  decide +kernel

lemma hom_comp_sr0 : hom_A2_to_D3 (hom_D3_to_A2 (DihedralGroup.sr 0)) = DihedralGroup.sr 0 := by
  decide +kernel

lemma hom_comp_s0 : hom_D3_to_A2 (hom_A2_to_D3 s0) = s0 := by
  exact?

lemma hom_comp_s1 : hom_D3_to_A2 (hom_A2_to_D3 s1) = s1 := by
  unfold hom_D3_to_A2; aesop;
  -- Since $s1$ is a generator in the Coxeter group, applying the homomorphism $hom_A2_to_D3$ to $s1$ gives us $sr 1$ in the Dihedral group.
  have h_hom_s1 : (hom_A2_to_D3 s1) = DihedralGroup.sr 1 := by
    decide +kernel;
  unfold map_D3_to_A2_fun; aesop;
  -- By simplifying, we can see that $s0 * (s0 * s1) ^ 1 = s0 * s0 * s1 = s1$.
  have h_simp : s0 * (s0 * s1) ^ 1 = s0 * s0 * s1 := by
    simp +decide [ mul_assoc ];
  exact h_simp.trans ( by simp +decide [ s0_sq ] )

/-
Simplification lemmas for hom_A2_to_D3.
-/
lemma hom_A2_to_D3_s0 : hom_A2_to_D3 s0 = DihedralGroup.sr 0 := by
  -- By definition of $hom_A2_to_D3$, we know that it maps $s0$ to $sr0$ because $s0$ is a generator of the group.
  apply PresentedGroup.toGroup.of

lemma hom_A2_to_D3_s1 : hom_A2_to_D3 s1 = DihedralGroup.sr 1 := by
  exact?

/-
Isomorphism between A2 and D3.
-/
def iso_A2_D3 : (CoxeterMatrix.Aₙ 2).Group ≃* DihedralGroup 3 where
  toFun := hom_A2_to_D3
  invFun := hom_D3_to_A2
  left_inv := by
    intro g;
    induction g using QuotientGroup.induction_on';
    induction ‹FreeGroup ( Fin 2 ) › using FreeGroup.induction_on ; aesop;
    · rename_i i; fin_cases i <;> simp +decide [ hom_A2_to_D3, hom_D3_to_A2 ] ;
      · exact?;
      · convert hom_comp_s1;
    · aesop;
    · aesop
  right_inv := by
    decide +revert
  map_mul' := hom_A2_to_D3.map_mul

#check iso_A2_D3

/-
Isomorphism between A2 and D3.
-/
def iso_A2_D3_final : (CoxeterMatrix.Aₙ 2).Group ≃* DihedralGroup 3 where
  toFun := hom_A2_to_D3
  invFun := hom_D3_to_A2
  left_inv := by
    -- To prove the left inverse property, we use the fact that the composition of the two homomorphisms is the identity.
    apply iso_A2_D3.left_inv
  right_inv := by
    -- By definition of hom_D3_to_A2, we know that applying hom_A2_to_D3 to any element in DihedralGroup 3 gives back the original element.
    apply iso_A2_D3.right_inv
  map_mul' := hom_A2_to_D3.map_mul

end AristotleLemmas

lemma A2_weyl_group_card : Nat.card (CoxeterMatrix.Aₙ 2).Group = 6 := by
  convert Nat.card_congr iso_A2_D3_final.toEquiv;
  simp +decide [ DihedralGroup ]