Library mathcomp.fingroup.perm
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file contains the definition and properties associated to the group
+ of permutations of an arbitrary finite type.
+ {perm T} == the type of permutations of a finite type T, i.e.,
+ injective (finite) functions from T to T. Permutations
+ coerce to CiC functions.
+ 'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1}
+ perm_on A u == u is a permutation with support A, i.e., u only displaces
+ elements of A (u x != x implies x \in A).
+ tperm x y == the transposition of x, y.
+ aperm x s == the image of x under the action of the permutation s.
+ := s x
+ pcycle s x == the set of all elements that are in the same cycle of the
+ permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}.
+ pcycles s == the set of all the cycles of the permutation s.
+ (s : bool) == s is an odd permutation (the coercion is called odd_perm).
+ dpair u == u is a pair (x, y) of distinct objects (i.e., x != y).
+ lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over
+ (i |-> j), that maps i to j and lift i k to lift j (s k).
+ Canonical structures are defined allowing permutations to be an eqType,
+ choiceType, countType, finType, subType, finGroupType; permutations with
+ composition form a group, therefore inherit all generic group notations:
+ 1 == identity permutation, * == composition, ^-1 == inverse permutation.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section PermDefSection.
+ +
+Variable T : finType.
+ +
+Inductive perm_type : predArgType :=
+ Perm (pval : {ffun T → T}) & injectiveb pval.
+Definition pval p := let: Perm f _ := p in f.
+Definition perm_of of phant T := perm_type.
+Identity Coercion type_of_perm : perm_of >-> perm_type.
+ +
+Notation pT := (perm_of (Phant T)).
+ +
+Canonical perm_subType := Eval hnf in [subType for pval].
+Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
+Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
+Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
+Canonical perm_choiceType := Eval hnf in ChoiceType perm_type perm_choiceMixin.
+Definition perm_countMixin := [countMixin of perm_type by <:].
+Canonical perm_countType := Eval hnf in CountType perm_type perm_countMixin.
+Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
+Definition perm_finMixin := [finMixin of perm_type by <:].
+Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
+Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].
+ +
+Canonical perm_for_subType := Eval hnf in [subType of pT].
+Canonical perm_for_eqType := Eval hnf in [eqType of pT].
+Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
+Canonical perm_for_countType := Eval hnf in [countType of pT].
+Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
+Canonical perm_for_finType := Eval hnf in [finType of pT].
+Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].
+ +
+Lemma perm_proof (f : T → T) : injective f → injectiveb (finfun f).
+ +
+End PermDefSection.
+ +
+Notation "{ 'perm' T }" := (perm_of (Phant T))
+ (at level 0, format "{ 'perm' T }") : type_scope.
+ +
+ +
+ +
+Notation "''S_' n" := {perm 'I_n}
+ (at level 8, n at level 2, format "''S_' n").
+ +
+ +
+Module Type PermDefSig.
+Parameter fun_of_perm : ∀ T, perm_type T → T → T.
+Parameter perm : ∀ (T : finType) (f : T → T), injective f → {perm T}.
+Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
+Axiom permE : perm = perm_def.
+End PermDefSig.
+ +
+Module PermDef : PermDefSig.
+Definition fun_of_perm := fun_of_perm_def.
+Definition perm := perm_def.
+Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.
+Lemma permE : perm = perm_def.
+End PermDef.
+ +
+Notation fun_of_perm := PermDef.fun_of_perm.
+Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
+Notation perm := (@PermDef.perm _ _).
+Canonical fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
+Canonical perm_unlock := Unlockable PermDef.permE.
+Coercion fun_of_perm : perm_type >-> Funclass.
+ +
+Section Theory.
+ +
+Variable T : finType.
+Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).
+ +
+Lemma permP s t : s =1 t ↔ s = t.
+ +
+Lemma pvalE s : pval s = s :> (T → T).
+ +
+Lemma permE f f_inj : @perm T f f_inj =1 f.
+ +
+Lemma perm_inj s : injective s.
+ +
+Hint Resolve perm_inj.
+ +
+Lemma perm_onto s : codom s =i predT.
+ +
+Definition perm_one := perm (@inj_id T).
+ +
+Lemma perm_invK s : cancel (fun x ⇒ iinv (perm_onto s x)) s.
+ +
+Definition perm_inv s := perm (can_inj (perm_invK s)).
+ +
+Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).
+ +
+Lemma perm_oneP : left_id perm_one perm_mul.
+ +
+Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.
+ +
+Lemma perm_mulP : associative perm_mul.
+ +
+Definition perm_of_baseFinGroupMixin : FinGroup.mixin_of (perm_type T) :=
+ FinGroup.Mixin perm_mulP perm_oneP perm_invP.
+Canonical perm_baseFinGroupType :=
+ Eval hnf in BaseFinGroupType (perm_type T) perm_of_baseFinGroupMixin.
+Canonical perm_finGroupType := @FinGroupType perm_baseFinGroupType perm_invP.
+ +
+Canonical perm_of_baseFinGroupType :=
+ Eval hnf in [baseFinGroupType of {perm T}].
+Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].
+ +
+Lemma perm1 x : (1 : {perm T}) x = x.
+ +
+Lemma permM s t x : (s × t) x = t (s x).
+ +
+Lemma permK s : cancel s s^-1.
+ +
+Lemma permKV s : cancel s^-1 s.
+ +
+Lemma permJ s t x : (s ^ t) (t x) = t (s x).
+ +
+Lemma permX s x n : (s ^+ n) x = iter n s x.
+ +
+Lemma im_permV s S : s^-1 @: S = s @^-1: S.
+ +
+Lemma preim_permV s S : s^-1 @^-1: S = s @: S.
+ +
+Definition perm_on S : pred {perm T} := fun s ⇒ [pred x | s x != x] \subset S.
+ +
+Lemma perm_closed S s x : perm_on S s → (s x \in S) = (x \in S).
+ +
+Lemma perm_on1 H : perm_on H 1.
+ +
+Lemma perm_onM H s t : perm_on H s → perm_on H t → perm_on H (s × t).
+ +
+Lemma out_perm S u x : perm_on S u → x \notin S → u x = x.
+ +
+Lemma im_perm_on u S : perm_on S u → u @: S = S.
+ +
+Lemma tperm_proof x y : involutive [fun z ⇒ z with x |-> y, y |-> x].
+ +
+Definition tperm x y := perm (can_inj (tperm_proof x y)).
+ +
+CoInductive tperm_spec x y z : T → Type :=
+ | TpermFirst of z = x : tperm_spec x y z y
+ | TpermSecond of z = y : tperm_spec x y z x
+ | TpermNone of z ≠ x & z ≠ y : tperm_spec x y z z.
+ +
+Lemma tpermP x y z : tperm_spec x y z (tperm x y z).
+ +
+Lemma tpermL x y : tperm x y x = y.
+ +
+Lemma tpermR x y : tperm x y y = x.
+ +
+Lemma tpermD x y z : x != z → y != z → tperm x y z = z.
+ +
+Lemma tpermC x y : tperm x y = tperm y x.
+ +
+Lemma tperm1 x : tperm x x = 1.
+ +
+Lemma tpermK x y : involutive (tperm x y).
+ +
+Lemma tpermKg x y : involutive (mulg (tperm x y)).
+ +
+Lemma tpermV x y : (tperm x y)^-1 = tperm x y.
+ +
+Lemma tperm2 x y : tperm x y × tperm x y = 1.
+ +
+Lemma card_perm A : #|perm_on A| = (#|A|)`!.
+ +
+End Theory.
+ +
+ +
+Lemma inj_tperm (T T' : finType) (f : T → T') x y z :
+ injective f → f (tperm x y z) = tperm (f x) (f y) (f z).
+ +
+Lemma tpermJ (T : finType) x y (s : {perm T}) :
+ (tperm x y) ^ s = tperm (s x) (s y).
+ +
+Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
+ reflect (∃ p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
+ +
+Section PermutationParity.
+ +
+Variable T : finType.
+ +
+Implicit Types (s t u v : {perm T}) (x y z a b : T).
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section PermDefSection.
+ +
+Variable T : finType.
+ +
+Inductive perm_type : predArgType :=
+ Perm (pval : {ffun T → T}) & injectiveb pval.
+Definition pval p := let: Perm f _ := p in f.
+Definition perm_of of phant T := perm_type.
+Identity Coercion type_of_perm : perm_of >-> perm_type.
+ +
+Notation pT := (perm_of (Phant T)).
+ +
+Canonical perm_subType := Eval hnf in [subType for pval].
+Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
+Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
+Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
+Canonical perm_choiceType := Eval hnf in ChoiceType perm_type perm_choiceMixin.
+Definition perm_countMixin := [countMixin of perm_type by <:].
+Canonical perm_countType := Eval hnf in CountType perm_type perm_countMixin.
+Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
+Definition perm_finMixin := [finMixin of perm_type by <:].
+Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
+Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].
+ +
+Canonical perm_for_subType := Eval hnf in [subType of pT].
+Canonical perm_for_eqType := Eval hnf in [eqType of pT].
+Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
+Canonical perm_for_countType := Eval hnf in [countType of pT].
+Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
+Canonical perm_for_finType := Eval hnf in [finType of pT].
+Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].
+ +
+Lemma perm_proof (f : T → T) : injective f → injectiveb (finfun f).
+ +
+End PermDefSection.
+ +
+Notation "{ 'perm' T }" := (perm_of (Phant T))
+ (at level 0, format "{ 'perm' T }") : type_scope.
+ +
+ +
+ +
+Notation "''S_' n" := {perm 'I_n}
+ (at level 8, n at level 2, format "''S_' n").
+ +
+ +
+Module Type PermDefSig.
+Parameter fun_of_perm : ∀ T, perm_type T → T → T.
+Parameter perm : ∀ (T : finType) (f : T → T), injective f → {perm T}.
+Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
+Axiom permE : perm = perm_def.
+End PermDefSig.
+ +
+Module PermDef : PermDefSig.
+Definition fun_of_perm := fun_of_perm_def.
+Definition perm := perm_def.
+Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.
+Lemma permE : perm = perm_def.
+End PermDef.
+ +
+Notation fun_of_perm := PermDef.fun_of_perm.
+Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
+Notation perm := (@PermDef.perm _ _).
+Canonical fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
+Canonical perm_unlock := Unlockable PermDef.permE.
+Coercion fun_of_perm : perm_type >-> Funclass.
+ +
+Section Theory.
+ +
+Variable T : finType.
+Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).
+ +
+Lemma permP s t : s =1 t ↔ s = t.
+ +
+Lemma pvalE s : pval s = s :> (T → T).
+ +
+Lemma permE f f_inj : @perm T f f_inj =1 f.
+ +
+Lemma perm_inj s : injective s.
+ +
+Hint Resolve perm_inj.
+ +
+Lemma perm_onto s : codom s =i predT.
+ +
+Definition perm_one := perm (@inj_id T).
+ +
+Lemma perm_invK s : cancel (fun x ⇒ iinv (perm_onto s x)) s.
+ +
+Definition perm_inv s := perm (can_inj (perm_invK s)).
+ +
+Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).
+ +
+Lemma perm_oneP : left_id perm_one perm_mul.
+ +
+Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.
+ +
+Lemma perm_mulP : associative perm_mul.
+ +
+Definition perm_of_baseFinGroupMixin : FinGroup.mixin_of (perm_type T) :=
+ FinGroup.Mixin perm_mulP perm_oneP perm_invP.
+Canonical perm_baseFinGroupType :=
+ Eval hnf in BaseFinGroupType (perm_type T) perm_of_baseFinGroupMixin.
+Canonical perm_finGroupType := @FinGroupType perm_baseFinGroupType perm_invP.
+ +
+Canonical perm_of_baseFinGroupType :=
+ Eval hnf in [baseFinGroupType of {perm T}].
+Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].
+ +
+Lemma perm1 x : (1 : {perm T}) x = x.
+ +
+Lemma permM s t x : (s × t) x = t (s x).
+ +
+Lemma permK s : cancel s s^-1.
+ +
+Lemma permKV s : cancel s^-1 s.
+ +
+Lemma permJ s t x : (s ^ t) (t x) = t (s x).
+ +
+Lemma permX s x n : (s ^+ n) x = iter n s x.
+ +
+Lemma im_permV s S : s^-1 @: S = s @^-1: S.
+ +
+Lemma preim_permV s S : s^-1 @^-1: S = s @: S.
+ +
+Definition perm_on S : pred {perm T} := fun s ⇒ [pred x | s x != x] \subset S.
+ +
+Lemma perm_closed S s x : perm_on S s → (s x \in S) = (x \in S).
+ +
+Lemma perm_on1 H : perm_on H 1.
+ +
+Lemma perm_onM H s t : perm_on H s → perm_on H t → perm_on H (s × t).
+ +
+Lemma out_perm S u x : perm_on S u → x \notin S → u x = x.
+ +
+Lemma im_perm_on u S : perm_on S u → u @: S = S.
+ +
+Lemma tperm_proof x y : involutive [fun z ⇒ z with x |-> y, y |-> x].
+ +
+Definition tperm x y := perm (can_inj (tperm_proof x y)).
+ +
+CoInductive tperm_spec x y z : T → Type :=
+ | TpermFirst of z = x : tperm_spec x y z y
+ | TpermSecond of z = y : tperm_spec x y z x
+ | TpermNone of z ≠ x & z ≠ y : tperm_spec x y z z.
+ +
+Lemma tpermP x y z : tperm_spec x y z (tperm x y z).
+ +
+Lemma tpermL x y : tperm x y x = y.
+ +
+Lemma tpermR x y : tperm x y y = x.
+ +
+Lemma tpermD x y z : x != z → y != z → tperm x y z = z.
+ +
+Lemma tpermC x y : tperm x y = tperm y x.
+ +
+Lemma tperm1 x : tperm x x = 1.
+ +
+Lemma tpermK x y : involutive (tperm x y).
+ +
+Lemma tpermKg x y : involutive (mulg (tperm x y)).
+ +
+Lemma tpermV x y : (tperm x y)^-1 = tperm x y.
+ +
+Lemma tperm2 x y : tperm x y × tperm x y = 1.
+ +
+Lemma card_perm A : #|perm_on A| = (#|A|)`!.
+ +
+End Theory.
+ +
+ +
+Lemma inj_tperm (T T' : finType) (f : T → T') x y z :
+ injective f → f (tperm x y z) = tperm (f x) (f y) (f z).
+ +
+Lemma tpermJ (T : finType) x y (s : {perm T}) :
+ (tperm x y) ^ s = tperm (s x) (s y).
+ +
+Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
+ reflect (∃ p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
+ +
+Section PermutationParity.
+ +
+Variable T : finType.
+ +
+Implicit Types (s t u v : {perm T}) (x y z a b : T).
+ +
+
+ Note that pcycle s x is the orbit of x by < [s]> under the action aperm.
+ Hence, the pcycle lemmas below are special cases of more general lemmas
+ on orbits that will be stated in action.v.
+ Defining pcycle directly here avoids a dependency of matrix.v on
+ action.v and hence morphism.v.
+
+
+
+
+Definition aperm x s := s x.
+Definition pcycle s x := aperm x @: <[s]>.
+Definition pcycles s := pcycle s @: T.
+Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.
+ +
+Lemma apermE x s : aperm x s = s x.
+ +
+Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.
+ +
+Lemma pcycle_id s x : x \in pcycle s x.
+ +
+Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).
+ +
+Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.
+ +
+Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.
+ +
+Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).
+ +
+Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).
+ +
+Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.
+ +
+Lemma ncycles_mul_tperm s x y : let t := tperm x y in
+ #|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).
+ +
+Lemma odd_perm1 : odd_perm 1 = false.
+ +
+Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.
+ +
+Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
+ +
+Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].
+ +
+Lemma prod_tpermP s :
+ {ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
+ +
+Lemma odd_perm_prod ts :
+ all dpair ts → odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).
+ +
+Lemma odd_permM : {morph odd_perm : s1 s2 / s1 × s2 >-> s1 (+) s2}.
+ +
+Lemma odd_permV s : odd_perm s^-1 = odd_perm s.
+ +
+Lemma odd_permJ s1 s2 : odd_perm (s1 ^ s2) = odd_perm s1.
+ +
+End PermutationParity.
+ +
+Coercion odd_perm : perm_type >-> bool.
+ +
+Section LiftPerm.
+
+
++Definition aperm x s := s x.
+Definition pcycle s x := aperm x @: <[s]>.
+Definition pcycles s := pcycle s @: T.
+Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.
+ +
+Lemma apermE x s : aperm x s = s x.
+ +
+Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.
+ +
+Lemma pcycle_id s x : x \in pcycle s x.
+ +
+Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).
+ +
+Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.
+ +
+Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.
+ +
+Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).
+ +
+Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).
+ +
+Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.
+ +
+Lemma ncycles_mul_tperm s x y : let t := tperm x y in
+ #|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).
+ +
+Lemma odd_perm1 : odd_perm 1 = false.
+ +
+Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.
+ +
+Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
+ +
+Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].
+ +
+Lemma prod_tpermP s :
+ {ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
+ +
+Lemma odd_perm_prod ts :
+ all dpair ts → odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).
+ +
+Lemma odd_permM : {morph odd_perm : s1 s2 / s1 × s2 >-> s1 (+) s2}.
+ +
+Lemma odd_permV s : odd_perm s^-1 = odd_perm s.
+ +
+Lemma odd_permJ s1 s2 : odd_perm (s1 ^ s2) = odd_perm s1.
+ +
+End PermutationParity.
+ +
+Coercion odd_perm : perm_type >-> bool.
+ +
+Section LiftPerm.
+
+ Somewhat more specialised constructs for permutations on ordinals.
+
+
+
+
+Variable n : nat.
+Implicit Types i j : 'I_n.+1.
+Implicit Types s t : 'S_n.
+ +
+Definition lift_perm_fun i j s k :=
+ if unlift i k is Some k' then lift j (s k') else j.
+ +
+Lemma lift_permK i j s :
+ cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).
+ +
+Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).
+ +
+Lemma lift_perm_id i j s : lift_perm i j s i = j.
+ +
+Lemma lift_perm_lift i j s k' :
+ lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.
+ +
+Lemma lift_permM i j k s t :
+ lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).
+ +
+Lemma lift_perm1 i : lift_perm i i 1 = 1.
+ +
+Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.
+ +
+Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.
+ +
+End LiftPerm.
+ +
+
++Variable n : nat.
+Implicit Types i j : 'I_n.+1.
+Implicit Types s t : 'S_n.
+ +
+Definition lift_perm_fun i j s k :=
+ if unlift i k is Some k' then lift j (s k') else j.
+ +
+Lemma lift_permK i j s :
+ cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).
+ +
+Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).
+ +
+Lemma lift_perm_id i j s : lift_perm i j s i = j.
+ +
+Lemma lift_perm_lift i j s k' :
+ lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.
+ +
+Lemma lift_permM i j k s t :
+ lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).
+ +
+Lemma lift_perm1 i : lift_perm i i 1 = 1.
+ +
+Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.
+ +
+Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.
+ +
+End LiftPerm.
+ +
+