Cyclic permutations
Main definitions
In the following, f : equiv.perm β
.
equiv.perm.is_cycle
:f.is_cycle
when two nonfixed points ofβ
are related by repeated application off
.equiv.perm.same_cycle
:f.same_cycle x y
whenx
andy
are in the same cycle off
.
The following two definitions require that β
is a fintype
:
equiv.perm.cycle_of
:f.cycle_of x
is the cycle off
thatx
belongs to.equiv.perm.cycle_factors
:f.cycle_factors
is a list of disjoint cyclic permutations that multiply tof
.
is_cycle
theorem
equiv.perm.is_cycle.swap
{α : Type u_1}
[decidable_eq α]
{x y : α}
(hxy : x ≠ y) :
(equiv.swap x y).is_cycle
theorem
equiv.perm.is_cycle_swap_mul_aux₁
{α : Type u_1}
[decidable_eq α]
(n : ℕ)
{b x : α}
{f : equiv.perm α}
(hb : (⇑(equiv.swap x (⇑f x)) * f) b ≠ b)
(h : ⇑(f ^ n) (⇑f x) = b) :
theorem
equiv.perm.is_cycle_swap_mul_aux₂
{α : Type u_1}
[decidable_eq α]
(n : ℤ)
{b x : α}
{f : equiv.perm α}
(hb : (⇑(equiv.swap x (⇑f x)) * f) b ≠ b)
(h : ⇑(f ^ n) (⇑f x) = b) :
theorem
equiv.perm.is_cycle.eq_swap_of_apply_apply_eq_self
{α : Type u_1}
[decidable_eq α]
{f : equiv.perm α}
(hf : f.is_cycle)
{x : α}
(hfx : ⇑f x ≠ x)
(hffx : ⇑f (⇑f x) = x) :
f = equiv.swap x (⇑f x)
theorem
equiv.perm.is_cycle.swap_mul
{α : Type u_1}
[decidable_eq α]
{f : equiv.perm α}
(hf : f.is_cycle)
{x : α}
(hx : ⇑f x ≠ x)
(hffx : ⇑f (⇑f x) ≠ x) :
((equiv.swap x (⇑f x)) * f).is_cycle
theorem
equiv.perm.is_cycle.sign
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
(hf : f.is_cycle) :
same_cycle
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.is_cycle.same_cycle
{β : Type u_2}
{f : equiv.perm β}
(hf : f.is_cycle)
{x y : β}
(hx : ⇑f x ≠ x)
(hy : ⇑f y ≠ y) :
f.same_cycle x y
@[instance]
def
equiv.perm.same_cycle.decidable_rel
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α) :
Equations
- equiv.perm.same_cycle.decidable_rel f = λ (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
cycle_of
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.same_cycle.cycle_of_apply
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x y : α}
(h : f.same_cycle x y) :
theorem
equiv.perm.cycle_of_apply_of_not_same_cycle
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x y : α}
(h : ¬f.same_cycle x y) :
@[simp]
theorem
equiv.perm.cycle_of_apply_self
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
(x : α) :
theorem
equiv.perm.is_cycle.cycle_of_eq
{α : Type u_1}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
(hf : f.is_cycle)
{x : α}
(hx : ⇑f x ≠ x) :
theorem
equiv.perm.is_cycle_cycle_of
{α : Type u_1}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
{x : α}
(hx : ⇑f x ≠ x) :
cycle_factors
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
Fixed points
theorem
equiv.perm.one_lt_nonfixed_point_card_of_ne_one
{α : Type u_1}
[decidable_eq α]
[fintype α]
{σ : equiv.perm α}
(h : σ ≠ 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 α}
(h : σ ≠ 1) :
(finset.filter (λ (x : α), ⇑σ x = x) finset.univ).card < fintype.card α - 1