Circuit count decomposition via orientations

The orbit count of the walk permutation decomposes into the orbit counts of its restrictions to out-flags and in-flags (invariant predicates under the walk). Pairing-conjugation shows these two restrictions have the same orbit count, whence the circuit count (half the total orbit count) equals the orbit count of the out-restriction.

Orbit count of a permutation

noncomputable def RS.orbitCount {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) : ℕ

The orbit count of a permutation: number of non-trivial cycles plus number of fixed points.

Equations

• RS.orbitCount π = π.cycleType.card + Fintype.card ↑(Function.fixedPoints ⇑π)

theorem RS.perm_eq_ofSubtype_mul {β : Type} (π : Equiv.Perm β) (p : β → Prop) [DecidablePred p] (hp : ∀ (x : β), p (π x) ↔ p x) : π = Equiv.Perm.ofSubtype (π.subtypePerm hp) * Equiv.Perm.ofSubtype (π.subtypePerm ⋯)

Decomposition of a permutation into ofSubtype parts for an invariant predicate and its complement.

theorem RS.disjoint_ofSubtype_subtypePerm {β : Type} (π : Equiv.Perm β) (p : β → Prop) [DecidablePred p] (hp : ∀ (x : β), p (π x) ↔ p x) : (Equiv.Perm.ofSubtype (π.subtypePerm hp)).Disjoint (Equiv.Perm.ofSubtype (π.subtypePerm ⋯))

The ofSubtype lifts of the p-restriction and not-p-restriction are disjoint.

theorem RS.orbitCount_eq_add {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) (p : β → Prop) [DecidablePred p] (hp : ∀ (x : β), p (π x) ↔ p x) : orbitCount π = orbitCount (π.subtypePerm hp) + orbitCount (π.subtypePerm ⋯)

The orbit count of a permutation splits additively over an invariant predicate.

theorem RS.orbitCount_inv {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) : orbitCount π⁻¹ = orbitCount π

Orbit count is invariant under inversion.

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

Orbit count is invariant under transport along an equivalence.

theorem RS.neg_one_pow_orbitCount {β : Type} [Fintype β] [DecidableEq β] (π : Equiv.Perm β) : (-1) ^ orbitCount π = (-1) ^ Fintype.card β * ↑↑(Equiv.Perm.sign π)

The sign identity: (-1)^(orbitCount pi) = (-1)^(card beta) * sign pi.

Walk-orientation interaction

theorem RS.EdgeSubset.TransitionSystem.walk_isOut {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) (f : W.Flag) (hf : f ∈ F.flags) : o.isOut (κ.walk f) = o.isOut f

The walk preserves the orientation bit: pairing flips it once, the matching flips it back.

theorem RS.EdgeSubset.TransitionSystem.walkPerm_isOut_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) (x : ↥F.flags) : o.isOut ↑(κ.walkPerm x) = true ↔ o.isOut ↑x = true

The walk permutation preserves the out-flag predicate.

noncomputable def RS.EdgeSubset.TransitionSystem.outPerm {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : Equiv.Perm { f : ↥F.flags // o.isOut ↑f = true }

The out-flag restriction of the walk permutation.

Equations

• κ.outPerm o = κ.walkPerm.subtypePerm ⋯

In/out orbit equivalence

noncomputable def RS.EdgeSubset.TransitionSystem.outToIn {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : { x : ↥F.flags // o.isOut ↑x = true } ≃ { x : ↥F.flags // ¬o.isOut ↑x = true }

The equivalence between out-flags and in-flags induced by the edge pairing.

Equations

• κ.outToIn o = Equiv.subtypeEquiv F.pairingPerm ⋯

theorem RS.EdgeSubset.TransitionSystem.inPerm_eq_permCongr_outPerm_inv {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : κ.walkPerm.subtypePerm ⋯ = (κ.outToIn o).permCongr (κ.outPerm o)⁻¹

The in-restriction of the walk permutation equals the outToIn-transport of the inverse out-restriction.

theorem RS.EdgeSubset.TransitionSystem.orbitCount_inPerm_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : orbitCount (κ.walkPerm.subtypePerm ⋯) = orbitCount (κ.outPerm o)

The in-restriction and out-restriction of the walk permutation have the same orbit count.

Main theorems

theorem RS.EdgeSubset.TransitionSystem.circuitCount_eq_orbitCount_outPerm {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : κ.circuitCount = orbitCount (κ.outPerm o)

The circuit count of a transition system equals the orbit count of its out-flag restriction.

theorem RS.EdgeSubset.TransitionSystem.neg_one_pow_circuitCount {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.TransitionSystem) (o : κ.Orientation) : (-1) ^ κ.circuitCount = (-1) ^ Fintype.card { f : ↥F.flags // o.isOut ↑f = true } * ↑↑(Equiv.Perm.sign (κ.outPerm o))

The circuit sign decomposes as (-1)^(card out-flags) * sign(outPerm).