Library Combi.SymGroup.weak_order: The weak order on the Symmetric Group

The weak order on the Symmetric Group

We define the right (with the mathcomp convention of product of permutation) weak order on the symmetric group. We show that it is equivalent to inclusion of sets of inversions and that it is a lattice.

We define the following notations:

s <=R t == s is smaller than t for the right weak order.
s <R t == s is strictly smaller than t for the right weak order.
s \/R t == the meet of s and t for the right weak order.
s /\R t == the join of s and t for the right weak order.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup perm morphism presentation.

Require Import permcomp tools permuted combclass congr presentSn ordtype.

Set Implicit Arguments.

Import GroupScope.
Import Order.Theory.

#[local] Open Scope Combi_scope.

Reserved Notation "s '<=R' t" (at level 70, t at next level).
Reserved Notation "s '<R' t" (at level 70, t at next level).
Reserved Notation "s '/\R' t" (at level 70, t at next level).
Reserved Notation "s '\/R' t" (at level 70, t at next level).

Fact perm_display : unit.

Module WeakOrder.
Section Def.

Context {n0 : nat}.
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n).

Definition leperm s t :=
  [exists u, (t == s * u ) && (length t == length s + length u )].

#[local] Notation "s '<=R' t" := (leperm s t).

Fact lepermP s t :
  reflect (exists2 u , t = s * u & length t = length s + length u)
          (s <=R t).

Fact leperm_length s t : s <=R t -> length s <= length t.

Fact leperm_lengthE s t : s <=R t -> length s = length t -> s = t.

Fact leperm_refl s : s <=R s.

Fact leperm_trans : transitive leperm.

Fact leperm_anti : antisymmetric leperm.

#[export ] HB.instance Definition _ := Finite.on 'S_n.
#[export ] HB.instance Definition _ :=
  Order.Le_isPOrder.Build perm_display 'S_n
    leperm_refl leperm_anti leperm_trans.

End Def.

Module Exports.

Notation "x <=R y" := (@Order.le perm_display _ (x : 'S__) y) : Combi_scope.
Notation "x <R y" := (@Order.lt perm_display _ (x : 'S__) y) : Combi_scope.
Notation "x /\R y" := (@Order.meet perm_display _ (x : 'S__) y) : Combi_scope.
Notation "x \/R y" := (@Order.join perm_display _ (x : 'S__) y) : Combi_scope.

Section WeakOrder.

Variable (n0 : nat).
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n).

Definition lepermP s t :
  reflect
    (exists2 u : 'S_n, t = s * u & length t = length s + length u)
    (s <=R t)
  := lepermP s t.
Definition leperm_length : forall s t, s <=R t -> length s <= length t
  := leperm_length.
Definition leperm_lengthE : forall s t, s <=R t -> length s = length t -> s = t
  := leperm_lengthE.
End WeakOrder.
End Exports.
End WeakOrder.

Section LEPermTheory.

Variable (n0 : nat).
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n).

Lemma ltperm_length s t : s <R t -> length s < length t.

Lemma leperm1p s : (1%g : 'S_n) <=R s.

Lemma leperm_maxpermMl s t : (maxperm * t <=R maxperm * s ) = (s <=R t ).

Lemma leperm_maxperm s : s <=R maxperm.

Lemma leperm_factorP s t :
  reflect (exists2 w : seq 'I_n0, w \is reduced &
              exists2 l : nat , t = 's_[w ] & s = 's_[take l w ])
          (s <=R t).

Lemma leperm_succ s t :
  s <R t -> exists2 i : 'I_n0, (s <R s * 's_i ) & (s * 's_i <=R t ).

Lemma covers_permP s t :
  reflect (exists2 i : 'I_n0, s <R s * 's_i & t = s * 's_i) (covers s t).

Theorem leperm_invset s t : (s <=R t ) = (invset s \subset invset t ).

Corollary ltperm_invset s t : (s <R t ) = (invset s \proper invset t ).

End LEPermTheory.

Section TClosureInvset.

Variable (n0 : nat).
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n) (A B : {set 'I_n * 'I_n}).

Lemma tclosure_Delta A : A \subset Delta -> tclosure A \subset Delta.

Lemma tclosureP A : A \subset Delta -> transitive (srel (tclosure A)).

Lemma is_invset_tclosureU A B :
  is_invset A -> is_invset B -> is_invset (tclosure (A :|: B)).

End TClosureInvset.

Module PermLattice.
Section PermLattice.

Variable (n0 : nat).
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n) (A B : {set 'I_n * 'I_n}).

Definition supperm s t : 'S_n :=
  perm_of_invset (tclosure (invset s :|: invset t)).
Definition infperm s t : 'S_n :=
  maxperm * (supperm (maxperm * s) (maxperm * t)).

Lemma invset_supperm s t :
  invset (supperm s t) = tclosure (invset s :|: invset t).

Lemma suppermC s t : supperm s t = supperm t s.

Lemma suppermPr s t : s <=R (supperm s t ).

Lemma suppermPl s t : t <=R (supperm s t ).

Fact suppermP s t w : s <=R w -> t <=R w -> (supperm s t ) <=R w.

Fact supperm_is_join x y z : (supperm x y <=R z ) = (x <=R z ) && (y <=R z ).
Fact infperm_is_meet x y z : (x <=R infperm y z ) = (x <=R y ) && (x <=R z ).

#[export ] HB.instance Definition _ :=
  Order.POrder_MeetJoin_isLattice.Build perm_display ('S_n )
    infperm_is_meet supperm_is_join.
#[export ] HB.instance Definition _ :=
  Order.hasBottom.Build perm_display ('S_n ) (@leperm1p n0 ).
#[export ] HB.instance Definition _ :=
  Order.hasTop.Build perm_display ('S_n ) (@leperm_maxperm n0 ).

End PermLattice.

Module Exports.
Section PermLattice.

Variable (n0 : nat).
#[local] Notation n := n0.+1.
Implicit Type (s t u v : 'S_n) (A B : {set 'I_n * 'I_n}).

Lemma bottom_perm : Order.bottom = (1 : 'S_n).
Lemma top_perm : Order.top = @maxperm n.

Lemma invset_join s t : invset (s \/R t) = tclosure (invset s :|: invset t).

Lemma perm_join_meetE s t :
  s /\R t = maxperm * (maxperm * s \/R maxperm * t).

End PermLattice.
End Exports.
End PermLattice.