Documentation

Mathlib.GroupTheory.Perm.Sign

Sign of a permutation #

The main definition of this file is Equiv.Perm.sign, associating a ℤˣ sign with a permutation.

This file also contains miscellaneous lemmas about Equiv.Perm and Equiv.swap, building on top of those in Data/Equiv/Basic and other files in GroupTheory/Perm/*.

def Equiv.Perm.modSwap {α : Type u} [DecidableEq α] (i : α) (j : α) :

modSwap i j contains permutations up to swapping i and j.

We use this to partition permutations in Matrix.det_zero_of_row_eq, such that each partition sums up to 0.

Equations
Instances For
    noncomputable instance Equiv.Perm.instDecidableRelPermRModSwap {α : Type u_1} [Fintype α] [DecidableEq α] (i : α) (j : α) :
    DecidableRel Setoid.r
    Equations
    theorem Equiv.Perm.perm_inv_on_of_perm_on_finset {α : Type u} {s : Finset α} {f : Equiv.Perm α} (h : xs, f x s) {y : α} (hy : y s) :
    f⁻¹ y s
    theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo {α : Type u} (f : Equiv.Perm α) {s : Set α} [Finite s] (h : Set.MapsTo (f) s s) :
    Set.MapsTo (f⁻¹) s s
    @[simp]
    theorem Equiv.Perm.perm_inv_mapsTo_iff_mapsTo {α : Type u} {f : Equiv.Perm α} {s : Set α} [Finite s] :
    Set.MapsTo (f⁻¹) s s Set.MapsTo (f) s s
    theorem Equiv.Perm.perm_inv_on_of_perm_on_finite {α : Type u} {f : Equiv.Perm α} {p : αProp} [Finite { x : α // p x }] (h : ∀ (x : α), p xp (f x)) {x : α} (hx : p x) :
    p (f⁻¹ x)
    @[inline, reducible]
    abbrev Equiv.Perm.subtypePermOfFintype {α : Type u} (f : Equiv.Perm α) {p : αProp} [Fintype { x : α // p x }] (h : ∀ (x : α), p xp (f x)) :
    Equiv.Perm { x : α // p x }

    If the permutation f maps {x // p x} into itself, then this returns the permutation on {x // p x} induced by f. Note that the h hypothesis is weaker than for Equiv.Perm.subtypePerm.

    Equations
    Instances For
      @[simp]
      theorem Equiv.Perm.subtypePermOfFintype_apply {α : Type u} (f : Equiv.Perm α) {p : αProp} [Fintype { x : α // p x }] (h : ∀ (x : α), p xp (f x)) (x : { x : α // p x }) :
      (Equiv.Perm.subtypePermOfFintype f h) x = { val := f x, property := (_ : p (f x)) }
      theorem Equiv.Perm.subtypePermOfFintype_one {α : Type u} (p : αProp) [Fintype { x : α // p x }] (h : ∀ (x : α), p xp (1 x)) :
      theorem Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr {m : Type u_1} {n : Type u_2} [Finite m] [Finite n] (σ : Equiv.Perm (m n)) :
      Set.MapsTo (σ) (Set.range Sum.inl) (Set.range Sum.inl) Set.MapsTo (σ) (Set.range Sum.inr) (Set.range Sum.inr)
      theorem Equiv.Perm.Disjoint.orderOf {α : Type u} {σ : Equiv.Perm α} {τ : Equiv.Perm α} (hστ : Equiv.Perm.Disjoint σ τ) :
      orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ)
      def Equiv.Perm.swapFactorsAux {α : Type u} [DecidableEq α] (l : List α) (f : Equiv.Perm α) :
      (∀ {x : α}, f x xx l){ l : List (Equiv.Perm α) // List.prod l = f gl, Equiv.Perm.IsSwap g }

      Given a list l : List α and a permutation f : Perm α such that the nonfixed points of f are in l, recursively factors f as a product of transpositions.

      Equations
      Instances For
        def Equiv.Perm.swapFactors {α : Type u} [DecidableEq α] [Fintype α] [LinearOrder α] (f : Equiv.Perm α) :
        { l : List (Equiv.Perm α) // List.prod l = f gl, Equiv.Perm.IsSwap g }

        swapFactors represents a permutation as a product of a list of transpositions. The representation is non unique and depends on the linear order structure. For types without linear order truncSwapFactors can be used.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Equiv.Perm.truncSwapFactors {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) :
          Trunc { l : List (Equiv.Perm α) // List.prod l = f gl, Equiv.Perm.IsSwap g }

          This computably represents the fact that any permutation can be represented as the product of a list of transpositions.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Equiv.Perm.swap_induction_on {α : Type u} [DecidableEq α] [Finite α] {P : Equiv.Perm αProp} (f : Equiv.Perm α) :
            P 1(∀ (f : Equiv.Perm α) (x y : α), x yP fP (Equiv.swap x y * f))P f

            An induction principle for permutations. If P holds for the identity permutation, and is preserved under composition with a non-trivial swap, then P holds for all permutations.

            theorem Equiv.Perm.swap_induction_on' {α : Type u} [DecidableEq α] [Finite α] {P : Equiv.Perm αProp} (f : Equiv.Perm α) :
            P 1(∀ (f : Equiv.Perm α) (x y : α), x yP fP (f * Equiv.swap x y))P f

            Like swap_induction_on, but with the composition on the right of f.

            An induction principle for permutations. If P holds for the identity permutation, and is preserved under composition with a non-trivial swap, then P holds for all permutations.

            theorem Equiv.Perm.isConj_swap {α : Type u} [DecidableEq α] {w : α} {x : α} {y : α} {z : α} (hwx : w x) (hyz : y z) :
            def Equiv.Perm.finPairsLT (n : ) :
            Finset ((_ : Fin n) × Fin n)

            set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a

            Equations
            Instances For
              theorem Equiv.Perm.mem_finPairsLT {n : } {a : (_ : Fin n) × Fin n} :
              a Equiv.Perm.finPairsLT n a.snd < a.fst

              signAux σ is the sign of a permutation on Fin n, defined as the parity of the number of pairs (x₁, x₂) such that x₂ < x₁ but σ x₁ ≤ σ x₂

              Equations
              Instances For
                def Equiv.Perm.signBijAux {n : } (f : Equiv.Perm (Fin n)) (a : (_ : Fin n) × Fin n) :
                (_ : Fin n) × Fin n

                signBijAux f ⟨a, b⟩ returns the pair consisting of f a and f b in decreasing order.

                Equations
                • Equiv.Perm.signBijAux f a = if x : f a.snd < f a.fst then { fst := f a.fst, snd := f a.snd } else { fst := f a.snd, snd := f a.fst }
                Instances For
                  theorem Equiv.Perm.signBijAux_surj {n : } {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) :
                  theorem Equiv.Perm.signAux_swap {n : } {x : Fin n} {y : Fin n} (_hxy : x y) :
                  def Equiv.Perm.signAux2 {α : Type u} [DecidableEq α] :
                  List αEquiv.Perm αˣ

                  When the list l : List α contains all nonfixed points of the permutation f : Perm α, signAux2 l f recursively calculates the sign of f.

                  Equations
                  Instances For
                    theorem Equiv.Perm.signAux_eq_signAux2 {α : Type u} [DecidableEq α] {n : } (l : List α) (f : Equiv.Perm α) (e : α Fin n) (_h : ∀ (x : α), f x xx l) :
                    Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f
                    def Equiv.Perm.signAux3 {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) {s : Multiset α} :
                    (∀ (x : α), x s)ˣ

                    When the multiset s : Multiset α contains all nonfixed points of the permutation f : Perm α, signAux2 f _ recursively calculates the sign of f.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Equiv.Perm.signAux3_mul_and_swap {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) (s : Multiset α) (hs : ∀ (x : α), x s) :

                      SignType.sign of a permutation returns the signature or parity of a permutation, 1 for even permutations, -1 for odd permutations. It is the unique surjective group homomorphism from Perm α to the group with two elements.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem Equiv.Perm.sign_mul {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) :
                        Equiv.Perm.sign (f * g) = Equiv.Perm.sign f * Equiv.Perm.sign g
                        @[simp]
                        theorem Equiv.Perm.sign_trans {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) (g : Equiv.Perm α) :
                        Equiv.Perm.sign (f.trans g) = Equiv.Perm.sign g * Equiv.Perm.sign f
                        theorem Equiv.Perm.sign_one {α : Type u} [DecidableEq α] [Fintype α] :
                        Equiv.Perm.sign 1 = 1
                        @[simp]
                        theorem Equiv.Perm.sign_refl {α : Type u} [DecidableEq α] [Fintype α] :
                        Equiv.Perm.sign (Equiv.refl α) = 1
                        theorem Equiv.Perm.sign_inv {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) :
                        Equiv.Perm.sign f⁻¹ = Equiv.Perm.sign f
                        @[simp]
                        theorem Equiv.Perm.sign_symm {α : Type u} [DecidableEq α] [Fintype α] (e : Equiv.Perm α) :
                        Equiv.Perm.sign e.symm = Equiv.Perm.sign e
                        theorem Equiv.Perm.sign_swap {α : Type u} [DecidableEq α] [Fintype α] {x : α} {y : α} (h : x y) :
                        Equiv.Perm.sign (Equiv.swap x y) = -1
                        @[simp]
                        theorem Equiv.Perm.sign_swap' {α : Type u} [DecidableEq α] [Fintype α] {x : α} {y : α} :
                        Equiv.Perm.sign (Equiv.swap x y) = if x = y then 1 else -1
                        theorem Equiv.Perm.IsSwap.sign_eq {α : Type u} [DecidableEq α] [Fintype α] {f : Equiv.Perm α} (h : Equiv.Perm.IsSwap f) :
                        Equiv.Perm.sign f = -1
                        theorem Equiv.Perm.signAux3_symm_trans_trans {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (e : α β) {s : Multiset α} {t : Multiset β} (hs : ∀ (x : α), x s) (ht : ∀ (x : β), x t) :
                        Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = Equiv.Perm.signAux3 f hs
                        @[simp]
                        theorem Equiv.Perm.sign_symm_trans_trans {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (e : α β) :
                        Equiv.Perm.sign ((e.symm.trans f).trans e) = Equiv.Perm.sign f
                        @[simp]
                        theorem Equiv.Perm.sign_trans_trans_symm {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm β) (e : α β) :
                        Equiv.Perm.sign ((e.trans f).trans e.symm) = Equiv.Perm.sign f
                        theorem Equiv.Perm.sign_prod_list_swap {α : Type u} [DecidableEq α] [Fintype α] {l : List (Equiv.Perm α)} (hl : gl, Equiv.Perm.IsSwap g) :
                        Equiv.Perm.sign (List.prod l) = (-1) ^ List.length l
                        theorem Equiv.Perm.sign_surjective (α : Type u) [DecidableEq α] [Fintype α] [Nontrivial α] :
                        Function.Surjective Equiv.Perm.sign
                        theorem Equiv.Perm.eq_sign_of_surjective_hom {α : Type u} [DecidableEq α] [Fintype α] {s : Equiv.Perm α →* ˣ} (hs : Function.Surjective s) :
                        s = Equiv.Perm.sign
                        theorem Equiv.Perm.sign_subtypePerm {α : Type u} [DecidableEq α] [Fintype α] (f : Equiv.Perm α) {p : αProp} [DecidablePred p] (h₁ : ∀ (x : α), p x p (f x)) (h₂ : ∀ (x : α), f x xp x) :
                        Equiv.Perm.sign (Equiv.Perm.subtypePerm f h₁) = Equiv.Perm.sign f
                        theorem Equiv.Perm.sign_eq_sign_of_equiv {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (f : Equiv.Perm α) (g : Equiv.Perm β) (e : α β) (h : ∀ (x : α), e (f x) = g (e x)) :
                        Equiv.Perm.sign f = Equiv.Perm.sign g
                        theorem Equiv.Perm.sign_bij {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] {f : Equiv.Perm α} {g : Equiv.Perm β} (i : (x : α) → f x xβ) (h : ∀ (x : α) (hx : f x x) (hx' : f (f x) f x), i (f x) hx' = g (i x hx)) (hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ x₁) (hx₂ : f x₂ x₂), i x₁ hx₁ = i x₂ hx₂x₁ = x₂) (hg : ∀ (y : β), g y y∃ (x : α) (hx : f x x), i x hx = y) :
                        Equiv.Perm.sign f = Equiv.Perm.sign g
                        theorem Equiv.Perm.prod_prodExtendRight {β : Type v} {α : Type u_1} [DecidableEq α] (σ : αEquiv.Perm β) {l : List α} (hl : List.Nodup l) (mem_l : ∀ (a : α), a l) :

                        If we apply prod_extendRight a (σ a) for all a : α in turn, we get prod_congrRight σ.

                        @[simp]
                        theorem Equiv.Perm.sign_prodExtendRight {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (a : α) (σ : Equiv.Perm β) :
                        Equiv.Perm.sign (Equiv.Perm.prodExtendRight a σ) = Equiv.Perm.sign σ
                        theorem Equiv.Perm.sign_prodCongrRight {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σ : αEquiv.Perm β) :
                        Equiv.Perm.sign (Equiv.prodCongrRight σ) = Finset.prod Finset.univ fun (k : α) => Equiv.Perm.sign (σ k)
                        theorem Equiv.Perm.sign_prodCongrLeft {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σ : αEquiv.Perm β) :
                        Equiv.Perm.sign (Equiv.prodCongrLeft σ) = Finset.prod Finset.univ fun (k : α) => Equiv.Perm.sign (σ k)
                        @[simp]
                        theorem Equiv.Perm.sign_permCongr {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (e : α β) (p : Equiv.Perm α) :
                        Equiv.Perm.sign ((Equiv.permCongr e) p) = Equiv.Perm.sign p
                        @[simp]
                        theorem Equiv.Perm.sign_sumCongr {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (σa : Equiv.Perm α) (σb : Equiv.Perm β) :
                        Equiv.Perm.sign (Equiv.Perm.sumCongr σa σb) = Equiv.Perm.sign σa * Equiv.Perm.sign σb
                        @[simp]
                        theorem Equiv.Perm.sign_subtypeCongr {α : Type u} [DecidableEq α] [Fintype α] {p : αProp} [DecidablePred p] (ep : Equiv.Perm { a : α // p a }) (en : Equiv.Perm { a : α // ¬p a }) :
                        Equiv.Perm.sign (Equiv.Perm.subtypeCongr ep en) = Equiv.Perm.sign ep * Equiv.Perm.sign en
                        @[simp]
                        theorem Equiv.Perm.sign_extendDomain {α : Type u} {β : Type v} [DecidableEq α] [Fintype α] [DecidableEq β] [Fintype β] (e : Equiv.Perm α) {p : βProp} [DecidablePred p] (f : α Subtype p) :
                        Equiv.Perm.sign (Equiv.Perm.extendDomain e f) = Equiv.Perm.sign e
                        @[simp]
                        theorem Equiv.Perm.sign_ofSubtype {α : Type u} [DecidableEq α] [Fintype α] {p : αProp} [DecidablePred p] (f : Equiv.Perm (Subtype p)) :
                        Equiv.Perm.sign (Equiv.Perm.ofSubtype f) = Equiv.Perm.sign f