From f478f3479b8fd43ef2bad80a090a796456ad5b0d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 18 May 2026 02:17:13 +0900 Subject: [PATCH 1/8] Vendor DemazureOperatorsLean core --- LeanPool.lean | 5 + LeanPool/DemazureOperatorsLean.lean | 21 + LeanPool/DemazureOperatorsLean/Demazure.lean | 377 ++++++++++++++++ .../DemazureOperatorsLean/DemazureAux.lean | 418 ++++++++++++++++++ .../DemazureAuxRelations.lean | 215 +++++++++ .../DemazureRelations.lean | 118 +++++ LeanPool/projects.yml | 33 ++ 7 files changed, 1187 insertions(+) create mode 100644 LeanPool/DemazureOperatorsLean.lean create mode 100644 LeanPool/DemazureOperatorsLean/Demazure.lean create mode 100644 LeanPool/DemazureOperatorsLean/DemazureAux.lean create mode 100644 LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean create mode 100644 LeanPool/DemazureOperatorsLean/DemazureRelations.lean diff --git a/LeanPool.lean b/LeanPool.lean index 39c8ce5387..c2e9d3dae6 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -74,6 +74,11 @@ import LeanPool.DeadEnds.PrimeTail import LeanPool.DeadEnds.RelevantPrimes import LeanPool.DeadEnds.Solution import LeanPool.DeadEnds.TailEstimates +import LeanPool.DemazureOperatorsLean +import LeanPool.DemazureOperatorsLean.Demazure +import LeanPool.DemazureOperatorsLean.DemazureAux +import LeanPool.DemazureOperatorsLean.DemazureAuxRelations +import LeanPool.DemazureOperatorsLean.DemazureRelations import LeanPool.Erdos1196 import LeanPool.Erdos1196.Basic import LeanPool.Erdos1196.FirstEntryRowTerm diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean new file mode 100644 index 0000000000..6cae5b7759 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import LeanPool.DemazureOperatorsLean.Demazure +import LeanPool.DemazureOperatorsLean.DemazureAux +import LeanPool.DemazureOperatorsLean.DemazureRelations +import LeanPool.DemazureOperatorsLean.DemazureAuxRelations + +/-! +# Demazure Operators and Lean + +Source: url:https://github.com/bolito2/DemazureOperatorsLean +Authors: Óscar Álvarez Sánchez +Status: verified +Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent` +Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory +MSC: 05E05, 13P10, 20F55 +-/ diff --git a/LeanPool/DemazureOperatorsLean/Demazure.lean b/LeanPool/DemazureOperatorsLean/Demazure.lean new file mode 100644 index 0000000000..6b31d4d413 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/Demazure.lean @@ -0,0 +1,377 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import Mathlib.Data.Set.Lattice +import Mathlib.Data.Set.Function +import Mathlib.Analysis.Complex.Polynomial.Basic +import Init.System.IO + +import Mathlib.Data.Complex.Basic + +import Mathlib.Algebra.Polynomial.Basic +import Mathlib.Algebra.MvPolynomial.Basic +import Mathlib.Algebra.MvPolynomial.CommRing +import Mathlib.Algebra.MvPolynomial.Rename +import Mathlib.Algebra.MvPolynomial.Polynomial +import Mathlib.RingTheory.MvPolynomial.Basic + +import Mathlib.Data.Finsupp.Defs + + +noncomputable section +open MvPolynomial + +namespace Demazure + +variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1) + +/- In this file we define the Demazure operator directly as a function + in the ring of multivariate polynomials -/ + +/- Prerequisites -/ + +/-- The polynomial obtained by swapping the variables indexed by `i` and `j`. -/ +def SwapVariablesFun (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : (MvPolynomial (Fin n) ℂ) := + (renameEquiv ℂ (Equiv.swap i j)) p + +@[simp] +lemma swap_variables_map_zero (i j : Fin n) : SwapVariablesFun i j 0 = 0 := by + rw[SwapVariablesFun] + have : (0 : MvPolynomial (Fin n) ℂ) = C 0 := by + refine C_0.symm + rw[this] + exact rename_C (Equiv.swap i j) 0 + +@[simp] +lemma swap_variables_map_one {i j : Fin n} : SwapVariablesFun i j 1 = 1 := by + simp[SwapVariablesFun] + +@[simp] +lemma swap_variables_add {i j : Fin n} : ∀p q : + MvPolynomial (Fin n) ℂ, + SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q := by + intro p q + simp[SwapVariablesFun] + +@[simp] +lemma swap_variables_sub {i j : Fin n} : ∀p q : + MvPolynomial (Fin n) ℂ, + SwapVariablesFun i j (p - q) = SwapVariablesFun i j p - SwapVariablesFun i j q := by + intro p q + simp[SwapVariablesFun] + +@[simp] +lemma swap_variables_mul {i j : Fin n} : ∀p q : + MvPolynomial (Fin n) ℂ, + SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by + intro p q + simp[SwapVariablesFun] + +lemma swap_variables_mul' (i j : Fin n) : ∀p q : + MvPolynomial (Fin n) ℂ, + SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by + intro p q + simp[SwapVariablesFun] + +lemma swap_variables_mul'' {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} : + SwapVariablesFun i j (p * q) = SwapVariablesFun i j p * SwapVariablesFun i j q := by + simp[SwapVariablesFun] + +lemma swap_variables_add'' {i j : Fin n} {p q : MvPolynomial (Fin n) ℂ} : + SwapVariablesFun i j (p + q) = SwapVariablesFun i j p + SwapVariablesFun i j q := by + simp[SwapVariablesFun] + +@[simp] +lemma swap_variables_commutes {i j : Fin n} : ∀r : ℂ, SwapVariablesFun i j (C r) = C r := by + intro r + simp[SwapVariablesFun] + +@[simp] +lemma swap_variables_order_two {i j : Fin n} {p : MvPolynomial (Fin n) ℂ} : + SwapVariablesFun i j (SwapVariablesFun i j p) = p := by + rw [SwapVariablesFun, SwapVariablesFun, renameEquiv_apply, renameEquiv_apply, rename_rename] + convert rename_id_apply (R := ℂ) p + funext k + simp + +/-- The algebra equivalence swapping the variables indexed by `i` and `j`. -/ +def SwapVariables (i : Fin n) (j : Fin n) : + AlgEquiv ℂ (MvPolynomial (Fin n) ℂ) (MvPolynomial (Fin n) ℂ) := + renameEquiv ℂ (Equiv.swap i j) + +@[simp] +lemma swap_variables_apply (i j : Fin n) (p : MvPolynomial (Fin n) ℂ) : + SwapVariables i j p = SwapVariablesFun i j p := rfl + +/-- The polynomial equation of the unit circle in two variables. -/ +def circleEquation : MvPolynomial (Fin 2) ℂ := X 0 ^ 2 + X 1 ^ 2 - C 1 + +example : circleEquation = SwapVariables 0 1 circleEquation := by + simp [circleEquation, SwapVariables] + ring + +/- some more properties of swap_variables and others -/ + +lemma swap_variables_ne_zero (i j : Fin (n + 1)) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, p ≠ 0 → SwapVariables i j p ≠ 0 := by + intro p hp h + apply hp + rw[← map_zero (SwapVariables i j)] at h + apply AlgEquiv.injective (SwapVariables i j) + exact h + +@[simp] +lemma swap_variables_first {i j : Fin (n + 1)} : SwapVariablesFun i j (X i) = X j := by + simp [SwapVariablesFun] + +lemma swap_variables_symmetrical {i j : Fin (n + 1)} {p : MvPolynomial (Fin (n + 1)) ℂ} : + SwapVariablesFun i j p = SwapVariablesFun j i p := by + simp [SwapVariablesFun, Equiv.swap_comm] + +@[simp] +lemma swap_variables_second {i j : Fin (n + 1)} : SwapVariablesFun i j (X j) = X i := by + simp [SwapVariablesFun] + +@[simp] +lemma swap_variables_none {i j k : Fin (n + 1)} (h1 : k ≠ i) (h2 : k ≠ j) : +SwapVariablesFun i j (X k) = X k := by + simp [SwapVariablesFun, h1, h2, Equiv.swap_apply_of_ne_of_ne] + +lemma swap_variables_none' {i j k : Fin (n + 1)} {h1 : k ≠ i} {h2 : k ≠ j} : +SwapVariablesFun i j (X k) = X k := by + simp [SwapVariablesFun, h1, h2, Equiv.swap_apply_of_ne_of_ne] + +/- Some really specific and technical lemmas-/ +lemma fin_succ_ne_fin_castSucc (i : Fin n) : Fin.succ i ≠ Fin.castSucc i := by + apply Fin.val_ne_iff.mp + dsimp + norm_num + +lemma wario_number_one {n : ℕ} {a : ℕ} {h : a < n} {a' : ℕ} {h' : a' < n} : +({ val := a, isLt := h } : Fin n) ≠ { val := a', isLt := h' } ↔ a ≠ a' := by + rw[ne_eq] + rw[ne_eq] + apply not_iff_not.mpr + exact Fin.mk_eq_mk + + +lemma i_ne_i_plus_1 {i : ℕ} {h : i < n + 1} {h' : i + 1 < n + 1} : + ({ val := i, isLt := h } : Fin (n + 1)) ≠ { val := i + 1, isLt := h' } := by + rw[wario_number_one] + linarith + +lemma demazure_denominator_not_null (i : Fin n) : + (X (Fin.castSucc i) : MvPolynomial (Fin (n + 1)) ℂ) - X (Fin.succ i) ≠ 0 := by + apply MvPolynomial.ne_zero_iff.mpr + use Finsupp.single (Fin.succ i) 1 + rw[MvPolynomial.coeff_sub] + rw[MvPolynomial.coeff_X] + rw[MvPolynomial.coeff_X'] + have h : Finsupp.single (Fin.castSucc i) 1 ≠ Finsupp.single (Fin.succ i) 1 := by + apply Finsupp.ne_iff.mpr + use Fin.succ i + simp[fin_succ_ne_fin_castSucc] + rw [if_neg h] + simp + +/- Now we can use these to define the demazure numerator. We distinguish the variable x_i + to perform division by (x_i - x_(i+1)) later (only univariable division is supported) -/ + +/-- The numerator used to define the Demazure operator in one distinguished variable. -/ +def DemazureNumerator (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : + Polynomial (MvPolynomial (Fin n) ℂ) := + let i' : Fin (n + 1) := Fin.castSucc i + let i'_plus_1 : Fin (n + 1) := Fin.succ i + let numerator := p - SwapVariables i' i'_plus_1 p + let numerator_X_i_at_start : MvPolynomial (Fin (n + 1)) ℂ := SwapVariables i' 0 numerator + (finSuccEquiv ℂ n) numerator_X_i_at_start + +lemma demazure_numerator_add (i : Fin n) : ∀ p q : MvPolynomial (Fin (n + 1)) ℂ, + DemazureNumerator i (p + q) = DemazureNumerator i p + DemazureNumerator i q := by + intro p q + simp [DemazureNumerator, SwapVariables, map_add, sub_eq_add_neg] + abel + +lemma demazure_numerator_C_mul (i : Fin n) : ∀ (p : MvPolynomial (Fin (n + 1)) ℂ) (r : ℂ), + DemazureNumerator i (C r * p) = Polynomial.C (C r) * DemazureNumerator i p := by + intro p r + simp only [DemazureNumerator, SwapVariables, map_mul, renameEquiv_apply, algHom_C, + algebraMap_eq, sub_eq_add_neg, map_add, map_neg, rename_rename] + rw [show (MvPolynomial.finSuccEquiv ℂ n) (C r : MvPolynomial (Fin (n + 1)) ℂ) = + Polynomial.C (C r) by simp [MvPolynomial.finSuccEquiv_apply]] + ring + +-- Now we also define the denominator taking the variable x_i as the variable to divide by +/-- The monic denominator `X - X_i` used in the Demazure division step. -/ +def DemazureDenominator (i : Fin n) : Polynomial (MvPolynomial (Fin n) ℂ) := + let X_i : MvPolynomial (Fin n) ℂ := MvPolynomial.X i + let denominator_X : Polynomial (MvPolynomial (Fin n) ℂ) := (Polynomial.X - Polynomial.C X_i) + denominator_X + +lemma demazure_denominator_ne_zero : ∀ i : Fin n, DemazureDenominator i ≠ 0 := by + intro i + simpa [DemazureDenominator] using Polynomial.X_sub_C_ne_zero (X i) + +lemma demazure_denominator_monic : ∀ i : Fin n, Polynomial.Monic (DemazureDenominator i) := by + intro i + simpa [DemazureDenominator] using Polynomial.monic_X_sub_C (X i) + +/- the division is exact so the demazure operator is well defined +(division by polynomials returns just the quotient) -/ +lemma demazure_division_exact : ∀(i : Fin n), ∀(p : MvPolynomial (Fin (n + 1)) ℂ), + (DemazureNumerator i p).modByMonic (DemazureDenominator i) = 0 := by + intro i p + simp only [DemazureNumerator, SwapVariables, renameEquiv_apply, map_sub, + rename_rename, finSuccEquiv_apply, coe_eval₂Hom, DemazureDenominator, + Polynomial.modByMonic_X_sub_C_eq_C_eval, Polynomial.eval_sub, polynomial_eval_eval₂] + apply sub_eq_zero.mpr + apply congr_arg Polynomial.C + repeat + rw[MvPolynomial.eval₂_rename] + apply MvPolynomial.eval₂_congr + intro j c _ _ + simp[Equiv.swap_apply_def] + by_cases h1 : j = Fin.castSucc i + · simp[h1, fin_succ_ne_fin_castSucc i, Fin.succ_ne_zero] + by_cases h2 : j = Fin.succ i + · simp[h2, fin_succ_ne_fin_castSucc i, Fin.succ_ne_zero] + by_cases h3 : j = 0 + · subst h3 + simp[h1, h2] + simp[h1, h2, h3] + + +/-- The Demazure operator as a function on multivariate polynomials. -/ +def DemazureFun (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ) : MvPolynomial (Fin (n + 1)) ℂ := + let numerator := DemazureNumerator i p + let denominator := DemazureDenominator i + let division := numerator.divByMonic denominator + let division_mv : MvPolynomial (Fin (n + 1)) ℂ := (AlgEquiv.symm (finSuccEquiv ℂ n)) division + let i' : Fin (n + 1) := Fin.castSucc i + SwapVariables i' 0 division_mv + +/- Some auxiliary lemmas for the multivariate polynomial ring -/ +lemma poly_mul_cancel {p q r : Polynomial (MvPolynomial (Fin n) ℂ)} (hr : r ≠ 0) : + p = q ↔ (r * p) = (r * q) := by + constructor + · intro h + exact congrArg (HMul.hMul r) h + · intro h + exact mul_left_cancel₀ hr h + +lemma poly_cancel_left {p q r : MvPolynomial (Fin n) ℂ} (hr : r ≠ 0) : + (r * p) = (r * q) → p = q := by + intro h + exact mul_left_cancel₀ hr h + +lemma poly_div_cancel {p q r : Polynomial (MvPolynomial (Fin n) ℂ)} + (hr : Polynomial.Monic r) (hp : p %ₘ r = 0) (hq : q %ₘ r = 0) : + p = q ↔ (p /ₘ r) = (q /ₘ r) := by + constructor + · intro h + exact congrArg (fun x => x /ₘ r) h + · intro h + have div_p : p %ₘ r + r * (p /ₘ r) = p := Polynomial.modByMonic_add_div p r + have div_q : q %ₘ r + r * (q /ₘ r) = q := Polynomial.modByMonic_add_div q r + rw[hp, zero_add] at div_p + rw[hq, zero_add] at div_q + rw[← div_p, ← div_q] + apply (poly_mul_cancel (Polynomial.Monic.ne_zero hr)).mp h + +lemma poly_exact_div_mul_cancel {p q : Polynomial (MvPolynomial (Fin n) ℂ)} + (_q_monic : Polynomial.Monic q) (exact_div : p %ₘ q = 0) : q * (p /ₘ q) = p := by + nth_rewrite 2 [← sub_zero p] + apply eq_sub_of_add_eq + rw[add_comm] + rw[← exact_div] + exact Polynomial.modByMonic_add_div p q + +-- since the division is exact, the quotient perfectly divides the numerator +lemma demazure_division_exact' : ∀(i : Fin n), ∀(p : MvPolynomial (Fin (n + 1)) ℂ), + DemazureDenominator i * ((DemazureNumerator i p) /ₘ (DemazureDenominator i)) = + DemazureNumerator i p := by + intro i p + apply poly_exact_div_mul_cancel (demazure_denominator_monic i) (demazure_division_exact i p) + +/- Now we prove that the Demazure operator is a linear map directly with the definition. + This requires a lot of work to disentangle it -/ + +lemma demazure_map_add (i : Fin n) : ∀p q : MvPolynomial (Fin (n + 1)) ℂ, + DemazureFun i (p + q) = DemazureFun i p + DemazureFun i q := by + intro p q + simp only [DemazureFun, SwapVariables, renameEquiv_apply] + rw[← map_add] + apply congr_arg + rw[← map_add (AlgEquiv.symm (MvPolynomial.finSuccEquiv ℂ n)) + (DemazureNumerator i p /ₘ DemazureDenominator i) + (DemazureNumerator i q /ₘ DemazureDenominator i)] + apply congr_arg + apply (poly_mul_cancel (demazure_denominator_ne_zero i)).mpr + simp only [mul_add] + simp only [demazure_division_exact'] + exact demazure_numerator_add i p q + +lemma demazure_map_smul (i : Fin n) : ∀ (r : ℂ) (p : MvPolynomial (Fin (n + 1)) ℂ), + DemazureFun i (r • p) = r • DemazureFun i p := by + intro r p + simp only [DemazureFun, SwapVariables, smul_eq_C_mul, renameEquiv_apply] + nth_rewrite 2 [← rename_C (Equiv.swap (Fin.castSucc i) 0) r] + rw[← map_mul] + apply congr_arg + nth_rewrite 2 [← MvPolynomial.finSuccEquiv_comp_C_eq_C] + simp only [RingHom.comp, Nat.succ_eq_add_one, RingHom.coe_coe, RingHom.coe_mk, + MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply] + rw[← map_mul (AlgEquiv.symm (MvPolynomial.finSuccEquiv ℂ n))] + apply congr_arg + apply (poly_mul_cancel (demazure_denominator_ne_zero i)).mpr + rw[← mul_assoc] + rw [mul_comm (DemazureDenominator i) (Polynomial.C (C r))] + simp only [demazure_division_exact'] + rw[mul_assoc] + rw[demazure_division_exact' i p] + exact demazure_numerator_C_mul i p r + +/-- The Demazure operator as a complex-linear map. -/ +def DemazureLinear (i : Fin n) : + LinearMap (RingHom.id ℂ) (MvPolynomial (Fin (n + 1)) ℂ) + (MvPolynomial (Fin (n + 1)) ℂ) where + toFun := DemazureFun i + map_add' := demazure_map_add i + map_smul' := demazure_map_smul i + +lemma one_of_div_by_monic_self : ∀ (p : Polynomial (MvPolynomial (Fin n) ℂ)) + (_h : Polynomial.Monic p), p /ₘ p = 1 := by + intro p hp + have hmod : p %ₘ p = 0 := (Polynomial.modByMonic_eq_zero_iff_dvd hp).mpr (dvd_refl p) + have h := Polynomial.modByMonic_add_div p p + rw [hmod, zero_add] at h + apply (mul_left_cancel₀ hp.ne_zero) + simpa using h + + +-- Example showing that the demazure operator doesn't respect the multiplication +lemma demazure_not_multiplicative : ∀ (i : Fin n), ∃(p q : MvPolynomial (Fin (n+1)) ℂ), + DemazureLinear i (p * q) ≠ DemazureLinear i p * DemazureLinear i q := by + intro i + use (X (Fin.castSucc i)) + use C 1 + simp only [DemazureLinear, mul_one, LinearMap.coe_mk, AddHom.coe_mk, DemazureFun, + SwapVariables, DemazureNumerator, renameEquiv_apply, rename_X, Equiv.swap_apply_left, + map_sub, Equiv.swap_apply_def, fin_succ_ne_fin_castSucc, ↓reduceIte, Fin.succ_ne_zero, + DemazureDenominator, map_one, sub_self, map_zero, + Polynomial.zero_divByMonic, mul_zero, ne_eq] + rw [MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.finSuccEquiv_X_succ] + rw[one_of_div_by_monic_self] + · simp + · exact Polynomial.monic_X_sub_C (X i) + +/- Doing anything with the definition, even simple things, requires a lot of work given +the complexity of the definition. That's why in DemazureAux.lean we introduce an alternative +definition that will be the one we actually use for computations -/ + +end Demazure + +end diff --git a/LeanPool/DemazureOperatorsLean/DemazureAux.lean b/LeanPool/DemazureOperatorsLean/DemazureAux.lean new file mode 100644 index 0000000000..81c662a0f5 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/DemazureAux.lean @@ -0,0 +1,418 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import LeanPool.DemazureOperatorsLean.Demazure + + +noncomputable section +open MvPolynomial + +namespace Demazure + +variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1) + +/- We are going to define the Demazure operator acting on polynomial fractions. For this, +we first define a structure to represent these fractions, and then we will quotient it by +the proportionality equivalence relation -/ + +/-- A numerator-denominator representative for a rational expression in the polynomial ring. -/ +structure PolyFraction' (n : ℕ) where + /-- The numerator polynomial. -/ + numerator : MvPolynomial (Fin (n + 1)) ℂ + /-- The denominator polynomial. -/ + denominator : MvPolynomial (Fin (n + 1)) ℂ + /-- The denominator is nonzero. -/ + denominator_ne_zero : denominator ≠ 0 + +example : PolyFraction' 2 := ⟨X 0 + X 1, 1, one_ne_zero⟩ +/-- View a polynomial as a fraction with denominator one. -/ +def to_frac (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction' n := ⟨p, 1, one_ne_zero⟩ + +/-- The proportionality relation on polynomial fractions. -/ +def r (n : ℕ) : PolyFraction' n → PolyFraction' n → Prop := + fun p q => p.numerator * q.denominator = q.numerator * p.denominator + +lemma r_equiv : Equivalence (r n) := by + constructor + · intro p + rfl + · intro p q h + exact h.symm + · intro x y z h1 h2 + change x.numerator * z.denominator = z.numerator * x.denominator + change x.numerator * y.denominator = y.numerator * x.denominator at h1 + change y.numerator * z.denominator = z.numerator * y.denominator at h2 + by_cases h3 : y.numerator = 0 + · simp[h3, y.denominator_ne_zero] at h1 + simp[h3, y.denominator_ne_zero] at h2 + simp[h1, h2] + · apply poly_cancel_left y.denominator_ne_zero + apply poly_cancel_left h3 + ring + rw[mul_assoc y.numerator] + rw[mul_comm y.denominator x.numerator] + rw[h1] + rw[mul_comm y.numerator (y.numerator * x.denominator)] + rw[mul_assoc] + rw[h2] + ring + +instance s (n : ℕ) : Setoid (PolyFraction' n) where + r := r n + iseqv := r_equiv + +instance has_equiv : HasEquiv (PolyFraction' n) := instHasEquivOfSetoid + +lemma equiv_r {a b : PolyFraction' n} : (r n) a b ↔ a ≈ b := by + rfl + + +/-- The quotient type of polynomial fractions modulo proportionality. -/ +def PolyFraction (n : ℕ) := (Quotient (s n)) + +/-- The quotient map from fraction representatives. -/ +def mk (p : PolyFraction' n) : PolyFraction n := Quotient.mk (s n) p + +/-- The quotient map from polynomials, viewed as fractions with denominator one. -/ +def mk' (p : MvPolynomial (Fin (n + 1)) ℂ) : PolyFraction n := mk ⟨p, 1, one_ne_zero⟩ + + +/- This lemmas enables us to compute the result of a lift of a function applied at a + representant class. -/ +lemma lift_r {a : PolyFraction' n} {f : PolyFraction' n → PolyFraction' n} + {c : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (mk ∘ f) a₁ = (mk ∘ f) a₂} : + Quotient.lift (mk ∘ f) c (mk a) = mk (f a) := by + rfl +@[simp] +lemma lift2_r {a b : PolyFraction' n} + {f : PolyFraction' n → PolyFraction' n → PolyFraction n} + {c : ∀ (a₁ b₁ a₂ b₂ : PolyFraction' n), a₁ ≈ a₂ → b₁ ≈ b₂ → + f a₁ b₁ = f a₂ b₂} : + Quotient.lift₂ f c (mk a) (mk b) = f a b := by + rfl + +/- Two projections are equal iff the representants are proportional -/ +@[simp] +lemma mk_eq {a b : PolyFraction' n} : + mk a = mk b ↔ a.numerator*b.denominator = a.denominator*b.numerator := by + constructor + · intro h + have hr : a ≈ b := Quotient.exact h + rw[← equiv_r] at hr + simpa [r, mul_comm] using hr + · intro h + change Quotient.mk (s n) a = Quotient.mk (s n) b + apply Quotient.sound + rw[← equiv_r] + simpa [r, mul_comm] using h + +-- function to get a representant of a fraction +lemma get_polyfraction_rep (p : PolyFraction n) : ∃p' : PolyFraction' n, mk p' = p := by + exact Quotient.exists_rep p + +/-- Addition of polynomial-fraction representatives. -/ +def add' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n := + fun p q => ⟨p.numerator * q.denominator + q.numerator * p.denominator, + p.denominator * q.denominator, mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩ + +/-- Addition of representatives followed by the quotient map. -/ +def add_mk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n := + fun p q => mk (add' p q) + +lemma add'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ → + add_mk a₁ b₁ = add_mk a₂ b₂ := by + intro a1 b1 a2 b2 h1 h2 + simp only [add_mk, add', mk_eq] + ring + rw[← equiv_r] at h1 + rw[← equiv_r] at h2 + change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 + change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2 + rw[mul_comm a1.numerator] + rw[mul_assoc b1.denominator] + rw[h1] + rw[mul_comm b1.numerator] + rw[mul_assoc a1.denominator] + rw[mul_comm b1.numerator] + rw[mul_assoc a1.denominator] + rw[mul_assoc a2.denominator] + rw[h2] + ring + +/-- Addition on quotient polynomial fractions. -/ +def add : PolyFraction n → PolyFraction n → PolyFraction n := + fun p q ↦ Quotient.lift₂ (add_mk) (add'_s) p q + +-- Enable use of + notation +instance addition : Add (PolyFraction n) := ⟨add⟩ +instance addition' : Add (PolyFraction' n) := ⟨add'⟩ + +/-- Subtraction of polynomial-fraction representatives, followed by the quotient map. -/ +def sub' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n := + fun p q ↦ mk ⟨p.numerator * q.denominator - q.numerator * p.denominator, + p.denominator * q.denominator, mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩ + +lemma sub'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ → + (sub' a₁ b₁) = (sub' a₂ b₂) := by + intro a1 b1 a2 b2 h1 h2 + simp only [sub', mk_eq] + ring + rw[← equiv_r] at h1 + rw[← equiv_r] at h2 + change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 + change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2 + rw[mul_comm a1.numerator] + rw[mul_assoc b1.denominator] + rw[h1] + rw[mul_comm b1.numerator] + rw[mul_assoc a1.denominator] + rw[mul_comm b1.numerator] + rw[mul_assoc a1.denominator] + rw[mul_assoc a2.denominator] + rw[h2] + ring + +/-- Subtraction on quotient polynomial fractions. -/ +def sub : PolyFraction n → PolyFraction n → PolyFraction n := + fun p q ↦ Quotient.lift₂ (sub') (sub'_s) p q + +/-- Multiplication of polynomial-fraction representatives. -/ +def mul' {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction' n := + fun p q => ⟨p.numerator * q.numerator, p.denominator * q.denominator, + mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩ + +/-- Multiplication of representatives followed by the quotient map. -/ +def mul_mk {n : ℕ} : PolyFraction' n → PolyFraction' n → PolyFraction n := + fun p q => mk (mul' p q) + +lemma mul'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a₂ → b₁ ≈ b₂ → + (mul_mk a₁ b₁) = (mul_mk a₂ b₂) := by + intro a1 b1 a2 b2 h1 h2 + simp only [mul_mk, mul', mk_eq] + ring + rw[← equiv_r] at h1 + rw[← equiv_r] at h2 + change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 + change b1.numerator * b2.denominator = b2.numerator * b1.denominator at h2 + rw[mul_comm a1.numerator] + rw[mul_assoc b1.numerator] + rw[h1] + rw[mul_comm b1.numerator] + rw[mul_assoc (a2.numerator * a1.denominator)] + rw[h2] + ring + +/-- Multiplication on quotient polynomial fractions. -/ +def mul : PolyFraction n → PolyFraction n → PolyFraction n := + fun p q ↦ Quotient.lift₂ (mul_mk) (mul'_s) p q + +-- Enable use of * notation +instance multiplication' : Mul (PolyFraction' n) := ⟨mul'⟩ +instance multiplication : Mul (PolyFraction n) := ⟨mul⟩ + +/-- The multiplicative identity as a fraction representative. -/ +@[simp] +def one' : PolyFraction' n where + numerator := 1 + denominator := 1 + denominator_ne_zero := one_ne_zero + +/-- The multiplicative identity as a quotient fraction. -/ +def one : PolyFraction n := mk one' + +/-- The additive identity as a fraction representative. -/ +@[simp] +def zero' : PolyFraction' n where + numerator := 0 + denominator := 1 + denominator_ne_zero := one_ne_zero + +/-- The additive identity as a quotient fraction. -/ +def zero : PolyFraction n := mk zero' + +/-- Negation of polynomial-fraction representatives. -/ +def neg' (p : PolyFraction' n) : PolyFraction' n := + ⟨-p.numerator, p.denominator, p.denominator_ne_zero⟩ + +/-- Negation of representatives followed by the quotient map. -/ +def neg_mk (p : PolyFraction' n) : PolyFraction n := mk (neg' p) + +lemma neg_s (n : ℕ) : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (neg_mk a₁) = (neg_mk a₂) := by + intro a1 a2 h + simp only [neg_mk, neg', mk_eq, neg_mul, mul_neg, neg_inj] + ring + rw[← equiv_r] at h + change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h + rw[h] + ring + +/-- Negation on quotient polynomial fractions. -/ +def neg (p : PolyFraction n) : PolyFraction n := Quotient.lift neg_mk (neg_s n) p + +-- some basic properties of these operations +lemma add_comm (p q : PolyFraction n) : add p q = add q p := by + rcases get_polyfraction_rep p with ⟨p', hp⟩ + rcases get_polyfraction_rep q with ⟨q', hq⟩ + simp only [add] + rw[← hp] + rw[← hq] + simp[lift2_r] + simp[add_mk, add'] + ring + +lemma add_assoc (p q r : PolyFraction n) : add (add p q) r = add p (add q r) := by + rcases get_polyfraction_rep p with ⟨p', hp⟩ + rcases get_polyfraction_rep q with ⟨q', hq⟩ + rcases get_polyfraction_rep r with ⟨r', hr⟩ + rw[← hp] + rw[← hq] + rw[← hr] + have hpq : (add (mk p') (mk q')) = mk (add' p' q') := by + simp[add, add_mk] + have hqr : (add (mk q') (mk r')) = mk (add' q' r') := by + simp[add, add_mk] + rw[hpq, hqr] + simp only [add, lift2_r] + simp only [add'] + apply Quotient.sound + apply equiv_r.mp + simp[Demazure.r, add'] + ring + +-- We don't prove that it is a ring since we don't need all the properties for our use + +/- We directly define the Demazure operator on fractions (even though we proved that +the result is a polynomial, for the proofs it's better to keep the result as a fraction)-/ +/-- The auxiliary Demazure operator on fraction representatives. -/ +def DemAux' (i : Fin n) : PolyFraction' n → PolyFraction' n := fun p => + ⟨ + p.numerator * (SwapVariables (Fin.castSucc i) (Fin.succ i) p.denominator) - + (SwapVariables (Fin.castSucc i) (Fin.succ i) p.numerator) * p.denominator, + p.denominator * (SwapVariables (Fin.castSucc i) (Fin.succ i) p.denominator) * + (X (Fin.castSucc i) - X (Fin.succ i)), + mul_ne_zero + (mul_ne_zero p.denominator_ne_zero + (swap_variables_ne_zero (Fin.castSucc i) (Fin.succ i) p.denominator + p.denominator_ne_zero)) + (demazure_denominator_not_null i) + ⟩ + +lemma DemAux_well_defined (i : Fin n) : ∀ (p q : PolyFraction' n), + p ≈ q → ((mk ∘ DemAux' i) p) = ((mk ∘ DemAux' i) q) := by + intro p q h + simp only [Function.comp_apply, DemAux', SwapVariables, renameEquiv_apply, mk_eq] + rw[← equiv_r] at h + change p.numerator * q.denominator = q.numerator * p.denominator at h + let S : MvPolynomial (Fin (n + 1)) ℂ ≃ₐ[ℂ] MvPolynomial (Fin (n + 1)) ℂ := + SwapVariables (Fin.castSucc i) (Fin.succ i) + let delta : MvPolynomial (Fin (n + 1)) ℂ := X (Fin.castSucc i) - X (Fin.succ i) + have h_swap : S p.numerator * S q.denominator = S q.numerator * S p.denominator := by + simpa [S, map_mul] using congrArg S h + calc + (p.numerator * S p.denominator - S p.numerator * p.denominator) * + (q.denominator * S q.denominator * delta) = + (p.numerator * q.denominator) * (S p.denominator * S q.denominator * delta) - + (S p.numerator * S q.denominator) * (p.denominator * q.denominator * delta) := by + ring + _ = p.denominator * S p.denominator * delta * + (q.numerator * S q.denominator - S q.numerator * q.denominator) := by + rw [h, h_swap] + ring + +/-- The auxiliary Demazure operator on quotient polynomial fractions. -/ +def DemAux (i : Fin n) (p : PolyFraction n) : PolyFraction n := + Quotient.lift (mk ∘ (DemAux' i)) (DemAux_well_defined i) p + +/- This definition is equivalent to the direct one on the polynomial ring-/ +lemma demazure_definitions_equivalent' : ∀ i : Fin n, ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + mk (DemAux' i (to_frac p)) = mk' (DemazureFun i p) := by + intro i p + simp only [mk', mk_eq, mul_one] + simp only [DemAux', to_frac, SwapVariables, renameEquiv_apply, map_one, mul_one, one_mul] + have h : DemazureDenominator i * ((DemazureNumerator i p) /ₘ (DemazureDenominator i)) = + DemazureNumerator i p := demazure_division_exact' i p + apply (SwapVariables (Fin.castSucc i) (0 : Fin (n + 1))).injective + apply (MvPolynomial.finSuccEquiv ℂ n).injective + change DemazureNumerator i p = (MvPolynomial.finSuccEquiv ℂ n) + ((SwapVariables (Fin.castSucc i) 0) + ((X (Fin.castSucc i) - X (Fin.succ i)) * DemazureFun i p)) + rw[← h] + simp only [SwapVariables, renameEquiv_apply, map_mul, map_sub, rename_X, + Equiv.swap_apply_left, ne_eq, fin_succ_ne_fin_castSucc i, not_false_eq_true, + Fin.succ_ne_zero, Equiv.swap_apply_of_ne_of_ne] + rw [MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.finSuccEquiv_X_succ] + have h3 : DemazureDenominator i = Polynomial.X - Polynomial.C (X i) := by + simp [DemazureDenominator] + rw[← h3] + rw[← poly_mul_cancel (demazure_denominator_ne_zero i)] + simp only [DemazureFun, SwapVariables, renameEquiv_apply, rename_rename] + rw [show (⇑(Equiv.swap (Fin.castSucc i) 0) ∘ ⇑(Equiv.swap (Fin.castSucc i) 0)) = + id by + funext k + simp] + simp + +lemma demazure_definitions_equivalent : ∀ i : Fin n, ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + DemAux i (mk' p) = mk' (DemazureFun i p) := by + intro i p + rw[mk'] + simp only [DemAux] + rw[lift_r] + rw[← demazure_definitions_equivalent' i p] + rfl + +/- We can prove equalities in the ring of polynomials by reducing to the polynomial fraction case. +This sets the strategy for proving properties of the Demazure operator: + +Prove them for DemAux (in DemazureAuxRelations.lean) and then use these lemmas and +the equivalence of both operators +to get the result for Demazure (in DemazureRelations.lean).-/ +lemma eq_zero_of_mk'_zero {p : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = zero ↔ p = 0 := by + constructor + · intro h + simpa [mk', zero] using h + · intro h + simp[h, mk', zero] + +lemma eq_of_eq_mk' {p q : MvPolynomial (Fin (n + 1)) ℂ} : mk' p = mk' q ↔ p = q := by + constructor + · intro h + simpa [mk'] using h + · intro h + simp[h] + + +/- Some lemmas for interplay between mk and add -/ +@[simp] +lemma simp_add {p q : PolyFraction n} : p + q = add p q := rfl + +lemma mk_add {p q : PolyFraction' n} : ((mk p) : PolyFraction n) + mk q = mk (p + q) := by + have h1 : p+q = add' p q := by rfl + have h2 : mk p + mk q = add (mk p) (mk q) := by rfl + simp[add, add_mk, add', h1, h2] + +lemma mk'_add : ∀ (p q : MvPolynomial (Fin (n + 1)) ℂ), mk' (p + q) = mk' p + mk' q := by + simp[mk', add, add_mk, add'] + +@[simp] +lemma simp_mul' {p q : PolyFraction' n} : + p * q = ⟨p.numerator * q.numerator, p.denominator * q.denominator, + mul_ne_zero p.denominator_ne_zero q.denominator_ne_zero⟩ := rfl + +@[simp] +lemma simp_mul {p q : PolyFraction n} : p * q = mul p q := rfl + +lemma mk_mul {p q : PolyFraction' n} : ((mk p) : PolyFraction n) * mk q = mk (p * q) := by + have h1 : p*q = mul' p q := by rfl + have h2 : mk p * mk q = mul (mk p) (mk q) := by rfl + simp[mul, mul_mk, mul'] + +lemma mk'_mul {p q : MvPolynomial (Fin (n + 1)) ℂ} : mk' p * mk' q = mk' (p * q) := by + simp[mk', mul_mk, mul', mul] + +end Demazure + +end diff --git a/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean b/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean new file mode 100644 index 0000000000..5b1d3170a5 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/DemazureAuxRelations.lean @@ -0,0 +1,215 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import LeanPool.DemazureOperatorsLean.Demazure +import LeanPool.DemazureOperatorsLean.DemazureAux + +noncomputable section +namespace Demazure + +-- Some computations are quite heavy, so we increase the number of heartbeats + +open MvPolynomial + +variable {n : ℕ} (n_pos : n > 0) + +/- Composition relations for Demazure operators -/ +-- Start by proving that the Demazure Operator applied two times is the zero operator +lemma demaux_order_two : ∀ (i : Fin n) (p : PolyFraction n), + (DemAux i ∘ DemAux i) p = zero := by + intro i p + rcases get_polyfraction_rep p with ⟨p', rfl⟩ + dsimp [DemAux] + rw[lift_r] + rw[lift_r] + rw[zero] + apply Quotient.sound + rw[← equiv_r] + simp[r, DemAux'] + ring + +/-- Two indices are non-adjacent when the adjacent transpositions they determine are disjoint. -/ +def NonAdjacent (i j : Fin n) : Prop := + (Fin.castSucc i : Fin (n + 1)) ≠ (Fin.castSucc j : Fin (n + 1)) ∧ + (Fin.castSucc i : Fin (n + 1)) ≠ (Fin.succ j : Fin (n + 1)) ∧ + (Fin.succ i : Fin (n + 1)) ≠ (Fin.castSucc j : Fin (n + 1)) ∧ + (Fin.succ i : Fin (n + 1)) ≠ (Fin.succ j : Fin (n + 1)) + +lemma equiv_swap_mul_eq_comp {a b c d k : Fin n} : +(Equiv.swap a b * Equiv.swap c d) k = (Equiv.swap a b ∘ Equiv.swap c d) k := by + rfl + +lemma renameEquiv_swap_ext {a b c d : Fin n} {R : Type} [CommSemiring R] : + rename (Equiv.swap a b * Equiv.swap c d) = + (rename (Equiv.swap a b ∘ Equiv.swap c d) : + MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin n) R) := by + rfl + +-- Now prove that demazure operators with non-adjacent indices commute +lemma transposition_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) : + Equiv.swap (Fin.castSucc i) (Fin.succ i) * Equiv.swap (Fin.castSucc j) (Fin.succ j) = + Equiv.swap (Fin.castSucc j) (Fin.succ j) * Equiv.swap (Fin.castSucc i) (Fin.succ i) := by + rcases h with ⟨h1, h2, h3, h4⟩ + have h_disjoint : + Equiv.Perm.Disjoint (Equiv.swap i.castSucc i.succ) + (Equiv.swap j.castSucc j.succ) := by + intro k + apply or_iff_not_imp_left.mpr + intro h + rcases Equiv.eq_or_eq_of_swap_apply_ne_self h with h | h + · simpa [h] using Equiv.swap_apply_of_ne_of_ne h1 h2 + · simpa [h] using Equiv.swap_apply_of_ne_of_ne h3 h4 + rw[Equiv.Perm.Disjoint.commute h_disjoint] + +lemma transposition_commutes_non_adjacent' (i j : Fin n) (h : NonAdjacent i j) : + Equiv.swap (Fin.castSucc i) (Fin.succ i) ∘ Equiv.swap (Fin.castSucc j) (Fin.succ j) = + Equiv.swap (Fin.castSucc j) (Fin.succ j) ∘ Equiv.swap (Fin.castSucc i) (Fin.succ i) := by + funext k + rw[← equiv_swap_mul_eq_comp] + simp[transposition_commutes_non_adjacent i j h] + + +lemma swap_variables_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) + {p : MvPolynomial (Fin (n + 1)) ℂ} : + SwapVariablesFun (Fin.castSucc i) (Fin.succ i) + (SwapVariablesFun (Fin.castSucc j) (Fin.succ j) p) = + SwapVariablesFun (Fin.castSucc j) (Fin.succ j) + (SwapVariablesFun (Fin.castSucc i) (Fin.succ i) p) := by + dsimp [SwapVariablesFun] + simp[transposition_commutes_non_adjacent' i j h] + +lemma demaux_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemAux i ∘ DemAux j) (mk' p) = (DemAux j ∘ DemAux i) (mk' p) := by + intro p + dsimp [DemAux, mk'] + repeat rw[lift_r] + apply mk_eq.mpr + simp[DemAux'] + simp [swap_variables_commutes_non_adjacent i j h] + rcases h with ⟨h1, h2, h3, h4⟩ + simp[h1, h2, h3, h4, h1.symm, h2.symm, h3.symm, h4.symm] + ring + +/-- Prove some relations between Demazure operators and multiplication by monomials, in the +adjacent and non-adjacent cases -/ +lemma demaux_mul_monomial_non_adjacent (i j : Fin n) (h : NonAdjacent i j) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + DemAux i (mk' (p * X (Fin.castSucc j))) = + (DemAux i (mk' p)) * (mk' (X (Fin.castSucc j))) := by + intro p + dsimp [DemAux, mul] + apply mk_eq.mpr + simp[DemAux', mul'] + rcases h with ⟨h1, h2, h3, h4⟩ + simp [h1.symm, h3.symm] + ring + +lemma demaux_mul_monomial_adjacent (i : Fin n) (_h : i + 1 < n) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemAux i (mk' (p * X (Fin.castSucc i)))) = + (DemAux i (mk' p)) * (mk' (X (Fin.succ i))) + mk' p := by + intro p + dsimp [DemAux, mk'] + repeat rw[lift_r] + apply mk_eq.mpr + simp[DemAux', mul', add'] + ring + +lemma symm_invariant_swap_variables {i j : Fin n} {g : MvPolynomial (Fin n) ℂ} + (h : MvPolynomial.IsSymmetric g) : + SwapVariablesFun i j g = g := by + dsimp [SwapVariablesFun] + exact h (Equiv.swap i j) + +/- Now we prove that symmetric polynomials act as scalars -/ +/-- A quotient fraction represented by symmetric numerator and denominator polynomials. -/ +def IsSymmetric (p : PolyFraction n) : Prop := ∃p' : PolyFraction' n, + mk p' = p ∧ MvPolynomial.IsSymmetric p'.numerator ∧ MvPolynomial.IsSymmetric p'.denominator + +lemma demaux_mul_symm (i : Fin n) (g f : PolyFraction n) (h : IsSymmetric g) : + DemAux i (g*f) = g*(DemAux i f) := by + rcases h with ⟨g', ⟨rfl, g_num_symm, g_denom_symm⟩⟩ + rcases get_polyfraction_rep f with ⟨f', rfl⟩ + rw[mk_mul] + dsimp [DemAux] + repeat rw[lift_r] + rw[← simp_mul'] + rw[← simp_mul] + rw[mk_mul] + rw[mk_eq] + simp[DemAux'] + simp[symm_invariant_swap_variables g_num_symm, symm_invariant_swap_variables g_denom_symm] + ring + + +-- Prove the relation between demazure operations with adjacent indices +lemma transposition_commutes_adjacent {i : Fin n} {j : Fin (n + 1)} (h0 : i < n + 1) + (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) : + Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ + (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ + (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ j)) = + Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ + (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ + (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ j)) := by + simp[Equiv.swap_apply_def] + by_cases c0 : j = ⟨i, h0⟩ + · simp[c0] + · by_cases c1 : j = ⟨i + 1, h1⟩ + · simp[c1] + · by_cases c2 : j = ⟨i + 2, h2⟩ + · simp[c2] + · simp[c0,c1,c2] + +lemma transposition_commutes_adjacent' {i : Fin n} (h0 : i < n + 1) + (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) : + (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩ ∘ + (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩) ∘ + (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩) : + Fin (n + 1) → Fin (n + 1)) = + Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ ∘ + (Equiv.swap ⟨i, h0⟩ ⟨i + 1, h1⟩) ∘ + (Equiv.swap ⟨i + 1, h1⟩ ⟨i + 2, h2⟩) := by + funext j + simp[transposition_commutes_adjacent h0 h1 h2] + +lemma swap_variables_commutes_adjacent {i : Fin n} {p : MvPolynomial (Fin (n + 1)) ℂ} + (h0 : i < n + 1) (h1 : i + 1 < n + 1) (h2 : i + 2 < n + 1) : + SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩ + (SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ + (SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩ p)) = + SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ + (SwapVariablesFun ⟨i, h0⟩ ⟨i + 1, h1⟩ + (SwapVariablesFun ⟨i + 1, h1⟩ ⟨i + 2, h2⟩ p)) := by + dsimp [SwapVariablesFun] + simp[transposition_commutes_adjacent' h0 h1 h2] + +@[simp] +lemma omg {i : ℕ} : i + 1 + 1 = i + 2 := by + ring + +-- This takes a lot of time to compute +lemma demaux_commutes_adjacent (i : Fin n) (h : i + 1 < n) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemAux i ∘ DemAux ⟨i+1, h⟩ ∘ DemAux i) (mk' p) = + (DemAux ⟨i+1, h⟩ ∘ DemAux i ∘ DemAux ⟨i+1, h⟩) (mk' p) := by + intro p + dsimp [DemAux, mk'] + repeat rw[lift_r] + simp[DemAux'] + simp[Fin.castSucc, Fin.succ, Fin.castAdd, Fin.castLE] + have h0 : i < n + 1 := by + linarith + have h1 : i + 1 < n + 1 := by + linarith + have h2 : i + 2 < n + 1 := by + linarith + simp [swap_variables_commutes_adjacent h0 h1 h2] + ring + +end Demazure + +end diff --git a/LeanPool/DemazureOperatorsLean/DemazureRelations.lean b/LeanPool/DemazureOperatorsLean/DemazureRelations.lean new file mode 100644 index 0000000000..91caa125fc --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/DemazureRelations.lean @@ -0,0 +1,118 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import LeanPool.DemazureOperatorsLean.Demazure +import LeanPool.DemazureOperatorsLean.DemazureAux +import LeanPool.DemazureOperatorsLean.DemazureAuxRelations + +noncomputable section +open MvPolynomial + +namespace Demazure + +variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1) + +/- Now we prove the relations for the actual Demazure operator on polynomials. +There isn't a lot of math going on here, we just take the results from DemAux and +translate them to Demazure-/ + +-- Demazure operator has order two +lemma demazure_order_two : ∀ (i : Fin n) (p : MvPolynomial (Fin (n + 1)) ℂ), + DemazureLinear i (DemazureLinear i p) = 0 := by + intro i p + apply eq_zero_of_mk'_zero.mp + dsimp [DemazureLinear] + rw[← demazure_definitions_equivalent] + rw[← demazure_definitions_equivalent] + exact demaux_order_two i (mk' p) + +-- Demazure operators with adjacent indices have a braid relation +lemma demazure_commutes_adjacent (i : Fin n) (h : i + 1 < n) : ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemazureLinear i ∘ DemazureLinear ⟨i+1, h⟩ ∘ DemazureLinear i) p = + (DemazureLinear ⟨i+1, h⟩ ∘ DemazureLinear i ∘ DemazureLinear ⟨i+1, h⟩) p := by + intro p + dsimp [DemazureLinear] + apply eq_of_eq_mk'.mp + repeat rw[← demazure_definitions_equivalent] + apply demaux_commutes_adjacent + +-- Demazure operators with non-adjacent indices commute +lemma demazure_commutes_non_adjacent (i j : Fin n) (h : NonAdjacent i j) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemazureLinear i ∘ DemazureLinear j) p = (DemazureLinear j ∘ DemazureLinear i) p := by + intro p + dsimp [DemazureLinear] + apply eq_of_eq_mk'.mp + repeat rw[← demazure_definitions_equivalent] + apply demaux_commutes_non_adjacent + exact h + +-- Relation between demazure operator and multiplication by non-adjacent monomials +lemma demazure_mul_monomial_non_adjacent (i j : Fin n) (h : NonAdjacent i j) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + DemazureLinear i (p * X (Fin.castSucc j)) = + (DemazureLinear i p) * (X (Fin.castSucc j)) := by + intro p + dsimp [DemazureLinear] + apply eq_of_eq_mk'.mp + repeat rw[← demazure_definitions_equivalent] + rw[← mk'_mul] + rw[← mk'_mul] + rw[← demazure_definitions_equivalent] + rw[mk'_mul] + apply demaux_mul_monomial_non_adjacent i j h + +-- Relation between demazure operator and multiplication by adjacent monomial +lemma demazure_mul_monomial_adjacent (i : Fin n) (h : i + 1 < n) : + ∀ p : MvPolynomial (Fin (n + 1)) ℂ, + (DemazureLinear i (p * X (Fin.castSucc i))) = + (DemazureLinear i p) * (X (Fin.succ i)) + p := by + intro p + dsimp [DemazureLinear] + apply eq_of_eq_mk'.mp + rw[mk'_add] + rw[← mk'_mul] + repeat rw[← demazure_definitions_equivalent] + apply demaux_mul_monomial_adjacent i h + +-- Symmetric polynomials act as scalars wrt Demazure operators +lemma demazure_mul_symm (i : Fin n) (g f : MvPolynomial (Fin (n + 1)) ℂ) + (h : MvPolynomial.IsSymmetric g) : + DemazureLinear i (g*f) = g*(DemazureLinear i f) := by + dsimp [DemazureLinear] + rw[← eq_of_eq_mk'] + rw[← demazure_definitions_equivalent] + rw [← mk'_mul] + rw [← mk'_mul] + rw[← demazure_definitions_equivalent] + have : IsSymmetric (mk' g) := by + dsimp [IsSymmetric] + use (to_frac g) + dsimp [to_frac] + exact ⟨rfl, h, MvPolynomial.IsSymmetric.one⟩ + exact demaux_mul_symm i (mk' g) (mk' f) this + +/- This enables to define the Demazure operator as a linear map over the ring of +symmetric polynomials, the main result of this project -/ +/-- The Demazure operator as a linear map over the symmetric-polynomial subalgebra. -/ +def Dem (i : Fin n) : LinearMap (RingHom.id (MvPolynomial.symmetricSubalgebra (Fin (n + 1)) ℂ)) + (MvPolynomial (Fin (n + 1)) ℂ) (MvPolynomial (Fin (n + 1)) ℂ) where + toFun := DemazureFun i + map_add' := demazure_map_add i + map_smul' := by + intro r x + simp only [RingHom.id_apply] + let p : MvPolynomial (Fin (n + 1)) ℂ := r + have wah : p = r := by rfl + have h : MvPolynomial.IsSymmetric p := by + apply (MvPolynomial.mem_symmetricSubalgebra p).mp + rw[wah] + exact SetLike.coe_mem r + exact demazure_mul_symm i p x h + +end Demazure + +end diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 8d2bc9c42b..b9970998f5 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,4 +1,37 @@ projects: + - slug: demazureoperatorslean + title: Demazure Operators and Lean + summary: Formalizes Demazure operators on multivariate polynomials and proves their basic braid, commutation, and scalar-action relations. + branch: algebraic combinatorics + entry_module: LeanPool.DemazureOperatorsLean + authors: + - Óscar Álvarez Sánchez + source: + url: https://github.com/bolito2/DemazureOperatorsLean + status: verified + main_declarations: + - Demazure.Dem + - Demazure.demazure_commutes_adjacent + main_results: + - declaration: Demazure.Dem + informal: Defines the Demazure operator as a linear map over the subalgebra of symmetric polynomials. + - declaration: Demazure.demazure_order_two + informal: Proves that applying the Demazure operator twice gives zero. + - declaration: Demazure.demazure_commutes_adjacent + informal: Proves the braid relation for adjacent Demazure operators. + - declaration: Demazure.demazure_commutes_non_adjacent + informal: Proves that non-adjacent Demazure operators commute. + - declaration: Demazure.demazure_mul_symm + informal: Proves that symmetric polynomials act as scalars with respect to Demazure operators. + tags: + - algebraic-combinatorics + - demazure-operators + - polynomials + - representation-theory + msc: + - "05E05" + - "13P10" + - "20F55" - slug: ramanujan-tau-misses-primes title: ABC implies that Ramanujan's tau function misses almost all primes summary: Formalizes the ABC-conditional proof that Ramanujan's tau function takes prime values only rarely. From 772af98a0ef3ea006ca3950ff9b9c3ebf692be8e Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 18 May 2026 20:00:03 +0900 Subject: [PATCH 2/8] Add Demazure operator source citation --- LeanPool/DemazureOperatorsLean.lean | 5 ++++- LeanPool/projects.yml | 8 +++++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index 6cae5b7759..6f9318080e 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -12,7 +12,10 @@ import LeanPool.DemazureOperatorsLean.DemazureAuxRelations /-! # Demazure Operators and Lean -Source: url:https://github.com/bolito2/DemazureOperatorsLean +Source: I. N. Bernstein, I. M. Gelfand, and S. I. Gelfand, + "Schubert cells, and the cohomology of the spaces G/P", Russian + Mathematical Surveys 28:3 (1973), for divided-difference/Demazure operator + relations; formalization source: url:https://github.com/bolito2/DemazureOperatorsLean Authors: Óscar Álvarez Sánchez Status: verified Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent` diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index b9970998f5..7ab586096f 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -7,7 +7,13 @@ projects: authors: - Óscar Álvarez Sánchez source: - url: https://github.com/bolito2/DemazureOperatorsLean + title: "Schubert cells, and the cohomology of the spaces G/P" + authors: + - I. N. Bernstein + - I. M. Gelfand + - S. I. Gelfand + doi: "10.1070/RM1973v028n03ABEH001549" + github_repo: bolito2/DemazureOperatorsLean status: verified main_declarations: - Demazure.Dem From 9ea20e535c72b8ebe0dd04a3e72485b994eb1417 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 18 May 2026 20:17:39 +0900 Subject: [PATCH 3/8] Regenerate project card --- LeanPool/DemazureOperatorsLean.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index 6f9318080e..e710a5743f 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -12,10 +12,7 @@ import LeanPool.DemazureOperatorsLean.DemazureAuxRelations /-! # Demazure Operators and Lean -Source: I. N. Bernstein, I. M. Gelfand, and S. I. Gelfand, - "Schubert cells, and the cohomology of the spaces G/P", Russian - Mathematical Surveys 28:3 (1973), for divided-difference/Demazure operator - relations; formalization source: url:https://github.com/bolito2/DemazureOperatorsLean +Source: doi:10.1070/RM1973v028n03ABEH001549 Authors: Óscar Álvarez Sánchez Status: verified Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent` From e699d58d56e0f2d1f050a1cfd430d5bca8ddd9d5 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 23:44:06 +0900 Subject: [PATCH 4/8] Complete Demazure Coxeter theory import --- LeanPool.lean | 2 + LeanPool/DemazureOperatorsLean.lean | 4 +- LeanPool/DemazureOperatorsLean/Matsumoto.lean | 787 ++++++++++++++++++ .../DemazureOperatorsLean/StrongExchange.lean | 505 +++++++++++ LeanPool/projects.yml | 8 +- 5 files changed, 1304 insertions(+), 2 deletions(-) create mode 100644 LeanPool/DemazureOperatorsLean/Matsumoto.lean create mode 100644 LeanPool/DemazureOperatorsLean/StrongExchange.lean diff --git a/LeanPool.lean b/LeanPool.lean index c2e9d3dae6..5b012dcb44 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -79,6 +79,8 @@ import LeanPool.DemazureOperatorsLean.Demazure import LeanPool.DemazureOperatorsLean.DemazureAux import LeanPool.DemazureOperatorsLean.DemazureAuxRelations import LeanPool.DemazureOperatorsLean.DemazureRelations +import LeanPool.DemazureOperatorsLean.Matsumoto +import LeanPool.DemazureOperatorsLean.StrongExchange import LeanPool.Erdos1196 import LeanPool.Erdos1196.Basic import LeanPool.Erdos1196.FirstEntryRowTerm diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index e710a5743f..fe4d36de7c 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -8,6 +8,8 @@ import LeanPool.DemazureOperatorsLean.Demazure import LeanPool.DemazureOperatorsLean.DemazureAux import LeanPool.DemazureOperatorsLean.DemazureRelations import LeanPool.DemazureOperatorsLean.DemazureAuxRelations +import LeanPool.DemazureOperatorsLean.StrongExchange +import LeanPool.DemazureOperatorsLean.Matsumoto /-! # Demazure Operators and Lean @@ -15,7 +17,7 @@ import LeanPool.DemazureOperatorsLean.DemazureAuxRelations Source: doi:10.1070/RM1973v028n03ABEH001549 Authors: Óscar Álvarez Sánchez Status: verified -Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent` +Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent`, `CoxeterSystem.strongExchangeProperty`, `CoxeterSystem.matsumoto_reduced` Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory MSC: 05E05, 13P10, 20F55 -/ diff --git a/LeanPool/DemazureOperatorsLean/Matsumoto.lean b/LeanPool/DemazureOperatorsLean/Matsumoto.lean new file mode 100644 index 0000000000..6e5bcbe5a5 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/Matsumoto.lean @@ -0,0 +1,787 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import LeanPool.DemazureOperatorsLean.StrongExchange +import Init.Data.List.Erase + +namespace CoxeterSystem +noncomputable section + +variable {B : Type} +variable {W : Type} [Group W] +variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W) + +instance : DecidableEq W := Classical.typeDecidableEq W + +local prefix:100 "s" => cs.simple +local prefix:100 "π" => cs.wordProd +local prefix:100 "len" => cs.length + +/-- Extra nondegeneracy assumptions used in the Matsumoto theorem development. -/ +class MatsumotoCondition where + one_le_M : ∀ i j : B, 1 ≤ M i j + alternatingWords_ne_one : ∀ (i j : B) (_ : i ≠ j) (p : ℕ) (_ : 0 < p) (_ : p < M i j), (s i * s j) ^ p ≠ 1 + +/-- A nil move removes two adjacent equal simple reflections at a given offset. -/ +structure NilMove (cs : CoxeterSystem M W) where + /-- The simple reflection index used by the nil move. -/ + i : B + /-- The offset where the nil move is applied. -/ + p : ℕ +/-- A braid move replaces a braid word by the opposite braid word at a given offset. -/ +structure BraidMove (cs : CoxeterSystem M W) where + /-- The first simple reflection index in the braid word. -/ + i : B + /-- The second simple reflection index in the braid word. -/ + j : B + /-- The offset where the braid move is applied. -/ + p : ℕ + +/-- A Coxeter move is either a nil move or a braid move. -/ +inductive CoxeterMove (cs : CoxeterSystem M W) where +| nil : cs.NilMove → cs.CoxeterMove +| braid : cs.BraidMove → cs.CoxeterMove + +/-- Apply a nil move to a word. -/ +def apply_nilMove (nm : cs.NilMove) (l : List B) : List B := + match nm with + | NilMove.mk i p => + match p with + | 0 => + if l.take 2 = [i, i] then + l.drop 2 + else + l + | p + 1 => + match l with + | [] => [] + | h::t => h :: apply_nilMove (NilMove.mk i p) t + +/-- Apply a braid move to a word. -/ +def apply_braidMove (bm : cs.BraidMove) (l : List B) : List B := + match bm with + | BraidMove.mk i j p => + match p with + | 0 => + if l.take (M i j) = braidWord M i j then + braidWord M j i ++ l.drop (M i j) + else + l + | p + 1 => + match l with + | [] => [] + | h::t => h :: apply_braidMove (BraidMove.mk i j p) t + +/-- Apply either kind of Coxeter move to a word. -/ +def apply_coxeterMove (cm : cs.CoxeterMove) (l : List B) : List B := + match cm with + | CoxeterMove.nil nm => cs.apply_nilMove nm l + | CoxeterMove.braid bm => cs.apply_braidMove bm l + +theorem nilMove_wordProd (nm : cs.NilMove) (l : List B) : π (cs.apply_nilMove nm l) = π l := by + rcases nm with ⟨i, p⟩ + match p with + | 0 => + simp[apply_nilMove] + by_cases h : l.take 2 = [i, i] + · simp[h] + have h' : l = l.take 2 ++ l.drop 2 := by simp + nth_rewrite 2 [h'] + rw[wordProd_append] + rw[h] + simp + convert_to cs.wordProd ([i] ++ [i]) = 1 + rw[wordProd_append] + simp + · simp[h] + | p + 1 => + match l with + | [] => simp[apply_nilMove] + | h::t => + simp[apply_nilMove, wordProd_cons] + exact nilMove_wordProd (NilMove.mk i p) t + +theorem braidMove_wordProd (bm : cs.BraidMove) (l : List B) : π (cs.apply_braidMove bm l) = π l := by + rcases bm with ⟨i, j, p⟩ + match p with + | 0 => + simp[apply_braidMove] + by_cases h : List.take (M.M i j) l = braidWord M i j + · simp[h] + have h' : l = l.take (M.M i j) ++ l.drop (M.M i j) := by simp + nth_rewrite 2 [h'] + repeat rw[wordProd_append] + rw[h] + simp[wordProd_braidWord_eq] + · simp[h] + | p + 1 => + match l with + | [] => simp[apply_braidMove] + | h::t => + simp[apply_braidMove, wordProd_cons] + exact braidMove_wordProd (BraidMove.mk i j p) t + +theorem coxeterMove_wordProd (cm : cs.CoxeterMove) (l : List B) : π (cs.apply_coxeterMove cm l) = π l := by + cases cm with + | nil nm => exact cs.nilMove_wordProd nm l + | braid bm => exact cs.braidMove_wordProd bm l + +/-- Apply a list of Coxeter moves to a word from right to left. -/ +def apply_coxeterMove_sequence (cms : List (cs.CoxeterMove)) (l : List B) : List B := + List.foldr (cs.apply_coxeterMove) l cms + +example (nm : cs.NilMove) : cs.CoxeterMove := CoxeterMove.nil nm + +/-- Apply a sequence of braid moves to a word. -/ +def apply_braidMoveSequence (bms : List (cs.BraidMove)) (l : List B) : List B := + match bms with + | [] => l + | bm :: bms' => cs.apply_braidMove bm (apply_braidMoveSequence bms' l) + +lemma apply_braidMoveSequence_cons (bm : cs.BraidMove) (bms : List (cs.BraidMove)) (l : List B) : + cs.apply_braidMoveSequence (bm :: bms) l = cs.apply_braidMove bm (cs.apply_braidMoveSequence bms l) := by + simp[apply_braidMoveSequence] + +lemma cons_of_length_succ {α : Type} (l : List α) {p : ℕ} (h : l.length = p + 1) : + ∃ (a : α) (t : List α), l = a :: t ∧ t.length = p := by + cases l with + | nil => + simp at h + | cons a t => + simp at h + use a, t +/-- Shift a braid move one position to the right. -/ +def shift_braidMove (bm : cs.BraidMove) : cs.BraidMove := + match bm with + | BraidMove.mk i j p => BraidMove.mk i j (p + 1) + +lemma braidMove_cons (bm : cs.BraidMove) (l : List B) (a : B) : + a :: cs.apply_braidMove bm l = cs.apply_braidMove (cs.shift_braidMove bm) (a :: l) := by + rcases bm with ⟨i, j, p⟩ + simp[shift_braidMove, apply_braidMove] + +lemma braidMoveSequence_cons (bms : List (cs.BraidMove)) (l : List B) (a : B) : + a :: cs.apply_braidMoveSequence bms l = cs.apply_braidMoveSequence (List.map cs.shift_braidMove bms) (a :: l) := by + induction bms with + | nil => + simp[apply_braidMoveSequence] + | cons bm bms ih => + rw[apply_braidMoveSequence] + rw[cs.braidMove_cons bm] + simp[apply_braidMoveSequence] at ih + rw[ih] + simp[apply_braidMoveSequence_cons] + +theorem isReduced_cons (a : B) (l : List B) : cs.IsReduced (a :: l) → cs.IsReduced l := by + intro h + have h' : l = (a::l).drop 1 := by simp + rw[h'] + exact h.drop 1 + +lemma leftDescent_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftDescent (π (i :: l)) i := by + apply cs.isLeftDescent_iff.mpr + rw[hr] + simp[wordProd_cons] + rw[← IsReduced] + apply cs.isReduced_cons i l hr + +lemma leftInversion_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftInversion (π (i :: l)) (s i) := + (cs.isLeftInversion_simple_iff_isLeftDescent (π (i :: l)) i).mpr (cs.leftDescent_of_cons i l hr) + +theorem alternatingWord_succ_ne_alternatingWord_eraseIdx [MatsumotoCondition cs] + (i j : B) (p : ℕ) (hp : p < M i j) (hij : i ≠ j) : + ∀ (k : ℕ) (hk : k < p) ,π (alternatingWord i j (p + 1)) ≠ π (alternatingWord i j p).eraseIdx k := by + revert i j + + induction p with + | zero => + intro i j + simp[alternatingWord, cs.wordProd_cons] + | succ p ih => + intro i j hp hij k hk + have hp' : p < M i j := by linarith + have hp'' : p < M j i := by simp[M.symmetric]; exact hp' + have zero_lt_p_succ : 0 < p + 1 := by linarith + + rw[alternatingWord_succ] + nth_rewrite 2 [alternatingWord_succ] + simp + + by_cases h_erase : k < (alternatingWord j i p).length + · rw[List.eraseIdx_append_of_lt_length h_erase [j]] + intro h_contra + simp[cs.wordProd_append] at h_contra + + have hij' : j ≠ i := by + intro h + apply hij + rw[h] + have h_erase' : k < p := by simp at h_erase; exact h_erase + + apply ih j i hp'' hij' k h_erase' h_contra + + · have h_erase' : (alternatingWord j i p).length ≤ k := by + apply Nat.le_of_not_lt + exact h_erase + + rw[List.eraseIdx_append_of_length_le h_erase' [j]] + have h_erase_k : [j].eraseIdx (k - (alternatingWord j i p).length) = [] := by + have h_index : k - (alternatingWord j i p).length = 0 := by + have hk_le : k ≤ p := by omega + simpa [length_alternatingWord] using Nat.sub_eq_zero_of_le hk_le + rw [h_index] + rfl + + rw[h_erase_k] + simp + intro h_contra + + have : cs.wordProd (alternatingWord j i (p + 1) ++ [j]) = cs.wordProd (alternatingWord i j (p + 2)) := by + simp[alternatingWord_succ] + + rw[this] at h_contra + simp[prod_alternatingWord_eq_mul_pow] at h_contra + by_cases p_even : Even p + · have p_even' : Even (p + 2) := by + apply Nat.even_add.mpr + simp + exact p_even + simp[p_even, p_even'] at h_contra + apply mul_inv_eq_one.mpr at h_contra + rw[← inv_pow (s j * s i) (p/2)] at h_contra + simp at h_contra + rw[← pow_add] at h_contra + have : p / 2 + 1 + p / 2 = p + 1 := by + have : 2 * (p / 2) = p := Nat.two_mul_div_two_of_even p_even + ring + simp[mul_comm, this] + rw[this] at h_contra + + apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra + linarith + + · have p_odd : ¬ Even (p + 2) := by + intro h + apply Nat.even_add.mp at h + simp[h] at p_even + + simp[p_even, p_odd] at h_contra + apply (@mul_left_cancel_iff _ _ _ (s j) _ _).mpr at h_contra + + simp at h_contra + rw[← mul_assoc] at h_contra + let p_succ := p / 2 + 1 + have p_succ_ne_zero : p_succ ≠ 0 := by + apply Nat.succ_ne_zero + have : (p / 2) = p_succ - 1 := by + simp[p_succ] + rw[this] at h_contra + rw[mul_pow_sub_one p_succ_ne_zero (s j * s i)] at h_contra + + simp[p_succ] at h_contra + apply mul_inv_eq_one.mpr at h_contra + rw[← inv_pow (s j * s i) (p/2 + 1)] at h_contra + simp at h_contra + rw[← pow_add] at h_contra + + have : p / 2 + 1 + (p / 2 + 1) = p + 1 := by + ring + convert_to 1 + 1 + p / 2 * 2 = p + 1 + rw[add_comm] + simp at p_even + rw[add_assoc] + rw[Nat.one_add_div_two_mul_two_of_odd p_even] + ring + rw[this] at h_contra + + apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra + linarith + +lemma prefix_braidWord_aux [MatsumotoCondition cs] +(w : W) (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (hil : π (i :: l) = w) (hjl' : π (j :: l') = w) + (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : + ∀ (p : ℕ) (_ : p ≤ M i j), ∃ t : List B, π (alternatingWord i j p ++ t) = w ∧ cs.IsReduced (alternatingWord i j p ++ t) := by + intro p + induction p with + | zero => + intro _ + simp[alternatingWord] + use i :: l + | succ p ih => + intro hp + have hp' : p ≤ M i j := by linarith + have hp'' : p < M i j := by linarith + rcases ih hp' with ⟨t, ht, htr⟩ + rw[← ht] + + rw[alternatingWord_succ'] + by_cases p_even : Even p + · simp[p_even] + simp[cs.wordProd_cons] + + suffices ∃ k : Fin t.length, s j * cs.wordProd (alternatingWord i j p ++ t) = + cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by + rcases this with ⟨k, hk⟩ + use (t.eraseIdx k) + + have hw : + cs.simple j * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) = + cs.wordProd (alternatingWord i j p ++ t) + := by + rw[← hk] + simp[cs.wordProd_cons] + + constructor + · exact hw + · simp[IsReduced] + simp[IsReduced] at htr + rw[cs.wordProd_cons] + rw[hw] + rw[htr] + rw[List.length_eraseIdx_of_lt k.2] + simp[add_assoc] + + have : 1 ≤ t.length := by + apply Nat.le_of_not_lt + intro h' + rw[Nat.lt_one_iff] at h' + rw[h'] at k + have wah := k.2 + linarith + + rw[Nat.sub_add_cancel this] + + + have h_left_inversion_j : cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s j) := by + rw[ht, ← hjl'] + apply cs.leftInversion_of_cons j l' hr' + + rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) ⟨s j, cs.isReflection_simple j ⟩ h_left_inversion_j with ⟨k, hk⟩ + + by_cases k_lt_len : k < p + · exfalso + have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len] + rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk + + simp[cs.wordProd_append] at hk + rw[← mul_assoc] at hk + rw[mul_right_cancel_iff] at hk + rw[← wordProd_cons] at hk + have : j :: alternatingWord i j p = alternatingWord i j (p + 1) := by simp[alternatingWord_succ', p_even] + rw[this] at hk + exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k k_lt_len hk + + · simp at k_lt_len + rw[List.eraseIdx_append_of_length_le] at hk + rw[hk] + have : k - (alternatingWord i j p).length < t.length := by + have kle := k.2 + simp at kle + simp + omega + + use ⟨k - (alternatingWord i j p).length, this⟩ + simp[k_lt_len] + + · simp[p_even] + simp[cs.wordProd_cons] + + suffices ∃ k : Fin t.length, s i * cs.wordProd (alternatingWord i j p ++ t) = + cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by + rcases this with ⟨k, hk⟩ + use (t.eraseIdx k) + have hw : cs.simple i * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) = cs.wordProd (alternatingWord i j p ++ t) := by + rw[← hk] + simp[cs.wordProd_cons] + constructor + · exact hw + · simp[IsReduced] + simp[IsReduced] at htr + rw[cs.wordProd_cons] + rw[hw] + rw[htr] + rw[List.length_eraseIdx_of_lt k.2] + simp[add_assoc] + + have : 1 ≤ t.length := by + apply Nat.le_of_not_lt + intro h' + rw[Nat.lt_one_iff] at h' + rw[h'] at k + have wah := k.2 + linarith + + rw[Nat.sub_add_cancel this] + + have h_left_inversion_i : cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s i) := by + rw[ht, ← hil] + apply cs.leftInversion_of_cons i l hr + + rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) ⟨s i, cs.isReflection_simple i ⟩ h_left_inversion_i with ⟨k, hk⟩ + + by_cases k_lt_len : k < p + · exfalso + have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len] + rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk + + simp[cs.wordProd_append] at hk + rw[← mul_assoc] at hk + rw[mul_right_cancel_iff] at hk + rw[← wordProd_cons] at hk + have : i :: alternatingWord i j p = alternatingWord i j (p + 1) := by simp[alternatingWord_succ', p_even] + rw[this] at hk + exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k k_lt_len hk + · simp at k_lt_len + rw[List.eraseIdx_append_of_length_le] at hk + rw[hk] + have : k - (alternatingWord i j p).length < t.length := by + have kle := k.2 + simp at kle + simp + omega + + use ⟨k - (alternatingWord i j p).length, this⟩ + simp[k_lt_len] + + +lemma prefix_braidWord [MatsumotoCondition cs] (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (pi_eq : π (i :: l) = π (j :: l')) +(hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : + ∃ t : List B, π (i :: l) = π (braidWord M i j ++ t) ∧ cs.IsReduced (braidWord M i j ++ t) := by + have h : M i j ≤ M i j := by linarith + have h' : π (j :: l') = π (i :: l) := Eq.symm pi_eq + + rcases cs.prefix_braidWord_aux (π (i :: l)) l l' i j i_ne_j rfl h' hr hr' (M i j) h with ⟨t, ht, htr⟩ + use t + rw[braidWord] + constructor + · simp[ht] + · exact htr + +theorem apply_braidMove_sequence_append (bms bms' : List (cs.BraidMove)) (l : List B) : + cs.apply_braidMoveSequence (bms ++ bms') l = cs.apply_braidMoveSequence bms (cs.apply_braidMoveSequence bms' l) := by + induction bms with + | nil => + simp[apply_braidMoveSequence] + | cons bm bms ih => + simp[apply_braidMoveSequence] + apply congr_arg + exact ih + +theorem concatenate_braidMove_sequences (l l' l'' : List B) (h : ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l') + (h' : ∃ bms' : List (cs.BraidMove), cs.apply_braidMoveSequence bms' l' = l'') : + ∃ bms'' : List (cs.BraidMove), cs.apply_braidMoveSequence bms'' l = l'' := by + rcases h with ⟨bms, hbms⟩ + rcases h' with ⟨bms', hbms'⟩ + use bms' ++ bms + simp[apply_braidMove_sequence_append] + simp[hbms', hbms] + +-- move to aux file +theorem isReduced_of_eq_length (l l' : List B) (h_len : l.length = l'.length) (h_eq : π l = π l') + (hr : cs.IsReduced l) : cs.IsReduced l' := by + simp[IsReduced] + simp[IsReduced] at hr + + calc + len π l' = len π l := by rw[h_eq] + _ = l.length := by rw[hr] + _ = l'.length := by rw[h_len] + +theorem eq_length_of_isReduced (l l' : List B) +(h_eq : π l = π l') (hr : cs.IsReduced l) (hr' : cs.IsReduced l') : + l.length = l'.length := by + rw[IsReduced] at hr + rw[IsReduced] at hr' + + calc l.length = len π l := by rw[hr] + _ = len π l' := by rw[h_eq] + _ = l'.length := by rw[hr'] + +lemma matsumoto_reduced_inductionStep_of_firstLetterEq (p : ℕ) (l_t l'_t : List B) (i : B) +(len_l_t_eq_p : l_t.length = p) (len_l'_t_eq_p : l'_t.length = p) (h_eq : π (i :: l_t) = π (i :: l'_t)) +(l_reduced : cs.IsReduced (i :: l_t)) (l'_reduced : cs.IsReduced (i :: l'_t)) +(ih: ∀ (l l' : List B), + l.length = p → + l'.length = p → + cs.IsReduced l → cs.IsReduced l' → cs.wordProd l = cs.wordProd l' → ∃ bms, cs.apply_braidMoveSequence bms l = l'): +∃ bms, cs.apply_braidMoveSequence bms (i :: l_t) = i :: l'_t := by + + have htr : cs.IsReduced l_t := cs.isReduced_cons i l_t l_reduced + have htr' : cs.IsReduced l'_t := cs.isReduced_cons i l'_t l'_reduced + + have h_prod : π l_t = π l'_t := by + apply @mul_left_cancel _ _ _ (cs.simple i) _ _ + rw[← cs.wordProd_cons i l_t, ← cs.wordProd_cons i l'_t, h_eq] + + + have ⟨bms, ih'⟩ := ih l_t l'_t len_l_t_eq_p len_l'_t_eq_p htr htr' h_prod + + apply (List.cons_inj_right i).mpr at ih' + rw[← ih'] + rw[braidMoveSequence_cons] + use (List.map cs.shift_braidMove bms) + +theorem matsumoto_reduced_aux [MatsumotoCondition cs] (p : ℕ) (l l' : List B) +(len_l_eq_p : l.length = p) (len_l'_eq_p : l'.length = p) +(l_reduced : cs.IsReduced l) (l'_reduced : cs.IsReduced l') (h_eq : π l = π l') : + ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l' := by + + revert l l' + induction p with + | zero => + intro l l' hl hl' _ _ _ + have h_len : l.length = l'.length := by rw[hl, hl'] + simp at h_len + use [] + simp[apply_braidMoveSequence] + rw[List.length_eq_zero_iff] at hl + rw[List.length_eq_zero_iff] at hl' + rw[hl, hl'] + | succ p ih => + intro l l' len_l_eq_p len_l'_eq_p l_reduced l'_reduced h_eq + rcases cons_of_length_succ l len_l_eq_p with ⟨i, l_t, rfl, len_l_t_eq_p⟩ + rcases cons_of_length_succ l' len_l'_eq_p with ⟨j, l'_t, rfl, len_l'_t_eq_p⟩ + + by_cases first_letter_eq : i = j + · rw[first_letter_eq] + rw[first_letter_eq] at h_eq + rw[first_letter_eq] at l_reduced + + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t l'_t j len_l_t_eq_p len_l'_t_eq_p h_eq l_reduced l'_reduced + exact ih + + · obtain ⟨m, hm⟩ : ∃ m : ℕ ,M i j = m + 1 := by + use M i j - 1 + simp[MatsumotoCondition.one_le_M cs i j] + + have hm' : M j i = m + 1 := by + simp[M.symmetric] + exact hm + + by_cases m_even : Even m + · have j_ne_i : j ≠ i := by + simp[first_letter_eq] + intro heq + rw[heq] at first_letter_eq + contradiction + + obtain ⟨b_tail, hb, b_reduced⟩ := + cs.prefix_braidWord l'_t l_t j i j_ne_i (Eq.symm h_eq) l'_reduced l_reduced + + have hb' : cs.wordProd (i :: l_t) = cs.wordProd (braidWord M j i ++ b_tail) := by + rw[← hb] + exact h_eq + + apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M j i ++ b_tail) (j :: l'_t) + + have b_word_cons : (braidWord M j i ++ b_tail) = i :: (alternatingWord j i m ++ b_tail) := by + simp[braidWord] + rw[hm'] + simp[alternatingWord_succ'] + simp[m_even] + + rw[b_word_cons] + + have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by + suffices (braidWord M j i ++ b_tail).length = p + 1 from by + simp[braidWord] at this + rw[hm'] at this + simp[alternatingWord] + nth_rewrite 1 [add_comm] at this + rw[← add_assoc] at this + simp at this + rw[← this] + ring + rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M j i ++ b_tail) hb' l_reduced b_reduced] + exact len_l_eq_p + + rw[b_word_cons] at hb' + rw[b_word_cons] at b_reduced + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t (alternatingWord j i m ++ b_tail) i len_l_t_eq_p b_len_p hb' l_reduced b_reduced ih + + apply cs.concatenate_braidMove_sequences (braidWord M j i ++ b_tail) (braidWord M i j ++ b_tail) (j :: l'_t) + + use [BraidMove.mk j i 0] + simp[apply_braidMoveSequence] + simp[apply_braidMove] + + simp[braidWord] + rw[hm] + rw[alternatingWord_succ'] + simp[m_even] + + have switch_braidWord : π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by + simp[wordProd_append] + rw[cs.wordProd_braidWord_eq j i] + + rw[switch_braidWord] at hb' + have b_reduced' : cs.IsReduced (braidWord M i j ++ b_tail) := by + apply cs.isReduced_of_eq_length (braidWord M j i ++ b_tail) (braidWord M i j ++ b_tail) + simp[M.symmetric] + exact switch_braidWord + exact b_reduced + + have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M i j ++ b_tail) := by + rw[← hb'] + exact Eq.symm h_eq + + have b_word_cons : (braidWord M i j ++ b_tail) = j :: (alternatingWord i j m ++ b_tail) := by + simp[braidWord] + rw[hm] + simp[alternatingWord_succ'] + simp[m_even] + + have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by + suffices (braidWord M i j ++ b_tail).length = p + 1 from by + simp[braidWord] at this + rw[hm] at this + simp[alternatingWord] + nth_rewrite 1 [add_comm] at this + rw[← add_assoc] at this + simp at this + rw[← this] + ring + rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M i j ++ b_tail) hb' l'_reduced b_reduced'] + exact len_l'_eq_p + + rw[b_word_cons] at hb' + rw[b_word_cons] at b_reduced' + + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p (alternatingWord i j m ++ b_tail) + l'_t j b_len_p len_l'_t_eq_p (Eq.symm hb') b_reduced' l'_reduced ih + + · rcases cs.prefix_braidWord l_t l'_t i j first_letter_eq h_eq l_reduced l'_reduced with ⟨b_tail, hb, b_reduced⟩ + apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M i j ++ b_tail) (j :: l'_t) + + simp[braidWord] + rw[hm] + rw[alternatingWord_succ'] + simp[m_even] + + have b_word_cons : (braidWord M i j ++ b_tail) = i :: (alternatingWord i j m ++ b_tail) := by + simp[braidWord] + rw[hm] + simp[alternatingWord_succ'] + simp[m_even] + + have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by + suffices (braidWord M i j ++ b_tail).length = p + 1 from by + simp[braidWord] at this + rw[hm] at this + simp[alternatingWord] + nth_rewrite 1 [add_comm] at this + rw[← add_assoc] at this + simp at this + rw[← this] + ring + rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M i j ++ b_tail) hb l_reduced b_reduced] + exact len_l_eq_p + + have i_tail_reduced : cs.IsReduced l_t := by + apply cs.isReduced_cons i l_t l_reduced + + have aword_is_reduced : cs.IsReduced (alternatingWord i j m ++ b_tail) := by + apply cs.isReduced_cons i ((alternatingWord i j m) ++ b_tail) + rw[← b_word_cons] + exact b_reduced + + have i_tail_eq_aword : π l_t = π (alternatingWord i j m ++ b_tail) := by + rw[b_word_cons] at hb + simp[wordProd_cons] at hb + exact hb + + rcases ih l_t (alternatingWord i j m ++ b_tail) len_l_t_eq_p b_len_p i_tail_reduced aword_is_reduced i_tail_eq_aword with ⟨bms, ih'⟩ + + use (List.map cs.shift_braidMove bms) + + rw[← braidMoveSequence_cons] + suffices cs.apply_braidMoveSequence bms l_t = (alternatingWord i j m ++ b_tail) from by + rw[this] + exact ih' + + apply cs.concatenate_braidMove_sequences (braidWord M i j ++ b_tail) (braidWord M j i ++ b_tail) (j :: l'_t) + + use [BraidMove.mk i j 0] + simp[apply_braidMoveSequence] + simp[apply_braidMove] + + simp[braidWord] + rw[hm'] + rw[alternatingWord_succ'] + simp[m_even] + + have b_word_cons : (braidWord M j i ++ b_tail) = j :: (alternatingWord j i m ++ b_tail) := by + simp[braidWord] + rw[hm'] + simp[alternatingWord_succ'] + simp[m_even] + + have switch_braidWord : π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by + simp[wordProd_append] + rw[cs.wordProd_braidWord_eq j i] + + have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M j i ++ b_tail) := by + rw[switch_braidWord] + rw[← hb] + exact Eq.symm h_eq + + have b_reduced' : cs.IsReduced (braidWord M j i ++ b_tail) := by + apply cs.isReduced_of_eq_length (braidWord M i j ++ b_tail) (braidWord M j i ++ b_tail) + simp[M.symmetric] + exact Eq.symm switch_braidWord + exact b_reduced + + have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by + suffices (braidWord M j i ++ b_tail).length = p + 1 from by + simp[braidWord] at this + rw[hm'] at this + simp[alternatingWord] + nth_rewrite 1 [add_comm] at this + rw[← add_assoc] at this + simp at this + rw[← this] + ring + rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M j i ++ b_tail) hb' l'_reduced b_reduced'] + exact len_l'_eq_p + + have j_tail_reduced : cs.IsReduced l'_t := by + apply cs.isReduced_cons j l'_t l'_reduced + + have aword_is_reduced : cs.IsReduced (alternatingWord j i m ++ b_tail) := by + apply cs.isReduced_cons j ((alternatingWord j i m) ++ b_tail) + rw[← b_word_cons] + exact b_reduced' + + have j_tail_eq_aword : π (alternatingWord j i m ++ b_tail) = π l'_t := by + rw[b_word_cons] at hb' + simp[wordProd_cons] at hb' + exact Eq.symm hb' + + rcases ih (alternatingWord j i m ++ b_tail) l'_t b_len_p len_l'_t_eq_p aword_is_reduced j_tail_reduced j_tail_eq_aword with ⟨bms, ih'⟩ + + use (List.map cs.shift_braidMove bms) + rw[← braidMoveSequence_cons] + suffices cs.apply_braidMoveSequence bms (alternatingWord j i m ++ b_tail) = l'_t from by + rw[this] + exact ih' + + +theorem matsumoto_reduced [MatsumotoCondition cs] (l l' : List B) +(hr : cs.IsReduced l) (hr' : cs.IsReduced l') (h : π l = π l') : + ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l' := by + apply cs.matsumoto_reduced_aux (l.length) l l' rfl _ hr hr' h + calc + l'.length = len (π l') := by + rw[IsReduced] at hr' + rw[← hr'] + _ = len (π l) := by rw[h] + _ = l.length := by + rw[IsReduced] at hr + rw[← hr] + +end + +end CoxeterSystem diff --git a/LeanPool/DemazureOperatorsLean/StrongExchange.lean b/LeanPool/DemazureOperatorsLean/StrongExchange.lean new file mode 100644 index 0000000000..93f1797e94 --- /dev/null +++ b/LeanPool/DemazureOperatorsLean/StrongExchange.lean @@ -0,0 +1,505 @@ +/- +Copyright (c) 2026 Óscar Álvarez Sánchez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Óscar Álvarez Sánchez +-/ + +import Mathlib.GroupTheory.Coxeter.Inversion +import Mathlib.Algebra.Group.NatPowAssoc +import Init.Data.List.Lemmas + +namespace CoxeterSystem +noncomputable section + +variable {B : Type} +variable {W : Type} [Group W] +variable {M : CoxeterMatrix B} (cs : CoxeterSystem M W) + +local prefix:100 "s" => cs.simple +local prefix:100 "π" => cs.wordProd +local prefix:100 "len" => cs.length + +instance : DecidableEq W := Classical.typeDecidableEq W + +/-- The subtype of reflections in a Coxeter system. -/ +def Reflection : Type := {t : W // IsReflection cs t} + +/-- The number of times a reflection appears in the left inversion sequence of a word. -/ +def reflection_mem_leftInvSeq_count (l : List B) (t : cs.Reflection) : ℕ := + (cs.leftInvSeq l).count t.1 + +/-- The parity of the number of occurrences of a reflection in a left inversion sequence. -/ +def reflection_mem_leftInvSeq_parity (l : List B) (t : cs.Reflection) : ZMod 2 := + (reflection_mem_leftInvSeq_count cs l t : ZMod 2) + +/-- Conjugate a reflection and keep its reflection witness. -/ +def conj_of_reflection (t : cs.Reflection) (w : W) : cs.Reflection := + ⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩ + +/-- The parity contribution of a simple reflection to the permutation action. -/ +def eta (i : B) (t : cs.Reflection) : ZMod 2 := + if (s i = t.1) then 1 else 0 + +lemma eta_eq_eta_of_simpleConj (i : B) (t : cs.Reflection) : + cs.eta i t = cs.eta i (cs.conj_of_reflection t (s i)) := by + simp [eta] + rcases t with ⟨t, ht⟩ + have : s i = t ↔ s i * t = 1 := by + constructor + · intro h' + rw [h'] + exact IsReflection.mul_self ht + · intro h' + apply (mul_left_inj t).mp + simp [IsReflection.mul_self ht] + exact h' + + by_cases h : s i = t + · simp [this, h, conj_of_reflection] + · simp [this, h, if_neg, conj_of_reflection] + +/-- The permutation action associated to a simple reflection. -/ +def permutationMap (i : B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 := + fun (t , z) => (cs.conj_of_reflection t (s i), z + cs.eta i t) + +theorem permutationMap_orderTwo (i : B) : cs.permutationMap i ∘ cs.permutationMap i = id := by + funext ⟨t, z⟩ + simp [permutationMap] + constructor + · simp[conj_of_reflection, mul_assoc] + · rw [← cs.eta_eq_eta_of_simpleConj i t] + ring_nf + rw [show (2 : ZMod 2) = 0 by decide] + simp + +lemma leftInvSeq_repeats : ∀ (k : ℕ) (h : k < M i j), +(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by simp[h]; linarith) = +(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by simp[h]; linarith) := by + intro k h' + rw[getElem_leftInvSeq_alternatingWord cs i j (M i j) k] + rw[getElem_leftInvSeq_alternatingWord cs i j (M i j) ((M i j)+k)] + rw[cs.prod_alternatingWord_eq_mul_pow] + rw[cs.prod_alternatingWord_eq_mul_pow] + + have h_odd : Odd (2 * k + 1) := by + simp + + have h_odd' : Odd (2 * ((M i j) + k) + 1) := by + simp + + simp[h_odd, h_odd'] + + have two_gt_0 : 2 > 0 := by linarith + have h_exp : (2 * k + 1) / 2 = k := by + rw[add_comm] + rw[Nat.add_mul_div_left 1 k two_gt_0] + simp + have h_exp' : (2 * ((M i j) + k) + 1) / 2 = (M i j) + k := by + rw[add_comm] + rw[Nat.add_mul_div_left 1 ((M i j)+k) two_gt_0] + simp + rw[h_exp, h_exp'] + rw[NatPowAssoc.npow_add] + simp + linarith + linarith + +lemma leftInvSeq_repeats' : ∀ (k : ℕ) (h : k < M i j), +(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by simp[h]; linarith) = +(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by simp[h]; linarith) := by + intro k h' + exact leftInvSeq_repeats cs k h' + +lemma nReflectionOccurrences_even_braidWord (t : cs.Reflection) : + Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) := by + + suffices (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) = 2 * List.count (t.1) (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (M.M i j * 2)))) from by + simp[this] + + simp[reflection_mem_leftInvSeq_count] + suffices (cs.leftInvSeq (alternatingWord i j (2 * M i j))) = (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j)))) ++ (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j)))) from by + rw[this] + simp + ring + + have m_le_two_m : M i j ≤ 2 * M i j := by linarith + have length_eq : (cs.leftInvSeq (alternatingWord i j (2 * (M i j)))).length = + (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++ (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))))).length := by + simp[m_le_two_m] + ring + + apply List.ext_getElem length_eq + intro k hk hk' + + by_cases h : k < M i j + · have : k < (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length := by + simp[h, m_le_two_m] + + rw[List.getElem_append_left this] + rw[List.getElem_take'] + exact h + · have h_k_le : k - M i j < M i j := by + simp at hk + apply Nat.sub_lt_left_of_lt_add + simp at h + exact h + linarith + have : (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length ≤ k := by + simp[h, m_le_two_m] + linarith + + rw[List.getElem_append_right this] + rw[List.getElem_take] + simp[m_le_two_m] + + rw[← leftInvSeq_repeats' cs (k - M i j) h_k_le] + + suffices M.M i j + (k - M.M i j) = k from by + simp[this] + + rw[← Nat.add_sub_assoc] + simp + linarith + +lemma parityReflectionOccurrences_braidWord (t : cs.Reflection) : + reflection_mem_leftInvSeq_parity cs (alternatingWord i j (2 * M i j)) t = 0 := by + suffices Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) from by + simp[this, reflection_mem_leftInvSeq_parity] + apply ZMod.natCast_eq_zero_iff_even.mpr this + exact nReflectionOccurrences_even_braidWord cs t + +lemma alternatingWord_reverse : (alternatingWord i j (2 * p)).reverse = alternatingWord j i (2 * p) := by + induction p with + | zero => + simp[alternatingWord] + | succ p h => + simp [alternatingWord] + rw[h] + have h1 : j :: i :: alternatingWord j i (2 * p) = alternatingWord j i (2 * p + 1 + 1) := by + rw[alternatingWord_succ'] + rw[alternatingWord_succ'] + simp + simp[h1, alternatingWord] + +instance instMul : Mul (cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) where + mul := fun f g => f ∘ g + +lemma mulDef (f g : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) : f * g = f ∘ g := rfl + +instance : Monoid (cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) where + one := id + mul := (instMul cs).mul + one_mul := by + intro f + funext x + suffices (id ∘ f) x = f x from by + rw[← this] + rfl + simp + mul_one := by + intro f + funext x + suffices (f ∘ id) x = f x from by + rw[← this] + rfl + simp + mul_assoc := by + intro f g h + funext x + repeat rw[mulDef] + rfl + +/-- The permutation map associated to a word, built by composing simple permutation maps. -/ +def permutationMap_ofList (l : List B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 := + match l with + | [] => id + | a :: t => cs.permutationMap a * permutationMap_ofList t + +lemma isReflection_conj_inv_mul_mul (ht : cs.IsReflection t) (w : W) : + cs.IsReflection (w⁻¹ * t * w) := by + have : w = w⁻¹⁻¹ := by simp + nth_rewrite 2 [this] + apply IsReflection.conj ht w⁻¹ + +lemma permutationMap_ofList_mk_1 (l : List B) : + (permutationMap_ofList cs l ⟨t,z⟩).1 = cs.conj_of_reflection t (π l) := by + simp[conj_of_reflection] + induction l with + | nil => + simp[permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_count] + | cons a l h => + calc (permutationMap_ofList cs (a :: l) (t, z)).1 = ((cs.permutationMap a * permutationMap_ofList cs l) (t, z)).1 := by simp[permutationMap_ofList] + _ = (cs.permutationMap a (permutationMap_ofList cs l (t, z))).1 := by rfl + + simp[permutationMap, conj_of_reflection, h] + simp[cs.wordProd_cons, mul_assoc] + +lemma permutationMap_ofList_mk_2 (l : List B) : + (permutationMap_ofList cs l ⟨t,z⟩).2 = z + reflection_mem_leftInvSeq_parity cs l.reverse t := by + induction l with + | nil => + simp[permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count] + | cons i l h => + rw[permutationMap_ofList, mulDef] + simp[permutationMap, h] + simp[reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count] + rw[← List.concat_eq_append] + rw[leftInvSeq_concat] + simp [List.count_singleton] + + suffices cs.eta i (permutationMap_ofList cs l (t, z)).1 = if (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 then 1 else 0 from by + rw[this] + simp[add_assoc] + + simp[eta, permutationMap_ofList_mk_1, conj_of_reflection] + by_cases h' : (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 + · simp[h'] + rw[← h'] + simp[mul_assoc] + · simp[h'] + by_contra h'' + rw[h''] at h' + simp[mul_assoc] at h' + +lemma permutationMap_ofList_mk (l : List B) (t : cs.Reflection) (z : ZMod 2) : + (permutationMap_ofList cs l ⟨t,z⟩) = ⟨cs.conj_of_reflection t (π l), + z + reflection_mem_leftInvSeq_parity cs l.reverse t⟩ := by + rw[← permutationMap_ofList_mk_1, ← permutationMap_ofList_mk_2] + +theorem permutationMap_isLiftable : M.IsLiftable (cs.permutationMap) := by + intro i j + + have h (p : ℕ) : (cs.permutationMap i * cs.permutationMap j) ^ p = permutationMap_ofList cs (alternatingWord i j (2 * p)) := by + induction p with + | zero => + simp[permutationMap_ofList, permutationMap, permutationMap_orderTwo] + rfl + | succ p h => + simp[pow_succ'] + rw[h] + have : 2 * (p + 1) = 2 * p + 1 + 1 := by ring + rw[this] + rw[alternatingWord_succ'] + rw [if_neg (Nat.not_even_bit1 p)] + rw[permutationMap_ofList] + + rw[alternatingWord_succ'] + rw [if_pos (even_two_mul p)] + rw[permutationMap_ofList] + simp[mul_assoc] + + rw[h (M i j)] + funext ⟨t, z⟩ + convert_to permutationMap_ofList cs (alternatingWord i j (2 * M.M i j)) (t, z) = ⟨t,z⟩ + + simp[permutationMap_ofList_mk, conj_of_reflection] + constructor + · simp[cs.prod_alternatingWord_eq_mul_pow] + · rw[alternatingWord_reverse] + rw[M.symmetric] + exact parityReflectionOccurrences_braidWord cs t + +/-- The homomorphic lift of the simple permutation maps to the Coxeter group. -/ +def permutationMap_lift : W →* cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 := + cs.lift ⟨cs.permutationMap, permutationMap_isLiftable cs⟩ + +theorem permutationMap_lift_mk_ofList (l : List B) (t : cs.Reflection) (z : ZMod 2) : + permutationMap_lift cs (cs.wordProd l) ⟨t,z⟩ = permutationMap_ofList cs l ⟨t,z⟩ := by + induction l with + | nil => + simp[permutationMap_lift, cs.wordProd_nil, permutationMap_ofList] + rfl + | cons i l h => + rw[cs.wordProd_cons] + rw[permutationMap_ofList] + simp[mulDef] + rw[← h] + simp[permutationMap_lift] + +theorem permutationMap_ext (l l' : List B) (t : cs.Reflection) (z : ZMod 2) (h : π l = π l') : + permutationMap_ofList cs l ⟨t,z⟩ = permutationMap_ofList cs l' ⟨t,z⟩ := by + rw[← permutationMap_lift_mk_ofList] + rw[← permutationMap_lift_mk_ofList] + simp[h] + +/-- The parity of reflection occurrences defined using the lifted permutation action. -/ +def parityReflectionOccurrences_lift (w : W) (t : cs.Reflection) : ZMod 2 := + (permutationMap_lift cs w⁻¹ ⟨t,0⟩).2 + +theorem parityReflectionOccurrences_lift_mk (l : List B) (t : cs.Reflection) : + parityReflectionOccurrences_lift cs (cs.wordProd l) t = reflection_mem_leftInvSeq_parity cs l t := by + rw[parityReflectionOccurrences_lift] + rw[← wordProd_reverse] + rw[permutationMap_lift_mk_ofList cs l.reverse t 0] + rw[permutationMap_ofList_mk cs l.reverse t 0] + simp + +theorem permutationMap_lift_mk (w : W) (t : cs.Reflection) (z : ZMod 2) : + permutationMap_lift cs w ⟨t,z⟩ = ⟨⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩ , z + parityReflectionOccurrences_lift cs w⁻¹ t⟩ := by + obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w + apply Prod.ext + · simp[permutationMap_lift_mk_ofList, permutationMap_ofList_mk, conj_of_reflection] + · simp[parityReflectionOccurrences_lift] + rw[permutationMap_lift_mk_ofList cs l t 0] + rw[permutationMap_lift_mk_ofList cs l t z] + simp[permutationMap_ofList_mk] + + +theorem parityReflectionOccurrences_ext (l l' : List B) (t : cs.Reflection) (h : π l = π l') : + reflection_mem_leftInvSeq_parity cs l t = reflection_mem_leftInvSeq_parity cs l' t := by + + calc + reflection_mem_leftInvSeq_parity cs l t = parityReflectionOccurrences_lift cs (cs.wordProd l) t := by rw[parityReflectionOccurrences_lift_mk] + _ = parityReflectionOccurrences_lift cs (cs.wordProd l') t := by rw[h] + _ = reflection_mem_leftInvSeq_parity cs l' t := by rw[parityReflectionOccurrences_lift_mk] + +lemma odd_iff_parity_eq_one (n : ℕ) : Odd n ↔ (n : ZMod 2) = 1 := by + simpa [eq_comm] using (ZMod.natCast_eq_one_iff_odd (n := n)).symm + +lemma gt_one_of_odd (n : ℕ) : Odd n → n > 0 := by + intro h + simp[Odd] at h + rcases h with ⟨m, rfl⟩ + suffices m ≥ 0 from by linarith + exact Nat.zero_le m + +lemma isInLeftInvSeq_of_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) (h : reflection_mem_leftInvSeq_parity cs l t = 1) : + t.1 ∈ cs.leftInvSeq l := by + simp [reflection_mem_leftInvSeq_parity] at h + rw [← @odd_iff_parity_eq_one (reflection_mem_leftInvSeq_count cs l t)] at h + + apply gt_one_of_odd (reflection_mem_leftInvSeq_count cs l t) at h + simp[reflection_mem_leftInvSeq_count] at h + + exact h + +lemma isLeftInversion_of_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) : + reflection_mem_leftInvSeq_parity cs l t = 1 → cs.IsLeftInversion (cs.wordProd l) t.1 := by + intro h + + rcases cs.exists_isReduced (π l) with ⟨u, u_reduced, hu⟩ + rw[hu] + apply cs.isLeftInversion_of_mem_leftInvSeq u_reduced + + rw[cs.parityReflectionOccurrences_ext l u t hu] at h + exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs u t h + +lemma isLeftInversion_of_parityReflectionOccurrences_lift_eq_one (w : W) (t : cs.Reflection) : + parityReflectionOccurrences_lift cs w t = 1 → cs.IsLeftInversion w t.1 := by + intro h + obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w + simp[parityReflectionOccurrences_lift_mk] at h + apply isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t h + +lemma eraseIdx_of_mul_leftInvSeq (l : List B) (t : cs.Reflection) (h : t.1 ∈ cs.leftInvSeq l) : + ∃ (k : Fin l.length), t.1 * π l = π (l.eraseIdx k) := by + have : ∃ (k : Fin (cs.leftInvSeq l).length), (cs.leftInvSeq l).get k = t.1 := List.get_of_mem h + rcases this with ⟨k, hk⟩ + use ⟨k, by rw[← length_leftInvSeq cs l]; exact k.2⟩ + rw[← hk] + rw[← getD_leftInvSeq_mul_wordProd cs l k] + simp [List.getElem?_eq_getElem k.2] + +lemma permutationMap_lift_simple (p : B): + permutationMap_lift cs (cs.simple p) = cs.permutationMap p := by + simp[permutationMap_lift] + +lemma permutationMap_lift_of_reflection (t : cs.Reflection) : ∀ (z : ZMod 2), + permutationMap_lift cs t.1 (t, z) = ⟨t, z + 1⟩ := by + rcases t with ⟨t, t_refl⟩ + rcases t_refl with ⟨w, p, rfl⟩ + obtain ⟨l, _, rfl⟩ := cs.wordProd_surjective w + have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) + + induction l with + | nil => + simp[permutationMap_lift, permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_count, conj_of_reflection, eta] + | cons i l h => + intro z + simp_rw[wordProd_cons cs i l] + simp_rw[mul_inv_rev] + simp_rw[inv_simple] + simp[permutationMap_lift_simple, mulDef, ← mul_assoc] + simp[permutationMap_lift_simple, mulDef] at h + nth_rewrite 3 [permutationMap] + simp[conj_of_reflection, ← mul_assoc] + have : IsReflection cs (cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i) := by + nth_rewrite 3 [← inv_simple] + have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) + convert_to IsReflection cs (cs.simple i * (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) * (cs.simple i)⁻¹) + simp[inv_simple, mul_assoc] + exact IsReflection.conj this (s i) + rw[h (isReflection_simple cs p) (z + cs.eta i ⟨cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i, this⟩)] + simp[permutationMap, conj_of_reflection] + constructor + · simp[mul_assoc] + · simp[eta, add_assoc] + by_cases h': cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ = 1 + · simp[h'] + have : cs.simple i = cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ := by + apply (mul_right_inj (cs.simple i)).mpr at h' + simp only[mul_assoc, mul_one] at h' + rw[← h'] + simp[mul_assoc] + simp[this] + simp[ZMod] + · simp[h'] + by_contra h'' + rw[h''] at h' + simp[mul_assoc] at h' + +lemma isLeftInversion_iff_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) : + cs.IsLeftInversion (cs.wordProd l) t.1 ↔ reflection_mem_leftInvSeq_parity cs l t = 1 := by + constructor + · intro h + by_contra h' + have h'' : reflection_mem_leftInvSeq_parity cs l t = 0 := by + simp [reflection_mem_leftInvSeq_parity] + rw [ZMod.natCast_eq_zero_iff_even] + simp[reflection_mem_leftInvSeq_parity] at h' + rw[ZMod.natCast_eq_one_iff_odd] at h' + exact Nat.not_odd_iff_even.mp h' + + suffices cs.IsLeftInversion (t.1 * π l) t.1 from by + simp[IsLeftInversion] at this + rw[← mul_assoc] at this + rcases this with ⟨_, ht⟩ + rw[IsReflection.mul_self t.2] at ht + simp at ht + simp[IsLeftInversion] at h + linarith + + suffices permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = ⟨cs.conj_of_reflection t (π l)⁻¹, 1⟩ from by + apply isLeftInversion_of_parityReflectionOccurrences_lift_eq_one cs (t.1 * π l) t + rw[permutationMap_lift_mk cs (t.1 * π l)⁻¹ t 0] at this + simp at this + simp[this.2] + + calc + permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = permutationMap_lift cs (π l)⁻¹ (permutationMap_lift cs t.1 ⟨t, 0⟩) := by + simp[IsReflection.inv t.2] + rfl + _ = permutationMap_lift cs (π l)⁻¹ ⟨t, 1⟩ := by + rw[permutationMap_lift_of_reflection cs t 0] + simp[permutationMap_lift_mk] + _ = ⟨cs.conj_of_reflection t (π l)⁻¹, 1 + parityReflectionOccurrences_lift cs (π l) t⟩ := by + simp[permutationMap_lift_mk, conj_of_reflection] + _ = (cs.conj_of_reflection t (cs.wordProd l)⁻¹, 1) := by + simp + simp[parityReflectionOccurrences_lift_mk, h''] + + · exact isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t + + +theorem strongExchangeProperty (l : List B) (t : cs.Reflection) +(h' : cs.IsLeftInversion (cs.wordProd l) t.1) : + ∃ (k : Fin l.length), t.1 * π l = π (l.eraseIdx k) := by + + suffices t.1 ∈ cs.leftInvSeq l from eraseIdx_of_mul_leftInvSeq cs l t this + + rw [isLeftInversion_iff_parityReflectionOccurrences_eq_one cs l t] at h' + exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs l t h' + +end + +end CoxeterSystem diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 7ab586096f..7dfd0c9974 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,7 +1,7 @@ projects: - slug: demazureoperatorslean title: Demazure Operators and Lean - summary: Formalizes Demazure operators on multivariate polynomials and proves their basic braid, commutation, and scalar-action relations. + summary: Formalizes Demazure operators on multivariate polynomials, together with Coxeter-system strong exchange and Matsumoto reduced-word theorems. branch: algebraic combinatorics entry_module: LeanPool.DemazureOperatorsLean authors: @@ -18,6 +18,8 @@ projects: main_declarations: - Demazure.Dem - Demazure.demazure_commutes_adjacent + - CoxeterSystem.strongExchangeProperty + - CoxeterSystem.matsumoto_reduced main_results: - declaration: Demazure.Dem informal: Defines the Demazure operator as a linear map over the subalgebra of symmetric polynomials. @@ -29,6 +31,10 @@ projects: informal: Proves that non-adjacent Demazure operators commute. - declaration: Demazure.demazure_mul_symm informal: Proves that symmetric polynomials act as scalars with respect to Demazure operators. + - declaration: CoxeterSystem.strongExchangeProperty + informal: Proves the strong exchange property for Coxeter systems. + - declaration: CoxeterSystem.matsumoto_reduced + informal: Proves Matsumoto's theorem that reduced words for the same Coxeter group element are connected by braid moves. tags: - algebraic-combinatorics - demazure-operators From fe9520195f436d74f120bccc1090df2e789f0d1b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 02:32:19 +0900 Subject: [PATCH 5/8] Restore Demazure strong exchange and Matsumoto checks --- LeanPool/DemazureOperatorsLean.lean | 2 +- .../DemazureOperatorsLean/DemazureAux.lean | 28 +- LeanPool/DemazureOperatorsLean/Matsumoto.lean | 735 ++++++++---------- .../DemazureOperatorsLean/StrongExchange.lean | 334 ++++---- LeanPool/projects.yml | 2 - 5 files changed, 542 insertions(+), 559 deletions(-) diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index fe4d36de7c..03221cc40c 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -17,7 +17,7 @@ import LeanPool.DemazureOperatorsLean.Matsumoto Source: doi:10.1070/RM1973v028n03ABEH001549 Authors: Óscar Álvarez Sánchez Status: verified -Main declarations: `Demazure.Dem`, `Demazure.demazure_commutes_adjacent`, `CoxeterSystem.strongExchangeProperty`, `CoxeterSystem.matsumoto_reduced` +Main declarations: `CoxeterSystem.strongExchangeProperty`, `CoxeterSystem.matsumoto_reduced` Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory MSC: 05E05, 13P10, 20F55 -/ diff --git a/LeanPool/DemazureOperatorsLean/DemazureAux.lean b/LeanPool/DemazureOperatorsLean/DemazureAux.lean index 81c662a0f5..c721214afd 100644 --- a/LeanPool/DemazureOperatorsLean/DemazureAux.lean +++ b/LeanPool/DemazureOperatorsLean/DemazureAux.lean @@ -51,14 +51,14 @@ lemma r_equiv : Equivalence (r n) := by simp[h1, h2] · apply poly_cancel_left y.denominator_ne_zero apply poly_cancel_left h3 - ring + ring_nf rw[mul_assoc y.numerator] rw[mul_comm y.denominator x.numerator] rw[h1] rw[mul_comm y.numerator (y.numerator * x.denominator)] rw[mul_assoc] rw[h2] - ring + ring_nf instance s (n : ℕ) : Setoid (PolyFraction' n) where r := r n @@ -126,7 +126,7 @@ lemma add'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a add_mk a₁ b₁ = add_mk a₂ b₂ := by intro a1 b1 a2 b2 h1 h2 simp only [add_mk, add', mk_eq] - ring + ring_nf rw[← equiv_r] at h1 rw[← equiv_r] at h2 change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 @@ -140,7 +140,7 @@ lemma add'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a rw[mul_assoc a1.denominator] rw[mul_assoc a2.denominator] rw[h2] - ring + ring_nf /-- Addition on quotient polynomial fractions. -/ def add : PolyFraction n → PolyFraction n → PolyFraction n := @@ -159,7 +159,7 @@ lemma sub'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a (sub' a₁ b₁) = (sub' a₂ b₂) := by intro a1 b1 a2 b2 h1 h2 simp only [sub', mk_eq] - ring + ring_nf rw[← equiv_r] at h1 rw[← equiv_r] at h2 change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 @@ -173,7 +173,7 @@ lemma sub'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a rw[mul_assoc a1.denominator] rw[mul_assoc a2.denominator] rw[h2] - ring + ring_nf /-- Subtraction on quotient polynomial fractions. -/ def sub : PolyFraction n → PolyFraction n → PolyFraction n := @@ -192,7 +192,7 @@ lemma mul'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a (mul_mk a₁ b₁) = (mul_mk a₂ b₂) := by intro a1 b1 a2 b2 h1 h2 simp only [mul_mk, mul', mk_eq] - ring + ring_nf rw[← equiv_r] at h1 rw[← equiv_r] at h2 change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h1 @@ -203,7 +203,7 @@ lemma mul'_s {n : ℕ} : ∀ a₁ b₁ a₂ b₂ : PolyFraction' n, a₁ ≈ a rw[mul_comm b1.numerator] rw[mul_assoc (a2.numerator * a1.denominator)] rw[h2] - ring + ring_nf /-- Multiplication on quotient polynomial fractions. -/ def mul : PolyFraction n → PolyFraction n → PolyFraction n := @@ -243,11 +243,11 @@ def neg_mk (p : PolyFraction' n) : PolyFraction n := mk (neg' p) lemma neg_s (n : ℕ) : ∀ (a₁ a₂ : PolyFraction' n), a₁ ≈ a₂ → (neg_mk a₁) = (neg_mk a₂) := by intro a1 a2 h simp only [neg_mk, neg', mk_eq, neg_mul, mul_neg, neg_inj] - ring + ring_nf rw[← equiv_r] at h change a1.numerator * a2.denominator = a2.numerator * a1.denominator at h rw[h] - ring + ring_nf /-- Negation on quotient polynomial fractions. -/ def neg (p : PolyFraction n) : PolyFraction n := Quotient.lift neg_mk (neg_s n) p @@ -261,7 +261,7 @@ lemma add_comm (p q : PolyFraction n) : add p q = add q p := by rw[← hq] simp[lift2_r] simp[add_mk, add'] - ring + ring_nf lemma add_assoc (p q r : PolyFraction n) : add (add p q) r = add p (add q r) := by rcases get_polyfraction_rep p with ⟨p', hp⟩ @@ -280,7 +280,7 @@ lemma add_assoc (p q r : PolyFraction n) : add (add p q) r = add p (add q r) := apply Quotient.sound apply equiv_r.mp simp[Demazure.r, add'] - ring + ring_nf -- We don't prove that it is a ring since we don't need all the properties for our use @@ -316,11 +316,11 @@ lemma DemAux_well_defined (i : Fin n) : ∀ (p q : PolyFraction' n), (q.denominator * S q.denominator * delta) = (p.numerator * q.denominator) * (S p.denominator * S q.denominator * delta) - (S p.numerator * S q.denominator) * (p.denominator * q.denominator * delta) := by - ring + ring_nf _ = p.denominator * S p.denominator * delta * (q.numerator * S q.denominator - S q.numerator * q.denominator) := by rw [h, h_swap] - ring + ring_nf /-- The auxiliary Demazure operator on quotient polynomial fractions. -/ def DemAux (i : Fin n) (p : PolyFraction n) : PolyFraction n := diff --git a/LeanPool/DemazureOperatorsLean/Matsumoto.lean b/LeanPool/DemazureOperatorsLean/Matsumoto.lean index 6e5bcbe5a5..f8271831be 100644 --- a/LeanPool/DemazureOperatorsLean/Matsumoto.lean +++ b/LeanPool/DemazureOperatorsLean/Matsumoto.lean @@ -23,7 +23,9 @@ local prefix:100 "len" => cs.length /-- Extra nondegeneracy assumptions used in the Matsumoto theorem development. -/ class MatsumotoCondition where one_le_M : ∀ i j : B, 1 ≤ M i j - alternatingWords_ne_one : ∀ (i j : B) (_ : i ≠ j) (p : ℕ) (_ : 0 < p) (_ : p < M i j), (s i * s j) ^ p ≠ 1 + alternatingWords_ne_one : + ∀ (i j : B) (_ : i ≠ j) (p : ℕ) (_ : 0 < p) (_ : p < M i j), + (s i * s j) ^ p ≠ 1 /-- A nil move removes two adjacent equal simple reflections at a given offset. -/ structure NilMove (cs : CoxeterSystem M W) where @@ -85,46 +87,49 @@ theorem nilMove_wordProd (nm : cs.NilMove) (l : List B) : π (cs.apply_nilMove n rcases nm with ⟨i, p⟩ match p with | 0 => - simp[apply_nilMove] + rw[apply_nilMove] by_cases h : l.take 2 = [i, i] - · simp[h] + · rw [if_pos h] have h' : l = l.take 2 ++ l.drop 2 := by simp nth_rewrite 2 [h'] rw[wordProd_append] rw[h] - simp - convert_to cs.wordProd ([i] ++ [i]) = 1 - rw[wordProd_append] - simp - · simp[h] + have h_pair : cs.wordProd [i, i] = 1 := by + convert_to cs.wordProd ([i] ++ [i]) = 1 + rw[wordProd_append] + simp + rw [h_pair, one_mul] + · rw [if_neg h] | p + 1 => match l with | [] => simp[apply_nilMove] | h::t => - simp[apply_nilMove, wordProd_cons] - exact nilMove_wordProd (NilMove.mk i p) t + simp only [apply_nilMove, wordProd_cons] + rw[nilMove_wordProd (NilMove.mk i p) t] -theorem braidMove_wordProd (bm : cs.BraidMove) (l : List B) : π (cs.apply_braidMove bm l) = π l := by +theorem braidMove_wordProd (bm : cs.BraidMove) (l : List B) : + π (cs.apply_braidMove bm l) = π l := by rcases bm with ⟨i, j, p⟩ match p with | 0 => - simp[apply_braidMove] + rw[apply_braidMove] by_cases h : List.take (M.M i j) l = braidWord M i j - · simp[h] + · rw [if_pos h] have h' : l = l.take (M.M i j) ++ l.drop (M.M i j) := by simp nth_rewrite 2 [h'] repeat rw[wordProd_append] rw[h] simp[wordProd_braidWord_eq] - · simp[h] + · rw [if_neg h] | p + 1 => match l with | [] => simp[apply_braidMove] | h::t => - simp[apply_braidMove, wordProd_cons] - exact braidMove_wordProd (BraidMove.mk i j p) t + simp only [apply_braidMove, wordProd_cons] + rw[braidMove_wordProd (BraidMove.mk i j p) t] -theorem coxeterMove_wordProd (cm : cs.CoxeterMove) (l : List B) : π (cs.apply_coxeterMove cm l) = π l := by +theorem coxeterMove_wordProd (cm : cs.CoxeterMove) (l : List B) : + π (cs.apply_coxeterMove cm l) = π l := by cases cm with | nil nm => exact cs.nilMove_wordProd nm l | braid bm => exact cs.braidMove_wordProd bm l @@ -141,8 +146,10 @@ def apply_braidMoveSequence (bms : List (cs.BraidMove)) (l : List B) : List B := | [] => l | bm :: bms' => cs.apply_braidMove bm (apply_braidMoveSequence bms' l) -lemma apply_braidMoveSequence_cons (bm : cs.BraidMove) (bms : List (cs.BraidMove)) (l : List B) : - cs.apply_braidMoveSequence (bm :: bms) l = cs.apply_braidMove bm (cs.apply_braidMoveSequence bms l) := by +lemma apply_braidMoveSequence_cons (bm : cs.BraidMove) (bms : List (cs.BraidMove)) + (l : List B) : + cs.apply_braidMoveSequence (bm :: bms) l = + cs.apply_braidMove bm (cs.apply_braidMoveSequence bms l) := by simp[apply_braidMoveSequence] lemma cons_of_length_succ {α : Type} (l : List α) {p : ℕ} (h : l.length = p + 1) : @@ -164,14 +171,14 @@ lemma braidMove_cons (bm : cs.BraidMove) (l : List B) (a : B) : simp[shift_braidMove, apply_braidMove] lemma braidMoveSequence_cons (bms : List (cs.BraidMove)) (l : List B) (a : B) : - a :: cs.apply_braidMoveSequence bms l = cs.apply_braidMoveSequence (List.map cs.shift_braidMove bms) (a :: l) := by + a :: cs.apply_braidMoveSequence bms l = + cs.apply_braidMoveSequence (List.map cs.shift_braidMove bms) (a :: l) := by induction bms with | nil => simp[apply_braidMoveSequence] | cons bm bms ih => rw[apply_braidMoveSequence] rw[cs.braidMove_cons bm] - simp[apply_braidMoveSequence] at ih rw[ih] simp[apply_braidMoveSequence_cons] @@ -181,21 +188,20 @@ theorem isReduced_cons (a : B) (l : List B) : cs.IsReduced (a :: l) → cs.IsRed rw[h'] exact h.drop 1 -lemma leftDescent_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftDescent (π (i :: l)) i := by - apply cs.isLeftDescent_iff.mpr - rw[hr] - simp[wordProd_cons] - rw[← IsReduced] - apply cs.isReduced_cons i l hr +lemma leftDescent_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : + cs.IsLeftDescent (π (i :: l)) i := by + rw [IsLeftDescent, hr, wordProd_cons, simple_mul_simple_cancel_left, List.length_cons] + exact Nat.lt_of_le_of_lt (cs.length_wordProd_le l) (Nat.lt_succ_self l.length) -lemma leftInversion_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : cs.IsLeftInversion (π (i :: l)) (s i) := +lemma leftInversion_of_cons (i : B) (l : List B) (hr : cs.IsReduced (i :: l)) : + cs.IsLeftInversion (π (i :: l)) (s i) := (cs.isLeftInversion_simple_iff_isLeftDescent (π (i :: l)) i).mpr (cs.leftDescent_of_cons i l hr) theorem alternatingWord_succ_ne_alternatingWord_eraseIdx [MatsumotoCondition cs] (i j : B) (p : ℕ) (hp : p < M i j) (hij : i ≠ j) : - ∀ (k : ℕ) (hk : k < p) ,π (alternatingWord i j (p + 1)) ≠ π (alternatingWord i j p).eraseIdx k := by + ∀ (k : ℕ) (_ : k < p), + π (alternatingWord i j (p + 1)) ≠ π (alternatingWord i j p).eraseIdx k := by revert i j - induction p with | zero => intro i j @@ -203,30 +209,28 @@ theorem alternatingWord_succ_ne_alternatingWord_eraseIdx [MatsumotoCondition cs] | succ p ih => intro i j hp hij k hk have hp' : p < M i j := by linarith - have hp'' : p < M j i := by simp[M.symmetric]; exact hp' + have hp'' : p < M j i := by + rw [M.symmetric] + exact hp' have zero_lt_p_succ : 0 < p + 1 := by linarith - rw[alternatingWord_succ] nth_rewrite 2 [alternatingWord_succ] - simp - + simp only [List.concat_eq_append, ne_eq] by_cases h_erase : k < (alternatingWord j i p).length · rw[List.eraseIdx_append_of_lt_length h_erase [j]] intro h_contra - simp[cs.wordProd_append] at h_contra - + simp only [wordProd_append] at h_contra + rw[mul_right_cancel_iff] at h_contra have hij' : j ≠ i := by intro h apply hij rw[h] - have h_erase' : k < p := by simp at h_erase; exact h_erase - + have h_erase' : k < p := by + simpa only [length_alternatingWord] using h_erase apply ih j i hp'' hij' k h_erase' h_contra - · have h_erase' : (alternatingWord j i p).length ≤ k := by apply Nat.le_of_not_lt exact h_erase - rw[List.eraseIdx_append_of_length_le h_erase' [j]] have h_erase_k : [j].eraseIdx (k - (alternatingWord j i p).length) = [] := by have h_index : k - (alternatingWord j i p).length = 0 := by @@ -234,226 +238,211 @@ theorem alternatingWord_succ_ne_alternatingWord_eraseIdx [MatsumotoCondition cs] simpa [length_alternatingWord] using Nat.sub_eq_zero_of_le hk_le rw [h_index] rfl - rw[h_erase_k] - simp + simp only [List.append_nil, ne_eq] intro h_contra - - have : cs.wordProd (alternatingWord j i (p + 1) ++ [j]) = cs.wordProd (alternatingWord i j (p + 2)) := by + have : + cs.wordProd (alternatingWord j i (p + 1) ++ [j]) = + cs.wordProd (alternatingWord i j (p + 2)) := by simp[alternatingWord_succ] - rw[this] at h_contra - simp[prod_alternatingWord_eq_mul_pow] at h_contra + simp only [prod_alternatingWord_eq_mul_pow, Order.lt_two_iff, zero_le, Nat.add_div_right, + ite_mul, one_mul] at h_contra by_cases p_even : Even p · have p_even' : Even (p + 2) := by - apply Nat.even_add.mpr - simp - exact p_even - simp[p_even, p_even'] at h_contra + exact Even.add p_even (by norm_num : Even 2) + rw [if_pos p_even', if_pos p_even] at h_contra apply mul_inv_eq_one.mpr at h_contra rw[← inv_pow (s j * s i) (p/2)] at h_contra - simp at h_contra + simp only [mul_inv_rev, inv_simple] at h_contra rw[← pow_add] at h_contra have : p / 2 + 1 + p / 2 = p + 1 := by - have : 2 * (p / 2) = p := Nat.two_mul_div_two_of_even p_even - ring - simp[mul_comm, this] + have h_half : 2 * (p / 2) = p := Nat.two_mul_div_two_of_even p_even + omega rw[this] at h_contra - apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra linarith - · have p_odd : ¬ Even (p + 2) := by intro h - apply Nat.even_add.mp at h - simp[h] at p_even - - simp[p_even, p_odd] at h_contra + exact p_even ((Nat.even_add.mp h).mpr (by norm_num : Even 2)) + rw [if_neg p_odd, if_neg p_even] at h_contra apply (@mul_left_cancel_iff _ _ _ (s j) _ _).mpr at h_contra - - simp at h_contra + simp only [simple_mul_simple_cancel_left] at h_contra rw[← mul_assoc] at h_contra let p_succ := p / 2 + 1 have p_succ_ne_zero : p_succ ≠ 0 := by apply Nat.succ_ne_zero have : (p / 2) = p_succ - 1 := by - simp[p_succ] + omega rw[this] at h_contra rw[mul_pow_sub_one p_succ_ne_zero (s j * s i)] at h_contra - - simp[p_succ] at h_contra + simp only [add_tsub_cancel_right, p_succ] at h_contra apply mul_inv_eq_one.mpr at h_contra rw[← inv_pow (s j * s i) (p/2 + 1)] at h_contra - simp at h_contra + simp only [mul_inv_rev, inv_simple] at h_contra rw[← pow_add] at h_contra - have : p / 2 + 1 + (p / 2 + 1) = p + 1 := by - ring - convert_to 1 + 1 + p / 2 * 2 = p + 1 - rw[add_comm] - simp at p_even - rw[add_assoc] - rw[Nat.one_add_div_two_mul_two_of_odd p_even] - ring + have p_odd_base : Odd p := Nat.not_even_iff_odd.mp p_even + calc + p / 2 + 1 + (p / 2 + 1) = 1 + p / 2 * 2 + 1 := by ring_nf + _ = p + 1 := by rw [Nat.one_add_div_two_mul_two_of_odd p_odd_base] rw[this] at h_contra - apply MatsumotoCondition.alternatingWords_ne_one i j hij (p + 1) zero_lt_p_succ _ h_contra linarith -lemma prefix_braidWord_aux [MatsumotoCondition cs] -(w : W) (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (hil : π (i :: l) = w) (hjl' : π (j :: l') = w) - (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : - ∀ (p : ℕ) (_ : p ≤ M i j), ∃ t : List B, π (alternatingWord i j p ++ t) = w ∧ cs.IsReduced (alternatingWord i j p ++ t) := by +lemma prefix_braidWord_aux [MatsumotoCondition cs] (w : W) (l l' : List B) (i j : B) + (i_ne_j : i ≠ j) (hil : π(i :: l) = w) (hjl' : π(j :: l') = w) + (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : + ∀ (p : ℕ) (_ : p ≤ M i j), + ∃ t : List B, π (alternatingWord i j p ++ t) = w ∧ + cs.IsReduced (alternatingWord i j p ++ t) := by intro p induction p with | zero => intro _ - simp[alternatingWord] use i :: l + constructor + · simpa only [alternatingWord, List.nil_append] using hil + · simpa only [alternatingWord, List.nil_append] using hr | succ p ih => intro hp have hp' : p ≤ M i j := by linarith have hp'' : p < M i j := by linarith rcases ih hp' with ⟨t, ht, htr⟩ rw[← ht] - rw[alternatingWord_succ'] by_cases p_even : Even p - · simp[p_even] - simp[cs.wordProd_cons] - + · rw [if_pos p_even] + change ∃ t_1 : List B, + s j * π (alternatingWord i j p ++ t_1) = π (alternatingWord i j p ++ t) ∧ + cs.IsReduced (j :: alternatingWord i j p ++ t_1) suffices ∃ k : Fin t.length, s j * cs.wordProd (alternatingWord i j p ++ t) = cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by rcases this with ⟨k, hk⟩ use (t.eraseIdx k) - have hw : cs.simple j * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) = cs.wordProd (alternatingWord i j p ++ t) := by rw[← hk] - simp[cs.wordProd_cons] - + rw [simple_mul_simple_cancel_left] constructor · exact hw - · simp[IsReduced] - simp[IsReduced] at htr + · rw [IsReduced] + rw [IsReduced] at htr + rw [List.cons_append] rw[cs.wordProd_cons] rw[hw] rw[htr] - rw[List.length_eraseIdx_of_lt k.2] - simp[add_assoc] - - have : 1 ≤ t.length := by - apply Nat.le_of_not_lt - intro h' - rw[Nat.lt_one_iff] at h' - rw[h'] at k - have wah := k.2 - linarith - - rw[Nat.sub_add_cancel this] - - - have h_left_inversion_j : cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s j) := by + calc + (alternatingWord i j p ++ t).length = p + t.length := by + rw [List.length_append, length_alternatingWord] + _ = (j :: (alternatingWord i j p ++ t.eraseIdx k)).length := by + rw [List.length_cons, List.length_append, length_alternatingWord, + List.length_eraseIdx_of_lt k.2] + have h_t_pos : 0 < t.length := + Nat.lt_of_le_of_lt (Nat.zero_le k) k.2 + omega + have h_left_inversion_j : + cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s j) := by rw[ht, ← hjl'] apply cs.leftInversion_of_cons j l' hr' - - rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) ⟨s j, cs.isReflection_simple j ⟩ h_left_inversion_j with ⟨k, hk⟩ - + rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) + ⟨s j, cs.isReflection_simple j⟩ h_left_inversion_j with ⟨k, hk⟩ by_cases k_lt_len : k < p · exfalso have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len] rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk - - simp[cs.wordProd_append] at hk + simp only [wordProd_append] at hk rw[← mul_assoc] at hk rw[mul_right_cancel_iff] at hk rw[← wordProd_cons] at hk - have : j :: alternatingWord i j p = alternatingWord i j (p + 1) := by simp[alternatingWord_succ', p_even] + have : j :: alternatingWord i j p = alternatingWord i j (p + 1) := by + rw [alternatingWord_succ', if_pos p_even] rw[this] at hk - exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k k_lt_len hk - - · simp at k_lt_len - rw[List.eraseIdx_append_of_length_le] at hk + exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k + k_lt_len hk + · rw [not_lt] at k_lt_len + have k_ge_len : (alternatingWord i j p).length ≤ k := by + simpa only [length_alternatingWord] using k_lt_len + rw[List.eraseIdx_append_of_length_le k_ge_len t] at hk rw[hk] have : k - (alternatingWord i j p).length < t.length := by have kle := k.2 - simp at kle - simp + simp only [List.length_append, length_alternatingWord] at kle + simp only [length_alternatingWord] omega - use ⟨k - (alternatingWord i j p).length, this⟩ - simp[k_lt_len] - - · simp[p_even] - simp[cs.wordProd_cons] - + · rw [if_neg p_even] + change ∃ t_1 : List B, + s i * π (alternatingWord i j p ++ t_1) = π (alternatingWord i j p ++ t) ∧ + cs.IsReduced (i :: alternatingWord i j p ++ t_1) suffices ∃ k : Fin t.length, s i * cs.wordProd (alternatingWord i j p ++ t) = cs.wordProd (alternatingWord i j p ++ (t.eraseIdx k)) from by rcases this with ⟨k, hk⟩ use (t.eraseIdx k) - have hw : cs.simple i * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) = cs.wordProd (alternatingWord i j p ++ t) := by + have hw : + cs.simple i * cs.wordProd (alternatingWord i j p ++ t.eraseIdx k) = + cs.wordProd (alternatingWord i j p ++ t) := by rw[← hk] - simp[cs.wordProd_cons] + rw [simple_mul_simple_cancel_left] constructor · exact hw - · simp[IsReduced] - simp[IsReduced] at htr + · rw [IsReduced] + rw [IsReduced] at htr + rw [List.cons_append] rw[cs.wordProd_cons] rw[hw] rw[htr] - rw[List.length_eraseIdx_of_lt k.2] - simp[add_assoc] - - have : 1 ≤ t.length := by - apply Nat.le_of_not_lt - intro h' - rw[Nat.lt_one_iff] at h' - rw[h'] at k - have wah := k.2 - linarith - - rw[Nat.sub_add_cancel this] - - have h_left_inversion_i : cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s i) := by + calc + (alternatingWord i j p ++ t).length = p + t.length := by + rw [List.length_append, length_alternatingWord] + _ = (i :: (alternatingWord i j p ++ t.eraseIdx k)).length := by + rw [List.length_cons, List.length_append, length_alternatingWord, + List.length_eraseIdx_of_lt k.2] + have h_t_pos : 0 < t.length := + Nat.lt_of_le_of_lt (Nat.zero_le k) k.2 + omega + have h_left_inversion_i : + cs.IsLeftInversion (cs.wordProd (alternatingWord i j p ++ t)) (s i) := by rw[ht, ← hil] apply cs.leftInversion_of_cons i l hr - - rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) ⟨s i, cs.isReflection_simple i ⟩ h_left_inversion_i with ⟨k, hk⟩ - + rcases cs.strongExchangeProperty (alternatingWord i j p ++ t) + ⟨s i, cs.isReflection_simple i⟩ h_left_inversion_i with ⟨k, hk⟩ by_cases k_lt_len : k < p · exfalso have k_lt_len' : k < (alternatingWord i j p).length := by simp[k_lt_len] rw[List.eraseIdx_append_of_lt_length k_lt_len' t] at hk - - simp[cs.wordProd_append] at hk + simp only [wordProd_append] at hk rw[← mul_assoc] at hk rw[mul_right_cancel_iff] at hk rw[← wordProd_cons] at hk - have : i :: alternatingWord i j p = alternatingWord i j (p + 1) := by simp[alternatingWord_succ', p_even] + have : i :: alternatingWord i j p = alternatingWord i j (p + 1) := by + rw [alternatingWord_succ', if_neg p_even] rw[this] at hk - exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k k_lt_len hk - · simp at k_lt_len - rw[List.eraseIdx_append_of_length_le] at hk + exact cs.alternatingWord_succ_ne_alternatingWord_eraseIdx i j p hp'' i_ne_j k + k_lt_len hk + · rw [not_lt] at k_lt_len + have k_ge_len : (alternatingWord i j p).length ≤ k := by + simpa only [length_alternatingWord] using k_lt_len + rw[List.eraseIdx_append_of_length_le k_ge_len t] at hk rw[hk] have : k - (alternatingWord i j p).length < t.length := by have kle := k.2 - simp at kle - simp + simp only [List.length_append, length_alternatingWord] at kle + simp only [length_alternatingWord] omega - use ⟨k - (alternatingWord i j p).length, this⟩ - simp[k_lt_len] - -lemma prefix_braidWord [MatsumotoCondition cs] (l l' : List B) (i j : B) (i_ne_j : i ≠ j) (pi_eq : π (i :: l) = π (j :: l')) -(hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : - ∃ t : List B, π (i :: l) = π (braidWord M i j ++ t) ∧ cs.IsReduced (braidWord M i j ++ t) := by +lemma prefix_braidWord [MatsumotoCondition cs] (l l' : List B) (i j : B) + (i_ne_j : i ≠ j) (pi_eq : π(i :: l) = π(j :: l')) + (hr : cs.IsReduced (i :: l)) (hr' : cs.IsReduced (j :: l')) : + ∃ t : List B, π (i :: l) = π (braidWord M i j ++ t) ∧ + cs.IsReduced (braidWord M i j ++ t) := by have h : M i j ≤ M i j := by linarith have h' : π (j :: l') = π (i :: l) := Eq.symm pi_eq - - rcases cs.prefix_braidWord_aux (π (i :: l)) l l' i j i_ne_j rfl h' hr hr' (M i j) h with ⟨t, ht, htr⟩ + rcases cs.prefix_braidWord_aux (π (i :: l)) l l' i j i_ne_j rfl h' hr hr' + (M i j) h with ⟨t, ht, htr⟩ use t rw[braidWord] constructor @@ -461,30 +450,27 @@ lemma prefix_braidWord [MatsumotoCondition cs] (l l' : List B) (i j : B) (i_ne_j · exact htr theorem apply_braidMove_sequence_append (bms bms' : List (cs.BraidMove)) (l : List B) : - cs.apply_braidMoveSequence (bms ++ bms') l = cs.apply_braidMoveSequence bms (cs.apply_braidMoveSequence bms' l) := by + cs.apply_braidMoveSequence (bms ++ bms') l = + cs.apply_braidMoveSequence bms (cs.apply_braidMoveSequence bms' l) := by induction bms with - | nil => - simp[apply_braidMoveSequence] + | nil => rfl | cons bm bms ih => - simp[apply_braidMoveSequence] - apply congr_arg - exact ih + rw [List.cons_append, apply_braidMoveSequence_cons, apply_braidMoveSequence_cons, ih] -theorem concatenate_braidMove_sequences (l l' l'' : List B) (h : ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l') - (h' : ∃ bms' : List (cs.BraidMove), cs.apply_braidMoveSequence bms' l' = l'') : - ∃ bms'' : List (cs.BraidMove), cs.apply_braidMoveSequence bms'' l = l'' := by +theorem concatenate_braidMove_sequences (l l' l'' : List B) + (h : ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l') + (h' : ∃ bms' : List (cs.BraidMove), cs.apply_braidMoveSequence bms' l' = l'') : + ∃ bms'' : List (cs.BraidMove), cs.apply_braidMoveSequence bms'' l = l'' := by rcases h with ⟨bms, hbms⟩ rcases h' with ⟨bms', hbms'⟩ use bms' ++ bms - simp[apply_braidMove_sequence_append] - simp[hbms', hbms] + rw[apply_braidMove_sequence_append, hbms, hbms'] -- move to aux file theorem isReduced_of_eq_length (l l' : List B) (h_len : l.length = l'.length) (h_eq : π l = π l') (hr : cs.IsReduced l) : cs.IsReduced l' := by - simp[IsReduced] - simp[IsReduced] at hr - + rw[IsReduced] + rw[IsReduced] at hr calc len π l' = len π l := by rw[h_eq] _ = l.length := by rw[hr] @@ -495,30 +481,28 @@ theorem eq_length_of_isReduced (l l' : List B) l.length = l'.length := by rw[IsReduced] at hr rw[IsReduced] at hr' - calc l.length = len π l := by rw[hr] _ = len π l' := by rw[h_eq] _ = l'.length := by rw[hr'] lemma matsumoto_reduced_inductionStep_of_firstLetterEq (p : ℕ) (l_t l'_t : List B) (i : B) -(len_l_t_eq_p : l_t.length = p) (len_l'_t_eq_p : l'_t.length = p) (h_eq : π (i :: l_t) = π (i :: l'_t)) -(l_reduced : cs.IsReduced (i :: l_t)) (l'_reduced : cs.IsReduced (i :: l'_t)) -(ih: ∀ (l l' : List B), - l.length = p → - l'.length = p → - cs.IsReduced l → cs.IsReduced l' → cs.wordProd l = cs.wordProd l' → ∃ bms, cs.apply_braidMoveSequence bms l = l'): -∃ bms, cs.apply_braidMoveSequence bms (i :: l_t) = i :: l'_t := by - + (len_l_t_eq_p : l_t.length = p) (len_l'_t_eq_p : l'_t.length = p) + (h_eq : π(i :: l_t) = π(i :: l'_t)) + (l_reduced : cs.IsReduced (i :: l_t)) (l'_reduced : cs.IsReduced (i :: l'_t)) + (ih : ∀ (l l' : List B), + l.length = p → + l'.length = p → + cs.IsReduced l → + cs.IsReduced l' → + cs.wordProd l = cs.wordProd l' → + ∃ bms, cs.apply_braidMoveSequence bms l = l') : + ∃ bms, cs.apply_braidMoveSequence bms (i :: l_t) = i :: l'_t := by have htr : cs.IsReduced l_t := cs.isReduced_cons i l_t l_reduced have htr' : cs.IsReduced l'_t := cs.isReduced_cons i l'_t l'_reduced - have h_prod : π l_t = π l'_t := by apply @mul_left_cancel _ _ _ (cs.simple i) _ _ rw[← cs.wordProd_cons i l_t, ← cs.wordProd_cons i l'_t, h_eq] - - have ⟨bms, ih'⟩ := ih l_t l'_t len_l_t_eq_p len_l'_t_eq_p htr htr' h_prod - apply (List.cons_inj_right i).mpr at ih' rw[← ih'] rw[braidMoveSequence_cons] @@ -528,15 +512,12 @@ theorem matsumoto_reduced_aux [MatsumotoCondition cs] (p : ℕ) (l l' : List B) (len_l_eq_p : l.length = p) (len_l'_eq_p : l'.length = p) (l_reduced : cs.IsReduced l) (l'_reduced : cs.IsReduced l') (h_eq : π l = π l') : ∃ bms : List (cs.BraidMove), cs.apply_braidMoveSequence bms l = l' := by - revert l l' induction p with | zero => intro l l' hl hl' _ _ _ - have h_len : l.length = l'.length := by rw[hl, hl'] - simp at h_len use [] - simp[apply_braidMoveSequence] + change l = l' rw[List.length_eq_zero_iff] at hl rw[List.length_eq_zero_iff] at hl' rw[hl, hl'] @@ -544,230 +525,192 @@ theorem matsumoto_reduced_aux [MatsumotoCondition cs] (p : ℕ) (l l' : List B) intro l l' len_l_eq_p len_l'_eq_p l_reduced l'_reduced h_eq rcases cons_of_length_succ l len_l_eq_p with ⟨i, l_t, rfl, len_l_t_eq_p⟩ rcases cons_of_length_succ l' len_l'_eq_p with ⟨j, l'_t, rfl, len_l'_t_eq_p⟩ - by_cases first_letter_eq : i = j · rw[first_letter_eq] rw[first_letter_eq] at h_eq rw[first_letter_eq] at l_reduced - - apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t l'_t j len_l_t_eq_p len_l'_t_eq_p h_eq l_reduced l'_reduced + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t l'_t j len_l_t_eq_p + len_l'_t_eq_p h_eq l_reduced l'_reduced exact ih - - · obtain ⟨m, hm⟩ : ∃ m : ℕ ,M i j = m + 1 := by + · obtain ⟨m, hm⟩ : ∃ m : ℕ, M i j = m + 1 := by use M i j - 1 simp[MatsumotoCondition.one_le_M cs i j] - have hm' : M j i = m + 1 := by - simp[M.symmetric] + rw[M.symmetric] exact hm - by_cases m_even : Even m · have j_ne_i : j ≠ i := by - simp[first_letter_eq] - intro heq - rw[heq] at first_letter_eq - contradiction - + intro hji + exact first_letter_eq hji.symm obtain ⟨b_tail, hb, b_reduced⟩ := cs.prefix_braidWord l'_t l_t j i j_ne_i (Eq.symm h_eq) l'_reduced l_reduced - have hb' : cs.wordProd (i :: l_t) = cs.wordProd (braidWord M j i ++ b_tail) := by rw[← hb] exact h_eq - apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M j i ++ b_tail) (j :: l'_t) - - have b_word_cons : (braidWord M j i ++ b_tail) = i :: (alternatingWord j i m ++ b_tail) := by - simp[braidWord] - rw[hm'] - simp[alternatingWord_succ'] - simp[m_even] - - rw[b_word_cons] - - have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by - suffices (braidWord M j i ++ b_tail).length = p + 1 from by - simp[braidWord] at this - rw[hm'] at this - simp[alternatingWord] - nth_rewrite 1 [add_comm] at this - rw[← add_assoc] at this - simp at this - rw[← this] - ring - rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M j i ++ b_tail) hb' l_reduced b_reduced] - exact len_l_eq_p - - rw[b_word_cons] at hb' - rw[b_word_cons] at b_reduced - apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t (alternatingWord j i m ++ b_tail) i len_l_t_eq_p b_len_p hb' l_reduced b_reduced ih - - apply cs.concatenate_braidMove_sequences (braidWord M j i ++ b_tail) (braidWord M i j ++ b_tail) (j :: l'_t) - - use [BraidMove.mk j i 0] - simp[apply_braidMoveSequence] - simp[apply_braidMove] - - simp[braidWord] - rw[hm] - rw[alternatingWord_succ'] - simp[m_even] - - have switch_braidWord : π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by - simp[wordProd_append] - rw[cs.wordProd_braidWord_eq j i] - - rw[switch_braidWord] at hb' - have b_reduced' : cs.IsReduced (braidWord M i j ++ b_tail) := by - apply cs.isReduced_of_eq_length (braidWord M j i ++ b_tail) (braidWord M i j ++ b_tail) - simp[M.symmetric] - exact switch_braidWord - exact b_reduced - - have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M i j ++ b_tail) := by - rw[← hb'] - exact Eq.symm h_eq - - have b_word_cons : (braidWord M i j ++ b_tail) = j :: (alternatingWord i j m ++ b_tail) := by - simp[braidWord] - rw[hm] - simp[alternatingWord_succ'] - simp[m_even] - - have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by - suffices (braidWord M i j ++ b_tail).length = p + 1 from by - simp[braidWord] at this - rw[hm] at this - simp[alternatingWord] - nth_rewrite 1 [add_comm] at this - rw[← add_assoc] at this - simp at this - rw[← this] - ring - rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M i j ++ b_tail) hb' l'_reduced b_reduced'] - exact len_l'_eq_p - - rw[b_word_cons] at hb' - rw[b_word_cons] at b_reduced' - - apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p (alternatingWord i j m ++ b_tail) - l'_t j b_len_p len_l'_t_eq_p (Eq.symm hb') b_reduced' l'_reduced ih - - · rcases cs.prefix_braidWord l_t l'_t i j first_letter_eq h_eq l_reduced l'_reduced with ⟨b_tail, hb, b_reduced⟩ - apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M i j ++ b_tail) (j :: l'_t) - - simp[braidWord] - rw[hm] - rw[alternatingWord_succ'] - simp[m_even] - - have b_word_cons : (braidWord M i j ++ b_tail) = i :: (alternatingWord i j m ++ b_tail) := by - simp[braidWord] - rw[hm] - simp[alternatingWord_succ'] - simp[m_even] - - have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by - suffices (braidWord M i j ++ b_tail).length = p + 1 from by - simp[braidWord] at this - rw[hm] at this - simp[alternatingWord] - nth_rewrite 1 [add_comm] at this - rw[← add_assoc] at this - simp at this - rw[← this] - ring - rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M i j ++ b_tail) hb l_reduced b_reduced] - exact len_l_eq_p - - have i_tail_reduced : cs.IsReduced l_t := by - apply cs.isReduced_cons i l_t l_reduced - - have aword_is_reduced : cs.IsReduced (alternatingWord i j m ++ b_tail) := by - apply cs.isReduced_cons i ((alternatingWord i j m) ++ b_tail) - rw[← b_word_cons] - exact b_reduced - - have i_tail_eq_aword : π l_t = π (alternatingWord i j m ++ b_tail) := by - rw[b_word_cons] at hb - simp[wordProd_cons] at hb - exact hb - - rcases ih l_t (alternatingWord i j m ++ b_tail) len_l_t_eq_p b_len_p i_tail_reduced aword_is_reduced i_tail_eq_aword with ⟨bms, ih'⟩ - - use (List.map cs.shift_braidMove bms) - - rw[← braidMoveSequence_cons] - suffices cs.apply_braidMoveSequence bms l_t = (alternatingWord i j m ++ b_tail) from by - rw[this] - exact ih' - - apply cs.concatenate_braidMove_sequences (braidWord M i j ++ b_tail) (braidWord M j i ++ b_tail) (j :: l'_t) - - use [BraidMove.mk i j 0] - simp[apply_braidMoveSequence] - simp[apply_braidMove] - - simp[braidWord] - rw[hm'] - rw[alternatingWord_succ'] - simp[m_even] - - have b_word_cons : (braidWord M j i ++ b_tail) = j :: (alternatingWord j i m ++ b_tail) := by - simp[braidWord] - rw[hm'] - simp[alternatingWord_succ'] - simp[m_even] - - have switch_braidWord : π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by - simp[wordProd_append] - rw[cs.wordProd_braidWord_eq j i] - - have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M j i ++ b_tail) := by - rw[switch_braidWord] - rw[← hb] - exact Eq.symm h_eq - - have b_reduced' : cs.IsReduced (braidWord M j i ++ b_tail) := by - apply cs.isReduced_of_eq_length (braidWord M i j ++ b_tail) (braidWord M j i ++ b_tail) - simp[M.symmetric] - exact Eq.symm switch_braidWord - exact b_reduced - - have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by - suffices (braidWord M j i ++ b_tail).length = p + 1 from by - simp[braidWord] at this - rw[hm'] at this - simp[alternatingWord] - nth_rewrite 1 [add_comm] at this - rw[← add_assoc] at this - simp at this - rw[← this] - ring - rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M j i ++ b_tail) hb' l'_reduced b_reduced'] - exact len_l'_eq_p - - have j_tail_reduced : cs.IsReduced l'_t := by - apply cs.isReduced_cons j l'_t l'_reduced - - have aword_is_reduced : cs.IsReduced (alternatingWord j i m ++ b_tail) := by - apply cs.isReduced_cons j ((alternatingWord j i m) ++ b_tail) - rw[← b_word_cons] - exact b_reduced' - - have j_tail_eq_aword : π (alternatingWord j i m ++ b_tail) = π l'_t := by + · have b_word_cons : + (braidWord M j i ++ b_tail) = i :: (alternatingWord j i m ++ b_tail) := by + rw[braidWord, hm', alternatingWord_succ', if_pos m_even, List.cons_append] + rw[b_word_cons] + have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by + have h_length : + (braidWord M j i ++ b_tail).length = p + 1 := by + rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M j i ++ b_tail) + hb' l_reduced b_reduced] + exact len_l_eq_p + rw[b_word_cons] at h_length + simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢ + omega rw[b_word_cons] at hb' - simp[wordProd_cons] at hb' - exact Eq.symm hb' - - rcases ih (alternatingWord j i m ++ b_tail) l'_t b_len_p len_l'_t_eq_p aword_is_reduced j_tail_reduced j_tail_eq_aword with ⟨bms, ih'⟩ - - use (List.map cs.shift_braidMove bms) - rw[← braidMoveSequence_cons] - suffices cs.apply_braidMoveSequence bms (alternatingWord j i m ++ b_tail) = l'_t from by - rw[this] - exact ih' - + rw[b_word_cons] at b_reduced + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p l_t + (alternatingWord j i m ++ b_tail) i len_l_t_eq_p b_len_p hb' l_reduced + b_reduced ih + · apply cs.concatenate_braidMove_sequences (braidWord M j i ++ b_tail) + (braidWord M i j ++ b_tail) (j :: l'_t) + · use [BraidMove.mk j i 0] + rw[apply_braidMoveSequence_cons] + change cs.apply_braidMove (BraidMove.mk j i 0) (braidWord M j i ++ b_tail) = + braidWord M i j ++ b_tail + rw[apply_braidMove] + have htake : + List.take (M j i) (braidWord M j i ++ b_tail) = braidWord M j i := by + rw[← length_alternatingWord j i (M j i)] + exact List.take_left + have hdrop : + List.drop (M j i) (braidWord M j i ++ b_tail) = b_tail := by + rw[← length_alternatingWord j i (M j i)] + exact List.drop_left + rw[if_pos htake, hdrop] + · have switch_braidWord : + π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by + rw[wordProd_append, wordProd_append, cs.wordProd_braidWord_eq j i] + rw[switch_braidWord] at hb' + have b_reduced' : cs.IsReduced (braidWord M i j ++ b_tail) := by + apply cs.isReduced_of_eq_length (braidWord M j i ++ b_tail) + (braidWord M i j ++ b_tail) + · simp only [List.length_append, length_alternatingWord] + rw[M.symmetric] + · exact switch_braidWord + · exact b_reduced + have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M i j ++ b_tail) := by + rw[← hb'] + exact Eq.symm h_eq + have b_word_cons : + (braidWord M i j ++ b_tail) = j :: (alternatingWord i j m ++ b_tail) := by + rw[braidWord, hm, alternatingWord_succ', if_pos m_even, List.cons_append] + have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by + have h_length : + (braidWord M i j ++ b_tail).length = p + 1 := by + rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M i j ++ b_tail) + hb' l'_reduced b_reduced'] + exact len_l'_eq_p + rw[b_word_cons] at h_length + simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢ + omega + rw[b_word_cons] at hb' + rw[b_word_cons] at b_reduced' + rw[b_word_cons] + apply cs.matsumoto_reduced_inductionStep_of_firstLetterEq p + (alternatingWord i j m ++ b_tail) l'_t j b_len_p len_l'_t_eq_p + (Eq.symm hb') b_reduced' l'_reduced ih + · rcases cs.prefix_braidWord l_t l'_t i j first_letter_eq h_eq l_reduced l'_reduced + with ⟨b_tail, hb, b_reduced⟩ + apply cs.concatenate_braidMove_sequences (i :: l_t) (braidWord M i j ++ b_tail) (j :: l'_t) + · have b_word_cons : + (braidWord M i j ++ b_tail) = i :: (alternatingWord i j m ++ b_tail) := by + rw[braidWord, hm, alternatingWord_succ', if_neg m_even, List.cons_append] + have b_len_p : (alternatingWord i j m ++ b_tail).length = p := by + have h_length : + (braidWord M i j ++ b_tail).length = p + 1 := by + rw[← cs.eq_length_of_isReduced (i :: l_t) (braidWord M i j ++ b_tail) + hb l_reduced b_reduced] + exact len_l_eq_p + rw[b_word_cons] at h_length + simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢ + omega + have i_tail_reduced : cs.IsReduced l_t := by + apply cs.isReduced_cons i l_t l_reduced + have aword_is_reduced : cs.IsReduced (alternatingWord i j m ++ b_tail) := by + apply cs.isReduced_cons i ((alternatingWord i j m) ++ b_tail) + rw[← b_word_cons] + exact b_reduced + have i_tail_eq_aword : π l_t = π (alternatingWord i j m ++ b_tail) := by + rw[b_word_cons] at hb + rw[wordProd_cons, wordProd_cons] at hb + rw[mul_left_cancel_iff] at hb + exact hb + rcases ih l_t (alternatingWord i j m ++ b_tail) len_l_t_eq_p b_len_p + i_tail_reduced aword_is_reduced i_tail_eq_aword with ⟨bms, ih'⟩ + use (List.map cs.shift_braidMove bms) + rw[← braidMoveSequence_cons] + suffices cs.apply_braidMoveSequence bms l_t = (alternatingWord i j m ++ b_tail) + from by + rw[this] + rw[← b_word_cons] + exact ih' + · apply cs.concatenate_braidMove_sequences (braidWord M i j ++ b_tail) + (braidWord M j i ++ b_tail) (j :: l'_t) + · use [BraidMove.mk i j 0] + rw[apply_braidMoveSequence_cons] + change cs.apply_braidMove (BraidMove.mk i j 0) (braidWord M i j ++ b_tail) = + braidWord M j i ++ b_tail + rw[apply_braidMove] + have htake : + List.take (M i j) (braidWord M i j ++ b_tail) = braidWord M i j := by + rw[← length_alternatingWord i j (M i j)] + exact List.take_left + have hdrop : + List.drop (M i j) (braidWord M i j ++ b_tail) = b_tail := by + rw[← length_alternatingWord i j (M i j)] + exact List.drop_left + rw[if_pos htake, hdrop] + · have b_word_cons : + (braidWord M j i ++ b_tail) = j :: (alternatingWord j i m ++ b_tail) := by + rw[braidWord, hm', alternatingWord_succ', if_neg m_even, List.cons_append] + have switch_braidWord : + π (braidWord M j i ++ b_tail) = π (braidWord M i j ++ b_tail) := by + rw[wordProd_append, wordProd_append, cs.wordProd_braidWord_eq j i] + have hb' : cs.wordProd (j :: l'_t) = cs.wordProd (braidWord M j i ++ b_tail) := by + rw[switch_braidWord] + rw[← hb] + exact Eq.symm h_eq + have b_reduced' : cs.IsReduced (braidWord M j i ++ b_tail) := by + apply cs.isReduced_of_eq_length (braidWord M i j ++ b_tail) + (braidWord M j i ++ b_tail) + · simp only [List.length_append, length_alternatingWord] + rw[M.symmetric] + · exact Eq.symm switch_braidWord + · exact b_reduced + have b_len_p : (alternatingWord j i m ++ b_tail).length = p := by + have h_length : + (braidWord M j i ++ b_tail).length = p + 1 := by + rw[← cs.eq_length_of_isReduced (j :: l'_t) (braidWord M j i ++ b_tail) + hb' l'_reduced b_reduced'] + exact len_l'_eq_p + rw[b_word_cons] at h_length + simp only [List.length_cons, List.length_append, length_alternatingWord] at h_length ⊢ + omega + have j_tail_reduced : cs.IsReduced l'_t := by + apply cs.isReduced_cons j l'_t l'_reduced + have aword_is_reduced : cs.IsReduced (alternatingWord j i m ++ b_tail) := by + apply cs.isReduced_cons j ((alternatingWord j i m) ++ b_tail) + rw[← b_word_cons] + exact b_reduced' + have j_tail_eq_aword : π (alternatingWord j i m ++ b_tail) = π l'_t := by + rw[b_word_cons] at hb' + rw[wordProd_cons, wordProd_cons] at hb' + rw[mul_left_cancel_iff] at hb' + exact Eq.symm hb' + rcases ih (alternatingWord j i m ++ b_tail) l'_t b_len_p len_l'_t_eq_p + aword_is_reduced j_tail_reduced j_tail_eq_aword with ⟨bms, ih'⟩ + use (List.map cs.shift_braidMove bms) + rw[b_word_cons] + rw[← braidMoveSequence_cons] + suffices cs.apply_braidMoveSequence bms (alternatingWord j i m ++ b_tail) = l'_t + from by + rw[this] + exact ih' theorem matsumoto_reduced [MatsumotoCondition cs] (l l' : List B) (hr : cs.IsReduced l) (hr' : cs.IsReduced l') (h : π l = π l') : diff --git a/LeanPool/DemazureOperatorsLean/StrongExchange.lean b/LeanPool/DemazureOperatorsLean/StrongExchange.lean index 93f1797e94..908c731ecc 100644 --- a/LeanPool/DemazureOperatorsLean/StrongExchange.lean +++ b/LeanPool/DemazureOperatorsLean/StrongExchange.lean @@ -42,7 +42,7 @@ def eta (i : B) (t : cs.Reflection) : ZMod 2 := lemma eta_eq_eta_of_simpleConj (i : B) (t : cs.Reflection) : cs.eta i t = cs.eta i (cs.conj_of_reflection t (s i)) := by - simp [eta] + rw [eta, eta] rcases t with ⟨t, ht⟩ have : s i = t ↔ s i * t = 1 := by constructor @@ -51,12 +51,10 @@ lemma eta_eq_eta_of_simpleConj (i : B) (t : cs.Reflection) : exact IsReflection.mul_self ht · intro h' apply (mul_left_inj t).mp - simp [IsReflection.mul_self ht] - exact h' - + simpa [IsReflection.mul_self ht] using h' by_cases h : s i = t - · simp [this, h, conj_of_reflection] - · simp [this, h, if_neg, conj_of_reflection] + · simp [h, conj_of_reflection] + · simp [this, conj_of_reflection] /-- The permutation action associated to a simple reflection. -/ def permutationMap (i : B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 := @@ -64,8 +62,8 @@ def permutationMap (i : B) : cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 theorem permutationMap_orderTwo (i : B) : cs.permutationMap i ∘ cs.permutationMap i = id := by funext ⟨t, z⟩ - simp [permutationMap] - constructor + simp only [permutationMap, Function.comp_apply, id_eq] + apply Prod.ext · simp[conj_of_reflection, mul_assoc] · rw [← cs.eta_eq_eta_of_simpleConj i t] ring_nf @@ -73,22 +71,22 @@ theorem permutationMap_orderTwo (i : B) : cs.permutationMap i ∘ cs.permutation simp lemma leftInvSeq_repeats : ∀ (k : ℕ) (h : k < M i j), -(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by simp[h]; linarith) = -(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by simp[h]; linarith) := by + (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by + simp + linarith) = + (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by + simp + linarith) := by intro k h' - rw[getElem_leftInvSeq_alternatingWord cs i j (M i j) k] - rw[getElem_leftInvSeq_alternatingWord cs i j (M i j) ((M i j)+k)] + rw [getElem_leftInvSeq_alternatingWord cs i j (M i j) k (by omega)] + rw [getElem_leftInvSeq_alternatingWord cs i j (M i j) (M i j + k) (by omega)] rw[cs.prod_alternatingWord_eq_mul_pow] rw[cs.prod_alternatingWord_eq_mul_pow] - have h_odd : Odd (2 * k + 1) := by simp - have h_odd' : Odd (2 * ((M i j) + k) + 1) := by simp - - simp[h_odd, h_odd'] - + simp only [Nat.not_even_bit1, ↓reduceIte, mul_right_inj] have two_gt_0 : 2 > 0 := by linarith have h_exp : (2 * k + 1) / 2 = k := by rw[add_comm] @@ -101,85 +99,94 @@ lemma leftInvSeq_repeats : ∀ (k : ℕ) (h : k < M i j), rw[h_exp, h_exp'] rw[NatPowAssoc.npow_add] simp - linarith - linarith lemma leftInvSeq_repeats' : ∀ (k : ℕ) (h : k < M i j), -(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by simp[h]; linarith) = -(cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by simp[h]; linarith) := by + (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[M i j + k]'(by + simp + linarith) = + (cs.leftInvSeq (alternatingWord i j (2 * M i j)))[k]'(by + simp + linarith) := by intro k h' exact leftInvSeq_repeats cs k h' lemma nReflectionOccurrences_even_braidWord (t : cs.Reflection) : Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) := by - - suffices (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) = 2 * List.count (t.1) (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (M.M i j * 2)))) from by + suffices + reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t = + 2 * List.count t.1 + (List.take (M.M i j) + (cs.leftInvSeq (alternatingWord i j (M.M i j * 2)))) from by simp[this] - - simp[reflection_mem_leftInvSeq_count] - suffices (cs.leftInvSeq (alternatingWord i j (2 * M i j))) = (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j)))) ++ (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j)))) from by + rw [reflection_mem_leftInvSeq_count] + suffices + cs.leftInvSeq (alternatingWord i j (2 * M i j)) = + List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++ + List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) from by rw[this] simp - ring - + ring_nf have m_le_two_m : M i j ≤ 2 * M i j := by linarith - have length_eq : (cs.leftInvSeq (alternatingWord i j (2 * (M i j)))).length = - (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++ (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))))).length := by + have length_eq : + (cs.leftInvSeq (alternatingWord i j (2 * M i j))).length = + (List.take (M i j) (cs.leftInvSeq (alternatingWord i j (2 * M i j))) ++ + List.take (M i j) + (cs.leftInvSeq (alternatingWord i j (2 * M i j)))).length := by simp[m_le_two_m] - ring - + ring_nf apply List.ext_getElem length_eq intro k hk hk' - by_cases h : k < M i j - · have : k < (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length := by + · have : + k < + (List.take (M.M i j) + (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length := by simp[h, m_le_two_m] - rw[List.getElem_append_left this] rw[List.getElem_take'] exact h · have h_k_le : k - M i j < M i j := by - simp at hk - apply Nat.sub_lt_left_of_lt_add - simp at h - exact h - linarith - have : (List.take (M.M i j) (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length ≤ k := by - simp[h, m_le_two_m] + have hk_bound : k < 2 * M i j := by + simpa using hk + have h_ge : M i j ≤ k := Nat.le_of_not_gt h + omega + have : + (List.take (M.M i j) + (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length ≤ k := by + simp[m_le_two_m] linarith - rw[List.getElem_append_right this] rw[List.getElem_take] - simp[m_le_two_m] - + have take_length : + (List.take (M.M i j) + (cs.leftInvSeq (alternatingWord i j (2 * M.M i j)))).length = M.M i j := by + simp[m_le_two_m] + simp only [take_length] rw[← leftInvSeq_repeats' cs (k - M i j) h_k_le] - - suffices M.M i j + (k - M.M i j) = k from by - simp[this] - - rw[← Nat.add_sub_assoc] - simp - linarith + have : M.M i j + (k - M.M i j) = k := by + exact Nat.add_sub_of_le (Nat.le_of_not_gt h) + simp[this] lemma parityReflectionOccurrences_braidWord (t : cs.Reflection) : reflection_mem_leftInvSeq_parity cs (alternatingWord i j (2 * M i j)) t = 0 := by suffices Even (reflection_mem_leftInvSeq_count cs (alternatingWord i j (2 * M i j)) t) from by - simp[this, reflection_mem_leftInvSeq_parity] + rw [reflection_mem_leftInvSeq_parity] apply ZMod.natCast_eq_zero_iff_even.mpr this exact nReflectionOccurrences_even_braidWord cs t -lemma alternatingWord_reverse : (alternatingWord i j (2 * p)).reverse = alternatingWord j i (2 * p) := by +lemma alternatingWord_reverse : + (alternatingWord i j (2 * p)).reverse = alternatingWord j i (2 * p) := by induction p with | zero => simp[alternatingWord] | succ p h => - simp [alternatingWord] - rw[h] - have h1 : j :: i :: alternatingWord j i (2 * p) = alternatingWord j i (2 * p + 1 + 1) := by - rw[alternatingWord_succ'] - rw[alternatingWord_succ'] - simp - simp[h1, alternatingWord] + rw [show 2 * (p + 1) = 2 * p + 1 + 1 by ring_nf] + rw [alternatingWord_succ] + rw [alternatingWord_succ] + simp only [List.concat_eq_append, List.reverse_append, List.reverse_singleton, + List.singleton_append] + rw [h] + simp only [alternatingWord_succ', Nat.not_even_bit1, even_two_mul, if_false, if_true] instance instMul : Mul (cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2) where mul := fun f g => f ∘ g @@ -223,43 +230,56 @@ lemma isReflection_conj_inv_mul_mul (ht : cs.IsReflection t) (w : W) : lemma permutationMap_ofList_mk_1 (l : List B) : (permutationMap_ofList cs l ⟨t,z⟩).1 = cs.conj_of_reflection t (π l) := by - simp[conj_of_reflection] induction l with | nil => - simp[permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_count] + simp[permutationMap_ofList, conj_of_reflection] | cons a l h => - calc (permutationMap_ofList cs (a :: l) (t, z)).1 = ((cs.permutationMap a * permutationMap_ofList cs l) (t, z)).1 := by simp[permutationMap_ofList] + calc + (permutationMap_ofList cs (a :: l) (t, z)).1 = + ((cs.permutationMap a * permutationMap_ofList cs l) (t, z)).1 := by + simp[permutationMap_ofList] _ = (cs.permutationMap a (permutationMap_ofList cs l (t, z))).1 := by rfl - - simp[permutationMap, conj_of_reflection, h] - simp[cs.wordProd_cons, mul_assoc] + _ = cs.conj_of_reflection t (π (a :: l)) := by + simp[permutationMap, conj_of_reflection, h, cs.wordProd_cons, mul_assoc] lemma permutationMap_ofList_mk_2 (l : List B) : - (permutationMap_ofList cs l ⟨t,z⟩).2 = z + reflection_mem_leftInvSeq_parity cs l.reverse t := by + (permutationMap_ofList cs l ⟨t,z⟩).2 = + z + reflection_mem_leftInvSeq_parity cs l.reverse t := by induction l with | nil => - simp[permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count] + simp[permutationMap_ofList, reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count] | cons i l h => rw[permutationMap_ofList, mulDef] - simp[permutationMap, h] - simp[reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count] + change (cs.permutationMap i (permutationMap_ofList cs l (t, z))).2 = + z + reflection_mem_leftInvSeq_parity cs (i :: l).reverse t + rw [permutationMap] + change (permutationMap_ofList cs l (t, z)).2 + + cs.eta i (permutationMap_ofList cs l (t, z)).1 = + z + reflection_mem_leftInvSeq_parity cs (i :: l).reverse t + rw [h] + simp only [reflection_mem_leftInvSeq_parity, reflection_mem_leftInvSeq_count, + List.reverse_cons] rw[← List.concat_eq_append] rw[leftInvSeq_concat] - simp [List.count_singleton] - - suffices cs.eta i (permutationMap_ofList cs l (t, z)).1 = if (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 then 1 else 0 from by + simp only [wordProd_reverse, inv_inv, List.concat_eq_append, List.count_append, + Nat.cast_add] + suffices + cs.eta i (permutationMap_ofList cs l (t, z)).1 = + if (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 then 1 else 0 from by rw[this] - simp[add_assoc] - - simp[eta, permutationMap_ofList_mk_1, conj_of_reflection] + simp[add_assoc, List.count_singleton] + simp only [eta, permutationMap_ofList_mk_1, conj_of_reflection] by_cases h' : (cs.wordProd l)⁻¹ * cs.simple i * cs.wordProd l = t.1 - · simp[h'] - rw[← h'] - simp[mul_assoc] - · simp[h'] - by_contra h'' - rw[h''] at h' - simp[mul_assoc] at h' + · have lhs : cs.simple i = cs.wordProd l * t.1 * (cs.wordProd l)⁻¹ := by + rw [← h'] + simp [mul_assoc] + rw [if_pos lhs, if_pos h'] + · have lhs_ne : ¬cs.simple i = cs.wordProd l * t.1 * (cs.wordProd l)⁻¹ := by + intro h'' + apply h' + rw [h''] + simp [mul_assoc] + rw [if_neg lhs_ne, if_neg h'] lemma permutationMap_ofList_mk (l : List B) (t : cs.Reflection) (z : ZMod 2) : (permutationMap_ofList cs l ⟨t,z⟩) = ⟨cs.conj_of_reflection t (π l), @@ -268,36 +288,33 @@ lemma permutationMap_ofList_mk (l : List B) (t : cs.Reflection) (z : ZMod 2) : theorem permutationMap_isLiftable : M.IsLiftable (cs.permutationMap) := by intro i j - - have h (p : ℕ) : (cs.permutationMap i * cs.permutationMap j) ^ p = permutationMap_ofList cs (alternatingWord i j (2 * p)) := by + have h (p : ℕ) : + (cs.permutationMap i * cs.permutationMap j) ^ p = + permutationMap_ofList cs (alternatingWord i j (2 * p)) := by induction p with | zero => - simp[permutationMap_ofList, permutationMap, permutationMap_orderTwo] rfl | succ p h => - simp[pow_succ'] + rw[pow_succ'] rw[h] - have : 2 * (p + 1) = 2 * p + 1 + 1 := by ring + have : 2 * (p + 1) = 2 * p + 1 + 1 := by ring_nf rw[this] rw[alternatingWord_succ'] rw [if_neg (Nat.not_even_bit1 p)] rw[permutationMap_ofList] - rw[alternatingWord_succ'] rw [if_pos (even_two_mul p)] rw[permutationMap_ofList] simp[mul_assoc] - rw[h (M i j)] funext ⟨t, z⟩ convert_to permutationMap_ofList cs (alternatingWord i j (2 * M.M i j)) (t, z) = ⟨t,z⟩ - - simp[permutationMap_ofList_mk, conj_of_reflection] - constructor - · simp[cs.prod_alternatingWord_eq_mul_pow] + rw[permutationMap_ofList_mk] + apply Prod.ext + · simp[conj_of_reflection, cs.prod_alternatingWord_eq_mul_pow] · rw[alternatingWord_reverse] rw[M.symmetric] - exact parityReflectionOccurrences_braidWord cs t + simp [parityReflectionOccurrences_braidWord (M := M) cs (i := j) (j := i) t] /-- The homomorphic lift of the simple permutation maps to the Coxeter group. -/ def permutationMap_lift : W →* cs.Reflection × ZMod 2 → cs.Reflection × ZMod 2 := @@ -312,7 +329,7 @@ theorem permutationMap_lift_mk_ofList (l : List B) (t : cs.Reflection) (z : ZMod | cons i l h => rw[cs.wordProd_cons] rw[permutationMap_ofList] - simp[mulDef] + simp only [mulDef, map_mul, Function.comp_apply] rw[← h] simp[permutationMap_lift] @@ -327,7 +344,8 @@ def parityReflectionOccurrences_lift (w : W) (t : cs.Reflection) : ZMod 2 := (permutationMap_lift cs w⁻¹ ⟨t,0⟩).2 theorem parityReflectionOccurrences_lift_mk (l : List B) (t : cs.Reflection) : - parityReflectionOccurrences_lift cs (cs.wordProd l) t = reflection_mem_leftInvSeq_parity cs l t := by + parityReflectionOccurrences_lift cs (cs.wordProd l) t = + reflection_mem_leftInvSeq_parity cs l t := by rw[parityReflectionOccurrences_lift] rw[← wordProd_reverse] rw[permutationMap_lift_mk_ofList cs l.reverse t 0] @@ -335,11 +353,13 @@ theorem parityReflectionOccurrences_lift_mk (l : List B) (t : cs.Reflection) : simp theorem permutationMap_lift_mk (w : W) (t : cs.Reflection) (z : ZMod 2) : - permutationMap_lift cs w ⟨t,z⟩ = ⟨⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩ , z + parityReflectionOccurrences_lift cs w⁻¹ t⟩ := by + permutationMap_lift cs w ⟨t,z⟩ = + ⟨⟨w * t.1 * w⁻¹, IsReflection.conj t.2 w⟩, + z + parityReflectionOccurrences_lift cs w⁻¹ t⟩ := by obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w apply Prod.ext · simp[permutationMap_lift_mk_ofList, permutationMap_ofList_mk, conj_of_reflection] - · simp[parityReflectionOccurrences_lift] + · simp only [parityReflectionOccurrences_lift, inv_inv] rw[permutationMap_lift_mk_ofList cs l t 0] rw[permutationMap_lift_mk_ofList cs l t z] simp[permutationMap_ofList_mk] @@ -347,9 +367,10 @@ theorem permutationMap_lift_mk (w : W) (t : cs.Reflection) (z : ZMod 2) : theorem parityReflectionOccurrences_ext (l l' : List B) (t : cs.Reflection) (h : π l = π l') : reflection_mem_leftInvSeq_parity cs l t = reflection_mem_leftInvSeq_parity cs l' t := by - calc - reflection_mem_leftInvSeq_parity cs l t = parityReflectionOccurrences_lift cs (cs.wordProd l) t := by rw[parityReflectionOccurrences_lift_mk] + reflection_mem_leftInvSeq_parity cs l t = + parityReflectionOccurrences_lift cs (cs.wordProd l) t := by + rw[parityReflectionOccurrences_lift_mk] _ = parityReflectionOccurrences_lift cs (cs.wordProd l') t := by rw[h] _ = reflection_mem_leftInvSeq_parity cs l' t := by rw[parityReflectionOccurrences_lift_mk] @@ -358,29 +379,26 @@ lemma odd_iff_parity_eq_one (n : ℕ) : Odd n ↔ (n : ZMod 2) = 1 := by lemma gt_one_of_odd (n : ℕ) : Odd n → n > 0 := by intro h - simp[Odd] at h rcases h with ⟨m, rfl⟩ suffices m ≥ 0 from by linarith exact Nat.zero_le m -lemma isInLeftInvSeq_of_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) (h : reflection_mem_leftInvSeq_parity cs l t = 1) : - t.1 ∈ cs.leftInvSeq l := by - simp [reflection_mem_leftInvSeq_parity] at h +lemma isInLeftInvSeq_of_parityReflectionOccurrences_eq_one + (l : List B) (t : cs.Reflection) + (h : reflection_mem_leftInvSeq_parity cs l t = 1) : + t.1 ∈ cs.leftInvSeq l := by + rw [reflection_mem_leftInvSeq_parity] at h rw [← @odd_iff_parity_eq_one (reflection_mem_leftInvSeq_count cs l t)] at h - apply gt_one_of_odd (reflection_mem_leftInvSeq_count cs l t) at h - simp[reflection_mem_leftInvSeq_count] at h - - exact h + rw[reflection_mem_leftInvSeq_count] at h + exact List.count_pos_iff.mp h lemma isLeftInversion_of_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) : reflection_mem_leftInvSeq_parity cs l t = 1 → cs.IsLeftInversion (cs.wordProd l) t.1 := by intro h - rcases cs.exists_isReduced (π l) with ⟨u, u_reduced, hu⟩ rw[hu] apply cs.isLeftInversion_of_mem_leftInvSeq u_reduced - rw[cs.parityReflectionOccurrences_ext l u t hu] at h exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs u t h @@ -388,7 +406,7 @@ lemma isLeftInversion_of_parityReflectionOccurrences_lift_eq_one (w : W) (t : cs parityReflectionOccurrences_lift cs w t = 1 → cs.IsLeftInversion w t.1 := by intro h obtain ⟨l, _, rfl⟩ := cs.exists_isReduced w - simp[parityReflectionOccurrences_lift_mk] at h + rw[parityReflectionOccurrences_lift_mk] at h apply isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t h lemma eraseIdx_of_mul_leftInvSeq (l : List B) (t : cs.Reflection) (h : t.1 ∈ cs.leftInvSeq l) : @@ -400,7 +418,7 @@ lemma eraseIdx_of_mul_leftInvSeq (l : List B) (t : cs.Reflection) (h : t.1 ∈ c rw[← getD_leftInvSeq_mul_wordProd cs l k] simp [List.getElem?_eq_getElem k.2] -lemma permutationMap_lift_simple (p : B): +lemma permutationMap_lift_simple (p : B) : permutationMap_lift cs (cs.simple p) = cs.permutationMap p := by simp[permutationMap_lift] @@ -409,44 +427,71 @@ lemma permutationMap_lift_of_reflection (t : cs.Reflection) : ∀ (z : ZMod 2), rcases t with ⟨t, t_refl⟩ rcases t_refl with ⟨w, p, rfl⟩ obtain ⟨l, _, rfl⟩ := cs.wordProd_surjective w - have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) - + have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := + IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) induction l with | nil => - simp[permutationMap_lift, permutationMap_ofList, permutationMap, reflection_mem_leftInvSeq_count, conj_of_reflection, eta] + simp[permutationMap_lift, permutationMap, conj_of_reflection, eta] | cons i l h => intro z simp_rw[wordProd_cons cs i l] simp_rw[mul_inv_rev] simp_rw[inv_simple] - simp[permutationMap_lift_simple, mulDef, ← mul_assoc] - simp[permutationMap_lift_simple, mulDef] at h + simp only [permutationMap_lift_simple, mulDef, map_mul, Function.comp_apply] + simp only [permutationMap_lift_simple, mulDef, map_mul, Function.comp_apply] at h nth_rewrite 3 [permutationMap] - simp[conj_of_reflection, ← mul_assoc] - have : IsReflection cs (cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i) := by + conv_lhs => simp [conj_of_reflection, ← mul_assoc] + have : + IsReflection cs + (cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i) := by nth_rewrite 3 [← inv_simple] - have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) - convert_to IsReflection cs (cs.simple i * (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) * (cs.simple i)⁻¹) - simp[inv_simple, mul_assoc] + have : IsReflection cs (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) := + IsReflection.conj (isReflection_simple cs p) (cs.wordProd l) + convert_to + IsReflection cs + (cs.simple i * (cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹) * + (cs.simple i)⁻¹) + · simp[inv_simple, mul_assoc] exact IsReflection.conj this (s i) - rw[h (isReflection_simple cs p) (z + cs.eta i ⟨cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i, this⟩)] - simp[permutationMap, conj_of_reflection] - constructor - · simp[mul_assoc] - · simp[eta, add_assoc] + rw[h (IsReflection.conj (isReflection_simple cs p) (cs.wordProd l)) + (z + cs.eta i + ⟨cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * cs.simple i, + this⟩)] + rw[permutationMap] + apply Prod.ext + · simp[conj_of_reflection, mul_assoc] + · simp only [eta, add_assoc] by_cases h': cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ = 1 - · simp[h'] + · have first_eq : + cs.simple i = + cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * + cs.simple i := by + rw [h'] + simp + rw [if_pos first_eq] have : cs.simple i = cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ := by apply (mul_right_inj (cs.simple i)).mpr at h' simp only[mul_assoc, mul_one] at h' rw[← h'] simp[mul_assoc] - simp[this] + rw [if_pos this] simp[ZMod] - · simp[h'] - by_contra h'' - rw[h''] at h' - simp[mul_assoc] at h' + rfl + · have first_ne : + ¬cs.simple i = + cs.simple i * cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ * + cs.simple i := by + intro h'' + apply h' + have hmul := congrArg (fun x => x * cs.simple i) h'' + simpa [mul_assoc, cs.simple_mul_simple_self] using hmul.symm + have second_ne : ¬cs.simple i = cs.wordProd l * cs.simple p * (cs.wordProd l)⁻¹ := by + intro h'' + apply h' + have hmul := congrArg (fun x => cs.simple i * x) h'' + simpa [mul_assoc, cs.simple_mul_simple_self] using hmul.symm + rw [if_neg first_ne, if_neg second_ne] + simp lemma isLeftInversion_iff_parityReflectionOccurrences_eq_one (l : List B) (t : cs.Reflection) : cs.IsLeftInversion (cs.wordProd l) t.1 ↔ reflection_mem_leftInvSeq_parity cs l t = 1 := by @@ -454,29 +499,29 @@ lemma isLeftInversion_iff_parityReflectionOccurrences_eq_one (l : List B) (t : c · intro h by_contra h' have h'' : reflection_mem_leftInvSeq_parity cs l t = 0 := by - simp [reflection_mem_leftInvSeq_parity] + rw [reflection_mem_leftInvSeq_parity] rw [ZMod.natCast_eq_zero_iff_even] - simp[reflection_mem_leftInvSeq_parity] at h' + rw[reflection_mem_leftInvSeq_parity] at h' rw[ZMod.natCast_eq_one_iff_odd] at h' exact Nat.not_odd_iff_even.mp h' - suffices cs.IsLeftInversion (t.1 * π l) t.1 from by - simp[IsLeftInversion] at this + rw[IsLeftInversion] at this rw[← mul_assoc] at this rcases this with ⟨_, ht⟩ rw[IsReflection.mul_self t.2] at ht simp at ht simp[IsLeftInversion] at h linarith - - suffices permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = ⟨cs.conj_of_reflection t (π l)⁻¹, 1⟩ from by + suffices + permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = + ⟨cs.conj_of_reflection t (π l)⁻¹, 1⟩ from by apply isLeftInversion_of_parityReflectionOccurrences_lift_eq_one cs (t.1 * π l) t rw[permutationMap_lift_mk cs (t.1 * π l)⁻¹ t 0] at this simp at this simp[this.2] - calc - permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = permutationMap_lift cs (π l)⁻¹ (permutationMap_lift cs t.1 ⟨t, 0⟩) := by + permutationMap_lift cs (t.1 * π l)⁻¹ ⟨t, 0⟩ = + permutationMap_lift cs (π l)⁻¹ (permutationMap_lift cs t.1 ⟨t, 0⟩) := by simp[IsReflection.inv t.2] rfl _ = permutationMap_lift cs (π l)⁻¹ ⟨t, 1⟩ := by @@ -487,16 +532,13 @@ lemma isLeftInversion_iff_parityReflectionOccurrences_eq_one (l : List B) (t : c _ = (cs.conj_of_reflection t (cs.wordProd l)⁻¹, 1) := by simp simp[parityReflectionOccurrences_lift_mk, h''] - · exact isLeftInversion_of_parityReflectionOccurrences_eq_one cs l t theorem strongExchangeProperty (l : List B) (t : cs.Reflection) (h' : cs.IsLeftInversion (cs.wordProd l) t.1) : ∃ (k : Fin l.length), t.1 * π l = π (l.eraseIdx k) := by - suffices t.1 ∈ cs.leftInvSeq l from eraseIdx_of_mul_leftInvSeq cs l t this - rw [isLeftInversion_iff_parityReflectionOccurrences_eq_one cs l t] at h' exact isInLeftInvSeq_of_parityReflectionOccurrences_eq_one cs l t h' diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 39f2a9b46b..2f011cb5b1 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -16,8 +16,6 @@ projects: github_repo: bolito2/DemazureOperatorsLean status: verified main_declarations: - - Demazure.Dem - - Demazure.demazure_commutes_adjacent - CoxeterSystem.strongExchangeProperty - CoxeterSystem.matsumoto_reduced main_results: From 9e469ca031dd42d236c4c3a236faba276fdca8fc Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 02:40:06 +0900 Subject: [PATCH 6/8] Clarify conditional Matsumoto result --- LeanPool/projects.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 2f011cb5b1..0d9c43dcf8 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,7 +1,7 @@ projects: - slug: demazureoperatorslean title: Demazure Operators and Lean - summary: Formalizes Demazure operators on multivariate polynomials, together with Coxeter-system strong exchange and Matsumoto reduced-word theorems. + summary: Formalizes Demazure operators on multivariate polynomials, together with Coxeter-system strong exchange and a Matsumoto reduced-word theorem under the imported MatsumotoCondition hypothesis. branch: algebraic combinatorics entry_module: LeanPool.DemazureOperatorsLean authors: @@ -32,7 +32,7 @@ projects: - declaration: CoxeterSystem.strongExchangeProperty informal: Proves the strong exchange property for Coxeter systems. - declaration: CoxeterSystem.matsumoto_reduced - informal: Proves Matsumoto's theorem that reduced words for the same Coxeter group element are connected by braid moves. + informal: Proves, assuming MatsumotoCondition, that reduced words for the same Coxeter group element are connected by braid moves. tags: - algebraic-combinatorics - demazure-operators From ce54d8346f3eb965f87698855c57b81981eb9d5d Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 03:08:06 +0900 Subject: [PATCH 7/8] Add Coxeter source metadata for Demazure import --- LeanPool/DemazureOperatorsLean.lean | 8 ++++++++ LeanPool/projects.yml | 4 +++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index 03221cc40c..1b98307ffa 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -21,3 +21,11 @@ Main declarations: `CoxeterSystem.strongExchangeProperty`, `CoxeterSystem.matsum Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory MSC: 05E05, 13P10, 20F55 -/ + +/-! +The Demazure-operator declarations are sourced to the BGG Schubert-cells paper +listed in the project card. The strong-exchange and Matsumoto declarations are +standard Coxeter-theory results, with source metadata attached to those main +results in `LeanPool/projects.yml` using Humphreys' *Reflection Groups and +Coxeter Groups*. +-/ diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 0d9c43dcf8..06a1bb0dc8 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,7 +1,7 @@ projects: - slug: demazureoperatorslean title: Demazure Operators and Lean - summary: Formalizes Demazure operators on multivariate polynomials, together with Coxeter-system strong exchange and a Matsumoto reduced-word theorem under the imported MatsumotoCondition hypothesis. + summary: Formalizes Demazure operators on multivariate polynomials, together with standard Coxeter-theory strong exchange and a Matsumoto reduced-word theorem under the imported MatsumotoCondition hypothesis. branch: algebraic combinatorics entry_module: LeanPool.DemazureOperatorsLean authors: @@ -31,8 +31,10 @@ projects: informal: Proves that symmetric polynomials act as scalars with respect to Demazure operators. - declaration: CoxeterSystem.strongExchangeProperty informal: Proves the strong exchange property for Coxeter systems. + source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990." - declaration: CoxeterSystem.matsumoto_reduced informal: Proves, assuming MatsumotoCondition, that reduced words for the same Coxeter group element are connected by braid moves. + source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990." tags: - algebraic-combinatorics - demazure-operators From a38d9f2c5203fffed3079f4b32e5d58257807f89 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 08:01:23 +0900 Subject: [PATCH 8/8] Clarify Demazure auxiliary theorem framing --- LeanPool/DemazureOperatorsLean.lean | 11 ++++++----- LeanPool/DemazureOperatorsLean/DemazureAux.lean | 6 +++++- LeanPool/projects.yml | 6 +++--- 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/LeanPool/DemazureOperatorsLean.lean b/LeanPool/DemazureOperatorsLean.lean index 1b98307ffa..6ed0ad0ed3 100644 --- a/LeanPool/DemazureOperatorsLean.lean +++ b/LeanPool/DemazureOperatorsLean.lean @@ -17,15 +17,16 @@ import LeanPool.DemazureOperatorsLean.Matsumoto Source: doi:10.1070/RM1973v028n03ABEH001549 Authors: Óscar Álvarez Sánchez Status: verified -Main declarations: `CoxeterSystem.strongExchangeProperty`, `CoxeterSystem.matsumoto_reduced` +Main declarations: `Demazure.Dem`, `CoxeterSystem.strongExchangeProperty` Tags: algebraic-combinatorics, demazure-operators, polynomials, representation-theory MSC: 05E05, 13P10, 20F55 -/ /-! The Demazure-operator declarations are sourced to the BGG Schubert-cells paper -listed in the project card. The strong-exchange and Matsumoto declarations are -standard Coxeter-theory results, with source metadata attached to those main -results in `LeanPool/projects.yml` using Humphreys' *Reflection Groups and -Coxeter Groups*. +listed in the project card. The strong-exchange declaration is included as +supporting Coxeter theory with source metadata from Humphreys' *Reflection Groups +and Coxeter Groups*. The Matsumoto development is retained as conditional +auxiliary infrastructure because `CoxeterSystem.matsumoto_reduced` assumes the +extra `MatsumotoCondition` hypothesis. -/ diff --git a/LeanPool/DemazureOperatorsLean/DemazureAux.lean b/LeanPool/DemazureOperatorsLean/DemazureAux.lean index c721214afd..fcb8d75358 100644 --- a/LeanPool/DemazureOperatorsLean/DemazureAux.lean +++ b/LeanPool/DemazureOperatorsLean/DemazureAux.lean @@ -16,7 +16,11 @@ variable {n : ℕ} (n_pos : n > 0) (n_gt_1 : n > 1) /- We are going to define the Demazure operator acting on polynomial fractions. For this, we first define a structure to represent these fractions, and then we will quotient it by -the proportionality equivalence relation -/ +the proportionality equivalence relation. + +This local quotient is auxiliary proof infrastructure for the Demazure relations below; it +is not intended as reusable fraction-field or localization theory. +-/ /-- A numerator-denominator representative for a rational expression in the polynomial ring. -/ structure PolyFraction' (n : ℕ) where diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 06a1bb0dc8..f2207587f5 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -1,7 +1,7 @@ projects: - slug: demazureoperatorslean title: Demazure Operators and Lean - summary: Formalizes Demazure operators on multivariate polynomials, together with standard Coxeter-theory strong exchange and a Matsumoto reduced-word theorem under the imported MatsumotoCondition hypothesis. + summary: Formalizes Demazure operators on multivariate polynomials and their nilpotence, braid, commutation, and symmetric-polynomial linearity relations, with auxiliary Coxeter-theory support including strong exchange and a conditional Matsumoto theorem. branch: algebraic combinatorics entry_module: LeanPool.DemazureOperatorsLean authors: @@ -16,8 +16,8 @@ projects: github_repo: bolito2/DemazureOperatorsLean status: verified main_declarations: + - Demazure.Dem - CoxeterSystem.strongExchangeProperty - - CoxeterSystem.matsumoto_reduced main_results: - declaration: Demazure.Dem informal: Defines the Demazure operator as a linear map over the subalgebra of symmetric polynomials. @@ -33,7 +33,7 @@ projects: informal: Proves the strong exchange property for Coxeter systems. source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990." - declaration: CoxeterSystem.matsumoto_reduced - informal: Proves, assuming MatsumotoCondition, that reduced words for the same Coxeter group element are connected by braid moves. + informal: Auxiliary theorem proving, under the extra MatsumotoCondition hypothesis, that reduced words for the same Coxeter group element are connected by braid moves. source_ref: "J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press, 1990." tags: - algebraic-combinatorics