English
For a cycle f on s, the family of diagonals k ↦ s.map (a ↦ (a, f^k(a))) is pairwise disjoint as k ranges over range |s|.
Русский
Если f — цикл на s, семейство диагоналей, индексируемое k, состоит из попарно непересекающихся образов при k=0..|s|-1.
LaTeX
$$$(range(|s|)).PairwiseDisjoint\bigl( k \mapsto s.map( a \mapsto (a, f^k(a)) ) \bigr)$$$
Lean4
/-- We can partition the square `s ×ˢ s` into shifted diagonals as such:
```
01234
40123
34012
23401
12340
```
The diagonals are given by the cycle `f`.
-/
theorem product_self_eq_disjiUnion_perm (hf : f.IsCycleOn s) :
s ×ˢ s =
(range #s).disjiUnion (fun k => s.map ⟨fun i => (i, (f ^ k) i), fun _ _ => congr_arg Prod.fst⟩)
(product_self_eq_disjiUnion_perm_aux hf) :=
by
ext ⟨a, b⟩
simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map, Function.Embedding.coeFn_mk,
Prod.mk_inj]
refine ⟨fun hx => ?_, ?_⟩
· obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
· rintro ⟨n, -, a, ha, rfl, rfl⟩
exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩
