English
If an element g of a group G acting on a set α is nontrivial (g ≠ 1) and the image of the complement of the fixed-by-g set under the action of h is disjoint from its own complement, then g and h cannot commute.
Русский
Если элемент g группы G, действующий на множество α, не тождественен (g ≠ 1) и образ дополнения множества фиксированных точек g под действием h не пересекается с самим дополнением, то g и h не commute.
LaTeX
$$$\\text{If } g \\ne 1 \\text{ and } Disjoint((\\mathrm{Fix}_α(g))^c,\\; h\\cdot (\\mathrm{Fix}_α(g))^c)\\text{, then } g h \\ne h g.$$$
Lean4
/-- If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G`
is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute.
-/
@[to_additive /-- If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G`
is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute. -/
]
theorem not_commute_of_disjoint_movedBy_preimage {g h : G} (ne_one : g ≠ 1)
(disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h :=
by
contrapose! ne_one with comm
rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ, compl_inj_iff,
fixedBy_eq_univ_iff_eq_one] at disjoint
