The orbit count is the number of orbits

orbitCount is defined as the number of cycles plus the number of fixed points, which is convenient for computing signs but says nothing directly about orbits. This file identifies it with the cardinality of the quotient by "lies on the same cycle": an orbit is either the support of one of the permutation's cycles or a single fixed point, and those two possibilities are exclusive and exhaustive.

That identification is what lets two orbit counts be compared when their underlying sets are different — a walk on flags against a rotation on labels, say — since a bijection of quotients is then enough.

@[reducible, inline]

abbrev RS.Orbits {β : Type} (π : Equiv.Perm β) : Type

The orbits of a permutation, as a quotient of its ground set.

Equations

• RS.Orbits π = Quotient (Equiv.Perm.SameCycle.setoid π)

instance RS.instFiniteOrbits {β : Type} [Finite β] (π : Equiv.Perm β) : Finite (Orbits π)

The orbit space of a permutation of a finite type is finite.

@[instance_reducible]

noncomputable instance RS.instFintypeOrbits {β : Type} [Fintype β] (π : Equiv.Perm β) : Fintype (Orbits π)

Hence it carries a fintype structure.

Equations

• RS.instFintypeOrbits π = Fintype.ofFinite (RS.Orbits π)

@[instance_reducible]

noncomputable instance RS.instDecidableEqOrbits {β : Type} (π : Equiv.Perm β) : DecidableEq (Orbits π)

And orbits can be compared, classically.

Equations

• RS.instDecidableEqOrbits π = Classical.decEq (RS.Orbits π)

theorem RS.orbit_eq_iff {β : Type} {π : Equiv.Perm β} {x y : β} : ⟦x⟧ = ⟦y⟧ ↔ π.SameCycle x y

Two points give the same orbit exactly when they lie on a common cycle.

A fixed point's orbit is a singleton

theorem RS.eq_of_sameCycle_of_fixed {β : Type} {π : Equiv.Perm β} {x y : β} (hx : π x = x) (h : π.SameCycle x y) : y = x

Nothing else lies on a fixed point's cycle.

theorem RS.apply_ne_of_sameCycle {β : Type} {π : Equiv.Perm β} {x y : β} (hx : π x ≠ x) (h : π.SameCycle x y) : π y ≠ y

A point on the same cycle as a moved point is moved.

The orbit map

noncomputable def RS.orbitName {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) (x : β) : ↥π.cycleFactorsFinset ⊕ ↑(Function.fixedPoints ⇑π)

The orbit of a point, named by its cycle when the point moves and by the point itself when it does not.

Equations

• RS.orbitName π x = if h : π x = x then Sum.inr ⟨x, h⟩ else Sum.inl ⟨π.cycleOf x, ⋯⟩

theorem RS.orbitName_congr {β : Type} [Fintype β] [DecidableEq β] {π : Equiv.Perm β} {x y : β} (h : π.SameCycle x y) : orbitName π x = orbitName π y

Points on the same cycle get the same name, so the naming descends to orbits.

noncomputable def RS.cycleRep {β : Type} [Fintype β] [DecidableEq β] {π : Equiv.Perm β} (c : ↥π.cycleFactorsFinset) : β

A chosen point on one of the permutation's cycles.

Equations

• RS.cycleRep c = Exists.choose ⋯

theorem RS.cycleRep_mem {β : Type} [Fintype β] [DecidableEq β] {π : Equiv.Perm β} (c : ↥π.cycleFactorsFinset) : cycleRep c ∈ (↑c).support

The chosen point of a cycle lies on it.

noncomputable def RS.orbitsEquiv {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) : Orbits π ≃ ↥π.cycleFactorsFinset ⊕ ↑(Function.fixedPoints ⇑π)

The orbits are the cycles together with the fixed points.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.orbitCount_eq_card_orbits {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) : orbitCount π = Fintype.card (Orbits π)

The orbit count is the number of orbits.

Transporting orbits along a step-wise map

A map that moves each point within a single orbit of the target permutation carries orbits to orbits, whatever it does inside them. This is how a contracted matching's rotation is compared with the original's: one step of the contracted rotation is several steps of the original.

theorem RS.sameCycle_of_step {β γ : Type} {π : Equiv.Perm β} {ρ : Equiv.Perm γ} (f : γ → β) (hstep : ∀ (x : γ), π.SameCycle (f x) (f (ρ x))) {x y : γ} (h : ρ.SameCycle x y) : π.SameCycle (f x) (f y)

A map whose one-step images stay in one orbit respects the orbit relation.

The orbits partition the ground set

Grouping the ground set by orbit is what lets a construction be carried out one orbit at a time — gluing an interface component by component, say, rather than label by label.

theorem RS.orbitCount_congr_decEq {β : Type} [Fintype β] (d₁ d₂ : DecidableEq β) (π : Equiv.Perm β) : orbitCount π = orbitCount π

The orbit count does not read the decidability instance.

theorem RS.orbitCount_eq_of_orbitsEquiv {β : Type} [Fintype β] [DecidableEq β] {γ : Type} [Fintype γ] [DecidableEq γ] {π : Equiv.Perm β} {ρ : Equiv.Perm γ} (e : Orbits π ≃ Orbits ρ) : orbitCount π = orbitCount ρ

Orbit counts agree along a bijection of orbit sets.