Equiv.Perm.mem_support_cycleOf_iff
theorem Equiv.Perm.mem_support_cycleOf_iff :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x y : α},
y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
This theorem states that for any type `α` with decidable equality and finiteness, and given a permutation `f` of `α`, and elements `x` and `y` of `α`, `y` belongs to the non-fixed points of the cycle of `f` at `x` if and only if `y` is in the same cycle as `x` under `f` and `x` is a non-fixed point of `f`.
More concisely: For any permutation `f` of a type `α` with decidable equality and finiteness, `x` and `y` are in the same cycle of `f` and `x` is a non-fixed point of `f` if and only if `y` is a non-fixed point of `f` in the cycle of `x`.
|
Equiv.Perm.SameCycle.cycleOf_eq
theorem Equiv.Perm.SameCycle.cycleOf_eq :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x y : α},
f.SameCycle x y → f.cycleOf x = f.cycleOf y
This theorem states that for any type `α` that has a decidable equality and is a finite type, given a permutation `f` of `α` and any two elements `x` and `y` of `α`, if `x` and `y` are in the same cycle of the permutation `f` (as denoted by `Equiv.Perm.SameCycle f x y`), then the cycles of `x` and `y` in the permutation `f` (as denoted by `Equiv.Perm.cycleOf f x` and `Equiv.Perm.cycleOf f y`, respectively) are equal. In other words, if two elements are in the same cycle of a permutation, they share the same cycle.
More concisely: For any finite type `α` with decidable equality, if `x` and `y` are in the same cycle of a permutation `f` on `α`, then `Equiv.Perm.cycleOf f x` equals `Equiv.Perm.cycleOf f y`.
|
Equiv.Perm.cycleFactorsFinset_eq_finset
theorem Equiv.Perm.cycleFactorsFinset_eq_finset :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)},
σ.cycleFactorsFinset = s ↔
(∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Equiv.Perm.Disjoint), s.noncommProd id ⋯ = σ
This theorem establishes an equivalence for any type `α` with decidable equality and finite type, and any permutation `σ` on `α`. It states that a permutation `σ` is expressible as the cycle factors of a finset `s` if and only if every element `f` in `s` is a cycle and there exists a pairwise disjoint relation amongst the elements of `s` such that the non-commutative product of `s` equals `σ`. In other words, the permutation `σ` can be factored into a set of disjoint cycles.
More concisely: A permutation `σ` on a finite type `α` with decidable equality is equivalently expressible as a set of disjoint cycles if and only if every element in the set is a cycle and the non-commutative product of the cycles equals `σ`.
|
Equiv.Perm.cycleOf_apply
theorem Equiv.Perm.cycleOf_apply :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x y : α),
(f.cycleOf x) y = if f.SameCycle x y then f y else y
This theorem states that for a given permutation `f` on a finite type `α` with decidable equality, and for any two elements `x` and `y` of `α`, the action of the cycle of `f` that contains `x` on `y` is equal to either `f y` or `y` itself, depending on whether `x` and `y` are in the same cycle of the permutation `f`. In other words, if `x` and `y` are in the same cycle of the permutation `f` (as indicated by `Equiv.Perm.SameCycle f x y`), then applying `f` to `y` will give the result of the operation `Equiv.Perm.cycleOf f x` on `y`; otherwise, `y` remains unchanged.
More concisely: For any permutation `f` on a finite type `α` with decidable equality, and for all `x, y` in `α`, if `x` and `y` are in the same cycle of `f`, then `f y = Equiv.Perm.cycleOf f x y`, otherwise `y` is unchanged.
|
Equiv.Perm.cycle_is_cycleOf
theorem Equiv.Perm.cycle_is_cycleOf :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f c : Equiv.Perm α} {a : α},
a ∈ c.support → c ∈ f.cycleFactorsFinset → c = f.cycleOf a
The theorem `Equiv.Perm.cycle_is_cycleOf` states that for any type `α` with decidable equality and finite size, given a permutation `f`, a cycle `c`, and an element `a` of type `α`, if `a` is within the support of `c` and `c` is a cycle of `f`, then `c` is equal to the cycle of `f` at `a`. In other words, this theorem is about the uniqueness of cycles in a permutation. It tells us that if we have a cycle `c` in the permutation `f` and an element `a` is part of that cycle, then `c` is exactly the cycle created by repeatedly applying `f` to `a`.
More concisely: For any finite type `α` with decidable equality, given a permutation `f` and a cycle `c` of `f`, if an element `a` is in the support of `c` and is a fixed point of `c`, then `c` is the cycle of `f` containing `a`.
|
Equiv.Perm.cycleOf.proof_1
theorem Equiv.Perm.cycleOf.proof_1 :
∀ {α : Type u_1} (f : Equiv.Perm α) (x x_1 : α), f.SameCycle x x_1 ↔ f.SameCycle x (f x_1)
This theorem states that for all types `α` and for any permutation `f` of `α`, and any two elements `x` and `x_1` of `α`, the property that `x` and `x_1` are in the same cycle of the permutation `f` is equivalent to the property that `x` and `f(x_1)` are in the same cycle of the permutation `f`. In other words, changing `x_1` by applying the permutation `f` to it does not change whether `x` and `x_1` are in the same cycle of `f`.
More concisely: For all types `α` and permutations `f` of `α`, and all elements `x` and `x_1` of `α`, `x` and `x_1` are in the same cycle of `f` if and only if `x` and `f(x_1)` are in the same cycle of `f`.
|
Equiv.Perm.cycleFactorsFinset_injective
theorem Equiv.Perm.cycleFactorsFinset_injective :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α], Function.Injective Equiv.Perm.cycleFactorsFinset := by
sorry
This theorem states that the function `Equiv.Perm.cycleFactorsFinset` is injective for any type `α` that has decidable equality and is a finite set. In other words, if two permutations `f` and `g` of a finite set `α` yield the same set of cycle factors when passed to the `Equiv.Perm.cycleFactorsFinset` function, then these two permutations `f` and `g` must be identical. Here, a cycle factor of a permutation is a cyclic permutation (a permutation that moves all elements in its support in a cycle) such that multiplying all the cycle factors together yields the original permutation.
More concisely: For any type `α` with decidable equality that is a finite set, the function `Equiv.Perm.cycleFactorsFinset` maps equal permutations to equal sets of cycle factors.
|
Equiv.Perm.SameCycle.cycleOf_apply
theorem Equiv.Perm.SameCycle.cycleOf_apply :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x y : α},
f.SameCycle x y → (f.cycleOf x) y = f y
This theorem states that for any type `α` with decidable equality and finite size, and for any permutation `f` of `α` and any two elements `x` and `y` of `α`, if `x` and `y` are in the same cycle of the permutation `f`, then applying the cycle of permutation `f` at `x` to `y` is the same as applying `f` to `y`. In other words, the cycle that `x` belongs to under the permutation `f` acts on `y` just as `f` itself does, if `x` and `y` are in the same cycle of `f`.
More concisely: For any finite type `α` with decidable equality, permutation `f` of `α`, and elements `x` and `y` in the same cycle of `f`, `f^(cyc x) y` equals `f^(cyc y)`, where `cyc` denotes the cycle containing `x` under `f`.
|
Equiv.Perm.cycle_induction_on
theorem Equiv.Perm.cycle_induction_on :
∀ {β : Type u_3} [inst : Finite β] (P : Equiv.Perm β → Prop) (σ : Equiv.Perm β),
P 1 →
(∀ (σ : Equiv.Perm β), σ.IsCycle → P σ) →
(∀ (σ τ : Equiv.Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)) → P σ
The theorem `Equiv.Perm.cycle_induction_on` is a principle of mathematical induction for permutations over a finite type `β`. It states that for every property `P` and every permutation `σ` on `β`, if the property holds for the identity permutation, and if whenever the property holds for a cycle `σ` and any other permutation `τ` that is disjoint from `σ`, then it also holds for the product of `σ` and `τ`, then the property holds for all permutations. In other words, any property of permutations that holds for the identity, for cycles, and is preserved under taking disjoint products, holds for all permutations.
More concisely: If a property holds for the identity permutation and is closed under cyclic shifts and disjoint composition for permutations on a finite type, then it holds for all permutations.
|
Equiv.Perm.IsCycle.cycleOf_eq
theorem Equiv.Perm.IsCycle.cycleOf_eq :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x : α},
f.IsCycle → f x ≠ x → f.cycleOf x = f
The theorem `Equiv.Perm.IsCycle.cycleOf_eq` asserts that for all types `α`, given that `α` has a decidable equality and is a finite type, for any permutation `f` of `α` and any element `x` of `α`, if `f` is a cycle (a non-identity permutation in which any two non-fixed points are related by repeated application of the permutation) and `f` of `x` is not equal to `x`, then the cycle of the permutation `f` to which `x` belongs is equal to `f` itself.
More concisely: For any finite type `α` with decidable equality and any permutation `f` on `α` that is a cycle, if `x` is a non-fixed point of `f`, then the cycle containing `x` is equal to `f`.
|
Equiv.Perm.mem_cycleFactorsFinset_iff
theorem Equiv.Perm.mem_cycleFactorsFinset_iff :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f p : Equiv.Perm α},
p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
This theorem states that for any type `α` with decidable equality and being finite, and for any permutations `f` and `p` of `α`, `p` is a member of the cycle factors of `f` if and only if `p` is a cycle and for all elements `a` in the support of `p` (the set of nonfixed points of a permutation), `p` applied to `a` equals `f` applied to `a`. It essentially describes a condition for a permutation to be considered as one of the cyclic factors of another permutation.
More concisely: A permutation `p` is a cycle factor of `f` if and only if `p` is a cycle and for all elements `a` in the support of `p`, `p(a) = f(a)`.
|
Equiv.Perm.cycleFactorsFinset_noncommProd
theorem Equiv.Perm.cycleFactorsFinset_noncommProd :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α)
(comm : optParam ((↑f.cycleFactorsFinset).Pairwise Commute) ⋯), f.cycleFactorsFinset.noncommProd id comm = f
This theorem states that for any finite type `α` with a decidable equality, given a permutation `f` of `α`, the product of the cycle factors of `f` is equal to `f` itself. This is under the optional condition that the cycle factors pairwise commute, i.e., the order of multiplication of any two distinct cycle factors doesn't affect the result. The product of cycle factors is computed using `noncommProd`, which allows multiplication in any order if a proof of commutativity is provided. In this case, the identity function `id` is used as the function to transform each factor before multiplication.
More concisely: For any finite type `α` with decidable equality and a permutation `f` of `α` whose cycle factors pairwise commute, the product of the cycles factors of `f` using the identity function as transformation equals `f`.
|
Equiv.Perm.cycleOf_apply_of_not_sameCycle
theorem Equiv.Perm.cycleOf_apply_of_not_sameCycle :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x y : α},
¬f.SameCycle x y → (f.cycleOf x) y = y
The theorem `Equiv.Perm.cycleOf_apply_of_not_sameCycle` states that for any type `α` with decidable equality and finiteness, given a permutation `f` over `α` and any two elements `x` and `y` of `α`, if `x` and `y` do not belong to the same cycle of permutation `f` (`¬Equiv.Perm.SameCycle f x y`), then applying the cycle of `f` that contains `x` to `y` leaves `y` unchanged, i.e., `(Equiv.Perm.cycleOf f x) y = y`. In other words, if `x` and `y` are in different cycles of a permutation, the cycle of `x` does not affect `y`.
More concisely: If `x` and `y` are not in the same cycle of a permutation `f` over a type `α` with decidable equality and finiteness, then applying the cycle of `f` that contains `x` to `y` leaves `y` unchanged.
|
Equiv.Perm.cycleOf_pow_apply_self
theorem Equiv.Perm.cycleOf_pow_apply_self :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x : α) (n : ℕ),
(f.cycleOf x ^ n) x = (f ^ n) x
The theorem `Equiv.Perm.cycleOf_pow_apply_self` states that for any type `α` having decidable equality and is a finite type, and given a permutation `f` of `α`, an element `x` of `α`, and a natural number `n`, applying the `n`-th power of the cycle of `f` that `x` belongs to, to `x`, is the same as applying the `n`-th power of `f` to `x`. In other words, cycling `n` times in the cycle of `f` containing `x` and applying `f` `n` times to `x` lead to the same result.
More concisely: For any finite type `α` with decidable equality and permutation `f`, the `n`-th power of the cycle containing `x` and the `n`-th power of `f` applied to `x` yield equal results, i.e., `(cycleOf f x).pow n x = f.pow n x`.
|
Equiv.Perm.isCycle_cycleOf_iff
theorem Equiv.Perm.isCycle_cycleOf_iff :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {x : α} (f : Equiv.Perm α),
(f.cycleOf x).IsCycle ↔ f x ≠ x
In the type universe `α`, given a bijection `f` from `α` to itself, an element `x` of `α`, and assuming that equality is decidable in `α` and `α` is finite, the theorem states that `x` is in the cycle induced by `f` if and only if the action of `f` changes `x`. In other words, the cycle of `x` under `f` is a true permutation cycle if and only if `f(x)` is not equal to `x`.
More concisely: Given a finite type `α` with decidable equality, a bijection `f` from `α` to itself, and an element `x` in `α`, the cycle of `x` under `f` is a true permutation cycle if and only if `f(x) ≠ x`.
|
Equiv.Perm.isCycle_cycleOf
theorem Equiv.Perm.isCycle_cycleOf :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {x : α} (f : Equiv.Perm α),
f x ≠ x → (f.cycleOf x).IsCycle
The theorem `Equiv.Perm.isCycle_cycleOf` states that for any type `α` with decidable equality and finite structure, and for any element `x` of `α` and any permutation `f` of `α`, if the permutation `f` does not fix `x` (that is, `f x ≠ x`), then the cycle of permutation `f` to which `x` belongs is a non-identity permutation where any two non-fixed points are related by repeated application of the permutation. This implies that the cycle of `x` under `f` must be a cycle in the graph theoretic sense (i.e., it forms a closed loop without repetition except for the starting and ending point).
More concisely: For any finite type `α` with decidable equality and any permutation `f` of `α` that does not fix `x`, the cycle of `x` under `f` is a non-identity permutation forming a closed loop without repetition except for the starting and ending points.
|
Equiv.Perm.cycleOf_eq_one_iff
theorem Equiv.Perm.cycleOf_eq_one_iff :
∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {x : α} (f : Equiv.Perm α),
f.cycleOf x = 1 ↔ f x = x
This theorem states that for any type `α`, where `α` has decidable equality and is finite, for any element `x` of `α` and for any permutation `f` of `α`, the cycle of permutation `f` to which `x` belongs is equivalent to the identity permutation if and only if applying `f` to `x` returns `x`. In other words, `x` remains unchanged under the permutation `f` if and only if `x` belongs to a cycle of `f` that is the same as the identity permutation.
More concisely: For any finite type `α` with decidable equality, an element `x` of `α` is in the same cycle as the identity under a permutation `f` if and only if `f(x) = x`.
|