The equivalence relation indicating that two points are in the same cycle of a permutation.
theorem
equiv.perm.same_cycle.symm
{β : Type u_2}
(f : equiv.perm β)
{x y : β} :
f.same_cycle x y → f.same_cycle y x
theorem
equiv.perm.same_cycle.trans
{β : Type u_2}
(f : equiv.perm β)
{x y z : β} :
f.same_cycle x y → f.same_cycle y z → f.same_cycle x z
theorem
equiv.perm.same_cycle_of_is_cycle
{β : Type u_2}
{f : equiv.perm β}
(hf : f.is_cycle)
{x y : β} :
⇑f x ≠ x → ⇑f y ≠ y → f.same_cycle x y
@[instance]
Equations
- f.decidable_rel = λ (x y : α), decidable_of_iff (∃ (n : ℕ) (H : n ∈ list.range (order_of f)), ⇑(f ^ n) x = y) _
theorem
equiv.perm.same_cycle_apply
{β : Type u_2}
{f : equiv.perm β}
{x y : β} :
f.same_cycle x (⇑f y) ↔ f.same_cycle x y
theorem
equiv.perm.same_cycle_inv
{β : Type u_2}
(f : equiv.perm β)
{x y : β} :
f⁻¹.same_cycle x y ↔ f.same_cycle x y
theorem
equiv.perm.same_cycle_inv_apply
{β : Type u_2}
{f : equiv.perm β}
{x y : β} :
f.same_cycle x (⇑f⁻¹ y) ↔ f.same_cycle x y
def
equiv.perm.cycle_of
{α : Type u_1}
[decidable_eq α]
[fintype α] :
equiv.perm α → α → equiv.perm α
f.cycle_of x is the cycle of the permutation f to which x belongs.
Equations
- f.cycle_of x = ⇑equiv.perm.of_subtype (f.subtype_perm _)
theorem
equiv.perm.cycle_of_apply
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x y : α) :
theorem
equiv.perm.cycle_of_inv
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x : α) :
@[simp]
theorem
equiv.perm.cycle_of_pow_apply_self
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x : α)
(n : ℕ) :
@[simp]
theorem
equiv.perm.cycle_of_gpow_apply_self
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x : α)
(n : ℤ) :
theorem
equiv.perm.cycle_of_apply_of_same_cycle
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x y : α} :
f.same_cycle x y → ⇑(f.cycle_of x) y = ⇑f y
theorem
equiv.perm.cycle_of_apply_of_not_same_cycle
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x y : α} :
¬f.same_cycle x y → ⇑(f.cycle_of x) y = y
@[simp]
theorem
equiv.perm.cycle_of_apply_self
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x : α) :
theorem
equiv.perm.cycle_of_cycle
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
(hf : f.is_cycle)
{x : α} :
theorem
equiv.perm.is_cycle_cycle_of
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
{x : α} :
def
equiv.perm.cycle_factors_aux
{α : Type u_1}
[decidable_eq α]
[fintype α]
(l : list α)
(f : equiv.perm α) :
(∀ {x : α}, ⇑f x ≠ x → x ∈ l) → {l // l.prod = f ∧ (∀ (g : equiv.perm α), g ∈ l → g.is_cycle) ∧ list.pairwise equiv.perm.disjoint l}
Given a list l : list α and a permutation f : perm α whose nonfixed points are all in l,
recursively factors f into cycles.
Equations
- equiv.perm.cycle_factors_aux (x :: l) f h = dite (⇑f x = x) (λ (hx : ⇑f x = x), equiv.perm.cycle_factors_aux l f _) (λ (hx : ¬⇑f x = x), equiv.perm.cycle_factors_aux._match_1 x f hx (equiv.perm.cycle_factors_aux l ((f.cycle_of x)⁻¹ * f) _))
- equiv.perm.cycle_factors_aux list.nil f h = ⟨list.nil (equiv.perm α), _⟩
- equiv.perm.cycle_factors_aux._match_1 x f hx ⟨m, _⟩ = ⟨f.cycle_of x :: m, _⟩
def
equiv.perm.cycle_factors
{α : Type u_1}
[decidable_eq α]
[fintype α]
[linear_order α]
(f : equiv.perm α) :
{l // l.prod = f ∧ (∀ (g : equiv.perm α), g ∈ l → g.is_cycle) ∧ list.pairwise equiv.perm.disjoint l}
Factors a permutation f into a list of disjoint cyclic permutations that multiply to f.
Equations
theorem
equiv.perm.one_lt_nonfixed_point_card_of_ne_one
{α : Type u_1}
[decidable_eq α]
[fintype α]
{σ : equiv.perm α} :
σ ≠ 1 → 1 < (finset.filter (λ (x : α), ⇑σ x ≠ x) finset.univ).card
theorem
equiv.perm.fixed_point_card_lt_of_ne_one
{α : Type u_1}
[decidable_eq α]
[fintype α]
{σ : equiv.perm α} :
σ ≠ 1 → (finset.filter (λ (x : α), ⇑σ x = x) finset.univ).card < fintype.card α - 1