Infinite cyclic permutations

Stream: maths

[Yakov Pechersky]

What is the proper definition of "cyclic permutation" if working over an infinite type? The current definition in mathlib is

/-- A permutation is a cycle when any two nonfixed points of the permutation are related by repeated
  application of the permutation. -/
def is_cycle (f : perm β) : Prop := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y

However, that indicates that (+ 1) is a cyclic permutation:

import group_theory.perm.cycles

open equiv equiv.perm

@[simps apply symm_apply]
def succ_equiv : perm ℤ :=
{ to_fun := (+ 1),
  inv_fun := λ x, x - 1,
  left_inv := λ x, by simp,
  right_inv := λ x, by simp }

@[simp] lemma succ_equiv_inv_apply (x : ℤ) :
  succ_equiv⁻¹ x = x - 1 :=
by simp [inv_def]

@[simp] lemma succ_equiv_pow_apply (k : ℕ) (x : ℤ) :
  (succ_equiv ^ k) x = x + k :=
begin
  induction k with k hk generalizing x,
  { simp },
  { simp [pow_succ', hk, add_comm, add_assoc, add_left_comm] }
end

@[simp] lemma succ_equiv_gpow_apply (k : ℤ) (x : ℤ) :
  (succ_equiv ^ k) x = x + k :=
begin
  induction k using int.induction_on with k IH k IH,
  { simp },
  { simp [gpow_add, add_comm, add_assoc, add_left_comm] },
  { simp [gpow_sub, add_comm, add_assoc, add_left_comm, inv_def, symm_apply_eq,
        add_comm, add_assoc, add_left_comm, add_sub] }
end

lemma infinite_cycle : is_cycle succ_equiv :=
begin
  rw is_cycle,
  use 0,
  simp
end

Would it make sense to redefine is_cycle p to somehow encode that ∃ (k : ℕ) (hk : 1 < k), p ^ k = 1?

[Mario Carneiro]

Yes, (+ 1) is cyclic

[Mario Carneiro]

int is also a cyclic group

[Yakov Pechersky]

OK, and does factoring a permutation into its disjoint cycles only make sense in finite contexts?

[David Wärn]

It should always make sense with this definition

[Mario Carneiro]

well you have to do something special since there could be an ininite number of pairwise disjoint cycles but yes it works

[David Wärn]

It's the classification of group actions by Z. Generally if you have G acting on X, then X can be partitioned into orbits, such that each orbit looks like the action of G on G / H for some H

[Yakov Pechersky]

Even computably, it works?

[Yakov Pechersky]

cycle_factors as it is currently in mathlib assumes fintype. Does one rely on some sort of attach magic to make it work over infinite types?

@[simps apply]
protected def attach (p : perm α) : perm {x | p x ≠ x} :=
perm.subtype_perm p (by simp)

[Mario Carneiro]

Even computably, it works?

No, the "in the same cycle" relation is not decidable

[Yaël Dillies]

Why do we require f x ≠ x? Aren't one-cycles cycles?

[Mario Carneiro]

I think this is something like "1 is not a prime"

[Mario Carneiro]

if you include 1 cycles then you can't say that a cycle is a cycle since there are all those 1 cycles on all the other points

[Mario Carneiro]

I think you would need another representation of "cycle" that picks out the subset that is the cycle to be able to talk about 1-cycles properly

[Kevin Buzzard]

By "an element is a product of disjoint cycles" I've always implicitly assumed that the 1-cycles are there but not mentioned, but now I see there's another approach. It's a bit different to "1 is not prime" but it's very similar. Is a cycle in a symmetric group a pair (g,S) where S is a subset of the set plus a proof that the cycle acts transitively on the set and fixes everything else? If so then the identity is a cycle in more than one way in general. If the cycle is determined by g only then the identity will have to be the empty product of cycles (which is fine, but I had never thought of it like that, in contrast to 1 definitely being the empty product of primes)

[David Wärn]

Yes, this is a bit different to 1 not being prime. If you think about the partition of [n] into orbits, then a 1-cycle is just an orbit with one element (where the action of Z looks like the action on Z/1Z), and there's nothing special about this. But if you think of a cycle as a permutation, and the cycle decomposition as a product, then one-cycles look special, unless you remember their "support". Sometimes it's very important to remember one-cycles: for example if you have $\sigma \in A_n$, then it's a fact that the conjugacy classes of $\sigma$ in $S_n$ and $A_n$ agree precisely unless the cycle type of $\sigma$ consists of distinct odd numbers (in which case the conjugacy class in $S_n$ splits in two), and this only works if you count one-cycles (two one-cycles means no splitting). Similarly the formula for the number of permutations with a given cycle type looks more natural with one-cycles. In mathlib, the cycle type docs#equiv.perm.cycle_type doesn't count one-cycles, although docs#equiv.perm.partition does. I expect each definition works better in different circumstances.