From 8e3d61e7b5c2eeffd6a09ba219e4611e67b4725a Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Mon, 15 Jan 2024 09:13:01 +0100 Subject: [PATCH 01/15] WIP on Bruhat order --- theories/SymGroup/Bruhat.v | 372 +++++++++++++++++++++++++++++++++++++ 1 file changed, 372 insertions(+) create mode 100644 theories/SymGroup/Bruhat.v diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v new file mode 100644 index 00000000..f83dc5c1 --- /dev/null +++ b/theories/SymGroup/Bruhat.v @@ -0,0 +1,372 @@ +(** * Combi.SymGroup.Bruhat_order : The Bruhat order on the Symmetric Group *) +(******************************************************************************) +(* Copyright (C) 2016-2021 Florent Hivert *) +(* *) +(* Distributed under the terms of the GNU General Public License (GPL) *) +(* *) +(* This code is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU *) +(* General Public License for more details. *) +(* *) +(* The full text of the GPL is available at: *) +(* *) +(* http://www.gnu.org/licenses/ *) +(******************************************************************************) +(** * The (strong) Bruhat order on the Symmetric Group + +We define the (strong) Bruhat order on the symmetric group. + +We define the following notations: + +- [s <=B t] == [s] is smaller than [t] for the right weak order. +- [s [| ->]; last by rewrite perm_mx1. +rewrite /perm_mx row_permEsub => Heq. +apply/permP=> /= i; rewrite perm1. +have:= erefl (rowsub s 1%:M i i : R)%R; rewrite {1}Heq !mxE eq_refl /=. +by case: eqP => //= _ /eqP; rewrite oner_eq0. +Qed. + +Lemma perm_mx_inj : injective (@perm_mx R n). +Proof. +move=> s t /(congr1 (mulmx (perm_mx t^-1))) /eqP. +rewrite -!perm_mxM gnorm perm_mx1 perm_mx1P => /eqP/(congr1 (mulg t)). +by rewrite !gnorm. +Qed. + +End PermMX. + +Lemma card_set_ord_leq_lt n i j : + j < n.+1 -> #|[set k : 'I_n | i <= k < j]| = j - i. +Proof. +rewrite cardE /= /enum_mem size_filter -enumT /= => ltin. +rewrite (eq_count (a2 := preim val (fun k => i <= k < j))); + last by move=> l; rewrite !inE. +rewrite -count_map val_enum_ord -size_filter. +by rewrite filter_predI iota_ltn // iota_geq size_iota. +Qed. + +Lemma card_set_ord_lt n i : + i < n.+1 -> #|[set k : 'I_n | k < i]| = i. +Proof. +rewrite [[set k : _ | _]](_ : _ = [set k : 'I_n | 0 <= k & k < i]). + by move/card_set_ord_leq_lt => ->; rewrite subn0. +by apply/setP => /= k; rewrite inE. +Qed. + +Fact Bruhat_display : unit. Proof. exact: tt. Qed. + + +Section GRMatrix. + +Context {n0 : nat}. +#[local] Notation n := n0.+1. +Implicit Type (s t u v : 'S_n). + + +Definition grmx s : 'M_n.+1 := + \matrix_(i < n.+1, j < n.+1) + #|[set k : 'I_n | k < j] :&: [set s k | k : 'I_n & k < i]|. + +Lemma grmxV s : grmx s^-1 = ((grmx s)^T)%R. +Proof. +have sinj := perm_inj (s := s). +have s1inj := perm_inj (s := s^-1). +apply matrixP=> i j; rewrite !mxE. +rewrite -(card_imset _ sinj); congr (fun S : {set _} => #|S|). +rewrite -setP => /= k; rewrite inE. +rewrite -{1}(permKV s k) mem_imset // !inE mem_imset // inE. +rewrite andbC; congr andb. +by rewrite -{2}(permKV s k) mem_imset // inE. +Qed. + +Lemma grmx_pairE s : + grmx s = (\matrix_(i < n.+1, j < n.+1) + #|[set p : 'I_n * 'I_n | + [&& \val p.1 < i, \val p.2 < j & (s p.1 == p.2)]]|)%R. +Proof. +apply/matrixP => i j; rewrite !mxE. +have mkpair_inj : injective (fun k : 'I_n => (s^-1 k, k)) by move=> k l []. +rewrite -(card_imset _ mkpair_inj); congr (fun s : {set _} => #|s|). +apply/setP => [][/= k l]; rewrite inE /=. +apply/imsetP/idP => [[/= m] |]. +rewrite !inE => +[->{k} ->{l}] => /andP[-> /imsetP[k] /=]. + by rewrite inE => + ->; rewrite permKV eq_refl andbT permK. +rewrite andbA andbC => /and3P[/eqP <-{l} leki leskj] /=. +exists (s k); last by rewrite permK. +by rewrite !inE {}leskj /=; apply/imsetP; exists k; rewrite // inE. +Qed. + +(* +Lemma grmxV2 s : grmx s^-1 = ((grmx s)^T)%R. +Proof. +apply/matrixP => /= i j; rewrite !grmx_pairE !mxE /=. +pose swap p : 'I_n * 'I_n := (p.2, p.1). +have swapK : involutive swap by move=> [u v]. +rewrite -(card_imset _ (inv_inj swapK)); congr (fun S : {set _} => #|S|). +apply/setP => /= [][k l]; rewrite !inE. +apply/imsetP/and3P => [[/= m] | /= [lej lei /eqP eqs]]. + by rewrite inE /= => + [-> ->] /= => /and3P[-> -> /eqP <- /=]; rewrite permKV. +by exists (l, k) => //; rewrite inE /= -{2}eqs permK lei lej /=. +Qed. +*) + +Lemma grmxE s (i j : nat) : + i < n.+1 -> j < n.+1 -> + grmx s (inord i) (inord j) = + (\sum_(k < i) \sum_(l < j) (s (inord k) == inord l)%:R)%R. +Proof. +rewrite grmx_pairE mxE !ltnS => lti ltj. +rewrite [RHS](big_ord_widen _ + (fun k => \sum_(l < j) (s (inord k) == inord l)%:R)%R lti). +under eq_bigr => k _ do + rewrite (big_ord_widen _ (fun l => (s (inord k) == inord l)%:R)%R ltj). +rewrite pair_big_dep_idem //= -sum1dep_card. +rewrite -[LHS](eq_bigl (P1 := fun x : 'I_n * 'I_n => + (x.1 < i) && (x.2 < j) && (s x.1 == x.2))); first last. + by move=> k; rewrite -andbA !inordK. +rewrite [LHS]big_mkcondr_idem //=. +apply eq_bigr => [][k l] /= /andP[ltki ltlj]. +by rewrite !inord_val; case eqP. +Qed. + +(** Unused ! Also this is not a characterisation of the grmx. It also + include th growth matrix of alternating sign matrices *) +Definition is_grmx_row (m : 'M[nat]_n.+1) := + [forall i : 'I_n.+1, + [&& (m i ord0 == 0), (m i ord_max == i) & + [forall j : 'I_n.+1, + m i (inord j.-1) <= m i j <= (m i (inord j.-1)).+1]]]. + +Definition is_grmx (m : 'M[nat]_n.+1) := is_grmx_row m && is_grmx_row m^T. + +Lemma is_grmx_rowP s : is_grmx_row (grmx s). +Proof. +have setlt0 : [set i : 'I_n | i < (@ord0 n)] = set0. + by apply/setP => /= x; rewrite !inE. +apply/forallP => /= i; rewrite !mxE; apply/and3P; split. +- by rewrite setlt0 set0I cards0. +- have -> : [set i : 'I_n | i < (@ord_max n)] = [set: 'I_n]. + by apply/setP => /= x; rewrite !inE /= ltn_ord. + by rewrite setTI (card_imset _ (perm_inj (s := s))) card_set_ord_lt. +- apply/forallP => /= j; rewrite !mxE. + move: [set s k | k : 'I_n & _] => /= S. + have /inordK -> : j.-1 < n.+1 by apply(leq_ltn_trans (leq_pred _)). + case: j => [[|j] Hj] /=; first by rewrite setlt0 set0I cards0. + have -> : [set i0 : 'I_n | i0 < j.+1] = inord j |: [set i0 : 'I_n | i0 < j]. + apply/setP => /= k; rewrite !inE -val_eqE /=. + by rewrite inordK // ltnS leq_eqVlt. + apply/andP; split. + + apply/subset_leq_card/subsetP => /= k. + by rewrite !inE => /andP[-> ->]; rewrite orbT. + + have -> : (inord j |: [set i0 : 'I_n| i0 < j]) :&: S = + [set inord j] :&: S :|: [set i0 : 'I_n | i0 < j] :&: S. + by apply/setP => /= k; rewrite !inE Bool.andb_orb_distrib_l. + apply (leq_trans (leq_card_setU _ _)); rewrite -[leqRHS]add1n leq_add2r. + rewrite -[leqRHS](cards1 (@inord n0 j)). + apply/subset_leq_card/subsetP => /= k. + by rewrite !inE => /andP[]. +Qed. + +Lemma is_grmxP s : is_grmx (grmx s). +Proof. by rewrite /is_grmx -grmxV !is_grmx_rowP. Qed. + + +Definition perm_mx_of_grmx (m : 'M_n.+1) : 'M[int]_n := + \matrix_(i < n, j < n) + ( (m (inord i.+1) (inord j.+1))%:Z - (m (inord i) (inord j.+1))%:Z + - (m (inord i.+1) (inord j))%:Z + (m (inord i) (inord j))%:Z )%R. + +Lemma perm_mx_of_grmxP s : perm_mx_of_grmx (grmx s) = perm_mx s. +Proof. +apply/matrixP=> i j. +have lei1 : i.+1 < n.+1 by rewrite ltnS. +have lej1 : j.+1 < n.+1 by rewrite ltnS. +have lei : i < n.+1 by apply ltnW. +have lej : j < n.+1 by apply ltnW. +rewrite [LHS]mxE !grmxE // !mxE !big_ord_recr /= !inord_val. +rewrite !PoszD !opprD !addrA. +set S := (X in (_ + X)%R). +rewrite -/S -!addrA [(-S + _)%R]addrC !addrA addrK {S}. +set S := (X in (X + _ + _ + _ + _)%R). +rewrite -/S [(S + _)%R]addrC addrC -!addrA [(S + _)%R]addrC subrK {S}. +rewrite addrA addrC addrA subrK. +by case: eqP. +Qed. + +Lemma grmx_inj : injective grmx. +Proof. +move=> s t /(congr1 perm_mx_of_grmx); rewrite !perm_mx_of_grmxP. +exact: perm_mx_inj. +Qed. + +Lemma grmx1 i j : grmx 1 i j = minn i j. +Proof. +rewrite mxE (eq_imset (g := id)); last exact: perm1. +rewrite imset_id [_ :&: _](_ : _ = [set k : 'I_n | k < minn i j]); first last. + by apply/setP => k; rewrite !inE ltn_min andbC. +rewrite card_set_ord_lt // ltnS. +exact: (leq_trans (geq_minr i j) (ltn_ord j)). +Qed. + +Lemma grmx_maxperm i j : grmx maxperm i j = i + j - n. +Proof. +rewrite mxE. +rewrite [_ :&: _](_ : _ = [set k : 'I_n | n - i <= k < j]); first last. + apply/setP => /= k; rewrite !inE -{2}(maxpermK k). + rewrite mem_imset; last exact: (inv_inj (@maxpermK _)). + rewrite inE permE /= ltn_subCl //; last exact: (ltn_ord i). + by rewrite ltnS andbC. +by rewrite card_set_ord_leq_lt // subnCBA // -ltnS. +Qed. + +End GRMatrix. + + +Module BruhatOrder. +Section Def. + +Context {n0 : nat}. +#[local] Notation n := n0.+1. +Implicit Type (s t u v : 'S_n). + +#[local] Notation grmx := (@grmx n0). + +Definition Bruhat s t := [forall i, forall j, grmx s i j >= grmx t i j]. + +Lemma BruhatP s t : + reflect (forall i, forall j, grmx s i j >= grmx t i j) (Bruhat s t). +Proof. by apply (iffP forallP) => /= H i; apply/forallP. Qed. + +Fact Bruhat_refl : reflexive Bruhat. +Proof. by move=> s; apply/BruhatP. Qed. +Fact Bruhat_anti : antisymmetric Bruhat. +Proof. +move=>s t /andP[/BruhatP lets /BruhatP lest]. +apply grmx_inj; apply/matrixP=> i j; apply anti_leq. +by rewrite lest lets. +Qed. +Fact Bruhat_trans : transitive Bruhat. +Proof. +move=>t s u /BruhatP lets /BruhatP leut; apply/BruhatP=> i j. +exact: (leq_trans (leut i j) (lets i j)). +Qed. + +#[export] HB.instance Definition _ := Finite.on 'S_n. +#[export] HB.instance Definition _ := + Order.Le_isPOrder.Build Bruhat_display 'S_n + Bruhat_refl Bruhat_anti Bruhat_trans. + +Local Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). + +Fact Bruhat1s s : (1 <=B s). +Proof. +apply/BruhatP => i j; rewrite grmx1 !mxE leq_min. +rewrite -{2}(card_set_ord_lt (ltn_ord i)) -{3}(card_set_ord_lt (ltn_ord j)). +apply/andP; split; last exact/subset_leq_card/subsetIl. +rewrite -[X in _ <= X](card_imset _ (@perm_inj _ s)). +exact/subset_leq_card/subsetIr. +Qed. +#[export] HB.instance Definition _ := + Order.hasBottom.Build Bruhat_display ('S_n) Bruhat1s. + +Fact Bruhat_maxperm s : (s <=B maxperm). +Proof. +apply/BruhatP => i j; rewrite grmx_maxperm !mxE. +rewrite cardsI card_imset; last exact: perm_inj. +rewrite !card_set_ord_lt // addnC; apply: leq_sub2l. +rewrite -[X in _ <= X](card_ord n) -cardsT /=. +exact/subset_leq_card/subsetT. +Qed. + +#[export] HB.instance Definition _ := + Order.hasTop.Build Bruhat_display ('S_n) Bruhat_maxperm. + +End Def. + +Module Exports. +HB.reexport BruhatOrder. + +Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). +Notation "x = grmx t i j) (s <=B t) + := (BruhatP s t). + +Lemma bottom_Bruhat n0 : Order.bottom = (1 : 'S_n0.+1). Proof. by []. Qed. +Lemma top_Bruhat n0 : Order.top = @maxperm n0. Proof. by []. Qed. + +End Exports. +End BruhatOrder. +HB.export BruhatOrder.Exports. + + + +(* + 0 0 0 0 + x + 0 1 1 1 + x + 0 1 2 2 + x + 0 1 2 3 + + +0 0 0 0 0 0 0 0 + x x +0 1 1 1 0 0 1 1 + x x +0 1 1 2 0 1 2 2 + x 0 0 0 0 x +0 1 2 3 x 0 1 2 3 + 0 0 1 1 + x o x + 0 1 1 2 +0 0 0 0 x 0 0 0 0 + x 0 1 2 3 x +0 0 1 1 0 0 0 1 + x x +0 0 1 2 0 1 1 2 + x x +0 1 2 3 0 1 2 3 + + + 0 0 0 0 + x + 0 0 0 1 + x + 0 0 1 2 + x + 0 1 2 3 + + *) From 7528fdef8f39da297cfca16a206ab4ecbd0a3b79 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Wed, 17 Jan 2024 18:15:40 +0100 Subject: [PATCH 02/15] Before big cleanup --- theories/SymGroup/Bruhat.v | 419 +++++++++++++++++++++++++++++++++---- 1 file changed, 374 insertions(+), 45 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index f83dc5c1..2e0236b1 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -26,7 +26,7 @@ We define the following notations: From HB Require Import structures. From mathcomp Require Import all_ssreflect. From mathcomp Require Import fingroup perm morphism presentation. -From mathcomp Require Import ssralg matrix ssrint. +From mathcomp Require Import ssralg matrix. Require Import permcomp tools permuted combclass congr presentSn. Require Import std ordtype. @@ -47,24 +47,351 @@ Section PermMX. Variable (R : semiRingType) (n : nat). Implicit Type (s t : 'S_n). -Lemma perm_mx1P s : (@perm_mx R n s == (1%:M)%R) = (s == 1). +Lemma perm_mx_eq1 s : (@perm_mx R n s == (1%:M)%R) = (s == 1). Proof. apply/eqP/eqP=> [| ->]; last by rewrite perm_mx1. -rewrite /perm_mx row_permEsub => Heq. +rewrite /perm_mx row_permEsub => /esym Heq. apply/permP=> /= i; rewrite perm1. -have:= erefl (rowsub s 1%:M i i : R)%R; rewrite {1}Heq !mxE eq_refl /=. +move/(congr1 (fun m : 'M__ => m i i)): Heq; rewrite !mxE eq_refl /=. by case: eqP => //= _ /eqP; rewrite oner_eq0. Qed. -Lemma perm_mx_inj : injective (@perm_mx R n). +Lemma perm_mx_inj : injective (@perm_mx R n). Proof. -move=> s t /(congr1 (mulmx (perm_mx t^-1))) /eqP. -rewrite -!perm_mxM gnorm perm_mx1 perm_mx1P => /eqP/(congr1 (mulg t)). -by rewrite !gnorm. +move=> s t /(congr1 (mulmx (perm_mx t^-1)))/eqP. +rewrite -!perm_mxM mulVg perm_mx1 perm_mx_eq1 => /eqP/(congr1 (mulg t)). +by rewrite mulgA mulgV mulg1 mul1g. +Qed. + +Lemma is_perm_mx_sumP (m : 'M[nat]_n) : + reflect ((forall (i : 'I_n), \sum_j m i j = 1%R) /\ + (forall (j : 'I_n), \sum_i m i j = 1%R)) + (is_perm_mx m). +Proof. +apply (iffP existsP) => /= [[/= s /eqP ->{m}]| [sum_row sum_col]]. + have byrow : forall s (i : 'I_n), \sum_(j < n) perm_mx s i j = 1%R. + move=> {}s i; rewrite (bigD1 (s i)) //= !mxE eq_refl big1 ?addn0 // => j. + by rewrite !mxE eq_sym => /negbTE ->. + split => i; first exact: byrow. + rewrite -[RHS](byrow s^-1 i); apply eq_bigr => j _. + by rewrite !mxE -[in RHS](inj_eq (@perm_inj _ s)) permKV eq_sym. +have pex i : { j | (m i j == 1%N) && [forall k, (k != j) ==> (m i k == 0%N)] }. + apply sigW; have /eqP/sum_nat_eq1[/= j [_ mij1 mi0]] := sum_row i. + exists j; rewrite {}mij1 /=; apply/forallP => k. + by apply/implyP => /mi0 ->. +have pex_inj : injective (fun i : 'I_n => proj1_sig (pex i)). + move=> /= i j. + case: (pex i) => k /= /andP[/eqP mik _]. + case: (pex j) => kj /= /[swap] <-{kj} /andP[/eqP mjk _]. + have /eqP/sum_nat_eq1[/= i0 [_ mi0k neqi0]] := sum_col k. + have {neqi0} eqi0 l : m l k = 1%N -> l = i0. + by move/eqP; apply/contraTeq => /neqi0 ->. + by rewrite (eqi0 _ mik) (eqi0 _ mjk). +exists (perm pex_inj); apply/eqP/matrixP=> i j; rewrite !mxE permE. +case: (pex i) => k /= /andP[/eqP mik /forallP/= neq0]. +case: eqP => [<-{j} // | /eqP]; rewrite eq_sym. +by have /implyP/[apply]/eqP-> := neq0 j. Qed. End PermMX. +#[local] Lemma lti1 n (i : 'I_n) : i.+1 < n.+1. by rewrite ltnS. Qed. +#[local] Lemma lti n (i : 'I_n) : i < n.+1. exact: (ltnW (lti1 _)). Qed. +#[local] Lemma lei n (i : 'I_n.+1) : i <= n. by rewrite -ltnS. Qed. +Hint Resolve lti1 lti perm_inj lei : core. + +Lemma setIE (T : finType) (pA pB : pred T) : + [set y | pA y & pB y] = [set y | pA y] :&: [set y | pB y]. +Proof. by apply/setP=> x; rewrite !inE. Qed. + +Lemma sum_lt1 n k : k <= n -> \sum_(i < n | i < k) 1 = k. +Proof. +move=> lekn. +rewrite -(big_ord_widen _ (fun => 1%N) lekn). +by rewrite big_const_ord iter_addn_0 mul1n. +Qed. + + +Section MatrixSum. + +Context {n0 : nat}. +#[local] Notation n := n0.+1. +Implicit Type (s t u v : 'S_n). +Implicit Type (m : 'M[nat]_n). +Implicit Type (M : 'M[nat]_n.+1). + + +Definition mxsum m : 'M_n.+1 := + \matrix_(i < n.+1, j < n.+1) + \sum_(k < n | k < i) \sum_(l < n | l < j) m k l. + +Definition mxdiff M : 'M[nat]_n := + \matrix_(i < n, j < n) + ( M (inord i.+1) (inord j.+1) + M (inord i) (inord j) + - M (inord i) (inord j.+1) - M (inord i.+1) (inord j) ). + +Lemma mxsumE m (i j : nat) : + i < n.+1 -> j < n.+1 -> + mxsum m (inord i) (inord j) = + \sum_(k < i) \sum_(l < j) m (inord k) (inord l). +Proof. +rewrite mxE !ltnS => lti ltj. +rewrite [RHS](big_ord_widen _ + (fun k => \sum_(l < j) (m (inord k) (inord l))) lti). +rewrite inordK //; apply eq_bigr => k _. +rewrite (big_ord_widen _ (fun l => (m (inord k) (inord l))) ltj). +rewrite inordK //; apply eq_bigr => l _. +by rewrite !inord_val. +Qed. + +Lemma mxsum_tr m : (mxsum m^T = (mxsum m)^T)%R. +Proof. +apply matrixP=> i j; rewrite !mxE exchange_big_idem //=. +apply: eq_bigr => k ltkj; apply: eq_bigr => l ltli. +by rewrite mxE. +Qed. + +Lemma mxdiff_tr M : (mxdiff M^T = (mxdiff M)^T)%R. +Proof. +apply matrixP=> i j; rewrite !mxE. +Admitted. + +Lemma mxsumK : cancel mxsum mxdiff. +Proof. +move=> m; apply matrixP=> i j; rewrite mxE !mxsumE //. +rewrite !big_ord_recr /= !inord_val. +by rewrite -!addnA [X in X - _ - _]addnC addnK addnC -addnA addnK. +Qed. + +Lemma perm_mxsum_inj : injective (mxsum \o perm_mx). +Proof. exact: (inj_comp (can_inj mxsumK) (@perm_mx_inj _ _)). Qed. + +Lemma perm_mxsumE s i j : + (mxsum \o perm_mx) s i j = \sum_(k < n | (k < i) && (s k < j)) 1%N. +Proof. +rewrite !mxE big_mkcondr_idem //=; apply eq_bigr => k _. +under eq_bigr => l _ do rewrite !mxE /= eq_sym. +case: ltnP => [ltskj | lejsk]. + by rewrite (bigD1 (s k)) //= eq_refl big1 // => l /andP[_ /negbTE->]. +rewrite big1 // => l /leq_trans/(_ lejsk) /ltn_eqF. +by rewrite -(val_eqE l (s k)) => ->. +Qed. + +Lemma perm_mxsum1 i j : mxsum (perm_mx 1) i j = minn i j. +Proof. +rewrite perm_mxsumE. +rewrite (eq_bigl (fun k : 'I_n => k < minn i j)). + exact (sum_lt1 (leq_trans (geq_minr i j) (ltn_ord j))). +by move=> k; rewrite perm1 ltn_min. +Qed. + +Lemma perm_mxsum_maxperm i j : mxsum (perm_mx maxperm) i j = i + j - n. +Proof. +rewrite perm_mxsumE. +rewrite (eq_bigl (fun k : 'I_n => (k < i) && (n - j <= k))); first last. + by move=> k; rewrite permE /= ltn_subCl // ltnS. +rewrite -(big_geq_mkord _ _ (gtn i) (fun => 1%N)) /=. +rewrite -(big_nat_widen _ _ _ predT) //=. +by rewrite big_const_nat iter_addn_0 mul1n subnBA. +Qed. + + +Definition is_pmxsum_row M := + [forall i : 'I_n.+1, + [&& (M i ord0 == 0), (M i ord_max == i) & + [forall j : 'I_n.+1, + M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1]]]. + +Definition is_pmxsum_pos M := + [forall i : 'I_n, forall j : 'I_n, + M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= + M (inord i) (inord j.+1) + M (inord i.+1) (inord j) ]. + +Definition is_pmxsum M := + [&& is_pmxsum_row M, is_pmxsum_row M^T & is_pmxsum_pos M]. + +Lemma is_pmxsum_rowP M : + reflect + [/\ (forall i : 'I_n.+1, M i ord0 = 0), + (forall i : 'I_n.+1, M i ord_max = i) & + forall i j : 'I_n.+1, + M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1] + (is_pmxsum_row M). +Proof. +apply (iffP forallP) => /= [H | [H0 Hmax Hincr i]]. + by split => [i|i|i j]; move/(_ i): H => /and3P[/eqP H0 /eqP Hi /forallP]. +by apply/and3P; split; try exact/eqP; apply/forallP. +Qed. + +Lemma is_pmxsum_posP M : + reflect (forall i j : 'I_n, + M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= + M (inord i) (inord j.+1) + M (inord i.+1) (inord j)) + (is_pmxsum_pos M). +Proof. +apply (iffP forallP) => /= [H i j | H i]. + by move/(_ i)/forallP : H; apply. +by apply/forallP. +Qed. + +Lemma is_perm_mxsum_rowP s : is_pmxsum_row (mxsum (perm_mx s)). +Proof. +apply/is_pmxsum_rowP; split=> [i | i | i j]; rewrite !perm_mxsumE. +- by rewrite sum1dep_card setIE [X in _ :&: X](_ : _ = set0) ?setI0 ?cards0. +- rewrite sum1dep_card setIE [X in _ :&: X](_ : _ = setT). + by rewrite setIT -sum1dep_card sum_lt1. + by apply/setP=> /= k; rewrite !inE ltn_ord. +- apply/andP; split. + apply sub_le_big => //=; first by move=> a b; apply leq_addr. + move=> k /andP[->] /= /leq_trans; apply. + by rewrite inordK ?leq_pred // (leq_ltn_trans (leq_pred _)). + rewrite (bigID (fun k => s k == inord j.-1)) /= addnC. + set P := (P in (\sum_(i < _ | P i) _).+1). + rewrite (eq_bigl P) {}/P; first last. + move=> k; rewrite -andbA; congr (_ && _). + rewrite inordK ?(leq_ltn_trans (leq_pred _)) //. + case: j => [[|j] Hj] //=. + by rewrite [RHS]ltn_neqAle ltnS andbC -val_eqE /= inordK. + rewrite -[X in _ <= X]addn1 leq_add2l. + rewrite [X in _ <= X](_ : 1%N = \sum_(i0 < n | (s i0 == inord j.-1)) 1%N). + by apply sub_le_big => [||k /andP[]] //= a b; apply leq_addr. + rewrite (eq_bigl (pred1 (s^-1 (inord j.-1)))) ?big_pred1_eq // => /= k /=. + by rewrite -(inj_eq (@perm_inj _ s^-1)) permK. +Qed. + +Lemma is_perm_mxsum_posP s : is_pmxsum_pos (mxsum (perm_mx s)). +Proof. +apply/is_pmxsum_posP => i j. +rewrite !mxsumE // !big_ord_recr /= !inord_val. +by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. +Qed. + +Lemma mxsum_perm_mx_is_pmxsum s : is_pmxsum (mxsum (perm_mx s)). +Proof. +rewrite /is_pmxsum -mxsum_tr tr_perm_mx. +by rewrite !is_perm_mxsum_rowP is_perm_mxsum_posP. +Qed. + +Lemma is_pmxsum_tr M : is_pmxsum M = is_pmxsum M^T. +Proof. +suff {M} impl M : is_pmxsum M -> is_pmxsum M^T. + apply/idP/idP; first exact: impl. + by rewrite -{2}(trmxK M); apply: impl. +rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. +by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. +Qed. + +Lemma is_pmxsumP M : is_pmxsum M -> is_perm_mx (mxdiff M). +Proof. +suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. + move=> H; apply/is_perm_mx_sumP; split => i; first exact: rowsum. + transitivity (\sum_j mxdiff M^T i j). + apply eq_bigr => j _. +(* +move/and3P=> [Hrow Hcol Hpos]. + + /forallP/= Hrow /forallP/= Hcol /forallP/= Hpos]. +apply/is_perm_mx_sumP. *) +Admitted. + +End MatrixSum. + + + +Fact Bruhat_display : unit. Proof. exact: tt. Qed. + +Module BruhatOrder. +Section Def. + +Context {n0 : nat}. +#[local] Notation n := n0.+1. +Implicit Type (s t u v : 'S_n). + +#[local] Notation perm_mxsum := (mxsum \o (perm_mx (n := n))). + +Definition Bruhat s t := + [forall i, forall j, perm_mxsum s i j >= perm_mxsum t i j]. + +Lemma BruhatP s t : + reflect (forall i, forall j, perm_mxsum s i j >= perm_mxsum t i j) + (Bruhat s t). +Proof. by apply (iffP forallP) => /= H i; apply/forallP. Qed. + +Fact Bruhat_refl : reflexive Bruhat. +Proof. by move=> s; apply/BruhatP. Qed. +Fact Bruhat_anti : antisymmetric Bruhat. +Proof. +move=>s t /andP[/BruhatP lets /BruhatP lest]. +apply perm_mxsum_inj; apply/matrixP=> i j; apply anti_leq. +by rewrite lest lets. +Qed. +Fact Bruhat_trans : transitive Bruhat. +Proof. +move=>t s u /BruhatP lets /BruhatP leut; apply/BruhatP=> i j. +exact: (leq_trans (leut i j) (lets i j)). +Qed. + +#[export] HB.instance Definition _ := Finite.on 'S_n. +#[export] HB.instance Definition _ := + Order.Le_isPOrder.Build Bruhat_display 'S_n + Bruhat_refl Bruhat_anti Bruhat_trans. + +Local Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). + +Fact Bruhat1s s : 1 <=B s. +Proof. +suff lecoeff t i j : perm_mxsum t i j <= i. + apply/BruhatP => i j; rewrite perm_mxsum1 leq_min lecoeff /=. + rewrite [X in X <= _](_ : _ = (mxsum (perm_mx s))^T j i)%R; last by rewrite !mxE. + by rewrite -mxsum_tr tr_perm_mx lecoeff. +rewrite perm_mxsumE. +have /sum_lt1 {2}<- : i <= n by []. +rewrite [X in _ <= X](bigID (fun k => t k < j)) /=. +exact: leq_addr. +Qed. +#[export] HB.instance Definition _ := + Order.hasBottom.Build Bruhat_display 'S_n Bruhat1s. + +Fact Bruhat_maxperm s : s <=B maxperm. +Proof. +apply/BruhatP => i j; rewrite perm_mxsum_maxperm perm_mxsumE. +rewrite sum1dep_card setIE cardsI. +rewrite -[X in _ <=_ + X - _](card_imset _ (@perm_inj _ s)) /=. +rewrite [imset _ _](_ : _ = [set x : 'I_n | x < j]); first last. + apply/setP => /= k; rewrite inE. + by rewrite -(permKV s k) mem_imset // inE permKV. +rewrite -![in X in _ <= X - _]sum1dep_card !sum_lt1 //; apply: leq_sub2l. +rewrite -[X in _ <= X](card_ord n) -cardsT /=. +exact/subset_leq_card/subsetT. +Qed. + +#[export] HB.instance Definition _ := + Order.hasTop.Build Bruhat_display 'S_n Bruhat_maxperm. + +End Def. + +Module Exports. +HB.reexport BruhatOrder. + +Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). +Notation "x = mxsum (perm_mx t) i j) (s <=B t) + := BruhatP s t. + +Lemma bottom_Bruhat n0 : Order.bottom = (1 : 'S_n0.+1). Proof. by []. Qed. +Lemma top_Bruhat n0 : Order.top = @maxperm n0. Proof. by []. Qed. + +End Exports. +End BruhatOrder. +HB.export BruhatOrder.Exports. + + + + + Lemma card_set_ord_leq_lt n i j : j < n.+1 -> #|[set k : 'I_n | i <= k < j]| = j - i. Proof. @@ -92,6 +419,10 @@ Context {n0 : nat}. #[local] Notation n := n0.+1. Implicit Type (s t u v : 'S_n). +#[local] Lemma lei1 (i : 'I_n) : i.+1 < n.+1. by rewrite ltnS. Qed. +#[local] Lemma lei (i : 'I_n) : i < n.+1. exact: (ltnW (lei1 _)). Qed. +Hint Resolve lei1 lei perm_inj : core. + Definition grmx s : 'M_n.+1 := \matrix_(i < n.+1, j < n.+1) @@ -99,10 +430,8 @@ Definition grmx s : 'M_n.+1 := Lemma grmxV s : grmx s^-1 = ((grmx s)^T)%R. Proof. -have sinj := perm_inj (s := s). -have s1inj := perm_inj (s := s^-1). apply matrixP=> i j; rewrite !mxE. -rewrite -(card_imset _ sinj); congr (fun S : {set _} => #|S|). +rewrite -(card_imset _ (@perm_inj _ s)); congr (fun S : {set _} => #|S|). rewrite -setP => /= k; rewrite inE. rewrite -{1}(permKV s k) mem_imset // !inE mem_imset // inE. rewrite andbC; congr andb. @@ -143,13 +472,13 @@ Qed. Lemma grmxE s (i j : nat) : i < n.+1 -> j < n.+1 -> grmx s (inord i) (inord j) = - (\sum_(k < i) \sum_(l < j) (s (inord k) == inord l)%:R)%R. + \sum_(k < i) \sum_(l < j) (s (inord k) == inord l). Proof. rewrite grmx_pairE mxE !ltnS => lti ltj. rewrite [RHS](big_ord_widen _ - (fun k => \sum_(l < j) (s (inord k) == inord l)%:R)%R lti). + (fun k => \sum_(l < j) (s (inord k) == inord l)) lti). under eq_bigr => k _ do - rewrite (big_ord_widen _ (fun l => (s (inord k) == inord l)%:R)%R ltj). + rewrite (big_ord_widen _ (fun l => (s (inord k) == inord l) : nat) ltj). rewrite pair_big_dep_idem //= -sum1dep_card. rewrite -[LHS](eq_bigl (P1 := fun x : 'I_n * 'I_n => (x.1 < i) && (x.2 < j) && (s x.1 == x.2))); first last. @@ -159,15 +488,21 @@ apply eq_bigr => [][k l] /= /andP[ltki ltlj]. by rewrite !inord_val; case eqP. Qed. -(** Unused ! Also this is not a characterisation of the grmx. It also - include th growth matrix of alternating sign matrices *) + Definition is_grmx_row (m : 'M[nat]_n.+1) := [forall i : 'I_n.+1, [&& (m i ord0 == 0), (m i ord_max == i) & [forall j : 'I_n.+1, m i (inord j.-1) <= m i j <= (m i (inord j.-1)).+1]]]. -Definition is_grmx (m : 'M[nat]_n.+1) := is_grmx_row m && is_grmx_row m^T. +Definition is_grmx_pos (m : 'M_n.+1) := + [forall i : 'I_n, forall j : 'I_n, + m (inord i.+1) (inord j.+1) + m (inord i) (inord j) >= + m (inord i) (inord j.+1) + m (inord i.+1) (inord j) ]. + +Definition is_grmx (m : 'M[nat]_n.+1) := + [&& is_grmx_row m, is_grmx_row m^T & is_grmx_pos m]. + Lemma is_grmx_rowP s : is_grmx_row (grmx s). Proof. @@ -177,7 +512,7 @@ apply/forallP => /= i; rewrite !mxE; apply/and3P; split. - by rewrite setlt0 set0I cards0. - have -> : [set i : 'I_n | i < (@ord_max n)] = [set: 'I_n]. by apply/setP => /= x; rewrite !inE /= ltn_ord. - by rewrite setTI (card_imset _ (perm_inj (s := s))) card_set_ord_lt. + by rewrite setTI (card_imset _ (@perm_inj _ s)) card_set_ord_lt. - apply/forallP => /= j; rewrite !mxE. move: [set s k | k : 'I_n & _] => /= S. have /inordK -> : j.-1 < n.+1 by apply(leq_ltn_trans (leq_pred _)). @@ -197,32 +532,34 @@ apply/forallP => /= i; rewrite !mxE; apply/and3P; split. by rewrite !inE => /andP[]. Qed. -Lemma is_grmxP s : is_grmx (grmx s). -Proof. by rewrite /is_grmx -grmxV !is_grmx_rowP. Qed. +Lemma is_grmx_posP s : is_grmx_pos (grmx s). +Proof. +apply/forallP => /= i; apply/forallP => /= j. +rewrite !grmxE // !big_ord_recr /= !inord_val. +by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. +Qed. -Definition perm_mx_of_grmx (m : 'M_n.+1) : 'M[int]_n := +Lemma is_grmxP s : is_grmx (grmx s). +Proof. by rewrite /is_grmx -grmxV !is_grmx_rowP is_grmx_posP. Qed. + +Definition perm_mx_of_grmx (m : 'M_n.+1) : 'M[nat]_n := \matrix_(i < n, j < n) - ( (m (inord i.+1) (inord j.+1))%:Z - (m (inord i) (inord j.+1))%:Z - - (m (inord i.+1) (inord j))%:Z + (m (inord i) (inord j))%:Z )%R. + ( m (inord i.+1) (inord j.+1) - m (inord i) (inord j.+1) + + m (inord i) (inord j) - m (inord i.+1) (inord j) ). Lemma perm_mx_of_grmxP s : perm_mx_of_grmx (grmx s) = perm_mx s. Proof. apply/matrixP=> i j. -have lei1 : i.+1 < n.+1 by rewrite ltnS. -have lej1 : j.+1 < n.+1 by rewrite ltnS. -have lei : i < n.+1 by apply ltnW. -have lej : j < n.+1 by apply ltnW. rewrite [LHS]mxE !grmxE // !mxE !big_ord_recr /= !inord_val. -rewrite !PoszD !opprD !addrA. -set S := (X in (_ + X)%R). -rewrite -/S -!addrA [(-S + _)%R]addrC !addrA addrK {S}. -set S := (X in (X + _ + _ + _ + _)%R). -rewrite -/S [(S + _)%R]addrC addrC -!addrA [(S + _)%R]addrC subrK {S}. -rewrite addrA addrC addrA subrK. +rewrite [X in X - _ + _ - _]addnC addnK. +rewrite [X in _ - X]addnC subnDr addnC addnK. by case: eqP. Qed. +Lemma is_perm_mx_grmx m : is_grmx m -> is_perm_mx m. +Admitted. + Lemma grmx_inj : injective grmx. Proof. move=> s t /(congr1 perm_mx_of_grmx); rewrite !perm_mx_of_grmxP. @@ -338,12 +675,8 @@ HB.export BruhatOrder.Exports. 0 1 1 1 x 0 1 2 2 - x - 0 1 2 3 - - -0 0 0 0 0 0 0 0 - x x +0 0 0 0 x 0 0 0 0 + x 0 1 2 3 x 0 1 1 1 0 0 1 1 x x 0 1 1 2 0 1 2 2 @@ -357,12 +690,8 @@ HB.export BruhatOrder.Exports. 0 0 1 1 0 0 0 1 x x 0 0 1 2 0 1 1 2 - x x -0 1 2 3 0 1 2 3 - - - 0 0 0 0 - x + x 0 0 0 0 x +0 1 2 3 x 0 1 2 3 0 0 0 1 x 0 0 1 2 From f47ec806e871eaf97e0551322693e4eba9917991 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 18 Jan 2024 03:32:46 +0100 Subject: [PATCH 03/15] Characterization of permutation growth matrices --- theories/SymGroup/Bruhat.v | 354 ++++++------------------------------- 1 file changed, 56 insertions(+), 298 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 2e0236b1..25506e4c 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -42,6 +42,19 @@ Reserved Notation "s '<=B' t" (at level 70, t at next level). Reserved Notation "s ' + {in [pred i | n <= i <= m] &, {homo f : x y / x <= y}} -> + \sum_(n <= k < m) (f k.+1 - f k) = f m - f n. +Proof. +move=> nm fle; rewrite (telescope_big (fun i j => f j - f i)). + by case: ltngtP nm => // ->; rewrite subnn. +move=> k /andP[nk km] /=; rewrite addnBAC ?fle 1?ltnW// ?subnKC// ?fle// inE. +- by rewrite (ltnW nk) ltnW. +- by rewrite ltnW // (ltn_trans nk). +- by rewrite leqnn ltnW // (ltn_trans nk). +- by rewrite ltnW //= ltnW. +Qed. + Section PermMX. Variable (R : semiRingType) (n : nat). @@ -152,9 +165,7 @@ by rewrite mxE. Qed. Lemma mxdiff_tr M : (mxdiff M^T = (mxdiff M)^T)%R. -Proof. -apply matrixP=> i j; rewrite !mxE. -Admitted. +Proof. by apply matrixP=> i j; rewrite !mxE -subnDAC subnDA. Qed. Lemma mxsumK : cancel mxsum mxdiff. Proof. @@ -195,17 +206,18 @@ rewrite -(big_nat_widen _ _ _ predT) //=. by rewrite big_const_nat iter_addn_0 mul1n subnBA. Qed. +Local Notation H i := (@inord n i). Definition is_pmxsum_row M := [forall i : 'I_n.+1, [&& (M i ord0 == 0), (M i ord_max == i) & [forall j : 'I_n.+1, - M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1]]]. + M i (H j.-1) <= M i j <= (M i (H j.-1)).+1]]]. Definition is_pmxsum_pos M := [forall i : 'I_n, forall j : 'I_n, - M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= - M (inord i) (inord j.+1) + M (inord i.+1) (inord j) ]. + M (H i.+1) (H j.+1) + M (H i) (H j) >= + M (H i) (H j.+1) + M (H i.+1) (H j) ]. Definition is_pmxsum M := [&& is_pmxsum_row M, is_pmxsum_row M^T & is_pmxsum_pos M]. @@ -215,7 +227,7 @@ Lemma is_pmxsum_rowP M : [/\ (forall i : 'I_n.+1, M i ord0 = 0), (forall i : 'I_n.+1, M i ord_max = i) & forall i j : 'I_n.+1, - M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1] + M i (H j.-1) <= M i j <= (M i (H j.-1)).+1] (is_pmxsum_row M). Proof. apply (iffP forallP) => /= [H | [H0 Hmax Hincr i]]. @@ -225,8 +237,8 @@ Qed. Lemma is_pmxsum_posP M : reflect (forall i j : 'I_n, - M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= - M (inord i) (inord j.+1) + M (inord i.+1) (inord j)) + M (H i.+1) (H j.+1) + M (H i) (H j) >= + M (H i) (H j.+1) + M (H i.+1) (H j)) (is_pmxsum_pos M). Proof. apply (iffP forallP) => /= [H i j | H i]. @@ -272,27 +284,53 @@ rewrite /is_pmxsum -mxsum_tr tr_perm_mx. by rewrite !is_perm_mxsum_rowP is_perm_mxsum_posP. Qed. -Lemma is_pmxsum_tr M : is_pmxsum M = is_pmxsum M^T. +Lemma is_pmxsum_tr M : is_pmxsum M^T = is_pmxsum M. Proof. suff {M} impl M : is_pmxsum M -> is_pmxsum M^T. - apply/idP/idP; first exact: impl. + apply/idP/idP; last exact: impl. by rewrite -{2}(trmxK M); apply: impl. rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. Qed. +Lemma bounded_le_homo (m n : nat) f : + (forall i, m <= i < n -> f i <= f i.+1) -> + {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}. +Proof. +move=> H i j; rewrite !inE /= => lein. +elim: j => [_ |j IHj]; first by rewrite leqn0 => /eqP ->. +move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij]. +have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply. +by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW. +Qed. + Lemma is_pmxsumP M : is_pmxsum M -> is_perm_mx (mxdiff M). Proof. suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. move=> H; apply/is_perm_mx_sumP; split => i; first exact: rowsum. transitivity (\sum_j mxdiff M^T i j). - apply eq_bigr => j _. -(* -move/and3P=> [Hrow Hcol Hpos]. - - /forallP/= Hrow /forallP/= Hcol /forallP/= Hpos]. -apply/is_perm_mx_sumP. *) -Admitted. + by apply eq_bigr => j _; rewrite mxdiff_tr [RHS]mxE. + by apply: rowsum; rewrite is_pmxsum_tr. +move/and3P=> [/is_pmxsum_rowP[R0 Rmax _] /is_pmxsum_rowP[_ _ Cincr] + /is_pmxsum_posP Mpos]. +have {}Cincr j : j <= n -> M (H i) (H j) <= M (H i.+1) (H j). + by move/(_ (H j) (H i.+1)): Cincr; rewrite !mxE inordK // => /andP[]. +pose f j := M (H i.+1) (H j) - M (H i) (H j). +have {Mpos} /(telescope_sumn_in2 (leq0n _)) : + {in [pred i | 0 <= i & i <= n] &, {homo f : x y / x <= y}}. + apply: bounded_le_homo => j /= ltjn; rewrite {}/f. + rewrite leq_subLR addnBA; last exact: Cincr. + move/(_ i (Ordinal ltjn)): Mpos => /= Mpos. + rewrite leq_subRL [X in _ <= X]addnC //. + exact: (leq_trans (leq_addr _ _) Mpos). +rewrite {}/f /=. +have -> : H 0 = ord0 :> 'I_n.+1 by apply val_inj; rewrite /= inordK. +have -> : H n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. +rewrite !{}R0 !subn0 !{}Rmax !inordK // subSnn /= natr1E => <-. +rewrite big_mkord; apply eq_bigr => j _. +rewrite mxE subnBA; last exact/Cincr/ltnW. +congr (_ - _); rewrite addnBAC //; exact: Cincr. +Qed. End MatrixSum. @@ -389,286 +427,6 @@ End BruhatOrder. HB.export BruhatOrder.Exports. - - - -Lemma card_set_ord_leq_lt n i j : - j < n.+1 -> #|[set k : 'I_n | i <= k < j]| = j - i. -Proof. -rewrite cardE /= /enum_mem size_filter -enumT /= => ltin. -rewrite (eq_count (a2 := preim val (fun k => i <= k < j))); - last by move=> l; rewrite !inE. -rewrite -count_map val_enum_ord -size_filter. -by rewrite filter_predI iota_ltn // iota_geq size_iota. -Qed. - -Lemma card_set_ord_lt n i : - i < n.+1 -> #|[set k : 'I_n | k < i]| = i. -Proof. -rewrite [[set k : _ | _]](_ : _ = [set k : 'I_n | 0 <= k & k < i]). - by move/card_set_ord_leq_lt => ->; rewrite subn0. -by apply/setP => /= k; rewrite inE. -Qed. - -Fact Bruhat_display : unit. Proof. exact: tt. Qed. - - -Section GRMatrix. - -Context {n0 : nat}. -#[local] Notation n := n0.+1. -Implicit Type (s t u v : 'S_n). - -#[local] Lemma lei1 (i : 'I_n) : i.+1 < n.+1. by rewrite ltnS. Qed. -#[local] Lemma lei (i : 'I_n) : i < n.+1. exact: (ltnW (lei1 _)). Qed. -Hint Resolve lei1 lei perm_inj : core. - - -Definition grmx s : 'M_n.+1 := - \matrix_(i < n.+1, j < n.+1) - #|[set k : 'I_n | k < j] :&: [set s k | k : 'I_n & k < i]|. - -Lemma grmxV s : grmx s^-1 = ((grmx s)^T)%R. -Proof. -apply matrixP=> i j; rewrite !mxE. -rewrite -(card_imset _ (@perm_inj _ s)); congr (fun S : {set _} => #|S|). -rewrite -setP => /= k; rewrite inE. -rewrite -{1}(permKV s k) mem_imset // !inE mem_imset // inE. -rewrite andbC; congr andb. -by rewrite -{2}(permKV s k) mem_imset // inE. -Qed. - -Lemma grmx_pairE s : - grmx s = (\matrix_(i < n.+1, j < n.+1) - #|[set p : 'I_n * 'I_n | - [&& \val p.1 < i, \val p.2 < j & (s p.1 == p.2)]]|)%R. -Proof. -apply/matrixP => i j; rewrite !mxE. -have mkpair_inj : injective (fun k : 'I_n => (s^-1 k, k)) by move=> k l []. -rewrite -(card_imset _ mkpair_inj); congr (fun s : {set _} => #|s|). -apply/setP => [][/= k l]; rewrite inE /=. -apply/imsetP/idP => [[/= m] |]. -rewrite !inE => +[->{k} ->{l}] => /andP[-> /imsetP[k] /=]. - by rewrite inE => + ->; rewrite permKV eq_refl andbT permK. -rewrite andbA andbC => /and3P[/eqP <-{l} leki leskj] /=. -exists (s k); last by rewrite permK. -by rewrite !inE {}leskj /=; apply/imsetP; exists k; rewrite // inE. -Qed. - -(* -Lemma grmxV2 s : grmx s^-1 = ((grmx s)^T)%R. -Proof. -apply/matrixP => /= i j; rewrite !grmx_pairE !mxE /=. -pose swap p : 'I_n * 'I_n := (p.2, p.1). -have swapK : involutive swap by move=> [u v]. -rewrite -(card_imset _ (inv_inj swapK)); congr (fun S : {set _} => #|S|). -apply/setP => /= [][k l]; rewrite !inE. -apply/imsetP/and3P => [[/= m] | /= [lej lei /eqP eqs]]. - by rewrite inE /= => + [-> ->] /= => /and3P[-> -> /eqP <- /=]; rewrite permKV. -by exists (l, k) => //; rewrite inE /= -{2}eqs permK lei lej /=. -Qed. -*) - -Lemma grmxE s (i j : nat) : - i < n.+1 -> j < n.+1 -> - grmx s (inord i) (inord j) = - \sum_(k < i) \sum_(l < j) (s (inord k) == inord l). -Proof. -rewrite grmx_pairE mxE !ltnS => lti ltj. -rewrite [RHS](big_ord_widen _ - (fun k => \sum_(l < j) (s (inord k) == inord l)) lti). -under eq_bigr => k _ do - rewrite (big_ord_widen _ (fun l => (s (inord k) == inord l) : nat) ltj). -rewrite pair_big_dep_idem //= -sum1dep_card. -rewrite -[LHS](eq_bigl (P1 := fun x : 'I_n * 'I_n => - (x.1 < i) && (x.2 < j) && (s x.1 == x.2))); first last. - by move=> k; rewrite -andbA !inordK. -rewrite [LHS]big_mkcondr_idem //=. -apply eq_bigr => [][k l] /= /andP[ltki ltlj]. -by rewrite !inord_val; case eqP. -Qed. - - -Definition is_grmx_row (m : 'M[nat]_n.+1) := - [forall i : 'I_n.+1, - [&& (m i ord0 == 0), (m i ord_max == i) & - [forall j : 'I_n.+1, - m i (inord j.-1) <= m i j <= (m i (inord j.-1)).+1]]]. - -Definition is_grmx_pos (m : 'M_n.+1) := - [forall i : 'I_n, forall j : 'I_n, - m (inord i.+1) (inord j.+1) + m (inord i) (inord j) >= - m (inord i) (inord j.+1) + m (inord i.+1) (inord j) ]. - -Definition is_grmx (m : 'M[nat]_n.+1) := - [&& is_grmx_row m, is_grmx_row m^T & is_grmx_pos m]. - - -Lemma is_grmx_rowP s : is_grmx_row (grmx s). -Proof. -have setlt0 : [set i : 'I_n | i < (@ord0 n)] = set0. - by apply/setP => /= x; rewrite !inE. -apply/forallP => /= i; rewrite !mxE; apply/and3P; split. -- by rewrite setlt0 set0I cards0. -- have -> : [set i : 'I_n | i < (@ord_max n)] = [set: 'I_n]. - by apply/setP => /= x; rewrite !inE /= ltn_ord. - by rewrite setTI (card_imset _ (@perm_inj _ s)) card_set_ord_lt. -- apply/forallP => /= j; rewrite !mxE. - move: [set s k | k : 'I_n & _] => /= S. - have /inordK -> : j.-1 < n.+1 by apply(leq_ltn_trans (leq_pred _)). - case: j => [[|j] Hj] /=; first by rewrite setlt0 set0I cards0. - have -> : [set i0 : 'I_n | i0 < j.+1] = inord j |: [set i0 : 'I_n | i0 < j]. - apply/setP => /= k; rewrite !inE -val_eqE /=. - by rewrite inordK // ltnS leq_eqVlt. - apply/andP; split. - + apply/subset_leq_card/subsetP => /= k. - by rewrite !inE => /andP[-> ->]; rewrite orbT. - + have -> : (inord j |: [set i0 : 'I_n| i0 < j]) :&: S = - [set inord j] :&: S :|: [set i0 : 'I_n | i0 < j] :&: S. - by apply/setP => /= k; rewrite !inE Bool.andb_orb_distrib_l. - apply (leq_trans (leq_card_setU _ _)); rewrite -[leqRHS]add1n leq_add2r. - rewrite -[leqRHS](cards1 (@inord n0 j)). - apply/subset_leq_card/subsetP => /= k. - by rewrite !inE => /andP[]. -Qed. - - -Lemma is_grmx_posP s : is_grmx_pos (grmx s). -Proof. -apply/forallP => /= i; apply/forallP => /= j. -rewrite !grmxE // !big_ord_recr /= !inord_val. -by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. -Qed. - -Lemma is_grmxP s : is_grmx (grmx s). -Proof. by rewrite /is_grmx -grmxV !is_grmx_rowP is_grmx_posP. Qed. - -Definition perm_mx_of_grmx (m : 'M_n.+1) : 'M[nat]_n := - \matrix_(i < n, j < n) - ( m (inord i.+1) (inord j.+1) - m (inord i) (inord j.+1) - + m (inord i) (inord j) - m (inord i.+1) (inord j) ). - -Lemma perm_mx_of_grmxP s : perm_mx_of_grmx (grmx s) = perm_mx s. -Proof. -apply/matrixP=> i j. -rewrite [LHS]mxE !grmxE // !mxE !big_ord_recr /= !inord_val. -rewrite [X in X - _ + _ - _]addnC addnK. -rewrite [X in _ - X]addnC subnDr addnC addnK. -by case: eqP. -Qed. - -Lemma is_perm_mx_grmx m : is_grmx m -> is_perm_mx m. -Admitted. - -Lemma grmx_inj : injective grmx. -Proof. -move=> s t /(congr1 perm_mx_of_grmx); rewrite !perm_mx_of_grmxP. -exact: perm_mx_inj. -Qed. - -Lemma grmx1 i j : grmx 1 i j = minn i j. -Proof. -rewrite mxE (eq_imset (g := id)); last exact: perm1. -rewrite imset_id [_ :&: _](_ : _ = [set k : 'I_n | k < minn i j]); first last. - by apply/setP => k; rewrite !inE ltn_min andbC. -rewrite card_set_ord_lt // ltnS. -exact: (leq_trans (geq_minr i j) (ltn_ord j)). -Qed. - -Lemma grmx_maxperm i j : grmx maxperm i j = i + j - n. -Proof. -rewrite mxE. -rewrite [_ :&: _](_ : _ = [set k : 'I_n | n - i <= k < j]); first last. - apply/setP => /= k; rewrite !inE -{2}(maxpermK k). - rewrite mem_imset; last exact: (inv_inj (@maxpermK _)). - rewrite inE permE /= ltn_subCl //; last exact: (ltn_ord i). - by rewrite ltnS andbC. -by rewrite card_set_ord_leq_lt // subnCBA // -ltnS. -Qed. - -End GRMatrix. - - -Module BruhatOrder. -Section Def. - -Context {n0 : nat}. -#[local] Notation n := n0.+1. -Implicit Type (s t u v : 'S_n). - -#[local] Notation grmx := (@grmx n0). - -Definition Bruhat s t := [forall i, forall j, grmx s i j >= grmx t i j]. - -Lemma BruhatP s t : - reflect (forall i, forall j, grmx s i j >= grmx t i j) (Bruhat s t). -Proof. by apply (iffP forallP) => /= H i; apply/forallP. Qed. - -Fact Bruhat_refl : reflexive Bruhat. -Proof. by move=> s; apply/BruhatP. Qed. -Fact Bruhat_anti : antisymmetric Bruhat. -Proof. -move=>s t /andP[/BruhatP lets /BruhatP lest]. -apply grmx_inj; apply/matrixP=> i j; apply anti_leq. -by rewrite lest lets. -Qed. -Fact Bruhat_trans : transitive Bruhat. -Proof. -move=>t s u /BruhatP lets /BruhatP leut; apply/BruhatP=> i j. -exact: (leq_trans (leut i j) (lets i j)). -Qed. - -#[export] HB.instance Definition _ := Finite.on 'S_n. -#[export] HB.instance Definition _ := - Order.Le_isPOrder.Build Bruhat_display 'S_n - Bruhat_refl Bruhat_anti Bruhat_trans. - -Local Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). - -Fact Bruhat1s s : (1 <=B s). -Proof. -apply/BruhatP => i j; rewrite grmx1 !mxE leq_min. -rewrite -{2}(card_set_ord_lt (ltn_ord i)) -{3}(card_set_ord_lt (ltn_ord j)). -apply/andP; split; last exact/subset_leq_card/subsetIl. -rewrite -[X in _ <= X](card_imset _ (@perm_inj _ s)). -exact/subset_leq_card/subsetIr. -Qed. -#[export] HB.instance Definition _ := - Order.hasBottom.Build Bruhat_display ('S_n) Bruhat1s. - -Fact Bruhat_maxperm s : (s <=B maxperm). -Proof. -apply/BruhatP => i j; rewrite grmx_maxperm !mxE. -rewrite cardsI card_imset; last exact: perm_inj. -rewrite !card_set_ord_lt // addnC; apply: leq_sub2l. -rewrite -[X in _ <= X](card_ord n) -cardsT /=. -exact/subset_leq_card/subsetT. -Qed. - -#[export] HB.instance Definition _ := - Order.hasTop.Build Bruhat_display ('S_n) Bruhat_maxperm. - -End Def. - -Module Exports. -HB.reexport BruhatOrder. - -Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). -Notation "x = grmx t i j) (s <=B t) - := (BruhatP s t). - -Lemma bottom_Bruhat n0 : Order.bottom = (1 : 'S_n0.+1). Proof. by []. Qed. -Lemma top_Bruhat n0 : Order.top = @maxperm n0. Proof. by []. Qed. - -End Exports. -End BruhatOrder. -HB.export BruhatOrder.Exports. - - - (* 0 0 0 0 x From 62b0c83476630c4bae67a29b528d75f6949c3a1a Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 18 Jan 2024 17:23:49 +0100 Subject: [PATCH 04/15] Better notations --- theories/SymGroup/Bruhat.v | 70 ++++++++++++++++++-------------------- 1 file changed, 34 insertions(+), 36 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 25506e4c..7b6c299d 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -42,6 +42,18 @@ Reserved Notation "s '<=B' t" (at level 70, t at next level). Reserved Notation "s ' f i <= f i.+1) -> + {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}. +Proof. +move=> H i j; rewrite !inE /= => lein. +elim: j => [_ |j IHj]; first by rewrite leqn0 => /eqP ->. +move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij]. +have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply. +by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW. +Qed. + Lemma telescope_sumn_in2 n m f : n <= m -> {in [pred i | n <= i <= m] &, {homo f : x y / x <= y}} -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n. @@ -206,18 +218,16 @@ rewrite -(big_nat_widen _ _ _ predT) //=. by rewrite big_const_nat iter_addn_0 mul1n subnBA. Qed. -Local Notation H i := (@inord n i). - Definition is_pmxsum_row M := [forall i : 'I_n.+1, [&& (M i ord0 == 0), (M i ord_max == i) & [forall j : 'I_n.+1, - M i (H j.-1) <= M i j <= (M i (H j.-1)).+1]]]. + M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1]]]. Definition is_pmxsum_pos M := [forall i : 'I_n, forall j : 'I_n, - M (H i.+1) (H j.+1) + M (H i) (H j) >= - M (H i) (H j.+1) + M (H i.+1) (H j) ]. + M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= + M (inord i) (inord j.+1) + M (inord i.+1) (inord j) ]. Definition is_pmxsum M := [&& is_pmxsum_row M, is_pmxsum_row M^T & is_pmxsum_pos M]. @@ -227,7 +237,7 @@ Lemma is_pmxsum_rowP M : [/\ (forall i : 'I_n.+1, M i ord0 = 0), (forall i : 'I_n.+1, M i ord_max = i) & forall i j : 'I_n.+1, - M i (H j.-1) <= M i j <= (M i (H j.-1)).+1] + M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1] (is_pmxsum_row M). Proof. apply (iffP forallP) => /= [H | [H0 Hmax Hincr i]]. @@ -237,8 +247,8 @@ Qed. Lemma is_pmxsum_posP M : reflect (forall i j : 'I_n, - M (H i.+1) (H j.+1) + M (H i) (H j) >= - M (H i) (H j.+1) + M (H i.+1) (H j)) + M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= + M (inord i) (inord j.+1) + M (inord i.+1) (inord j)) (is_pmxsum_pos M). Proof. apply (iffP forallP) => /= [H i j | H i]. @@ -293,17 +303,6 @@ rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. Qed. -Lemma bounded_le_homo (m n : nat) f : - (forall i, m <= i < n -> f i <= f i.+1) -> - {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}. -Proof. -move=> H i j; rewrite !inE /= => lein. -elim: j => [_ |j IHj]; first by rewrite leqn0 => /eqP ->. -move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij]. -have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply. -by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW. -Qed. - Lemma is_pmxsumP M : is_pmxsum M -> is_perm_mx (mxdiff M). Proof. suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. @@ -313,23 +312,22 @@ suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. by apply: rowsum; rewrite is_pmxsum_tr. move/and3P=> [/is_pmxsum_rowP[R0 Rmax _] /is_pmxsum_rowP[_ _ Cincr] /is_pmxsum_posP Mpos]. -have {}Cincr j : j <= n -> M (H i) (H j) <= M (H i.+1) (H j). - by move/(_ (H j) (H i.+1)): Cincr; rewrite !mxE inordK // => /andP[]. -pose f j := M (H i.+1) (H j) - M (H i) (H j). -have {Mpos} /(telescope_sumn_in2 (leq0n _)) : - {in [pred i | 0 <= i & i <= n] &, {homo f : x y / x <= y}}. - apply: bounded_le_homo => j /= ltjn; rewrite {}/f. - rewrite leq_subLR addnBA; last exact: Cincr. - move/(_ i (Ordinal ltjn)): Mpos => /= Mpos. - rewrite leq_subRL [X in _ <= X]addnC //. - exact: (leq_trans (leq_addr _ _) Mpos). -rewrite {}/f /=. -have -> : H 0 = ord0 :> 'I_n.+1 by apply val_inj; rewrite /= inordK. -have -> : H n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. -rewrite !{}R0 !subn0 !{}Rmax !inordK // subSnn /= natr1E => <-. -rewrite big_mkord; apply eq_bigr => j _. -rewrite mxE subnBA; last exact/Cincr/ltnW. -congr (_ - _); rewrite addnBAC //; exact: Cincr. +have {}Cincr j : j <= n -> M (inord i) (inord j) <= M (inord i.+1) (inord j). + by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // => /andP[]. +pose f j := M (inord i.+1) (inord j) - M (inord i) (inord j). +transitivity (\sum_(0 <= k < n) (f k.+1 - f k)). + rewrite big_mkord; apply eq_bigr => j _. + rewrite mxE subnBA; last exact/Cincr/ltnW. + by congr (_ - _); rewrite addnBAC //; exact: Cincr. +rewrite telescope_sumn_in2 // {}/f. + have -> : inord 0 = ord0 :> 'I_n.+1 by apply val_inj; rewrite /= inordK. + have -> : inord n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. + by rewrite !R0 !subn0 !Rmax !inordK // subSnn /= natr1E. +apply: bounded_le_homo => j /= ltjn {R0 Rmax}. +rewrite leq_subLR addnBA; last exact: Cincr. +move/(_ i (Ordinal ltjn)): Mpos => /= Mpos. +rewrite leq_subRL [X in _ <= X]addnC //. +exact: (leq_trans (leq_addr _ _) Mpos). Qed. End MatrixSum. From 42d5654137ef340e06062888a0a3aa6db2d7a4d0 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 19 Jan 2024 00:52:21 +0100 Subject: [PATCH 05/15] Proof of is_pmxsumP --- theories/SymGroup/Bruhat.v | 106 +++++++++++++++++++++++-------------- 1 file changed, 66 insertions(+), 40 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 7b6c299d..0b9511dd 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -123,7 +123,10 @@ End PermMX. #[local] Lemma lti1 n (i : 'I_n) : i.+1 < n.+1. by rewrite ltnS. Qed. #[local] Lemma lti n (i : 'I_n) : i < n.+1. exact: (ltnW (lti1 _)). Qed. #[local] Lemma lei n (i : 'I_n.+1) : i <= n. by rewrite -ltnS. Qed. -Hint Resolve lti1 lti perm_inj lei : core. +#[local] Lemma inord0 n : inord 0 = ord0 :> 'I_n.+1. +by apply val_inj; rewrite /= inordK. Qed. + + Hint Resolve lti1 lti perm_inj lei : core. Lemma setIE (T : finType) (pA pB : pred T) : [set y | pA y & pB y] = [set y | pA y] :&: [set y | pB y]. @@ -221,8 +224,7 @@ Qed. Definition is_pmxsum_row M := [forall i : 'I_n.+1, [&& (M i ord0 == 0), (M i ord_max == i) & - [forall j : 'I_n.+1, - M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1]]]. + [forall j : 'I_n.+1, M i (inord j.-1) <= M i j]]]. Definition is_pmxsum_pos M := [forall i : 'I_n, forall j : 'I_n, @@ -236,8 +238,7 @@ Lemma is_pmxsum_rowP M : reflect [/\ (forall i : 'I_n.+1, M i ord0 = 0), (forall i : 'I_n.+1, M i ord_max = i) & - forall i j : 'I_n.+1, - M i (inord j.-1) <= M i j <= (M i (inord j.-1)).+1] + forall i j : 'I_n.+1, M i (inord j.-1) <= M i j] (is_pmxsum_row M). Proof. apply (iffP forallP) => /= [H | [H0 Hmax Hincr i]]. @@ -263,22 +264,9 @@ apply/is_pmxsum_rowP; split=> [i | i | i j]; rewrite !perm_mxsumE. - rewrite sum1dep_card setIE [X in _ :&: X](_ : _ = setT). by rewrite setIT -sum1dep_card sum_lt1. by apply/setP=> /= k; rewrite !inE ltn_ord. -- apply/andP; split. - apply sub_le_big => //=; first by move=> a b; apply leq_addr. - move=> k /andP[->] /= /leq_trans; apply. - by rewrite inordK ?leq_pred // (leq_ltn_trans (leq_pred _)). - rewrite (bigID (fun k => s k == inord j.-1)) /= addnC. - set P := (P in (\sum_(i < _ | P i) _).+1). - rewrite (eq_bigl P) {}/P; first last. - move=> k; rewrite -andbA; congr (_ && _). - rewrite inordK ?(leq_ltn_trans (leq_pred _)) //. - case: j => [[|j] Hj] //=. - by rewrite [RHS]ltn_neqAle ltnS andbC -val_eqE /= inordK. - rewrite -[X in _ <= X]addn1 leq_add2l. - rewrite [X in _ <= X](_ : 1%N = \sum_(i0 < n | (s i0 == inord j.-1)) 1%N). - by apply sub_le_big => [||k /andP[]] //= a b; apply leq_addr. - rewrite (eq_bigl (pred1 (s^-1 (inord j.-1)))) ?big_pred1_eq // => /= k /=. - by rewrite -(inj_eq (@perm_inj _ s^-1)) permK. +- apply sub_le_big => //=; first by move=> a b; apply leq_addr. + move=> k /andP[->] /= /leq_trans; apply. + by rewrite inordK ?leq_pred // (leq_ltn_trans (leq_pred _)). Qed. Lemma is_perm_mxsum_posP s : is_pmxsum_pos (mxsum (perm_mx s)). @@ -303,31 +291,69 @@ rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. Qed. -Lemma is_pmxsumP M : is_pmxsum M -> is_perm_mx (mxdiff M). +Lemma sum_mxdiff M k j: + is_pmxsum M -> k < n -> j <= n -> + \sum_(l < j) mxdiff M (inord k) (inord l) = + M (inord k.+1) (inord j) - M (inord k) (inord j). +Proof. +move=> /[dup] HM /and3P[/is_pmxsum_rowP[R0 _ _] + /is_pmxsum_rowP[_ _ Cincr] + /is_pmxsum_posP Mpos ] ltkn lejn. +have {}Cincr i l (ltin : i < n) : + M (inord i) (inord l) <= M (inord i.+1) (inord l). + by move/(_ (inord l) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. +pose F l := M (inord k.+1) (inord l) - M (inord k) (inord l). +transitivity (\sum_(0 <= l < j) (F l.+1 - F l)). + rewrite big_mkord; apply: eq_bigr => [][l /leq_trans/(_ lejn) ltln /= _]. + rewrite mxE !inordK // subnBA; last exact: Cincr. + by congr (_ - _); rewrite addnBAC //; exact: Cincr. +rewrite {}/F telescope_sumn_in2 //; first by rewrite !inord0 !R0 !subn0. +apply: bounded_le_homo => l /= /leq_trans/(_ lejn) ltln. +rewrite leq_subLR addnBA /=; last exact: Cincr. +move/(_ (Ordinal ltkn) (Ordinal ltln)): Mpos => /= Mpos. +rewrite leq_subRL [X in _ <= X]addnC //. +exact: (leq_trans (leq_addr _ _) Mpos). +Qed. + +Lemma is_pmxsum_mxdiff M : is_pmxsum M -> is_perm_mx (mxdiff M). Proof. suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. move=> H; apply/is_perm_mx_sumP; split => i; first exact: rowsum. transitivity (\sum_j mxdiff M^T i j). by apply eq_bigr => j _; rewrite mxdiff_tr [RHS]mxE. by apply: rowsum; rewrite is_pmxsum_tr. -move/and3P=> [/is_pmxsum_rowP[R0 Rmax _] /is_pmxsum_rowP[_ _ Cincr] - /is_pmxsum_posP Mpos]. -have {}Cincr j : j <= n -> M (inord i) (inord j) <= M (inord i.+1) (inord j). - by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // => /andP[]. -pose f j := M (inord i.+1) (inord j) - M (inord i) (inord j). -transitivity (\sum_(0 <= k < n) (f k.+1 - f k)). - rewrite big_mkord; apply eq_bigr => j _. - rewrite mxE subnBA; last exact/Cincr/ltnW. - by congr (_ - _); rewrite addnBAC //; exact: Cincr. -rewrite telescope_sumn_in2 // {}/f. - have -> : inord 0 = ord0 :> 'I_n.+1 by apply val_inj; rewrite /= inordK. - have -> : inord n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. - by rewrite !R0 !subn0 !Rmax !inordK // subSnn /= natr1E. -apply: bounded_le_homo => j /= ltjn {R0 Rmax}. -rewrite leq_subLR addnBA; last exact: Cincr. -move/(_ i (Ordinal ltjn)): Mpos => /= Mpos. -rewrite leq_subRL [X in _ <= X]addnC //. -exact: (leq_trans (leq_addr _ _) Mpos). +move=> /[dup] HM /and3P[/is_pmxsum_rowP[_ Rmax _] _ _]. +transitivity (\sum_(l < n) mxdiff M (inord i) (inord l)). + by apply eq_bigr => j _; rewrite !inord_val. +rewrite sum_mxdiff //. +have -> : inord n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. +by rewrite !Rmax !inordK // subSnn. +Qed. + +Lemma mxdiffK : {in is_pmxsum, cancel mxdiff mxsum}. +Proof. +move=> M /[dup] HM /and3P[_ /is_pmxsum_rowP[C0 _ Cincr] _]. +have {}C0 i : M ord0 i = 0 by move/(_ i): C0; rewrite mxE. +have {}Cincr i j (ltin : i < n) : + M (inord i) (inord j) <= M (inord i.+1) (inord j). + by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. +apply matrixP=> i j; rewrite -{1}(inord_val i) -{1}(inord_val j) mxsumE //. +transitivity + (\sum_(0 <= k < i) (M (inord k.+1) (inord j) - M (inord k) (inord j)) ); + first last. + rewrite telescope_sumn_in2 //; first by rewrite !inord_val inord0 C0 subn0. + apply: bounded_le_homo => k /= ltki. + by apply/Cincr/(leq_trans ltki). +rewrite big_mkord /=. +apply: eq_bigr => [][k /leq_trans/(_ (ltn_ord i)) ltkn /= _]. +by rewrite sum_mxdiff. +Qed. + +Lemma is_pmxsumP M : reflect (exists s, M = mxsum (perm_mx s)) (is_pmxsum M). +Proof. +apply (iffP idP) => [H | [s ->]]; last exact: mxsum_perm_mx_is_pmxsum. +have/is_pmxsum_mxdiff/existsP[/= s /eqP Heq] := H. +by exists s; rewrite -{}Heq mxdiffK. Qed. End MatrixSum. From 01ec9162903313ce3c67abea54f50d6c2979a399 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 19 Jan 2024 01:11:47 +0100 Subject: [PATCH 06/15] Added Bruhat to _CoqProject --- _CoqProject | 1 + 1 file changed, 1 insertion(+) diff --git a/_CoqProject b/_CoqProject index 685ba484..f56dbebb 100644 --- a/_CoqProject +++ b/_CoqProject @@ -45,6 +45,7 @@ theories/Basic/ordtype.v theories/Basic/unitriginv.v theories/SymGroup/cycles.v theories/SymGroup/cycletype.v +theories/SymGroup/Bruhat.v theories/SymGroup/Frobenius_char.v theories/SymGroup/permcent.v theories/SymGroup/presentSn.v From deec0ea8a37399d1ae42a73580f0a3e1a79e6323 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 19 Jan 2024 01:50:46 +0100 Subject: [PATCH 07/15] Minor proof improvements --- theories/SymGroup/Bruhat.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 0b9511dd..a72a919b 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -124,6 +124,8 @@ End PermMX. #[local] Lemma lti n (i : 'I_n) : i < n.+1. exact: (ltnW (lti1 _)). Qed. #[local] Lemma lei n (i : 'I_n.+1) : i <= n. by rewrite -ltnS. Qed. #[local] Lemma inord0 n : inord 0 = ord0 :> 'I_n.+1. +by apply val_inj; rewrite /= inordK. Qed. +#[local] Lemma inord_max n : inord n = ord_max :> 'I_n.+1. by apply val_inj; rewrite /= inordK. Qed. Hint Resolve lti1 lti perm_inj lei : core. @@ -292,7 +294,7 @@ by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. Qed. Lemma sum_mxdiff M k j: - is_pmxsum M -> k < n -> j <= n -> + is_pmxsum M -> k < n -> j <= n -> \sum_(l < j) mxdiff M (inord k) (inord l) = M (inord k.+1) (inord j) - M (inord k) (inord j). Proof. @@ -325,9 +327,7 @@ suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. move=> /[dup] HM /and3P[/is_pmxsum_rowP[_ Rmax _] _ _]. transitivity (\sum_(l < n) mxdiff M (inord i) (inord l)). by apply eq_bigr => j _; rewrite !inord_val. -rewrite sum_mxdiff //. -have -> : inord n = ord_max :> 'I_n.+1 by apply val_inj; rewrite /= inordK. -by rewrite !Rmax !inordK // subSnn. +by rewrite sum_mxdiff // inord_max !Rmax !inordK ?subSnn. Qed. Lemma mxdiffK : {in is_pmxsum, cancel mxdiff mxsum}. @@ -339,7 +339,7 @@ have {}Cincr i j (ltin : i < n) : by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. apply matrixP=> i j; rewrite -{1}(inord_val i) -{1}(inord_val j) mxsumE //. transitivity - (\sum_(0 <= k < i) (M (inord k.+1) (inord j) - M (inord k) (inord j)) ); + ( \sum_(0 <= k < i) (M (inord k.+1) (inord j) - M (inord k) (inord j)) ); first last. rewrite telescope_sumn_in2 //; first by rewrite !inord_val inord0 C0 subn0. apply: bounded_le_homo => k /= ltki. From aaccbbff5c77802048717d6494099a18ea3720c8 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Fri, 19 Jan 2024 15:30:20 +0100 Subject: [PATCH 08/15] Documentation in Bruhat --- theories/SymGroup/Bruhat.v | 72 +++++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 28 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index a72a919b..15169f95 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -15,9 +15,31 @@ (******************************************************************************) (** * The (strong) Bruhat order on the Symmetric Group -We define the (strong) Bruhat order on the symmetric group. +The goal of this file is to define the (strong) Bruhat order on the symmetric +group. We use the technique of growth matrices. -We define the following notations: +We define the following notations where the matrices [m] and [M] have types +[m : 'M[nat]_n] and [M : 'M[nat]_(n.+1)]: + +Matrix sums: + +- [mxsum m] == matrix in ['M[nat]_(n.+1)] whose entries are the sum of the + entries strictly at its north-west in [m]. +- [mxdiff M] == the matrix in ['M[nat]_n] such that + + [mxdiff M i j = M i.+1 j.+1 + M i j - M i j.+1 - M i.+1 j]. + +Matrix sum of permutation matrices: + +- [is_pmxsum_row M] == for any [i] the i-th row of [M] is increassing + from [0] to [i]. +- [is_pmxsum_pos M] == for any [i j] one have the following inegality + + [M i.+1 j.+1 + M i j >= M i j.+1 - M i.+1 j]. + +- [is_pmxsum M] == M is the matrix sum of a permutation matrix + +Bruhat Order: - [s <=B t] == [s] is smaller than [t] for the right weak order. - [s 'I_n.+1. by apply val_inj; rewrite /= inordK. Qed. - - Hint Resolve lti1 lti perm_inj lei : core. +Hint Resolve lti1 lti perm_inj lei : core. Lemma setIE (T : finType) (pA pB : pred T) : [set y | pA y & pB y] = [set y | pA y] :&: [set y | pB y]. @@ -151,9 +172,8 @@ Implicit Type (m : 'M[nat]_n). Implicit Type (M : 'M[nat]_n.+1). -Definition mxsum m : 'M_n.+1 := - \matrix_(i < n.+1, j < n.+1) - \sum_(k < n | k < i) \sum_(l < n | l < j) m k l. +Definition mxsum m : 'M[nat]_n.+1 := + \matrix_(i, j) \sum_(k < n | k < i) \sum_(l < n | l < j) m k l. Definition mxdiff M : 'M[nat]_n := \matrix_(i < n, j < n) @@ -163,15 +183,13 @@ Definition mxdiff M : 'M[nat]_n := Lemma mxsumE m (i j : nat) : i < n.+1 -> j < n.+1 -> mxsum m (inord i) (inord j) = - \sum_(k < i) \sum_(l < j) m (inord k) (inord l). + \sum_(0 <= k < i) \sum_(0 <= l < j) m (inord k) (inord l). Proof. -rewrite mxE !ltnS => lti ltj. -rewrite [RHS](big_ord_widen _ - (fun k => \sum_(l < j) (m (inord k) (inord l))) lti). -rewrite inordK //; apply eq_bigr => k _. -rewrite (big_ord_widen _ (fun l => (m (inord k) (inord l))) ltj). -rewrite inordK //; apply eq_bigr => l _. -by rewrite !inord_val. +rewrite mxE !ltnS => lein lejn. +rewrite [RHS](big_nat_widen _ _ n) //= big_mkord inordK //. +apply eq_bigr => k _. +rewrite [RHS](big_nat_widen _ _ n) //= big_mkord inordK //. +by apply eq_bigr => l _; rewrite !inord_val. Qed. Lemma mxsum_tr m : (mxsum m^T = (mxsum m)^T)%R. @@ -187,7 +205,7 @@ Proof. by apply matrixP=> i j; rewrite !mxE -subnDAC subnDA. Qed. Lemma mxsumK : cancel mxsum mxdiff. Proof. move=> m; apply matrixP=> i j; rewrite mxE !mxsumE //. -rewrite !big_ord_recr /= !inord_val. +rewrite !big_nat_recr /= // !inord_val. by rewrite -!addnA [X in X - _ - _]addnC addnK addnC -addnA addnK. Qed. @@ -249,14 +267,13 @@ by apply/and3P; split; try exact/eqP; apply/forallP. Qed. Lemma is_pmxsum_posP M : - reflect (forall i j : 'I_n, + reflect (forall i j : 'I_n, M (inord i.+1) (inord j.+1) + M (inord i) (inord j) >= M (inord i) (inord j.+1) + M (inord i.+1) (inord j)) (is_pmxsum_pos M). Proof. -apply (iffP forallP) => /= [H i j | H i]. - by move/(_ i)/forallP : H; apply. -by apply/forallP. +apply (iffP forallP) => /= [H i j | H i]; last exact/forallP. +by move/(_ i)/forallP : H; apply. Qed. Lemma is_perm_mxsum_rowP s : is_pmxsum_row (mxsum (perm_mx s)). @@ -274,7 +291,7 @@ Qed. Lemma is_perm_mxsum_posP s : is_pmxsum_pos (mxsum (perm_mx s)). Proof. apply/is_pmxsum_posP => i j. -rewrite !mxsumE // !big_ord_recr /= !inord_val. +rewrite !mxsumE // !big_nat_recr //=. by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. Qed. @@ -295,7 +312,7 @@ Qed. Lemma sum_mxdiff M k j: is_pmxsum M -> k < n -> j <= n -> - \sum_(l < j) mxdiff M (inord k) (inord l) = + \sum_(0 <= l < j) mxdiff M (inord k) (inord l) = M (inord k.+1) (inord j) - M (inord k) (inord j). Proof. move=> /[dup] HM /and3P[/is_pmxsum_rowP[R0 _ _] @@ -306,7 +323,7 @@ have {}Cincr i l (ltin : i < n) : by move/(_ (inord l) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. pose F l := M (inord k.+1) (inord l) - M (inord k) (inord l). transitivity (\sum_(0 <= l < j) (F l.+1 - F l)). - rewrite big_mkord; apply: eq_bigr => [][l /leq_trans/(_ lejn) ltln /= _]. + rewrite !big_nat; apply eq_bigr => l /= /leq_trans/(_ lejn) ltln. rewrite mxE !inordK // subnBA; last exact: Cincr. by congr (_ - _); rewrite addnBAC //; exact: Cincr. rewrite {}/F telescope_sumn_in2 //; first by rewrite !inord0 !R0 !subn0. @@ -325,8 +342,8 @@ suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. by apply eq_bigr => j _; rewrite mxdiff_tr [RHS]mxE. by apply: rowsum; rewrite is_pmxsum_tr. move=> /[dup] HM /and3P[/is_pmxsum_rowP[_ Rmax _] _ _]. -transitivity (\sum_(l < n) mxdiff M (inord i) (inord l)). - by apply eq_bigr => j _; rewrite !inord_val. +transitivity (\sum_(0 <= l < n) mxdiff M (inord i) (inord l)). + by rewrite big_mkord; apply eq_bigr => j _; rewrite !inord_val. by rewrite sum_mxdiff // inord_max !Rmax !inordK ?subSnn. Qed. @@ -344,9 +361,8 @@ transitivity rewrite telescope_sumn_in2 //; first by rewrite !inord_val inord0 C0 subn0. apply: bounded_le_homo => k /= ltki. by apply/Cincr/(leq_trans ltki). -rewrite big_mkord /=. -apply: eq_bigr => [][k /leq_trans/(_ (ltn_ord i)) ltkn /= _]. -by rewrite sum_mxdiff. +rewrite !big_nat; apply: eq_bigr => k /= /leq_trans/(_ (ltn_ord i)) ltkn /=. +exact: sum_mxdiff. Qed. Lemma is_pmxsumP M : reflect (exists s, M = mxsum (perm_mx s)) (is_pmxsum M). From 0145cd22101b9220fd65900e44781851d3a6878b Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sat, 20 Jan 2024 16:45:31 +0100 Subject: [PATCH 09/15] Generalized n0.+1 -> n when possible --- theories/SymGroup/Bruhat.v | 130 +++++++++++++++++++++++-------------- 1 file changed, 80 insertions(+), 50 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 15169f95..23913162 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -163,26 +163,17 @@ by rewrite big_const_ord iter_addn_0 mul1n. Qed. -Section MatrixSum. - -Context {n0 : nat}. -#[local] Notation n := n0.+1. -Implicit Type (s t u v : 'S_n). -Implicit Type (m : 'M[nat]_n). -Implicit Type (M : 'M[nat]_n.+1). - - -Definition mxsum m : 'M[nat]_n.+1 := +Definition mxsum {n : nat} (m : 'M[nat]_n) : 'M[nat]_n.+1 := \matrix_(i, j) \sum_(k < n | k < i) \sum_(l < n | l < j) m k l. -Definition mxdiff M : 'M[nat]_n := +Definition mxdiff {n : nat} (M : 'M[nat]_n.+1) : 'M[nat]_n := \matrix_(i < n, j < n) ( M (inord i.+1) (inord j.+1) + M (inord i) (inord j) - M (inord i) (inord j.+1) - M (inord i.+1) (inord j) ). -Lemma mxsumE m (i j : nat) : +Lemma mxsumE n0 (n := n0.+1) (m : 'M[nat]_n) (i j : nat) : i < n.+1 -> j < n.+1 -> - mxsum m (inord i) (inord j) = + @mxsum n m (inord i) (inord j) = \sum_(0 <= k < i) \sum_(0 <= l < j) m (inord k) (inord l). Proof. rewrite mxE !ltnS => lein lejn. @@ -192,6 +183,16 @@ rewrite [RHS](big_nat_widen _ _ n) //= big_mkord inordK //. by apply eq_bigr => l _; rewrite !inord_val. Qed. + +Section MatrixSum. + +Context {n : nat}. +Implicit Type (m : 'M[nat]_n). +Implicit Type (M : 'M[nat]_n.+1). +Implicit Type (s : 'S_n). + +Local Notation mxsum := (@mxsum n). + Lemma mxsum_tr m : (mxsum m^T = (mxsum m)^T)%R. Proof. apply matrixP=> i j; rewrite !mxE exchange_big_idem //=. @@ -204,13 +205,14 @@ Proof. by apply matrixP=> i j; rewrite !mxE -subnDAC subnDA. Qed. Lemma mxsumK : cancel mxsum mxdiff. Proof. +case: n => [|n0]; first by move=> m; apply matrixP => [[]] . move=> m; apply matrixP=> i j; rewrite mxE !mxsumE //. rewrite !big_nat_recr /= // !inord_val. by rewrite -!addnA [X in X - _ - _]addnC addnK addnC -addnA addnK. Qed. Lemma perm_mxsum_inj : injective (mxsum \o perm_mx). -Proof. exact: (inj_comp (can_inj mxsumK) (@perm_mx_inj _ _)). Qed. +Proof. exact (inj_comp (can_inj mxsumK) (@perm_mx_inj _ _)). Qed. Lemma perm_mxsumE s i j : (mxsum \o perm_mx) s i j = \sum_(k < n | (k < i) && (s k < j)) 1%N. @@ -231,7 +233,8 @@ rewrite (eq_bigl (fun k : 'I_n => k < minn i j)). by move=> k; rewrite perm1 ltn_min. Qed. -Lemma perm_mxsum_maxperm i j : mxsum (perm_mx maxperm) i j = i + j - n. +Lemma perm_mxsum_maxperm i j : + mxsum (perm_mx maxperm) i j = i + j - n. Proof. rewrite perm_mxsumE. rewrite (eq_bigl (fun k : 'I_n => (k < i) && (n - j <= k))); first last. @@ -241,6 +244,16 @@ rewrite -(big_nat_widen _ _ _ predT) //=. by rewrite big_const_nat iter_addn_0 mul1n subnBA. Qed. +End MatrixSum. + + +Section IsPermMatrixSum. + +Context {n : nat}. +Implicit Type (m : 'M[nat]_n). +Implicit Type (M : 'M[nat]_n.+1). +Implicit Type (s : 'S_n). + Definition is_pmxsum_row M := [forall i : 'I_n.+1, [&& (M i ord0 == 0), (M i ord_max == i) & @@ -276,6 +289,15 @@ apply (iffP forallP) => /= [H i j | H i]; last exact/forallP. by move/(_ i)/forallP : H; apply. Qed. +Lemma is_pmxsum_tr M : is_pmxsum M^T = is_pmxsum M. +Proof. +suff {M} impl M : is_pmxsum M -> is_pmxsum M^T. + apply/idP/idP; last exact: impl. + by rewrite -{2}(trmxK M); apply: impl. +rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. +by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. +Qed. + Lemma is_perm_mxsum_rowP s : is_pmxsum_row (mxsum (perm_mx s)). Proof. apply/is_pmxsum_rowP; split=> [i | i | i j]; rewrite !perm_mxsumE. @@ -288,29 +310,10 @@ apply/is_pmxsum_rowP; split=> [i | i | i j]; rewrite !perm_mxsumE. by rewrite inordK ?leq_pred // (leq_ltn_trans (leq_pred _)). Qed. -Lemma is_perm_mxsum_posP s : is_pmxsum_pos (mxsum (perm_mx s)). -Proof. -apply/is_pmxsum_posP => i j. -rewrite !mxsumE // !big_nat_recr //=. -by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. -Qed. +End IsPermMatrixSum. -Lemma mxsum_perm_mx_is_pmxsum s : is_pmxsum (mxsum (perm_mx s)). -Proof. -rewrite /is_pmxsum -mxsum_tr tr_perm_mx. -by rewrite !is_perm_mxsum_rowP is_perm_mxsum_posP. -Qed. -Lemma is_pmxsum_tr M : is_pmxsum M^T = is_pmxsum M. -Proof. -suff {M} impl M : is_pmxsum M -> is_pmxsum M^T. - apply/idP/idP; last exact: impl. - by rewrite -{2}(trmxK M); apply: impl. -rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. -by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. -Qed. - -Lemma sum_mxdiff M k j: +#[local] Lemma sum_mxdiff n0 (n := n0.+1) (M : 'M[nat]_n.+1) k j: is_pmxsum M -> k < n -> j <= n -> \sum_(0 <= l < j) mxdiff M (inord k) (inord l) = M (inord k.+1) (inord j) - M (inord k) (inord j). @@ -320,7 +323,7 @@ move=> /[dup] HM /and3P[/is_pmxsum_rowP[R0 _ _] /is_pmxsum_posP Mpos ] ltkn lejn. have {}Cincr i l (ltin : i < n) : M (inord i) (inord l) <= M (inord i.+1) (inord l). - by move/(_ (inord l) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. + by move/(_ (inord l) (inord i.+1)): Cincr; rewrite !mxE inordK // !ltnS. pose F l := M (inord k.+1) (inord l) - M (inord k) (inord l). transitivity (\sum_(0 <= l < j) (F l.+1 - F l)). rewrite !big_nat; apply eq_bigr => l /= /leq_trans/(_ lejn) ltln. @@ -334,24 +337,48 @@ rewrite leq_subRL [X in _ <= X]addnC //. exact: (leq_trans (leq_addr _ _) Mpos). Qed. + +Section PermMatrixSum. + +Context {n : nat}. +Implicit Types (s : 'S_n) (M : 'M[nat]_n.+1). + +Lemma is_perm_mxsum_posP s : is_pmxsum_pos (mxsum (perm_mx s)). +Proof. +case: n s => [|n0] s; apply/is_pmxsum_posP => i j; first by case: i. +rewrite !mxsumE // !big_nat_recr //=. +by rewrite -!addnA leq_add2l addnC leq_add2l leq_addl. +Qed. + +Lemma mxsum_perm_mx_is_pmxsum s : is_pmxsum (mxsum (perm_mx s)). +Proof. +rewrite /is_pmxsum -mxsum_tr tr_perm_mx. +by rewrite !is_perm_mxsum_rowP is_perm_mxsum_posP. +Qed. + Lemma is_pmxsum_mxdiff M : is_pmxsum M -> is_perm_mx (mxdiff M). Proof. -suff {M} rowsum M i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. +case: n M => [|n0] M. + by move=> _; apply/existsP; exists 1; apply/eqP/matrixP => [][]. +suff {M} rowsum (M : 'M_n0.+2) i : is_pmxsum M -> \sum_j mxdiff M i j = 1%R. move=> H; apply/is_perm_mx_sumP; split => i; first exact: rowsum. transitivity (\sum_j mxdiff M^T i j). by apply eq_bigr => j _; rewrite mxdiff_tr [RHS]mxE. by apply: rowsum; rewrite is_pmxsum_tr. move=> /[dup] HM /and3P[/is_pmxsum_rowP[_ Rmax _] _ _]. -transitivity (\sum_(0 <= l < n) mxdiff M (inord i) (inord l)). +transitivity (\sum_(0 <= l < n0.+1) mxdiff M (inord i) (inord l)). by rewrite big_mkord; apply eq_bigr => j _; rewrite !inord_val. by rewrite sum_mxdiff // inord_max !Rmax !inordK ?subSnn. Qed. -Lemma mxdiffK : {in is_pmxsum, cancel mxdiff mxsum}. +Lemma mxdiffK : {in @is_pmxsum n, cancel (@mxdiff n) (@mxsum n)}. Proof. -move=> M /[dup] HM /and3P[_ /is_pmxsum_rowP[C0 _ Cincr] _]. +case: n => [|n0]. + move=> M /and3P[/is_pmxsum_rowP[C0 _ _] _ _]. + by apply/matrixP => i j; rewrite !mxE !big_ord0 !ord1 C0. +set n' := n0.+1 => M /[dup] HM /and3P[_ /is_pmxsum_rowP[C0 _ Cincr] _]. have {}C0 i : M ord0 i = 0 by move/(_ i): C0; rewrite mxE. -have {}Cincr i j (ltin : i < n) : +have {}Cincr i j (ltin : i < n') : M (inord i) (inord j) <= M (inord i.+1) (inord j). by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. apply matrixP=> i j; rewrite -{1}(inord_val i) -{1}(inord_val j) mxsumE //. @@ -372,8 +399,7 @@ have/is_pmxsum_mxdiff/existsP[/= s /eqP Heq] := H. by exists s; rewrite -{}Heq mxdiffK. Qed. -End MatrixSum. - +End PermMatrixSum. Fact Bruhat_display : unit. Proof. exact: tt. Qed. @@ -381,11 +407,10 @@ Fact Bruhat_display : unit. Proof. exact: tt. Qed. Module BruhatOrder. Section Def. -Context {n0 : nat}. -#[local] Notation n := n0.+1. +Context {n : nat}. Implicit Type (s t u v : 'S_n). -#[local] Notation perm_mxsum := (mxsum \o (perm_mx (n := n))). +#[local] Notation perm_mxsum := (@mxsum n \o (perm_mx (n := n))). Definition Bruhat s t := [forall i, forall j, perm_mxsum s i j >= perm_mxsum t i j]. @@ -454,14 +479,19 @@ HB.reexport BruhatOrder. Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). Notation "x = mxsum (perm_mx t) i j) (s <=B t) := BruhatP s t. -Lemma bottom_Bruhat n0 : Order.bottom = (1 : 'S_n0.+1). Proof. by []. Qed. -Lemma top_Bruhat n0 : Order.top = @maxperm n0. Proof. by []. Qed. +Lemma bottom_Bruhat : Order.bottom = (1 : 'S_n). Proof. by []. Qed. +Lemma top_Bruhat : Order.top = (maxperm : 'S_n). Proof. by []. Qed. +End Exports. End Exports. End BruhatOrder. HB.export BruhatOrder.Exports. From b48cc795f97615b25e2aacc0774920fc8934308c Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 21 Jan 2024 17:15:37 +0100 Subject: [PATCH 10/15] Bruhat Order Symmetry --- theories/SymGroup/Bruhat.v | 104 ++++++++++++++++++++++++++----------- 1 file changed, 74 insertions(+), 30 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 23913162..dbd33e05 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -57,6 +57,8 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Local Open Scope ring_scope. +Local Open Scope nat_scope. Import GroupScope GRing.Theory. Import Order.Theory. @@ -69,8 +71,8 @@ Lemma bounded_le_homo (m n : nat) f : (forall i, m <= i < n -> f i <= f i.+1) -> {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}. Proof. -move=> H i j; rewrite !inE /= => lein. -elim: j => [_ |j IHj]; first by rewrite leqn0 => /eqP ->. +move=> H i j /[!inE] lein. +elim: j => [_ /[!leqn0]/eqP -> // | j IHj]. move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij]. have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply. by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW. @@ -81,7 +83,7 @@ Lemma telescope_sumn_in2 n m f : n <= m -> \sum_(n <= k < m) (f k.+1 - f k) = f m - f n. Proof. move=> nm fle; rewrite (telescope_big (fun i j => f j - f i)). - by case: ltngtP nm => // ->; rewrite subnn. + by case: ltngtP nm => // -> /[!subnn]. move=> k /andP[nk km] /=; rewrite addnBAC ?fle 1?ltnW// ?subnKC// ?fle// inE. - by rewrite (ltnW nk) ltnW. - by rewrite ltnW // (ltn_trans nk). @@ -89,18 +91,19 @@ move=> k /andP[nk km] /=; rewrite addnBAC ?fle 1?ltnW// ?subnKC// ?fle// inE. - by rewrite ltnW //= ltnW. Qed. + Section PermMX. Variable (R : semiRingType) (n : nat). Implicit Type (s t : 'S_n). -Lemma perm_mx_eq1 s : (@perm_mx R n s == (1%:M)%R) = (s == 1). +Lemma perm_mx_eq1 s : (@perm_mx R n s == 1%:M) = (s == 1). Proof. -apply/eqP/eqP=> [| ->]; last by rewrite perm_mx1. +apply/eqP/eqP=> [| -> /[!perm_mx1] //]. rewrite /perm_mx row_permEsub => /esym Heq. -apply/permP=> /= i; rewrite perm1. +apply/permP=> /= i /[!perm1]. move/(congr1 (fun m : 'M__ => m i i)): Heq; rewrite !mxE eq_refl /=. -by case: eqP => //= _ /eqP; rewrite oner_eq0. +by case: eqP => //= _ /eqP /[!oner_eq0]. Qed. Lemma perm_mx_inj : injective (@perm_mx R n). @@ -134,7 +137,7 @@ have pex_inj : injective (fun i : 'I_n => proj1_sig (pex i)). have {neqi0} eqi0 l : m l k = 1%N -> l = i0. by move/eqP; apply/contraTeq => /neqi0 ->. by rewrite (eqi0 _ mik) (eqi0 _ mjk). -exists (perm pex_inj); apply/eqP/matrixP=> i j; rewrite !mxE permE. +exists (perm pex_inj); apply/eqP/matrixP=> i j /[!mxE] /[!permE]. case: (pex i) => k /= /andP[/eqP mik /forallP/= neq0]. case: eqP => [<-{j} // | /eqP]; rewrite eq_sym. by have /implyP/[apply]/eqP-> := neq0 j. @@ -153,7 +156,7 @@ Hint Resolve lti1 lti perm_inj lei : core. Lemma setIE (T : finType) (pA pB : pred T) : [set y | pA y & pB y] = [set y | pA y] :&: [set y | pB y]. -Proof. by apply/setP=> x; rewrite !inE. Qed. +Proof. by apply/setP=> x /[!inE]. Qed. Lemma sum_lt1 n k : k <= n -> \sum_(i < n | i < k) 1 = k. Proof. @@ -193,20 +196,19 @@ Implicit Type (s : 'S_n). Local Notation mxsum := (@mxsum n). -Lemma mxsum_tr m : (mxsum m^T = (mxsum m)^T)%R. +Lemma mxsum_tr m : mxsum m^T = (mxsum m)^T. Proof. -apply matrixP=> i j; rewrite !mxE exchange_big_idem //=. -apply: eq_bigr => k ltkj; apply: eq_bigr => l ltli. -by rewrite mxE. +apply matrixP=> i j /[!mxE]; rewrite exchange_big_idem //=. +by apply: eq_bigr => k ltkj; apply: eq_bigr => l ltli /[!mxE]. Qed. -Lemma mxdiff_tr M : (mxdiff M^T = (mxdiff M)^T)%R. -Proof. by apply matrixP=> i j; rewrite !mxE -subnDAC subnDA. Qed. +Lemma mxdiff_tr M : mxdiff M^T = (mxdiff M)^T. +Proof. by apply matrixP=> i j /[!mxE]; rewrite -subnDAC subnDA. Qed. Lemma mxsumK : cancel mxsum mxdiff. Proof. -case: n => [|n0]; first by move=> m; apply matrixP => [[]] . -move=> m; apply matrixP=> i j; rewrite mxE !mxsumE //. +case: n => [| n0] m; first by apply matrixP => [[]] . +apply matrixP=> i j /[1!mxE] /[!mxsumE] //. rewrite !big_nat_recr /= // !inord_val. by rewrite -!addnA [X in X - _ - _]addnC addnK addnC -addnA addnK. Qed. @@ -227,14 +229,12 @@ Qed. Lemma perm_mxsum1 i j : mxsum (perm_mx 1) i j = minn i j. Proof. -rewrite perm_mxsumE. -rewrite (eq_bigl (fun k : 'I_n => k < minn i j)). +rewrite perm_mxsumE (eq_bigl (fun k : 'I_n => k < minn i j)). exact (sum_lt1 (leq_trans (geq_minr i j) (ltn_ord j))). by move=> k; rewrite perm1 ltn_min. Qed. -Lemma perm_mxsum_maxperm i j : - mxsum (perm_mx maxperm) i j = i + j - n. +Lemma perm_mxsum_maxperm i j : mxsum (perm_mx maxperm) i j = i + j - n. Proof. rewrite perm_mxsumE. rewrite (eq_bigl (fun k : 'I_n => (k < i) && (n - j <= k))); first last. @@ -295,16 +295,15 @@ suff {M} impl M : is_pmxsum M -> is_pmxsum M^T. apply/idP/idP; last exact: impl. by rewrite -{2}(trmxK M); apply: impl. rewrite /is_pmxsum trmxK => /and3P[-> -> /=] /is_pmxsum_posP H. -by apply/is_pmxsum_posP => i j; rewrite !mxE addnC. +by apply/is_pmxsum_posP => i j /[!mxE] /[1!addnC]. Qed. Lemma is_perm_mxsum_rowP s : is_pmxsum_row (mxsum (perm_mx s)). Proof. apply/is_pmxsum_rowP; split=> [i | i | i j]; rewrite !perm_mxsumE. -- by rewrite sum1dep_card setIE [X in _ :&: X](_ : _ = set0) ?setI0 ?cards0. -- rewrite sum1dep_card setIE [X in _ :&: X](_ : _ = setT). - by rewrite setIT -sum1dep_card sum_lt1. - by apply/setP=> /= k; rewrite !inE ltn_ord. +- by rewrite !big_mkcondr_idem //=; apply big1. +- rewrite (eq_bigl (fun k : 'I_n => k < i)) ?sum_lt1 // => k /=. + by rewrite ltn_ord andbC. - apply sub_le_big => //=; first by move=> a b; apply leq_addr. move=> k /andP[->] /= /leq_trans; apply. by rewrite inordK ?leq_pred // (leq_ltn_trans (leq_pred _)). @@ -313,7 +312,7 @@ Qed. End IsPermMatrixSum. -#[local] Lemma sum_mxdiff n0 (n := n0.+1) (M : 'M[nat]_n.+1) k j: +Lemma sum_mxdiff n0 (n := n0.+1) (M : 'M[nat]_n.+1) k j: is_pmxsum M -> k < n -> j <= n -> \sum_(0 <= l < j) mxdiff M (inord k) (inord l) = M (inord k.+1) (inord j) - M (inord k) (inord j). @@ -377,7 +376,7 @@ case: n => [|n0]. move=> M /and3P[/is_pmxsum_rowP[C0 _ _] _ _]. by apply/matrixP => i j; rewrite !mxE !big_ord0 !ord1 C0. set n' := n0.+1 => M /[dup] HM /and3P[_ /is_pmxsum_rowP[C0 _ Cincr] _]. -have {}C0 i : M ord0 i = 0 by move/(_ i): C0; rewrite mxE. +have {}C0 i : M ord0 i = 0 by move/(_ i): C0 => /[!mxE]. have {}Cincr i j (ltin : i < n') : M (inord i) (inord j) <= M (inord i.+1) (inord j). by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. @@ -445,7 +444,8 @@ Fact Bruhat1s s : 1 <=B s. Proof. suff lecoeff t i j : perm_mxsum t i j <= i. apply/BruhatP => i j; rewrite perm_mxsum1 leq_min lecoeff /=. - rewrite [X in X <= _](_ : _ = (mxsum (perm_mx s))^T j i)%R; last by rewrite !mxE. + rewrite [X in X <= _](_ : _ = (mxsum (perm_mx s))^T j i); + last by rewrite !mxE. by rewrite -mxsum_tr tr_perm_mx lecoeff. rewrite perm_mxsumE. have /sum_lt1 {2}<- : i <= n by []. @@ -461,7 +461,7 @@ apply/BruhatP => i j; rewrite perm_mxsum_maxperm perm_mxsumE. rewrite sum1dep_card setIE cardsI. rewrite -[X in _ <=_ + X - _](card_imset _ (@perm_inj _ s)) /=. rewrite [imset _ _](_ : _ = [set x : 'I_n | x < j]); first last. - apply/setP => /= k; rewrite inE. + apply/setP => /= k /[!inE]. by rewrite -(permKV s k) mem_imset // inE permKV. rewrite -![in X in _ <= X - _]sum1dep_card !sum_lt1 //; apply: leq_sub2l. rewrite -[X in _ <= X](card_ord n) -cardsT /=. @@ -497,6 +497,50 @@ End BruhatOrder. HB.export BruhatOrder.Exports. +Section Symmetry. + +Context {n : nat}. +Implicit Types (s t : 'S_n). + +Lemma BruhatV s t : (s^-1 <=B t^-1) = (s <=B t). +Proof. +suff {s t} impl (s t : 'S_n) : (s <=B t) -> (s^-1 <=B t^-1). + apply/idP/idP; last exact: impl. + by move/impl; rewrite !invgK. +move/BruhatP=> H; apply/BruhatP=> i j. +by rewrite -!tr_perm_mx !mxsum_tr ![_^T _ _]mxE. +Qed. + +Lemma Bruhat_maxM s t : (s * maxperm <=B t * maxperm) = (t <=B s). +Proof. +case: n s t => [|n0] s t; first by rewrite !permS0 lexx. +suff {s t} impl (s t : 'S_n0.+1) : (s <=B t) -> (t * maxperm<=B s * maxperm). + apply/idP/idP; last exact: impl. + by move/impl; rewrite -!mulgA -{2 4}maxpermV !mulgV !mulg1. +set N := n0.+1 in s t *. +suff {s t} mxsum_maxpermM i j (s : 'S_N) : + mxsum (perm_mx (s * maxperm)) i j = i - mxsum (perm_mx s) i (rev_ord j). + move/BruhatP=> HB; apply/BruhatP=> i j. + by rewrite !{}mxsum_maxpermM; apply/leq_sub2l/HB. +have /[!ltnS]/sum_lt1 <- := ltn_ord i. +rewrite !perm_mxsumE !big_mkcondr_idem //=. +set S := (X in _ = _ - X); apply/eqP; rewrite -(eqn_add2r S) subnK; first last. + by rewrite {}/S; apply leq_sum => k _; case: ltnP. +rewrite {}/S -big_split_idem //=. +apply/eqP/eq_bigr => k ltki; rewrite permM permE /=. +rewrite -subSn // !subSS leq_subCl leqNgt. +by case: ltnP => /= _; rewrite ?addn0 ?add0n. +Qed. + +Lemma Bruhat_Mmax s t : (maxperm * s <=B maxperm * t) = (t <=B s). +Proof. by rewrite -[LHS]BruhatV !invMg !maxpermV Bruhat_maxM BruhatV. Qed. + +Lemma Bruhat_conj_max s t : (s ^ maxperm <=B t ^ maxperm) = (s <=B t). +Proof. by rewrite /conjg maxpermV Bruhat_Mmax Bruhat_maxM. Qed. + +End Symmetry. + + (* 0 0 0 0 x From e0407b1f609432c2a9d3f2be864cd8740a654309 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 21 Jan 2024 18:35:46 +0100 Subject: [PATCH 11/15] Minor cleanup --- theories/SymGroup/Bruhat.v | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index dbd33e05..3cb1d68e 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -57,15 +57,18 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Local Open Scope ring_scope. -Local Open Scope nat_scope. +#[local] Open Scope ring_scope. +#[local] Open Scope nat_scope. Import GroupScope GRing.Theory. Import Order.Theory. + Reserved Notation "s '<=B' t" (at level 70, t at next level). Reserved Notation "s ' f i <= f i.+1) -> @@ -84,11 +87,9 @@ Lemma telescope_sumn_in2 n m f : n <= m -> Proof. move=> nm fle; rewrite (telescope_big (fun i j => f j - f i)). by case: ltngtP nm => // -> /[!subnn]. -move=> k /andP[nk km] /=; rewrite addnBAC ?fle 1?ltnW// ?subnKC// ?fle// inE. -- by rewrite (ltnW nk) ltnW. -- by rewrite ltnW // (ltn_trans nk). -- by rewrite leqnn ltnW // (ltn_trans nk). -- by rewrite ltnW //= ltnW. +move=> k /andP[nk km] /=. +by rewrite addnBAC ?fle 1?ltnW// ?subnKC// ?fle// + inE ?leqnn ltnW // ?(ltn_trans nk) //= ltnW. Qed. @@ -194,7 +195,7 @@ Implicit Type (m : 'M[nat]_n). Implicit Type (M : 'M[nat]_n.+1). Implicit Type (s : 'S_n). -Local Notation mxsum := (@mxsum n). +#[local] Notation mxsum := (@mxsum n). Lemma mxsum_tr m : mxsum m^T = (mxsum m)^T. Proof. @@ -438,7 +439,7 @@ Qed. Order.Le_isPOrder.Build Bruhat_display 'S_n Bruhat_refl Bruhat_anti Bruhat_trans. -Local Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). +#[local] Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). Fact Bruhat1s s : 1 <=B s. Proof. @@ -476,8 +477,8 @@ End Def. Module Exports. HB.reexport BruhatOrder. -Notation "x <=B y" := (@Order.le Bruhat_display _ (x : 'S__) y). -Notation "x Date: Sun, 11 Feb 2024 01:17:13 +0100 Subject: [PATCH 12/15] Used Order.NatMonotonyTheory.nondecn_inP --- theories/SymGroup/Bruhat.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 3cb1d68e..4a299576 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -74,11 +74,11 @@ Lemma bounded_le_homo (m n : nat) f : (forall i, m <= i < n -> f i <= f i.+1) -> {in [pred i | m <= i & i <= n] &, {homo f : x y / x <= y}}. Proof. -move=> H i j /[!inE] lein. -elim: j => [_ /[!leqn0]/eqP -> // | j IHj]. -move=> /andP[_ ltjn]; rewrite leq_eqVlt ltnS => /orP [/eqP <- // | leij]. -have lemj : m <= j by move: lein => /andP[/[swap] _ /leq_trans]; apply. -by apply: (leq_trans (IHj _ leij) (H _ _)); rewrite lemj //= ltnW. +rewrite -!leEnat => H; apply Order.NatMonotonyTheory.nondecn_inP. + move=> i j /[!inE] /andP[lemi _] /andP[_ lejn]. + move=> k /andP[/ltW/(le_trans lemi) lemk /ltW/le_trans/(_ lejn) lekn]. + by rewrite inE lemk lekn. +by move=> i /[!inE] /andP[lemi _] /andP[_ lein]; apply: H; rewrite lemi. Qed. Lemma telescope_sumn_in2 n m f : n <= m -> From 0230b357fb750c20f43a8247fd31e0d975eda975 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 11 Feb 2024 07:53:44 +0100 Subject: [PATCH 13/15] Added #[local] + proof --- theories/SymGroup/Bruhat.v | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index 4a299576..e648743c 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -153,7 +153,7 @@ End PermMX. by apply val_inj; rewrite /= inordK. Qed. #[local] Lemma inord_max n : inord n = ord_max :> 'I_n.+1. by apply val_inj; rewrite /= inordK. Qed. -Hint Resolve lti1 lti perm_inj lei : core. +#[local] Hint Resolve lti1 lti perm_inj lei : core. Lemma setIE (T : finType) (pA pB : pred T) : [set y | pA y & pB y] = [set y | pA y] :&: [set y | pB y]. @@ -383,13 +383,12 @@ have {}Cincr i j (ltin : i < n') : by move/(_ (inord j) (inord i.+1)): Cincr; rewrite !mxE inordK // ltnS. apply matrixP=> i j; rewrite -{1}(inord_val i) -{1}(inord_val j) mxsumE //. transitivity - ( \sum_(0 <= k < i) (M (inord k.+1) (inord j) - M (inord k) (inord j)) ); - first last. - rewrite telescope_sumn_in2 //; first by rewrite !inord_val inord0 C0 subn0. - apply: bounded_le_homo => k /= ltki. - by apply/Cincr/(leq_trans ltki). -rewrite !big_nat; apply: eq_bigr => k /= /leq_trans/(_ (ltn_ord i)) ltkn /=. -exact: sum_mxdiff. + ( \sum_(0 <= k < i) (M (inord k.+1) (inord j) - M (inord k) (inord j)) ). + rewrite !big_nat; apply: eq_bigr => k /= /leq_trans/(_ (ltn_ord i)) ltkn /=. + exact: sum_mxdiff. +rewrite telescope_sumn_in2 //; first by rewrite !inord_val inord0 C0 subn0. +apply: bounded_le_homo => k /= ltki. +by apply/Cincr/(leq_trans ltki). Qed. Lemma is_pmxsumP M : reflect (exists s, M = mxsum (perm_mx s)) (is_pmxsum M). From 18c69b759e0be2fd167cac2533283dafc8ac537a Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Wed, 8 Jan 2025 14:56:54 +0100 Subject: [PATCH 14/15] Fix the doc --- theories/SymGroup/Bruhat.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index e648743c..af2d2246 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -41,8 +41,8 @@ Matrix sum of permutation matrices: Bruhat Order: -- [s <=B t] == [s] is smaller than [t] for the right weak order. -- [s Date: Mon, 22 Jun 2026 23:14:05 +0200 Subject: [PATCH 15/15] Rebased Bruhat on Master and MC-2.5 --- theories/SymGroup/Bruhat.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/SymGroup/Bruhat.v b/theories/SymGroup/Bruhat.v index af2d2246..b34c3d5d 100644 --- a/theories/SymGroup/Bruhat.v +++ b/theories/SymGroup/Bruhat.v @@ -46,7 +46,7 @@ Bruhat Order: ***************************) From HB Require Import structures. -From mathcomp Require Import all_ssreflect. +From mathcomp Require Import all_boot order. From mathcomp Require Import fingroup perm morphism presentation. From mathcomp Require Import ssralg matrix. @@ -95,7 +95,7 @@ Qed. Section PermMX. -Variable (R : semiRingType) (n : nat). +Variable (R : nzSemiRingType) (n : nat). Implicit Type (s t : 'S_n). Lemma perm_mx_eq1 s : (@perm_mx R n s == 1%:M) = (s == 1). @@ -110,7 +110,7 @@ Qed. Lemma perm_mx_inj : injective (@perm_mx R n). Proof. move=> s t /(congr1 (mulmx (perm_mx t^-1)))/eqP. -rewrite -!perm_mxM mulVg perm_mx1 perm_mx_eq1 => /eqP/(congr1 (mulg t)). +rewrite -!perm_mxM mulVg perm_mx1 perm_mx_eq1 => /eqP/(congr1 (mul t)). by rewrite mulgA mulgV mulg1 mul1g. Qed. @@ -401,7 +401,7 @@ Qed. End PermMatrixSum. -Fact Bruhat_display : unit. Proof. exact: tt. Qed. +Fact Bruhat_display : Order.disp_t. Proof. by []. Qed. Module BruhatOrder. Section Def.