/CoxeterAristotle2.lean at c314c45fd1c615c3e67faacc0edab1a21d5fb5bb

/-
Sorry, Aristotle was unable to complete the task in time.
-/
/-
This file was generated by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
-/

import Mathlib

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

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

set_option relaxedAutoImplicit false
set_option autoImplicit false

noncomputable section

/-
The Weyl group of type A_n is the Coxeter group associated with the Coxeter matrix A_n.
-/
open CoxeterMatrix

def WeylGroupA (n : ℕ) := CoxeterMatrix.Group (Aₙ n)


/-
Checking definitions and instances.
-/
open CoxeterMatrix

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

/-
There is a homomorphism from the Weyl group of type A_n to the symmetric group S_{n+1}.
-/
open CoxeterMatrix

def perm_of_gen (n : ℕ) (i : Fin n) : Equiv.Perm (Fin (n + 1)) :=
  Equiv.swap (Fin.castSucc i) (Fin.succ i)

def toPerm (n : ℕ) : CoxeterMatrix.Group (Aₙ n) →* Equiv.Perm (Fin (n + 1)) :=
  PresentedGroup.toGroup (f := perm_of_gen n) (by
  unfold CoxeterMatrix.Aₙ;
  simp ( config := { decide := Bool.true } ) [ CoxeterMatrix.relationsSet ];
  unfold CoxeterMatrix.relation; aesop;
  · ext i ; unfold perm_of_gen ; aesop;
  · ext i;
    unfold perm_of_gen;
    rcases x with ⟨ _ | x, hx ⟩ <;> rcases x_1 with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [ Fin.ext_iff, pow_succ', Equiv.swap_apply_def ] at *;
    · aesop;
      rcases i with ⟨ _ | _ | _ | i, hi ⟩ <;> norm_num [ pow_three, Equiv.swap_apply_def ];
      simp +arith +decide [ Fin.ext_iff ];
    · grind;
  · ext y ; simp ( config := { decide := Bool.true } ) [ *, perm_of_gen ];
    rcases x with ⟨ _ | x, hx ⟩ <;> rcases x_1 with ⟨ _ | x_1, hx_1 ⟩ <;> norm_num [ Fin.ext_iff, Equiv.swap_apply_def ] at *;
    · aesop;
      rcases y with ⟨ _ | _ | _ | y, hy ⟩ <;> norm_num [ pow_succ, Equiv.swap_apply_def ];
      simp ( config := { decide := Bool.true } ) [ Fin.ext_iff, Nat.succ_eq_add_one ] at *;
    · -- By definition of permutation multiplication, we can see that applying the permutation three times returns each element to its original position.
      simp [Equiv.swap_apply_def, pow_succ'];
      grind;
  · -- Since $x \neq x_1$, the permutations $perm_of_gen n x$ and $perm_of_gen n x_1$ commute.
    have h_comm : perm_of_gen n x * perm_of_gen n x_1 = perm_of_gen n x_1 * perm_of_gen n x := by
      ext y; simp [perm_of_gen];
      by_cases hy : y = x.castSucc <;> by_cases hy' : y = x.succ <;> by_cases hy'' : y = x_1.castSucc <;> by_cases hy''' : y = x_1.succ <;> simp_all +decide [ Equiv.swap_apply_def ];
      all_goals simp_all ( config := { decide := Bool.true } ) [ Fin.ext_iff, Fin.val_add ];
      · aesop;
      · aesop;
    simp_all +decide [ pow_succ, mul_assoc ];
    simp_all +decide [ ← mul_assoc ];
    simp_all +decide [ mul_assoc, perm_of_gen ])

/-
The homomorphism `toPerm` from the Weyl group of type A_n to the symmetric group S_{n+1} is surjective.
-/
theorem toPerm_surjective (n : ℕ) : Function.Surjective (toPerm n) := by
  -- To prove surjectivity, it suffices to show that the image of `toPerm` contains all the adjacent transpositions, which generate the symmetric group.
  have h_adj_transpositions : ∀ i : Fin n, ∃ g : CoxeterMatrix.Group (Aₙ n), toPerm n g = Equiv.swap (Fin.castSucc i) (Fin.succ i) := by
    intro i;
    exact ⟨ PresentedGroup.of i, by aesop ⟩;
  -- Since the symmetric group is generated by the adjacent transpositions, and we have shown that the image of `toPerm` contains all these transpositions, the image must be the entire symmetric group.
  have h_image : ∀ p : Equiv.Perm (Fin (n + 1)), ∃ g : CoxeterMatrix.Group (Aₙ n), toPerm n g = p := by
    intro p
    have h_gen : p ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by
      -- The symmetric group $S_{n+1}$ is generated by the adjacent transpositions $(i, i+1)$ for $i \in \{0, 1, \ldots, n-1\}$.
      have h_gen : ∀ p : Equiv.Perm (Fin (n + 1)), p ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by
        intro p
        have h_adj_transpositions : ∀ i : Fin (n + 1), ∀ j : Fin (n + 1), i < j → Equiv.swap i j ∈ Subgroup.closure (Set.range (fun i : Fin n => Equiv.swap (Fin.castSucc i) (Fin.succ i))) := by
          intro i j hij; induction' j using Fin.inductionOn with j ih ih; aesop;
          cases lt_or_eq_of_le ( show i ≤ Fin.castSucc j from Nat.le_of_lt_succ hij ) <;> simp_all +decide [ Subgroup.mem_closure ];
          · intro K hK; specialize ih K hK; specialize hK ( Set.mem_range_self j ) ; aesop;
            exact?;
          · exact fun K hK => hK ⟨ j, rfl ⟩
        induction' p using Equiv.Perm.swap_induction_on' with p i j hij ih;
        · exact OneMemClass.one_mem _;
        · exact Subgroup.mul_mem _ ih ( if hij' : i < j then h_adj_transpositions i j hij' else by simpa only [ Equiv.swap_comm ] using h_adj_transpositions j i ( lt_of_le_of_ne ( le_of_not_gt hij' ) hij.symm ) );
      exact h_gen p
    refine' Subgroup.closure_induction ( fun x hx => _ ) _ _ _ h_gen;
    · aesop;
    · exact ⟨ 1, map_one _ ⟩;
    · rintro x y hx hy ⟨ g, rfl ⟩ ⟨ h, rfl ⟩ ; exact ⟨ g * h, by simp +decide ⟩ ;
    · rintro x hx ⟨ g, rfl ⟩ ; exact ⟨ g⁻¹, by simp +decide ⟩ ;
  exact h_image

/-
We define the index set for the roots of type A_n as the set of pairs of distinct indices from 0 to n. We prove it is a finite type.
-/
variable (n : ℕ)

def TypeA.ι := { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 }

instance : Fintype (TypeA.ι n) :=
  have : DecidablePred (fun x : Fin (n + 1) × Fin (n + 1) => x.1 ≠ x.2) := fun _ => inferInstance
  inferInstanceAs (Fintype { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 })

instance : DecidableEq (TypeA.ι n) := inferInstance

/-
We define the index set for the roots of type A_n as the set of pairs of distinct indices from 0 to n. We prove it is a finite type.
-/
variable (n : ℕ)

abbrev TypeA_Indices := { x : Fin (n + 1) × Fin (n + 1) // x.1 ≠ x.2 }

instance : Fintype (TypeA_Indices n) := inferInstance
instance : DecidableEq (TypeA_Indices n) := inferInstance

/-
We define the roots and coroots for the root system of type A. For each index pair (i, j), the root and coroot are both the vector e_i - e_j in Z^{n+1}.
-/
variable (n : ℕ)

def TypeA.root (i : TypeA_Indices n) : Fin (n + 1) → ℤ :=
  Pi.single i.1.1 1 - Pi.single i.1.2 1

def TypeA.coroot (i : TypeA_Indices n) : Fin (n + 1) → ℤ :=
  Pi.single i.1.1 1 - Pi.single i.1.2 1

/-
Checking the type of Matrix.toBilin.
-/
#check Matrix.toBilin

/-
We define the perfect pairing for the root system of type A as the standard dot product. We also define the reflection permutation associated with a root index (i, j) as the permutation of indices induced by the transposition (i, j).
-/
variable (n : ℕ)

def TypeA.pairing : PerfectPairing ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) :=
  { toLinearMap := LinearMap.mk₂ ℤ dotProduct (by
      -- The dot product is linear in the first argument, so we can split the sum into two parts.
      intros m₁ m₂ n
      simp [dotProduct, add_mul, Finset.sum_add_distrib]) (by
      -- The dot product is linear in both arguments, so we can distribute the scalar multiplication over the dot product.
      intros c m n
      simp [dotProduct, mul_assoc, mul_comm, mul_left_comm];
      -- Apply the distributive property of multiplication over addition.
      rw [Finset.mul_sum]) (by
      -- By the distributive property of multiplication over addition, we can split the sum into two separate sums.
      intros m n₁ n₂
      simp [mul_add, Finset.sum_add_distrib]) (by
      -- The dot product is linear, so we can distribute the scalar multiplication over the dot product.
      intros c m n_1
      simp [dotProduct, smul_eq_mul];
      -- By the properties of multiplication, we can factor out the scalar $c$ from the sum.
      simp [mul_assoc, mul_comm, mul_left_comm, Finset.mul_sum])
    bijective_left := by
      constructor;
      · intro m m' h; ext i; replace h := congr_arg ( fun f => f ( Pi.single i 1 ) ) h; aesop;
      · -- To show surjectivity, take any linear functional $f$ on $\mathbb{Z}^{n+1}$. We can represent $f$ as the dot product with some vector $v$.
        intro f
        use fun i => f (Pi.single i 1);
        bound
    bijective_right := by
      constructor <;> intro f <;> aesop
      generalize_proofs at *;
      ext i; have := congr_arg ( fun f => f ( Pi.single i 1 ) ) a; norm_num at this; aesop; }

def TypeA.reflectionPerm (i : TypeA_Indices n) : Equiv.Perm (TypeA_Indices n) :=
  let σ := Equiv.swap i.1.1 i.1.2
  { toFun := fun x => ⟨(σ x.1.1, σ x.1.2), by
      intro h
      apply x.2
      apply σ.injective
      exact h⟩
    invFun := fun x => ⟨(σ x.1.1, σ x.1.2), by
      intro h
      apply x.2
      apply σ.injective
      exact h⟩
    left_inv := by intro x; simp; apply Subtype.ext; simp; rw [Equiv.swap_apply_self, Equiv.swap_apply_self]
    right_inv := by intro x; simp; apply Subtype.ext; simp; rw [Equiv.swap_apply_self, Equiv.swap_apply_self] }

/-
Checking the definition of RootPairing.
-/
#print RootPairing

/-
Checking if TypeA.pairing and TypeA.reflectionPerm are already defined.
-/
variable (n : ℕ)

#check TypeA.pairing
#check TypeA.reflectionPerm

/-
We define the embedding of the roots of type A into the ambient space. The injectivity proof is left as a sorry.
-/
variable (n : ℕ)

def TypeA.rootEmbedding : TypeA_Indices n ↪ (Fin (n + 1) → ℤ) :=
  Function.Embedding.mk (TypeA.root n) (by
  intro x y hxy;
  unfold TypeA.root at hxy;
  replace hxy := congr_fun hxy;
  have := hxy x.1.1; have := hxy x.1.2; have := hxy y.1.1; have := hxy y.1.2; simp_all +decide [ Fin.ext_iff, Pi.single_apply ] ;
  grind +ring)

/-
We define the embedding of the coroots of type A into the ambient space. The injectivity proof is identical to that of the roots.
-/
variable (n : ℕ)

def TypeA.corootEmbedding : TypeA_Indices n ↪ (Fin (n + 1) → ℤ) :=
  Function.Embedding.mk (TypeA.coroot n) (by
  intro x y hxy;
  unfold TypeA.coroot at hxy;
  replace hxy := congr_fun hxy;
  have := hxy x.1.1; have := hxy x.1.2; have := hxy y.1.1; have := hxy y.1.2; simp_all +decide [ Fin.ext_iff, Pi.single_apply ] ;
  grind +ring)

/-
The map `TypeA.root` is injective.
-/
variable (n : ℕ)

lemma TypeA.root_injective : Function.Injective (TypeA.root n) := by
  intro i j h
  unfold TypeA.root at h
  -- We have e_i - e_j = e_k - e_l
  -- This implies {i, l} = {k, j} as multisets if we look at the support,
  -- but since i != j and k != l, we can deduce i = k and j = l.
  -- We can use function extensionality to look at specific coordinates.
  have h_i := congr_fun h i.1.1
  have h_j := congr_fun h i.1.2
  simp [Pi.single_apply] at h_i h_j
  -- We need to handle cases where indices might coincide.
  -- Since i.1.1 != i.1.2, we know the value at i.1.1 is 1 and at i.1.2 is -1.
  -- The RHS must match this.
  grind

/-
We define the root pairing for type A_n. We register the perfect pairing instance and then construct the `RootPairing` structure using the embeddings and permutations defined earlier. We leave the verification of the axioms as sorries.
-/
variable (n : ℕ)

instance : LinearMap.IsPerfPair (TypeA.pairing n).toLinearMap :=
  { bijective_left := (TypeA.pairing n).bijective_left
    bijective_right := (TypeA.pairing n).bijective_right }

def RootPairingA : RootPairing (TypeA_Indices n) ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) where
  toLinearMap := (TypeA.pairing n).toLinearMap
  root := TypeA.rootEmbedding n
  coroot := TypeA.corootEmbedding n
  root_coroot_two := by
    unfold TypeA.rootEmbedding TypeA.corootEmbedding;
    unfold TypeA.pairing;
    unfold TypeA.root TypeA.coroot; aesop
  reflectionPerm := TypeA.reflectionPerm n
  reflectionPerm_root := by
    unfold TypeA.rootEmbedding TypeA.corootEmbedding TypeA.reflectionPerm;
    -- By definition of reflection permutation, we have that the reflection of j under i is equal to the permutation of j under the swap of i's components.
    simp [TypeA.root, TypeA.coroot, Equiv.swap_apply_def];
    intro a b hab a' b' hab'; ext i; aesop;
    unfold TypeA.pairing; simp +decide [ Pi.single_apply ] ;
    grind +ring
  reflectionPerm_coroot := by
    bound;
    unfold TypeA.corootEmbedding TypeA.rootEmbedding TypeA.pairing TypeA.reflectionPerm;
    -- By definition of reflection permutation, we have σ(j.1) = snd and σ(j.2) = fst if j.1 = fst and j.2 = snd, and vice versa.
    simp [Equiv.swap_apply_def];
    unfold TypeA.root TypeA.coroot; aesop;
    · ext; simp ( config := { decide := Bool.true } ) [ two_mul, sub_eq_add_neg ] ; ring;
    · ext; norm_num; ring

/-
We define the root pairing for type A_n. We register the perfect pairing instance and then construct the `RootPairing` structure using the embeddings and permutations defined earlier. We leave the verification of the axioms as sorries.
-/
variable (n : ℕ)

def RootPairingTypeA : RootPairing (TypeA_Indices n) ℤ (Fin (n + 1) → ℤ) (Fin (n + 1) → ℤ) where
  toLinearMap := (TypeA.pairing n).toLinearMap
  root := TypeA.rootEmbedding n
  coroot := TypeA.corootEmbedding n
  root_coroot_two := by
    intro i
    unfold TypeA.rootEmbedding TypeA.corootEmbedding TypeA.pairing TypeA.root TypeA.coroot
    simp only [Function.Embedding.coeFn_mk]
    -- We need to evaluate the pairing of (e_i - e_j) with itself.
    -- The pairing is the dot product.
    -- (e_i - e_j) . (e_i - e_j) = e_i.e_i - e_i.e_j - e_j.e_i + e_j.e_j
    -- Since i != j, e_i.e_j = 0.
    -- e_i.e_i = 1, e_j.e_j = 1.
    -- So 1 - 0 - 0 + 1 = 2.
    aesop
  reflectionPerm := TypeA.reflectionPerm n
  reflectionPerm_root := by
    -- By definition of reflection, we know that $s_i(j) = j - \langle j, i^\vee \rangle i$.
    intros i j
    simp [TypeA.reflectionPerm, TypeA.rootEmbedding, TypeA.corootEmbedding];
    unfold TypeA.pairing TypeA.root TypeA.coroot; aesop;
    simp ( config := { decide := Bool.true } ) [ Pi.single_apply, Equiv.swap_apply_def ];
    grind +ring
  reflectionPerm_coroot := by
    -- By definition of reflection permutation, we have that the reflection of j by i is the swap of the indices.
    simp [TypeA.reflectionPerm];
    intro a b hab a' b' hab'; ext x; simp +decide [ Equiv.swap_apply_def ] ;
    unfold TypeA.corootEmbedding TypeA.rootEmbedding; simp +decide [ TypeA.pairing ] ;
    simp +decide [ TypeA.coroot, TypeA.root, dotProduct ];
    simp +decide [ Finset.sum_add_distrib, sub_mul, mul_sub, Pi.single_apply ];
    grind +ring

/-
The reflection corresponding to the root indexed by `i` acts on the basis vector `e_k` by swapping indices according to the transposition `(i.1, i.2)`.
-/
variable (n : ℕ)

def WeylGroupTypeA := (RootPairingTypeA n).weylGroup

lemma reflection_apply_basis (i : TypeA_Indices n) (k : Fin (n + 1)) :
  (RootPairingTypeA n).reflection i (Pi.single k 1) = Pi.single (Equiv.swap i.1.1 i.1.2 k) 1 := by
    unfold RootPairingTypeA;
    -- By definition of reflection, we have that the reflection of the root i on the basis vector e_k is equal to the basis vector e_{σ(k)}, where σ is the transposition (i.1, i.2).
    simp [RootPairing.reflection, TypeA.reflectionPerm];
    simp +decide [ Module.reflection ];
    unfold Module.preReflection TypeA.pairing TypeA.corootEmbedding TypeA.rootEmbedding; aesop;
    unfold TypeA.coroot TypeA.root; aesop;
    by_cases hk : k = fst <;> by_cases hk' : k = snd <;> simp +decide [ *, Pi.single_apply ];
    rw [ Equiv.swap_apply_of_ne_of_ne hk hk' ]

/-
Checking the definition of RootPairing.Equiv.
-/
#print RootPairing.Equiv

/-
For every element `w` in the Weyl group of type A, there exists a permutation `σ` of the indices such that `w` acts on the basis vectors by permuting them according to `σ`.
-/
variable (n : ℕ)

lemma basis_perm_exists (w : WeylGroupTypeA n) :
  ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k, (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by
    -- By definition of the Weyl group, each element w corresponds to a permutation of the indices.
    have h_perm : ∀ w : WeylGroupTypeA n, ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k : Fin (n + 1), (w.val.weightMap (Pi.single k 1)) = Pi.single (σ k) 1 := by
      intro w
      have h_gen : ∀ i : TypeA_Indices n, ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k : Fin (n + 1), (RootPairingTypeA n).reflection i (Pi.single k 1) = Pi.single (σ k) 1 := by
        -- By definition of reflectionPerm, we know that it swaps the indices i.1.1 and i.1.2.
        intro i
        use Equiv.swap i.1.1 i.1.2;
        -- By definition of reflection, we know that it swaps the indices i.1.1 and i.1.2. Therefore, for any k, the reflection of e_k is equal to the single vector at the swapped position.
        intros k
        apply reflection_apply_basis
      induction' w with w hw;
      induction hw using Subgroup.closure_induction;
      · aesop;
      · exact ⟨ Equiv.refl _, fun k => rfl ⟩;
      · rename_i hx hy;
        obtain ⟨ σ, hσ ⟩ := hx; obtain ⟨ τ, hτ ⟩ := hy; use σ * τ; intro k; simp +decide [ hσ, hτ ] ;
      · rename_i hx;
        obtain ⟨ σ, hσ ⟩ := hx;
        use σ⁻¹;
        -- By definition of the inverse automorphism, we have that $x⁻¹.weightMap (Pi.single (σ k) 1) = Pi.single k 1$.
        have h_inv : ∀ k : Fin (n + 1), (‹(RootPairingTypeA n).Aut›⁻¹).weightMap (Pi.single (σ k) 1) = Pi.single k 1 := by
          intro k;
          rw [ ← hσ k ];
          convert LinearEquiv.symm_apply_apply _ _;
        intro k; specialize h_inv ( σ⁻¹ k ) ; aesop;
    exact h_perm w

/-
For every element `w` in the Weyl group of type A, there exists a permutation `σ` of the indices such that `w` acts on the basis vectors by permuting them according to `σ`.
-/
variable (n : ℕ)

lemma weyl_group_acts_as_perm (w : WeylGroupTypeA n) :
  ∃ σ : Equiv.Perm (Fin (n + 1)), ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single (σ k) 1 := by
    exact?

/-
Checking the type of Pi.single_injective.
-/
#check Pi.single_injective

/-
We define the map from the Weyl group to the symmetric group by extracting the permutation that acts on the basis vectors.
-/
variable (n : ℕ)

def weylToPerm (w : WeylGroupTypeA n) : Equiv.Perm (Fin (n + 1)) :=
  Classical.choose (basis_perm_exists n w)

lemma weylToPerm_apply (w : WeylGroupTypeA n) (k : Fin (n + 1)) :
  (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (weylToPerm n w k) 1 :=
  Classical.choose_spec (basis_perm_exists n w) k

/-
We define the group homomorphism from the Weyl group to the symmetric group.
-/
variable (n : ℕ)

def weylToPermHom : WeylGroupTypeA n →* Equiv.Perm (Fin (n + 1)) where
  toFun := weylToPerm n
  map_one' := by
    have h_id : (1 : WeylGroupTypeA n).val.weightMap (Pi.single 0 1) = Pi.single (weylToPerm n 1 0) 1 := by
      exact?;
    ext i; replace h_id := congr_fun h_id i; aesop;
    have := Classical.choose_spec ( basis_perm_exists n ( w := 1 ) ) i; aesop;
    replace this := congr_fun this ( ( Classical.choose ( basis_perm_exists n ( w := 1 ) ) ) i ) ; aesop;
    rw [ Pi.single_apply ] at this ; aesop;
    exact congr_arg Fin.val this
  map_mul' := by
    -- By definition of weylToPerm, we have that for any x and y in the Weyl group, weylToPerm n (x * y) is the permutation that acts on the basis vectors by first applying y and then x.
    intros x y
    apply Equiv.Perm.ext
    intro k
    simp [weylToPerm_apply];
    have h_comp : ∀ (x y : WeylGroupTypeA n), (x * y).val.weightMap (Pi.single k 1) = (x.val.weightMap) ((y.val.weightMap) (Pi.single k 1)) := by
      exact?;
    have h_comp : (weylToPerm n (x * y)) k = (weylToPerm n x) ((weylToPerm n y) k) := by
      have := h_comp x y
      rw [ weylToPerm_apply, weylToPerm_apply, weylToPerm_apply ] at * ; aesop;
      replace this := congr_fun this ( ( weylToPerm n ⟨ val, property ⟩ ) ( ( weylToPerm n ⟨ val_1, property_1 ⟩ ) k ) ) ; aesop;
      rw [ Pi.single_apply ] at this ; aesop;
    exact h_comp

/-
The homomorphism from the Weyl group of type A to the symmetric group is bijective.
-/
variable (n : ℕ)

theorem weylToPermHom_bijective : Function.Bijective (weylToPermHom n) := by
  -- To show surjectivity, notice that every permutation can be written as a product of simple reflections, which are in the image of the homomorphism.
  have h_surjective : Function.Surjective (weylToPermHom n) := by
    intro σ;
    -- Let's choose any permutation σ of the indices.
    obtain ⟨w, hw⟩ : ∃ w : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by
      -- Since the Weyl group is generated by the simple reflections, any permutation σ can be written as a product of these transpositions.
      have h_gen : ∀ σ : Equiv.Perm (Fin (n + 1)), ∃ w : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (σ k) 1 := by
        intro σ;
        induction' σ using Equiv.Perm.swap_induction_on with σ a b hab hσ;
        · refine' ⟨ ⟨ 1, _ ⟩, _ ⟩ <;> aesop;
        · obtain ⟨ w, hw ⟩ := hσ;
          -- Let $w'$ be the reflection corresponding to the transposition $(a, b)$.
          obtain ⟨w', hw'⟩ : ∃ w' : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w'.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (Equiv.swap a b k) 1 := by
            have h_reflection : ∀ i : TypeA_Indices n, ∃ w' : WeylGroupTypeA n, ∀ k : Fin (n + 1), (w'.val.weightMap : (Fin (n + 1) → ℤ) →ₗ[ℤ] (Fin (n + 1) → ℤ)) (Pi.single k 1) = Pi.single (Equiv.swap i.1.1 i.1.2 k) 1 := by
              bound;
              exact ⟨ ⟨ _, Subgroup.subset_closure <| Set.mem_range_self ⟨ ⟨ fst, snd ⟩, property_1 ⟩ ⟩, reflection_apply_basis _ _ ⟩;
            exact h_reflection ⟨ ( a, b ), hab ⟩;
          use w' * w;
          aesop;
      exact h_gen σ;
    use w;
    -- Since the permutation is determined by its action on the basis vectors, and we have shown that w and σ act the same on all basis vectors, they must be the same permutation.
    have h_perm_eq : ∀ k : Fin (n + 1), (weylToPerm n w) k = σ k := by
      intro k; specialize hw k; replace hw := congr_fun hw ( σ k ) ; aesop;
      have := weylToPerm_apply n ⟨ val, property ⟩ k; aesop;
      rw [ Pi.single_apply ] at hw ; aesop;
    exact Equiv.Perm.ext h_perm_eq;
  -- To show injectivity, we need to show that the kernel of the homomorphism is trivial.
  have h_kernel_trivial : ∀ w : WeylGroupTypeA n, weylToPermHom n w = 1 → w = 1 := by
    bound;
    -- If the permutation induced by the Weyl group element is the identity, then the Weyl group element itself must be the identity.
    have h_id : ∀ k : Fin (n + 1), val.weightMap (Pi.single k 1) = Pi.single k 1 := by
      intro k; have := Classical.choose_spec ( basis_perm_exists n ⟨ val, property ⟩ ) k; aesop;
      replace a := congr_arg ( fun f => f k ) a ; aesop;
      congr;
    -- Since the weight map of the Weyl group element is the identity, the Weyl group element itself must be the identity.
    have h_val_id : val.weightMap = LinearMap.id := by
      aesop;
    cases val ; aesop;
    cases toHom ; aesop;
    congr;
    · ext x;
      replace weight_coweight_transpose := congr_arg ( fun f => f ( Pi.single x 1 ) ) weight_coweight_transpose ; aesop;
      replace weight_coweight_transpose := congr_arg ( fun f => f ( Pi.single x_1 1 ) ) weight_coweight_transpose ; aesop;
      simp_all +decide [ RootPairingTypeA ];
      simp_all +decide [ TypeA.pairing ];
      simp_all +decide [ Pi.single_apply ];
      grind;
    · -- Since the root function is injective, we can conclude that indexEquiv is the identity permutation.
      have h_inj : Function.Injective (RootPairingTypeA n).root := by
        exact?;
      exact Equiv.ext fun x => h_inj <| by simpa using congr_fun root_weightMap.symm x;
  refine' ⟨ _, h_surjective ⟩;
  exact?

/-
The homomorphism from the Weyl group of type A to the symmetric group is surjective.
-/
variable (n : ℕ)

theorem weylToPermHom_surjective : Function.Surjective (weylToPermHom n) := by
  -- Since the homomorphism is bijective, it is surjective.
  apply Function.Bijective.surjective; exact weylToPermHom_bijective n

/-
If an element of the Weyl group acts as the identity on the basis vectors, then it is the identity element. This proves the action is faithful.
-/
variable (n : ℕ)

lemma weyl_group_faithful (w : WeylGroupTypeA n) (h : ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single k 1) : w = 1 := by
  -- Since the homomorphism is bijective, if it's the identity, the element must be the identity.
  have h_bijective : Function.Bijective (weylToPermHom n) := by
    exact?;
  have h_eq_1 : weylToPermHom n w = 1 := by
    ext k;
    have := weylToPerm_apply n w k; aesop;
    replace this := congr_fun this ( weylToPerm n ⟨ val, property ⟩ k ) ; aesop;
    rw [ Pi.single_apply ] at this ; aesop;
    exact congr_arg Fin.val this;
  exact h_bijective.injective <| by simpa using h_eq_1;

/-
The cardinality of the Weyl group for the root system A_n is (n+1)!. We prove this by establishing a bijection with the symmetric group S_{n+1}.
-/
variable (n : ℕ)

theorem card_WeylGroupTypeA : Nat.card (WeylGroupTypeA n) = (n + 1).factorial := by
  have h_bij : Function.Bijective (weylToPermHom n) := weylToPermHom_bijective n
  have h_equiv : WeylGroupTypeA n ≃ Equiv.Perm (Fin (n + 1)) := Equiv.ofBijective (weylToPermHom n) h_bij
  rw [Nat.card_congr h_equiv]
  rw [Nat.card_perm]
  simp

/-
The homomorphism from the Weyl group of type A to the symmetric group is injective.
-/
variable (n : ℕ)

theorem weylToPermHom_injective : Function.Injective (weylToPermHom n) := by
  -- Since the homomorphism is bijective, it is injective.
  apply (weylToPermHom_bijective n).injective

/-
If an element of the Weyl group acts as the identity on the basis vectors, then it is the identity element. This proves the action is faithful.
-/
variable (n : ℕ)

lemma weyl_group_faithful' (w : WeylGroupTypeA n) (h : ∀ k, w.val.weightMap (Pi.single k 1) = Pi.single k 1) : w = 1 := by
  exact?

/-
The Weyl group of type A_n is finite, and its cardinality is (n+1)!.
-/
variable (n : ℕ)

instance instFiniteWeylGroupTypeA : Finite (WeylGroupTypeA n) := Finite.of_injective (weylToPermHom n) (weylToPermHom_injective n)

theorem card_WeylGroupTypeA_eq_fact : Nat.card (WeylGroupTypeA n) = (n + 1).factorial := by
  exact?