Mathlib.GroupTheory.Perm.Finite

Equiv.Perm.isConj_of_support_equiv theorem

 (f : { x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
  (hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)), (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) : IsConj σ τ

Full source

theorem isConj_of_support_equiv
    (f : { x // x ∈ (σ.support : Set α) }{ x // x ∈ (σ.support : Set α) } ≃ { x // x ∈ (τ.support : Set α) })
    (hf : ∀ (x : α) (hx : x ∈ (σ.support : Set α)),
      (f ⟨σ x, apply_mem_support.2 hx⟩ : α) = τ ↑(f ⟨x, hx⟩)) :
    IsConj σ τ := by
  refine isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩
  rw [mul_inv_eq_iff_eq_mul]
  ext x
  simp only [Perm.mul_apply]
  by_cases hx : x ∈ σ.support
  · rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
    · exact hf x (Finset.mem_coe.2 hx)
  · rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
      Classical.not_not.1 ((not_congr mem_support).mp hx)]

Conjugacy of Permutations via Support Equivalence

Informal description

Let $\sigma$ and $\tau$ be permutations of a type $\alpha$. Suppose there exists an equivalence $f$ between the supports of $\sigma$ and $\tau$ (viewed as sets) such that for every $x$ in the support of $\sigma$, $f(\sigma x) = \tau(f x)$. Then $\sigma$ and $\tau$ are conjugate permutations, i.e., there exists a permutation $\rho$ such that $\sigma = \rho \tau \rho^{-1}$.

Equiv.Perm.perm_inv_on_of_perm_on_finset theorem

{s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α} (hy : y ∈ s) : f⁻¹ y ∈ s

Full source

theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
    (hy : y ∈ s) : f⁻¹f⁻¹ y ∈ s := by
  have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
    Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
      (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
  obtain ⟨y2, hy2, heq⟩ := h0 y hy
  convert hy2
  rw [heq]
  simp only [inv_apply_self]

Inverse Permutation Preserves Membership in Finite Set

Informal description

Let $s$ be a finite set of elements of type $\alpha$, and let $f$ be a permutation on $\alpha$ such that for every $x \in s$, $f(x) \in s$. Then for any $y \in s$, the inverse permutation $f^{-1}$ satisfies $f^{-1}(y) \in s$.

Equiv.Perm.perm_inv_mapsTo_of_mapsTo theorem

(f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) : Set.MapsTo (f⁻¹ :) s s

Full source

theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
    Set.MapsTo (f⁻¹ :) s s := by
  cases nonempty_fintype s
  exact fun x hx =>
    Set.mem_toFinset.mp <|
      perm_inv_on_of_perm_on_finset
        (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
        (Set.mem_toFinset.mpr hx)

Inverse Permutation Preserves Finite Set Membership under Forward Mapping

Informal description

Let $f$ be a permutation on a type $\alpha$, and let $s$ be a finite subset of $\alpha$. If $f$ maps every element of $s$ to another element of $s$, then the inverse permutation $f^{-1}$ also maps every element of $s$ to another element of $s$.

Equiv.Perm.perm_inv_mapsTo_iff_mapsTo theorem

{f : Perm α} {s : Set α} [Finite s] : Set.MapsTo (f⁻¹ :) s s ↔ Set.MapsTo f s s

Full source

@[simp]
theorem perm_inv_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] :
    Set.MapsToSet.MapsTo (f⁻¹ :) s s ↔ Set.MapsTo f s s :=
  ⟨perm_inv_mapsTo_of_mapsTo f⁻¹, perm_inv_mapsTo_of_mapsTo f⟩

Equivalence of Forward and Inverse Mapping for Permutations on Finite Sets

Informal description

Let $f$ be a permutation on a type $\alpha$, and let $s$ be a finite subset of $\alpha$. Then the inverse permutation $f^{-1}$ maps every element of $s$ to another element of $s$ if and only if $f$ maps every element of $s$ to another element of $s$.

Equiv.Perm.perm_inv_on_of_perm_on_finite theorem

{f : Perm α} {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x)

Full source

theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop} [Finite { x // p x }]
    (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x) := by
  have : Finite { x | p x } := by simpa
  simpa using perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx

Inverse Permutation Preserves Finite Subtype Property under Forward Preservation

Informal description

Let $f$ be a permutation on a type $\alpha$, and let $p : \alpha \to \text{Prop}$ be a predicate such that the subtype $\{x \mid p x\}$ is finite. If $f$ preserves $p$ (i.e., for all $x \in \alpha$, $p(x)$ implies $p(f(x))$), then for any $x \in \alpha$ satisfying $p(x)$, the inverse permutation $f^{-1}$ also preserves $p$ at $x$ (i.e., $p(f^{-1}(x))$ holds).

Equiv.Perm.subtypePermOfFintype abbrev

(f : Perm α) {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x)) : Perm { x // p x }

Full source

/-- 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`. -/
abbrev subtypePermOfFintype (f : Perm α) {p : α → Prop} [Finite { x // p x }]
    (h : ∀ x, p x → p (f x)) : Perm { x // p x } :=
  f.subtypePerm fun x => ⟨h x, fun h₂ => f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂⟩

Permutation Restriction to Finite Subtype

Informal description

Given a permutation $f$ of a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$ such that the subtype $\{x \mid p x\}$ is finite, if $f$ maps elements satisfying $p$ to elements satisfying $p$ (i.e., $\forall x, p x \to p (f x)$), then $f$ induces a permutation on the subtype $\{x \mid p x\}$.

Equiv.Perm.subtypePermOfFintype_apply theorem

 (f : Perm α) {p : α → Prop} [Finite { x // p x }] (h : ∀ x, p x → p (f x)) (x : { x // p x }) :
  subtypePermOfFintype f h x = ⟨f x, h x x.2⟩

Full source

@[simp]
theorem subtypePermOfFintype_apply (f : Perm α) {p : α → Prop} [Finite { x // p x }]
    (h : ∀ x, p x → p (f x)) (x : { x // p x }) : subtypePermOfFintype f h x = ⟨f x, h x x.2⟩ :=
  rfl

Application of Restricted Permutation to Finite Subtype

Informal description

Given a permutation $f$ of a type $\alpha$ and a predicate $p : \alpha \to \text{Prop}$ such that the subtype $\{x \mid p x\}$ is finite, if $f$ preserves $p$ (i.e., $\forall x, p x \to p (f x)$), then for any element $x$ in the subtype $\{x \mid p x\}$, the application of the restricted permutation $\text{subtypePermOfFintype}\,f\,h$ to $x$ equals $\langle f\,x, h\,x\,x.2\rangle$, where $x.2$ is the proof that $p\,x$ holds.

Equiv.Perm.subtypePermOfFintype_one theorem

(p : α → Prop) [Finite { x // p x }] (h : ∀ x, p x → p ((1 : Perm α) x)) : @subtypePermOfFintype α 1 p _ h = 1

Full source

theorem subtypePermOfFintype_one (p : α → Prop) [Finite { x // p x }]
    (h : ∀ x, p x → p ((1 : Perm α) x)) : @subtypePermOfFintype α 1 p _ h = 1 :=
  rfl

Identity Permutation Restriction to Finite Subtype is Identity

Informal description

For any predicate $p : \alpha \to \text{Prop}$ such that the subtype $\{x \mid p x\}$ is finite, if the identity permutation $1$ on $\alpha$ preserves $p$ (i.e., $\forall x, p x \to p (1 x)$), then the restricted permutation $\text{subtypePermOfFintype}\,1\,h$ on the subtype $\{x \mid p x\}$ is equal to the identity permutation $1$ on this subtype.

Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr theorem

 {m n : Type*} [Finite m] [Finite n] (σ : Perm (m ⊕ n)) :
  Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr)

Full source

theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : Perm (m ⊕ n)) :
    Set.MapsToSet.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔
      Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr) := by
  constructor <;>
    ( intro h
      classical
        rw [← perm_inv_mapsTo_iff_mapsTo] at h
        intro x
        rcases hx : σ x with l | r)
  · rintro ⟨a, rfl⟩
    obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
    rw [← hx, σ.inv_apply_self] at hy
    exact absurd hy Sum.inl_ne_inr
  · rintro _; exact ⟨r, rfl⟩
  · rintro _; exact ⟨l, rfl⟩
  · rintro ⟨a, rfl⟩
    obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
    rw [← hx, σ.inv_apply_self] at hy
    exact absurd hy Sum.inr_ne_inl

Permutation Preserves Left Inclusion iff it Preserves Right Inclusion in Disjoint Union of Finite Types

Informal description

Let $m$ and $n$ be finite types, and let $\sigma$ be a permutation of the disjoint union $m \sqcup n$. Then $\sigma$ maps the left inclusion $\text{inl}(m)$ into itself if and only if $\sigma$ maps the right inclusion $\text{inr}(n)$ into itself.

Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl theorem

 {m n : Type*} [Finite m] [Finite n] {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
  σ ∈ (sumCongrHom m n).range

Full source

theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n]
    {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
    σ ∈ (sumCongrHom m n).range := by
  classical
    have h1 : ∀ x : m ⊕ n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x := by
      rintro x ⟨a, ha⟩
      apply h
      rw [← ha]
      exact ⟨a, rfl⟩
    have h3 : ∀ x : m ⊕ n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x := by
      rintro x ⟨b, hb⟩
      apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
      rw [← hb]
      exact ⟨b, rfl⟩
    let σ₁' := subtypePermOfFintype σ h1
    let σ₂' := subtypePermOfFintype σ h3
    let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
    let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
    rw [MonoidHom.mem_range, Prod.exists]
    use σ₁, σ₂
    rw [Perm.sumCongrHom_apply]
    ext x
    rcases x with a | b
    · rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm,
        apply_ofInjective_symm Sum.inl_injective]
      rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
      dsimp [Set.range]
      rw [subtypePerm_apply]
    · rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
        apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
      dsimp [Set.range]
      rw [subtypePerm_apply]

Permutation Preserving Left Inclusion is in Sum Congruence Homomorphism Range

Informal description

Let $m$ and $n$ be finite types, and let $\sigma$ be a permutation of the disjoint union $m \sqcup n$. If $\sigma$ maps the left inclusion $\text{inl}(m)$ into itself, then $\sigma$ lies in the range of the homomorphism $\text{sumCongrHom}\,m\,n$ that constructs a permutation of $m \sqcup n$ from a pair of permutations of $m$ and $n$.

Equiv.Perm.Disjoint.orderOf theorem

{σ τ : Perm α} (hστ : Disjoint σ τ) : orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ)

Full source

nonrec theorem Disjoint.orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) :
    orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=
  haveI h : ∀ n : ℕ, (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1 := fun n => by
    rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
  Nat.dvd_antisymm hστ.commute.orderOf_mul_dvd_lcm
    (Nat.lcm_dvd
      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).1)
      (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).2))

Order of Composition of Disjoint Permutations is LCM of Individual Orders

Informal description

For any two disjoint permutations $\sigma$ and $\tau$ of a type $\alpha$, the order of their composition $\sigma \circ \tau$ is equal to the least common multiple of the orders of $\sigma$ and $\tau$.

Equiv.Perm.Disjoint.extendDomain theorem

 {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) {σ τ : Perm α} (h : Disjoint σ τ) :
  Disjoint (σ.extendDomain f) (τ.extendDomain f)

Full source

theorem Disjoint.extendDomain {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p)
    {σ τ : Perm α} (h : Disjoint σ τ) : Disjoint (σ.extendDomain f) (τ.extendDomain f) := by
  intro b
  by_cases pb : p b
  · refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_ <;>
      · intro h
        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
  · left
    rw [extendDomain_apply_not_subtype _ _ pb]

Extension of Disjoint Permutations Preserves Disjointness

Informal description

Let $p$ be a decidable predicate on a type $\beta$, and let $f : \alpha \simeq \{x \in \beta \mid p(x)\}$ be an equivalence between $\alpha$ and the subtype of $\beta$ satisfying $p$. For any two disjoint permutations $\sigma, \tau$ of $\alpha$, their extensions $\sigma.\text{extendDomain}\,f$ and $\tau.\text{extendDomain}\,f$ are also disjoint permutations of $\beta$.

Equiv.Perm.Disjoint.isConj_mul theorem

 [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) :
  IsConj (σ * τ) (π * ρ)

Full source

theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π)
    (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ) (hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
  classical
    cases nonempty_fintype α
    obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
    obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
    have hd1' := coe_inj.2 hd1.support_mul
    have hd2' := coe_inj.2 hd2.support_mul
    rw [coe_union] at *
    have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
    have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
    refine isConj_of_support_equiv ?_ ?_
    · refine
          ((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans
            ((Equiv.sumCongr (subtypeEquiv f fun a => ?_) (subtypeEquiv g fun a => ?_)).trans
              ((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm) <;>
      · simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map,
          apply_eq_iff_eq]
    · intro x hx
      simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply,
        Equiv.sumCongr_apply]
      rw [hd1', Set.mem_union] at hx
      rcases hx with hxσ | hxτ
      · rw [mem_coe, mem_support] at hxσ
        rw [Set.union_apply_left, Set.union_apply_left]
        · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
            Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq]
          have h := (hd2 (f x)).resolve_left ?_
          · rw [mul_apply, mul_apply] at h
            rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
        · rwa [Subtype.coe_mk, mem_coe, mem_support]
        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
            apply_mem_support, mem_support]
      · rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
        rw [Set.union_apply_right, Set.union_apply_right]
        · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
            Set.union_symm_apply_right, Subtype.coe_mk, apply_eq_iff_eq]
          have h := (hd2 (g (τ x))).resolve_right ?_
          · rw [mul_apply, mul_apply] at h
            rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
          · rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
        · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
        · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
            mem_coe, mem_support]

Conjugacy of Products of Disjoint Conjugate Permutations on Finite Types

Informal description

Let $\alpha$ be a finite type, and let $\sigma, \tau, \pi, \rho$ be permutations of $\alpha$. If $\sigma$ is conjugate to $\pi$, $\tau$ is conjugate to $\rho$, and the pairs $(\sigma, \tau)$ and $(\pi, \rho)$ are disjoint, then the product $\sigma \circ \tau$ is conjugate to the product $\pi \circ \rho$.

Equiv.Perm.mem_fixedPoints_iff_apply_mem_of_mem_centralizer theorem

 {g p : Perm α} (hp : p ∈ Subgroup.centralizer { g }) {x : α} :
  x ∈ Function.fixedPoints g ↔ p x ∈ Function.fixedPoints g

Full source

theorem mem_fixedPoints_iff_apply_mem_of_mem_centralizer {g p : Perm α}
    (hp : p ∈ Subgroup.centralizer {g}) {x : α} :
    x ∈ Function.fixedPoints gx ∈ Function.fixedPoints g ↔ p x ∈ Function.fixedPoints g :=  by
  simp only [Subgroup.mem_centralizer_singleton_iff] at hp
  simp only [Function.mem_fixedPoints_iff]
  rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

Fixed Points under Commuting Permutations

Informal description

For any permutations $g$ and $p$ of a type $\alpha$, if $p$ commutes with $g$ (i.e., $p$ is in the centralizer of the subgroup generated by $g$), then for any element $x \in \alpha$, $x$ is a fixed point of $g$ if and only if $p(x)$ is a fixed point of $g$.

Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self theorem

{g : Perm α} (u : Perm (Function.fixedPoints g)) : Disjoint (ofSubtype u) g

Full source

lemma disjoint_ofSubtype_of_memFixedPoints_self {g : Perm α}
    (u : Perm (Function.fixedPoints g)) :
    Disjoint (ofSubtype u) g := by
  rw [disjoint_iff_eq_or_eq]
  intro x
  by_cases hx : x ∈ Function.fixedPoints g
  · right; exact hx
  · left; rw [ofSubtype_apply_of_not_mem u hx]

Disjointness of Lifted Permutation and Original Permutation on Fixed Points

Informal description

For any permutation $g$ of a type $\alpha$ and any permutation $u$ of the fixed points of $g$, the permutation obtained by lifting $u$ to $\alpha$ (denoted as $\text{ofSubtype}\,u$) is disjoint from $g$. That is, for every $x \in \alpha$, either $(\text{ofSubtype}\,u)(x) = x$ or $g(x) = x$.

Equiv.Perm.support_pow_coprime theorem

{σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) : (σ ^ n).support = σ.support

Full source

theorem support_pow_coprime {σ : Perm α} {n : ℕ} (h : Nat.Coprime n (orderOf σ)) :
    (σ ^ n).support = σ.support := by
  obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
  exact
    le_antisymm (support_pow_le σ n)
      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Support Equality for Coprime Powers of a Permutation

Informal description

For any permutation $\sigma$ of a type $\alpha$ and any natural number $n$ coprime to the order of $\sigma$, the support of $\sigma^n$ is equal to the support of $\sigma$. That is, $\text{supp}(\sigma^n) = \text{supp}(\sigma)$.

Equiv.Perm.ofSubtype_support_disjoint theorem

{σ : Perm α} (x : Perm (Function.fixedPoints σ)) : _root_.Disjoint x.ofSubtype.support σ.support

Full source

lemma ofSubtype_support_disjoint {σ : Perm α} (x : Perm (Function.fixedPoints σ)) :
    _root_.Disjoint x.ofSubtype.support σ.support := by
  rw [Finset.disjoint_iff_ne]
  rintro a ha b hb rfl
  rw [mem_support] at ha hb
  exact ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

Disjointness of Lifted Permutation Support and Original Permutation Support

Informal description

For any permutation $\sigma$ of a type $\alpha$ and any permutation $x$ of the fixed points of $\sigma$, the support of the lifted permutation $x.\text{ofSubtype}$ is disjoint from the support of $\sigma$. That is, there is no element $y \in \alpha$ such that both $x.\text{ofSubtype}(y) \neq y$ and $\sigma(y) \neq y$.

Equiv.Perm.disjoint_of_disjoint_support theorem

{H K : Subgroup (Perm α)} (h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support) : _root_.Disjoint H K

Full source

lemma disjoint_of_disjoint_support {H K : Subgroup (Perm α)}
    (h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support) :
    _root_.Disjoint H K := by
  rw [disjoint_iff_inf_le]
  intro x ⟨hx1, hx2⟩
  specialize h x hx1 x hx2
  rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h

Disjointness of Permutation Subgroups via Disjoint Supports

Informal description

Let $H$ and $K$ be subgroups of the permutation group of a type $\alpha$. If for every permutation $a \in H$ and every permutation $b \in K$, the supports of $a$ and $b$ are disjoint, then the subgroups $H$ and $K$ themselves are disjoint.

Equiv.Perm.support_closure_subset_union theorem

(S : Set (Perm α)) : ∀ a ∈ closure S, (a.support : Set α) ⊆ ⋃ b ∈ S, b.support

Full source

lemma support_closure_subset_union (S : Set (Perm α)) :
    ∀ a ∈ closure S, (a.support : Set α) ⊆ ⋃ b ∈ S, b.support := by
  apply closure_induction
  · exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl
  · simp only [support_one, Finset.coe_empty, Set.empty_subset]
  · intro a b ha hb hc hd
    refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_
    rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]
    exact ⟨hc, hd⟩
  · simp only [support_inv, imp_self, implies_true]

Support of Permutation in Generated Subgroup is Contained in Union of Supports

Informal description

For any set $S$ of permutations of a type $\alpha$, the support of any permutation $a$ in the subgroup generated by $S$ is contained in the union of the supports of the permutations in $S$. That is, for all $a \in \langle S \rangle$, we have $\text{supp}(a) \subseteq \bigcup_{b \in S} \text{supp}(b)$.

Equiv.Perm.disjoint_support_closure_of_disjoint_support theorem

 {S T : Set (Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
  ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support

Full source

lemma disjoint_support_closure_of_disjoint_support {S T : Set (Perm α)}
    (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
    ∀ a ∈ closure S, ∀ b ∈ closure T, _root_.Disjoint a.support b.support := by
  intro a ha b hb
  have key1 := support_closure_subset_union S a ha
  have key2 := support_closure_subset_union T b hb
  have key := Set.disjoint_of_subset key1 key2
  simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key
  exact key h

Disjoint Supports in Generated Permutation Subgroups

Informal description

For any two sets $S$ and $T$ of permutations of a type $\alpha$, if for every $a \in S$ and $b \in T$ the supports of $a$ and $b$ are disjoint, then for every $a$ in the subgroup generated by $S$ and every $b$ in the subgroup generated by $T$, the supports of $a$ and $b$ remain disjoint. In other words, if $\text{supp}(a) \cap \text{supp}(b) = \emptyset$ for all $a \in S$ and $b \in T$, then $\text{supp}(a) \cap \text{supp}(b) = \emptyset$ for all $a \in \langle S \rangle$ and $b \in \langle T \rangle$.

Equiv.Perm.disjoint_closure_of_disjoint_support theorem

 {S T : Set (Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
  _root_.Disjoint (closure S) (closure T)

Full source

lemma disjoint_closure_of_disjoint_support {S T : Set (Perm α)}
    (h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support) :
    _root_.Disjoint (closure S) (closure T) := by
  apply disjoint_of_disjoint_support
  apply disjoint_support_closure_of_disjoint_support
  exact h

Disjointness of Generated Permutation Subgroups via Disjoint Supports

Informal description

For any two sets $S$ and $T$ of permutations of a type $\alpha$, if for every $a \in S$ and $b \in T$ the supports of $a$ and $b$ are disjoint, then the subgroups generated by $S$ and $T$ are disjoint. That is, if $\text{supp}(a) \cap \text{supp}(b) = \emptyset$ for all $a \in S$ and $b \in T$, then $\langle S \rangle \cap \langle T \rangle = \emptyset$.