Documentation

Mathlib.GroupTheory.Perm.Basic

The group of permutations (self-equivalences) of a type α #

This file defines the Group structure on Equiv.Perm α.

instance Equiv.Perm.permGroup {α : Type u} :
Equations
@[simp]
theorem Equiv.Perm.default_eq {α : Type u} :
default = 1
@[simp]
theorem Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply {α : Type u} (u : (Function.End α)ˣ) :
(↑(MulEquiv.symm Equiv.Perm.equivUnitsEnd) u).symm = u⁻¹
@[simp]
theorem Equiv.Perm.equivUnitsEnd_symm_apply_apply {α : Type u} (u : (Function.End α)ˣ) :
↑(↑(MulEquiv.symm Equiv.Perm.equivUnitsEnd) u) = u
@[simp]
theorem Equiv.Perm.val_inv_equivUnitsEnd_apply {α : Type u} (e : Equiv.Perm α) :
∀ (a : α), (Equiv.Perm.equivUnitsEnd e)⁻¹ a = Equiv.toFun e.symm a
@[simp]
theorem Equiv.Perm.val_equivUnitsEnd_apply {α : Type u} (e : Equiv.Perm α) :
∀ (a : α), ↑(Equiv.Perm.equivUnitsEnd e) a = Equiv.toFun e a

The permutation of a type is equivalent to the units group of the endomorphisms monoid of this type.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem MonoidHom.toHomPerm_apply_apply {α : Type u} {G : Type u_1} [Group G] (f : G →* Function.End α) :
    ∀ (a : G), ↑(↑(MonoidHom.toHomPerm f) a) = f a
    @[simp]
    theorem MonoidHom.toHomPerm_apply_symm_apply {α : Type u} {G : Type u_1} [Group G] (f : G →* Function.End α) :
    ∀ (a : G), (↑(MonoidHom.toHomPerm f) a).symm = (↑(MonoidHom.toHomUnits f) a)⁻¹
    def MonoidHom.toHomPerm {α : Type u} {G : Type u_1} [Group G] (f : G →* Function.End α) :

    Lift a monoid homomorphism f : G →* Function.End α to a monoid homomorphism f : G →* Equiv.Perm α.

    Equations
    Instances For
      theorem Equiv.Perm.mul_apply {α : Type u} (f : Equiv.Perm α) (g : Equiv.Perm α) (x : α) :
      ↑(f * g) x = f (g x)
      theorem Equiv.Perm.one_apply {α : Type u} (x : α) :
      1 x = x
      @[simp]
      theorem Equiv.Perm.inv_apply_self {α : Type u} (f : Equiv.Perm α) (x : α) :
      f⁻¹ (f x) = x
      @[simp]
      theorem Equiv.Perm.apply_inv_self {α : Type u} (f : Equiv.Perm α) (x : α) :
      f (f⁻¹ x) = x
      theorem Equiv.Perm.one_def {α : Type u} :
      theorem Equiv.Perm.mul_def {α : Type u} (f : Equiv.Perm α) (g : Equiv.Perm α) :
      f * g = g.trans f
      theorem Equiv.Perm.inv_def {α : Type u} (f : Equiv.Perm α) :
      f⁻¹ = f.symm
      @[simp]
      theorem Equiv.Perm.coe_one {α : Type u} :
      1 = id
      @[simp]
      theorem Equiv.Perm.coe_mul {α : Type u} (f : Equiv.Perm α) (g : Equiv.Perm α) :
      ↑(f * g) = f g
      theorem Equiv.Perm.coe_pow {α : Type u} (f : Equiv.Perm α) (n : ) :
      ↑(f ^ n) = (f)^[n]
      @[simp]
      theorem Equiv.Perm.iterate_eq_pow {α : Type u} (f : Equiv.Perm α) (n : ) :
      (f)^[n] = ↑(f ^ n)
      theorem Equiv.Perm.eq_inv_iff_eq {α : Type u} {f : Equiv.Perm α} {x : α} {y : α} :
      x = f⁻¹ y f x = y
      theorem Equiv.Perm.inv_eq_iff_eq {α : Type u} {f : Equiv.Perm α} {x : α} {y : α} :
      f⁻¹ x = y x = f y
      theorem Equiv.Perm.zpow_apply_comm {α : Type u_1} (σ : Equiv.Perm α) (m : ) (n : ) {x : α} :
      ↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)
      @[simp]
      theorem Equiv.Perm.image_inv {α : Type u} (f : Equiv.Perm α) (s : Set α) :
      f⁻¹ '' s = f ⁻¹' s
      @[simp]
      theorem Equiv.Perm.preimage_inv {α : Type u} (f : Equiv.Perm α) (s : Set α) :
      f⁻¹ ⁻¹' s = f '' s

      Lemmas about mixing Perm with Equiv. Because we have multiple ways to express Equiv.refl, Equiv.symm, and Equiv.trans, we want simp lemmas for every combination. The assumption made here is that if you're using the group structure, you want to preserve it after simp.

      @[simp]
      theorem Equiv.Perm.trans_one {α : Sort u_1} {β : Type u_2} (e : α β) :
      e.trans 1 = e
      @[simp]
      theorem Equiv.Perm.mul_refl {α : Type u} (e : Equiv.Perm α) :
      e * Equiv.refl α = e
      @[simp]
      theorem Equiv.Perm.one_symm {α : Type u} :
      1.symm = 1
      @[simp]
      theorem Equiv.Perm.refl_inv {α : Type u} :
      @[simp]
      theorem Equiv.Perm.one_trans {α : Type u_1} {β : Sort u_2} (e : α β) :
      1.trans e = e
      @[simp]
      theorem Equiv.Perm.refl_mul {α : Type u} (e : Equiv.Perm α) :
      Equiv.refl α * e = e
      @[simp]
      theorem Equiv.Perm.inv_trans_self {α : Type u} (e : Equiv.Perm α) :
      e⁻¹.trans e = 1
      @[simp]
      theorem Equiv.Perm.mul_symm {α : Type u} (e : Equiv.Perm α) :
      e * e.symm = 1
      @[simp]
      theorem Equiv.Perm.self_trans_inv {α : Type u} (e : Equiv.Perm α) :
      e.trans e⁻¹ = 1
      @[simp]
      theorem Equiv.Perm.symm_mul {α : Type u} (e : Equiv.Perm α) :
      e.symm * e = 1

      Lemmas about Equiv.Perm.sumCongr re-expressed via the group structure.

      @[simp]
      theorem Equiv.Perm.sumCongr_mul {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β) :
      @[simp]
      @[simp]
      theorem Equiv.Perm.sumCongr_one {α : Type u_1} {β : Type u_2} :
      @[simp]
      theorem Equiv.Perm.sumCongrHom_apply (α : Type u_1) (β : Type u_2) (a : Equiv.Perm α × Equiv.Perm β) :
      def Equiv.Perm.sumCongrHom (α : Type u_1) (β : Type u_2) :

      Equiv.Perm.sumCongr as a MonoidHom, with its two arguments bundled into a single prod.

      This is particularly useful for its MonoidHom.range projection, which is the subgroup of permutations which do not exchange elements between α and β.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Equiv.Perm.sumCongr_swap_one {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (i : α) (j : α) :
        @[simp]
        theorem Equiv.Perm.sumCongr_one_swap {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (i : β) (j : β) :

        Lemmas about Equiv.Perm.sigmaCongrRight re-expressed via the group structure.

        @[simp]
        theorem Equiv.Perm.sigmaCongrRight_mul {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) (G : (a : α) → Equiv.Perm (β a)) :
        @[simp]
        theorem Equiv.Perm.sigmaCongrRight_inv {α : Type u_1} {β : αType u_2} (F : (a : α) → Equiv.Perm (β a)) :
        @[simp]
        theorem Equiv.Perm.sigmaCongrRight_one {α : Type u_1} {β : αType u_2} :
        @[simp]
        theorem Equiv.Perm.sigmaCongrRightHom_apply {α : Type u_1} (β : αType u_2) (F : (a : α) → Equiv.Perm (β a)) :
        def Equiv.Perm.sigmaCongrRightHom {α : Type u_1} (β : αType u_2) :
        ((a : α) → Equiv.Perm (β a)) →* Equiv.Perm ((a : α) × β a)

        Equiv.Perm.sigmaCongrRight as a MonoidHom.

        This is particularly useful for its MonoidHom.range projection, which is the subgroup of permutations which do not exchange elements between fibers.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Equiv.Perm.subtypeCongrHom_apply {α : Type u} (p : αProp) [DecidablePred p] (pair : Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a }) :
          def Equiv.Perm.subtypeCongrHom {α : Type u} (p : αProp) [DecidablePred p] :
          Equiv.Perm { a // p a } × Equiv.Perm { a // ¬p a } →* Equiv.Perm α

          Equiv.Perm.subtypeCongr as a MonoidHom.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Equiv.Perm.permCongr_eq_mul {α : Type u} (e : Equiv.Perm α) (p : Equiv.Perm α) :
            ↑(Equiv.permCongr e) p = e * p * e⁻¹

            If e is also a permutation, we can write permCongr completely in terms of the group structure.

            Lemmas about Equiv.Perm.extendDomain re-expressed via the group structure.

            @[simp]
            theorem Equiv.Perm.extendDomain_one {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] (f : α Subtype p) :
            @[simp]
            @[simp]
            theorem Equiv.Perm.extendDomain_mul {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] (f : α Subtype p) (e : Equiv.Perm α) (e' : Equiv.Perm α) :
            @[simp]
            theorem Equiv.Perm.extendDomainHom_apply {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] (f : α Subtype p) (e : Equiv.Perm α) :
            def Equiv.Perm.extendDomainHom {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] (f : α Subtype p) :

            extendDomain as a group homomorphism

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Equiv.Perm.extendDomain_eq_one_iff {α : Type u} {β : Type v} {p : βProp} [DecidablePred p] {e : Equiv.Perm α} {f : α Subtype p} :
              @[simp]
              theorem Equiv.Perm.extendDomain_pow {α : Type u} {β : Type v} (e : Equiv.Perm α) {p : βProp} [DecidablePred p] (f : α Subtype p) (n : ) :
              @[simp]
              theorem Equiv.Perm.extendDomain_zpow {α : Type u} {β : Type v} (e : Equiv.Perm α) {p : βProp} [DecidablePred p] (f : α Subtype p) (n : ) :
              def Equiv.Perm.subtypePerm {α : Type u} {p : αProp} (f : Equiv.Perm α) (h : ∀ (x : α), p x p (f x)) :
              Equiv.Perm { x // p x }

              If the permutation f fixes the subtype {x // p x}, then this returns the permutation on {x // p x} induced by f.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Equiv.Perm.subtypePerm_apply {α : Type u} {p : αProp} (f : Equiv.Perm α) (h : ∀ (x : α), p x p (f x)) (x : { x // p x }) :
                ↑(Equiv.Perm.subtypePerm f h) x = { val := f x, property := (h x).mp x.property }
                @[simp]
                theorem Equiv.Perm.subtypePerm_one {α : Type u} (p : αProp) (h : optParam (∀ (x : α), p x p x) (_ : ∀ (x : α), p x p x)) :
                @[simp]
                theorem Equiv.Perm.subtypePerm_mul {α : Type u} {p : αProp} (f : Equiv.Perm α) (g : Equiv.Perm α) (hf : ∀ (x : α), p x p (f x)) (hg : ∀ (x : α), p x p (g x)) :
                Equiv.Perm.subtypePerm f hf * Equiv.Perm.subtypePerm g hg = Equiv.Perm.subtypePerm (f * g) (_ : ∀ (x : α), p x p (↑(f * g) x))
                theorem Equiv.Perm.subtypePerm_inv {α : Type u} {p : αProp} (f : Equiv.Perm α) (hf : ∀ (x : α), p x p (f⁻¹ x)) :
                Equiv.Perm.subtypePerm f⁻¹ hf = (Equiv.Perm.subtypePerm f (_ : ∀ (x : α), p x p (f x)))⁻¹

                See Equiv.Perm.inv_subtypePerm

                @[simp]
                theorem Equiv.Perm.inv_subtypePerm {α : Type u} {p : αProp} (f : Equiv.Perm α) (hf : ∀ (x : α), p x p (f x)) :
                (Equiv.Perm.subtypePerm f hf)⁻¹ = Equiv.Perm.subtypePerm f⁻¹ (_ : ∀ (x : α), p x p (f⁻¹ x))

                See Equiv.Perm.subtypePerm_inv

                @[simp]
                theorem Equiv.Perm.subtypePerm_pow {α : Type u} {p : αProp} (f : Equiv.Perm α) (n : ) (hf : ∀ (x : α), p x p (f x)) :
                Equiv.Perm.subtypePerm f hf ^ n = Equiv.Perm.subtypePerm (f ^ n) (_ : ∀ (x : α), p x p (↑(f ^ n) x))
                @[simp]
                theorem Equiv.Perm.subtypePerm_zpow {α : Type u} {p : αProp} (f : Equiv.Perm α) (n : ) (hf : ∀ (x : α), p x p (f x)) :
                Equiv.Perm.subtypePerm f hf ^ n = Equiv.Perm.subtypePerm (f ^ n) (_ : ∀ (x : α), p x p (↑(f ^ n) x))

                The inclusion map of permutations on a subtype of α into permutations of α, fixing the other points.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Equiv.Perm.ofSubtype_subtypePerm {α : Type u} {p : αProp} [DecidablePred p] {f : Equiv.Perm α} (h₁ : ∀ (x : α), p x p (f x)) (h₂ : (x : α) → f x xp x) :
                  Equiv.Perm.ofSubtype (Equiv.Perm.subtypePerm f h₁) = f
                  theorem Equiv.Perm.ofSubtype_apply_of_mem {α : Type u} {p : αProp} [DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (ha : p a) :
                  ↑(Equiv.Perm.ofSubtype f) a = ↑(f { val := a, property := ha })
                  @[simp]
                  theorem Equiv.Perm.ofSubtype_apply_coe {α : Type u} {p : αProp} [DecidablePred p] (f : Equiv.Perm (Subtype p)) (x : Subtype p) :
                  ↑(Equiv.Perm.ofSubtype f) x = ↑(f x)
                  theorem Equiv.Perm.ofSubtype_apply_of_not_mem {α : Type u} {p : αProp} [DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (ha : ¬p a) :
                  ↑(Equiv.Perm.ofSubtype f) a = a
                  theorem Equiv.Perm.mem_iff_ofSubtype_apply_mem {α : Type u} {p : αProp} [DecidablePred p] (f : Equiv.Perm (Subtype p)) (x : α) :
                  p x p (↑(Equiv.Perm.ofSubtype f) x)
                  @[simp]
                  theorem Equiv.Perm.subtypePerm_ofSubtype {α : Type u} {p : αProp} [DecidablePred p] (f : Equiv.Perm (Subtype p)) :
                  Equiv.Perm.subtypePerm (Equiv.Perm.ofSubtype f) (_ : ∀ (x : α), p x p (↑(Equiv.Perm.ofSubtype f) x)) = f
                  @[simp]
                  theorem Equiv.Perm.subtypeEquivSubtypePerm_symm_apply {α : Type u} (p : αProp) [DecidablePred p] (f : { f // ∀ (a : α), ¬p af a = a }) :
                  (Equiv.Perm.subtypeEquivSubtypePerm p).symm f = Equiv.Perm.subtypePerm f (_ : ∀ (a : α), p a p (f a))
                  @[simp]
                  theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_coe {α : Type u} (p : αProp) [DecidablePred p] (f : Equiv.Perm (Subtype p)) :
                  ↑(↑(Equiv.Perm.subtypeEquivSubtypePerm p) f) = Equiv.Perm.ofSubtype f
                  def Equiv.Perm.subtypeEquivSubtypePerm {α : Type u} (p : αProp) [DecidablePred p] :
                  Equiv.Perm (Subtype p) { f // ∀ (a : α), ¬p af a = a }

                  Permutations on a subtype are equivalent to permutations on the original type that fix pointwise the rest.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_of_mem {α : Type u} {p : αProp} [DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)) (h : p a) :
                    ↑(Equiv.toFun (Equiv.Perm.subtypeEquivSubtypePerm p) f) a = ↑(f { val := a, property := h })
                    @[simp]
                    theorem Equiv.swap_inv {α : Type u} [DecidableEq α] (x : α) (y : α) :
                    @[simp]
                    theorem Equiv.swap_mul_self {α : Type u} [DecidableEq α] (i : α) (j : α) :
                    theorem Equiv.swap_mul_eq_mul_swap {α : Type u} [DecidableEq α] (f : Equiv.Perm α) (x : α) (y : α) :
                    Equiv.swap x y * f = f * Equiv.swap (f⁻¹ x) (f⁻¹ y)
                    theorem Equiv.mul_swap_eq_swap_mul {α : Type u} [DecidableEq α] (f : Equiv.Perm α) (x : α) (y : α) :
                    f * Equiv.swap x y = Equiv.swap (f x) (f y) * f
                    theorem Equiv.swap_apply_apply {α : Type u} [DecidableEq α] (f : Equiv.Perm α) (x : α) (y : α) :
                    Equiv.swap (f x) (f y) = f * Equiv.swap x y * f⁻¹
                    @[simp]
                    theorem Equiv.swap_mul_self_mul {α : Type u} [DecidableEq α] (i : α) (j : α) (σ : Equiv.Perm α) :
                    Equiv.swap i j * (Equiv.swap i j * σ) = σ

                    Left-multiplying a permutation with swap i j twice gives the original permutation.

                    This specialization of swap_mul_self is useful when using cosets of permutations.

                    @[simp]
                    theorem Equiv.mul_swap_mul_self {α : Type u} [DecidableEq α] (i : α) (j : α) (σ : Equiv.Perm α) :
                    σ * Equiv.swap i j * Equiv.swap i j = σ

                    Right-multiplying a permutation with swap i j twice gives the original permutation.

                    This specialization of swap_mul_self is useful when using cosets of permutations.

                    @[simp]
                    theorem Equiv.swap_mul_involutive {α : Type u} [DecidableEq α] (i : α) (j : α) :
                    Function.Involutive ((fun x x_1 => x * x_1) (Equiv.swap i j))

                    A stronger version of mul_right_injective

                    @[simp]
                    theorem Equiv.mul_swap_involutive {α : Type u} [DecidableEq α] (i : α) (j : α) :

                    A stronger version of mul_left_injective

                    @[simp]
                    theorem Equiv.swap_eq_one_iff {α : Type u} [DecidableEq α] {i : α} {j : α} :
                    Equiv.swap i j = 1 i = j
                    theorem Equiv.swap_mul_eq_iff {α : Type u} [DecidableEq α] {i : α} {j : α} {σ : Equiv.Perm α} :
                    Equiv.swap i j * σ = σ i = j
                    theorem Equiv.mul_swap_eq_iff {α : Type u} [DecidableEq α] {i : α} {j : α} {σ : Equiv.Perm α} :
                    σ * Equiv.swap i j = σ i = j
                    theorem Equiv.swap_mul_swap_mul_swap {α : Type u} [DecidableEq α] {x : α} {y : α} {z : α} (hwz : x y) (hxz : x z) :
                    @[simp]
                    theorem Equiv.addLeft_zero {α : Type u} [AddGroup α] :
                    @[simp]
                    theorem Equiv.addRight_zero {α : Type u} [AddGroup α] :
                    @[simp]
                    theorem Equiv.addLeft_add {α : Type u} [AddGroup α] (a : α) (b : α) :
                    @[simp]
                    theorem Equiv.addRight_add {α : Type u} [AddGroup α] (a : α) (b : α) :
                    @[simp]
                    theorem Equiv.inv_addLeft {α : Type u} [AddGroup α] (a : α) :
                    @[simp]
                    theorem Equiv.inv_addRight {α : Type u} [AddGroup α] (a : α) :
                    @[simp]
                    theorem Equiv.pow_addLeft {α : Type u} [AddGroup α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.pow_addRight {α : Type u} [AddGroup α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.zpow_addLeft {α : Type u} [AddGroup α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.zpow_addRight {α : Type u} [AddGroup α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.mulLeft_one {α : Type u} [Group α] :
                    @[simp]
                    theorem Equiv.mulRight_one {α : Type u} [Group α] :
                    @[simp]
                    theorem Equiv.mulLeft_mul {α : Type u} [Group α] (a : α) (b : α) :
                    @[simp]
                    theorem Equiv.mulRight_mul {α : Type u} [Group α] (a : α) (b : α) :
                    @[simp]
                    theorem Equiv.inv_mulLeft {α : Type u} [Group α] (a : α) :
                    @[simp]
                    @[simp]
                    theorem Equiv.pow_mulLeft {α : Type u} [Group α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.pow_mulRight {α : Type u} [Group α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.zpow_mulLeft {α : Type u} [Group α] (a : α) (n : ) :
                    @[simp]
                    theorem Equiv.zpow_mulRight {α : Type u} [Group α] (a : α) (n : ) :
                    theorem Set.BijOn.perm_inv {α : Type u_1} {f : Equiv.Perm α} {s : Set α} (hf : Set.BijOn (f) s s) :
                    Set.BijOn (f⁻¹) s s
                    theorem Set.MapsTo.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} :
                    Set.MapsTo (f) s s∀ (n : ), Set.MapsTo (↑(f ^ n)) s s
                    theorem Set.SurjOn.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} :
                    Set.SurjOn (f) s s∀ (n : ), Set.SurjOn (↑(f ^ n)) s s
                    theorem Set.BijOn.perm_pow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} :
                    Set.BijOn (f) s s∀ (n : ), Set.BijOn (↑(f ^ n)) s s
                    theorem Set.BijOn.perm_zpow {α : Type u_1} {f : Equiv.Perm α} {s : Set α} (hf : Set.BijOn (f) s s) (n : ) :
                    Set.BijOn (↑(f ^ n)) s s