PermutationCycles.lean`

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Release075.PermCycles.Cycles line 13
instance OAI.Release075.PermCycles.(instance at line 14) line 14
def OAI.Release075.PermCycles.cl line 16
theorem OAI.Release075.PermCycles.cl_eq_iff line 19
theorem OAI.Release075.PermCycles.cl_surjective line 23
def OAI.Release075.PermCycles.orbit line 25
theorem OAI.Release075.PermCycles.mem_orbit line 29
theorem OAI.Release075.PermCycles.orbit_eq_image line 33
theorem OAI.Release075.PermCycles.orbit_card_of_period line 53
def OAI.Release075.PermCycles.fiberOrbitEquiv line 60
theorem OAI.Release075.PermCycles.card_fiber line 67
theorem OAI.Release075.PermCycles.sum_card_fibers line 72
theorem OAI.Release075.PermCycles.card_eq_mul_cycles line 78
theorem OAI.Release075.PermCycles.orbit_card_involution line 89
Source documentation
A fixed-point-free involution has precisely two darts in each edge orbit.
```
theorem orbit_card_involution (f : Perm A) (h : Function.Involutive f)
    (hne : ∀ a, f a ≠ a) (a : A) : (orbit f a).card = 2 := by
…
```
Mentions: OAI.Release075.PermCycles.orbit
theorem OAI.Release075.PermCycles.orbit_card_three line 97
Source documentation
A three-cycle orbit is counted with all corners, not merely its moved support.
```
theorem orbit_card_three (f : Perm A) (a : A) (hp : (f^3) a = a)
    (hne : f a ≠ a) : (orbit f a).card = 3 := by
…
```
Mentions: OAI.Release075.PermCycles.orbit
theorem OAI.Release075.PermCycles.minimalPeriod_pos line 120
theorem OAI.Release075.PermCycles.orbit_card_eq_minimalPeriod line 124
theorem OAI.Release075.PermCycles.cl_apply line 133
theorem OAI.Release075.PermCycles.invariant_sameCycle line 146
Source documentation
Any function invariant under one permutation step is constant on entire cycles. This includes negative powers without any infinite search.
```
theorem invariant_sameCycle {B : Type*} (f : Perm A) (q : A → B)
    (h : ∀ x, q (f x) = q x) {x y : A} (hxy : f.SameCycle x y) : q x = q y := by
…
```
def OAI.Release075.PermCycles.descend line 155
theorem OAI.Release075.PermCycles.descend_cl line 159
theorem OAI.Release075.PermCycles.swap_merges line 164
Source documentation
Switching the two outgoing cycle destinations joins distinct cycles. This is the elementary surgery used when gluing or cancelling planar picture arcs.
```
theorem swap_merges (f : Perm A) {a b : A} (hab : ¬ f.SameCycle a b) :
    (Equiv.swap a b * f).SameCycle a b := by
…
```
theorem OAI.Release075.PermCycles.old_cycles_of_swap_merged line 196
theorem OAI.Release075.PermCycles.card_subtype_ne_add_one line 214
theorem OAI.Release075.PermCycles.cycles_card_swap_of_not_same line 225
Source documentation
Exact cycle count for merging two different cycles by one swap. Fixed points are included in the count, unlike the support-cycle count in permutation sign.
```
theorem cycles_card_swap_of_not_same (f : Perm A) {a b : A} (hab : ¬ f.SameCycle a b) :
    Fintype.card (Cycles (Equiv.swap a b * f)) + 1 = Fintype.card (Cycles f) := by
…
```
Mentions: OAI.Release075.PermCycles.Cycles
theorem OAI.Release075.PermCycles.swap_splits line 277
Source documentation
Switching the destinations within one cycle cuts it into two. The proof uses the initial orbit segment from a to b, rather than assuming an unproved topological separation statement.
```
theorem swap_splits (f : Perm A) {a b : A} (hne : a ≠ b) (hab : f.SameCycle a b) :
    ¬ (Equiv.swap a b * f).SameCycle a b := by
…
```
theorem OAI.Release075.PermCycles.cycles_card_swap_of_same line 323
def OAI.Release075.PermCycles.joinPair line 340
Source documentation
Join just two classes of a partition.
```
def joinPair (s : Setoid A) (a b : A) : Setoid A :=
…
```
theorem OAI.Release075.PermCycles.le_joinPair line 344
theorem OAI.Release075.PermCycles.joinPair_rel line 348
theorem OAI.Release075.PermCycles.joinPair_le line 352
theorem OAI.Release075.PermCycles.joinPair_eq_of_rel line 361
theorem OAI.Release075.PermCycles.card_joinPair line 365
Source documentation
The exact loss of one component when two distinct classes are joined.
```
theorem card_joinPair (s : Setoid A) {a b : A} (hab : ¬ s a b) :
    Nat.card (Quotient (joinPair s a b)) + 1 = Nat.card (Quotient s) := by
…
```
Mentions: OAI.Release075.PermCycles.joinPair
abbrev OAI.Release075.PermCycles.components line 411
Source documentation
Components of the graph generated by two permutations; cycles of their product are contained in these components.
```
abbrev components (f g : Perm A) : Setoid A :=
…
```
def OAI.Release075.PermCycles.cycleCount line 414
def OAI.Release075.PermCycles.componentCount line 415
theorem OAI.Release075.PermCycles.sameCycle_le_of_step line 417
theorem OAI.Release075.PermCycles.sameCycle_mul_le_components line 428
theorem OAI.Release075.PermCycles.components_swap_of_not_same line 438
theorem OAI.Release075.PermCycles.cycleCount_one line 470
theorem OAI.Release075.PermCycles.components_one line 478
theorem OAI.Release075.PermCycles.componentCount_one line 486
theorem OAI.Release075.PermCycles.cycleCount_swap_of_not_same line 489
theorem OAI.Release075.PermCycles.cycleCount_swap_le line 493
theorem OAI.Release075.PermCycles.euler_bound line 509
Source documentation
Euler's upper bound for an arbitrary oriented combinatorial map, allowing multiple components and positive genus. No planarity theorem is assumed.
```
theorem euler_bound (f g : Perm A) :
    cycleCount f + cycleCount g + cycleCount (f*g) ≤
      Fintype.card A + 2 * componentCount f g := by
…
```
Mentions: OAI.Release075.PermCycles.cycleCount, OAI.Release075.PermCycles.componentCount