Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit e4da493

Browse files
tb65536tb65536
committed
feat(group_theory/perm/sign): exists_pow_eq_of_is_cycle (#5665)
Slight generalization of `exists_gpow_eq_of_is_cycle` in the case of a cycle on a finite set. Also move the following from `group_theory/perm/sign.lean` to `group_theory/perm/cycles.lean`: - is_cycle - is_cycle_swap - is_cycle_inv - exists_gpow_eq_of_is_cycle - is_cycle_swap_mul_aux₁ - is_cycle_swap_mul_aux₂ - eq_swap_of_is_cycle_of_apply_apply_eq_self - is_cycle_swap_mul - sign_cycle Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
1 parent d43f202 commit e4da493

File tree

2 files changed

+135
-123
lines changed

2 files changed

+135
-123
lines changed

‎src/group_theory/perm/cycles.lean‎

Lines changed: 134 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,145 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Hughes
55
-/
66
import group_theory.perm.sign
7-
import group_theory.order_of_element
87

98
namespace equiv.perm
109
open equiv function finset
10+
1111
variables {α : Type*} {β : Type*} [decidable_eq α]
1212

13+
section sign_cycle
14+
15+
variables [fintype α]
16+
17+
/-- A permutation is a cycle when any two nonfixed points of the permutation are related by repeated
18+
application of the permutation. -/
19+
def is_cycle (f : perm β) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
20+
21+
lemma is_cycle_swap {α : Type*} [decidable_eq α] {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
22+
⟨y, by rwa swap_apply_right,
23+
λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
24+
if hya : y = a then ⟨0, hya⟩
25+
else ⟨1, by rw [gpow_one, swap_apply_def]; split_ifs at *; cc⟩⟩
26+
27+
lemma is_cycle_inv {f : perm β} (hf : is_cycle f) : is_cycle (f⁻¹) :=
28+
let ⟨x, hx⟩ := hf in
29+
⟨x, by simp only [inv_eq_iff_eq, *, forall_prop_of_true, ne.def] at *; cc,
30+
λ y hy, let ⟨i, hi⟩ := hx.2 y (by simp only [inv_eq_iff_eq, *, forall_prop_of_true, ne.def] at *; cc) in
31+
⟨-i, by rwa [gpow_neg, inv_gpow, inv_inv]⟩⟩
32+
33+
lemma exists_gpow_eq_of_is_cycle {f : perm β} (hf : is_cycle f) {x y : β}
34+
(hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℤ, (f ^ i) x = y :=
35+
let ⟨g, hg⟩ := hf in
36+
let ⟨a, ha⟩ := hg.2 x hx in
37+
let ⟨b, hb⟩ := hg.2 y hy in
38+
⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
39+
40+
lemma exists_pow_eq_of_is_cycle [fintype β] {f : perm β}
41+
(hf : is_cycle f) {x y : β} (hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℕ, (f ^ i) x = y :=
42+
let ⟨n, hn⟩ := exists_gpow_eq_of_is_cycle hf hx hy in
43+
by classical; exact ⟨(n % order_of f).to_nat, by {
44+
have := int.mod_nonneg n (int.coe_nat_ne_zero.mpr (ne_of_gt (order_of_pos f))),
45+
rwa [←gpow_coe_nat, int.to_nat_of_nonneg this, ←gpow_eq_mod_order_of] }⟩
46+
47+
lemma is_cycle_swap_mul_aux₁ {α : Type*} [decidable_eq α] : ∀ (n : ℕ) {b x : α} {f : perm α}
48+
(hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
49+
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
50+
| 0 := λ b x f hb h, ⟨0, h⟩
51+
| (n+1 : ℕ) := λ b x f hb h,
52+
if hfbx : f x = b then ⟨0, hfbx⟩
53+
else
54+
have f b ≠ b ∧ b ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hb,
55+
have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
56+
by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
57+
ne.def, ← injective.eq_iff f.injective, apply_inv_self];
58+
exact this.1,
59+
let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb'
60+
(f.injective $
61+
by rw [apply_inv_self];
62+
rwa [pow_succ, mul_apply] at h) in
63+
⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
64+
swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (ne.symm hfbx)]⟩
65+
66+
lemma is_cycle_swap_mul_aux₂ {α : Type*} [decidable_eq α] : ∀ (n : ℤ) {b x : α} {f : perm α}
67+
(hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
68+
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
69+
| (n : ℕ) := λ b x f, is_cycle_swap_mul_aux₁ n
70+
| -[1+ n] := λ b x f hb h,
71+
if hfbx : f⁻¹ x = b then ⟨-1, by rwa [gpow_neg, gpow_one, mul_inv_rev, mul_apply, swap_inv, swap_apply_right]⟩
72+
else if hfbx' : f x = b then ⟨0, hfbx'⟩
73+
else
74+
have f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb,
75+
have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b,
76+
by rw [mul_apply, swap_apply_def];
77+
split_ifs;
78+
simp only [inv_eq_iff_eq, perm.mul_apply, gpow_neg_succ_of_nat, ne.def, perm.apply_inv_self] at *; cc,
79+
let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb
80+
(show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b, by
81+
rw [← gpow_coe_nat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, gpow_neg_succ_of_nat, ← inv_pow, pow_succ', mul_assoc,
82+
mul_assoc, inv_mul_self, mul_one, gpow_coe_nat, ← pow_succ', ← pow_succ]) in
83+
have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x, by rw [mul_apply, inv_apply_self, swap_apply_left],
84+
⟨-i, by rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, gpow_add, gpow_one, gpow_neg, ← inv_gpow,
85+
mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
86+
mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
87+
88+
lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {α : Type*} [decidable_eq α]
89+
{f : perm α} (hf : is_cycle f) {x : α}
90+
(hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
91+
equiv.ext $ λ y,
92+
let ⟨z, hz⟩ := hf in
93+
let ⟨i, hi⟩ := hz.2 x hfx in
94+
if hyx : y = x then by simp [hyx]
95+
else if hfyx : y = f x then by simp [hfyx, hffx]
96+
else begin
97+
rw [swap_apply_of_ne_of_ne hyx hfyx],
98+
refine by_contradiction (λ hy, _),
99+
cases hz.2 y hy with j hj,
100+
rw [← sub_add_cancel j i, gpow_add, mul_apply, hi] at hj,
101+
cases gpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji,
102+
{ rw [← hj, hji] at hyx, cc },
103+
{ rw [← hj, hji] at hfyx, cc }
104+
end
105+
106+
lemma is_cycle_swap_mul {α : Type*} [decidable_eq α] {f : perm α} (hf : is_cycle f) {x : α}
107+
(hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
108+
⟨f x, by simp only [swap_apply_def, mul_apply];
109+
split_ifs; simp [injective.eq_iff f.injective] at *; cc,
110+
λ y hy,
111+
let ⟨i, hi⟩ := exists_gpow_eq_of_is_cycle hf hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1 in
112+
have hi : (f ^ (i - 1)) (f x) = y, from
113+
calc (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ)) x : by rw [gpow_one, mul_apply]
114+
... = y : by rwa [← gpow_add, sub_add_cancel],
115+
is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
116+
117+
lemma sign_cycle : ∀ {f : perm α} (hf : is_cycle f),
118+
sign f = -(-1) ^ f.support.card
119+
| f := λ hf,
120+
let ⟨x, hx⟩ := hf in
121+
calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
122+
by rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
123+
... = -(-1) ^ f.support.card :
124+
if h1 : f (f x) = x
125+
then
126+
have h : swap x (f x) * f = 1,
127+
begin
128+
rw eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1,
129+
simp only [perm.mul_def, perm.one_def, swap_apply_left, swap_swap]
130+
end,
131+
by rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
132+
eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1, card_support_swap hx.1.symm]; refl
133+
else
134+
have h : card (support (swap x (f x) * f)) + 1 = card (support f),
135+
by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq h1,
136+
card_insert_of_not_mem (not_mem_erase _ _)],
137+
have wf : card (support (swap x (f x) * f)) < card (support f),
138+
from card_support_swap_mul hx.1,
139+
by rw [sign_mul, sign_swap hx.1.symm, sign_cycle (is_cycle_swap_mul hf hx.1 h1), ← h];
140+
simp only [pow_add, mul_one, units.neg_neg, one_mul, units.mul_neg, eq_self_iff_true,
141+
pow_one, units.neg_mul_neg]
142+
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
143+
144+
end sign_cycle
145+
13146
/-- The equivalence relation indicating that two points are in the same cycle of a permutation. -/
14147
def same_cycle (f : perm β) (x y : β) := ∃ i : ℤ, (f ^ i) x = y
15148

‎src/group_theory/perm/sign.lean‎

Lines changed: 1 addition & 122 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,8 @@ Authors: Chris Hughes
55
-/
66
import data.fintype.basic
77
import data.finset.sort
8-
import algebra.group.conj
9-
import algebra.big_operators.basic
108
import group_theory.perm.basic
9+
import group_theory.order_of_element
1110

1211
/-!
1312
# Sign of a permutation
@@ -604,133 +603,13 @@ calc sign f = sign (@subtype_perm _ f (λ x, f x ≠ x) (by simp)) :
604603
(λ ⟨x, _⟩, subtype.eq (h x _ _))
605604
... = sign g : sign_subtype_perm _ _ (λ _, id)
606605

607-
/-- A permutation is a cycle when any two nonfixed points of the permutation are related by repeated
608-
application of the permutation. -/
609-
def is_cycle (f : perm β) := ∃ x, f x ≠ x ∧ ∀ y, f y ≠ y → ∃ i : ℤ, (f ^ i) x = y
610-
611-
lemma is_cycle_swap {α : Type*} [decidable_eq α] {x y : α} (hxy : x ≠ y) : is_cycle (swap x y) :=
612-
⟨y, by rwa swap_apply_right,
613-
λ a (ha : ite (a = x) y (ite (a = y) x a) ≠ a),
614-
if hya : y = a then ⟨0, hya⟩
615-
else ⟨1, by rw [gpow_one, swap_apply_def]; split_ifs at *; cc⟩⟩
616-
617-
lemma is_cycle_inv {f : perm β} (hf : is_cycle f) : is_cycle (f⁻¹) :=
618-
let ⟨x, hx⟩ := hf in
619-
⟨x, by simp only [inv_eq_iff_eq, *, forall_prop_of_true, ne.def] at *; cc,
620-
λ y hy, let ⟨i, hi⟩ := hx.2 y (by simp only [inv_eq_iff_eq, *, forall_prop_of_true, ne.def] at *; cc) in
621-
⟨-i, by rwa [gpow_neg, inv_gpow, inv_inv]⟩⟩
622-
623-
lemma exists_gpow_eq_of_is_cycle {f : perm β} (hf : is_cycle f) {x y : β}
624-
(hx : f x ≠ x) (hy : f y ≠ y) : ∃ i : ℤ, (f ^ i) x = y :=
625-
let ⟨g, hg⟩ := hf in
626-
let ⟨a, ha⟩ := hg.2 x hx in
627-
let ⟨b, hb⟩ := hg.2 y hy in
628-
⟨b - a, by rw [← ha, ← mul_apply, ← gpow_add, sub_add_cancel, hb]⟩
629-
630-
lemma is_cycle_swap_mul_aux₁ {α : Type*} [decidable_eq α] : ∀ (n : ℕ) {b x : α} {f : perm α}
631-
(hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
632-
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
633-
| 0 := λ b x f hb h, ⟨0, h⟩
634-
| (n+1 : ℕ) := λ b x f hb h,
635-
if hfbx : f x = b then ⟨0, hfbx⟩
636-
else
637-
have f b ≠ b ∧ b ≠ x, from ne_and_ne_of_swap_mul_apply_ne_self hb,
638-
have hb' : (swap x (f x) * f) (f⁻¹ b) ≠ f⁻¹ b,
639-
by rw [mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx),
640-
ne.def, ← injective.eq_iff f.injective, apply_inv_self];
641-
exact this.1,
642-
let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb'
643-
(f.injective $
644-
by rw [apply_inv_self];
645-
rwa [pow_succ, mul_apply] at h) in
646-
⟨i + 1, by rw [add_comm, gpow_add, mul_apply, hi, gpow_one, mul_apply, apply_inv_self,
647-
swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 (ne.symm hfbx)]⟩
648-
649-
lemma is_cycle_swap_mul_aux₂ {α : Type*} [decidable_eq α] : ∀ (n : ℤ) {b x : α} {f : perm α}
650-
(hb : (swap x (f x) * f) b ≠ b) (h : (f ^ n) (f x) = b),
651-
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b
652-
| (n : ℕ) := λ b x f, is_cycle_swap_mul_aux₁ n
653-
| -[1+ n] := λ b x f hb h,
654-
if hfbx : f⁻¹ x = b then ⟨-1, by rwa [gpow_neg, gpow_one, mul_inv_rev, mul_apply, swap_inv, swap_apply_right]⟩
655-
else if hfbx' : f x = b then ⟨0, hfbx'⟩
656-
else
657-
have f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb,
658-
have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b,
659-
by rw [mul_apply, swap_apply_def];
660-
split_ifs;
661-
simp only [inv_eq_iff_eq, perm.mul_apply, gpow_neg_succ_of_nat, ne.def, perm.apply_inv_self] at *; cc,
662-
let ⟨i, hi⟩ := is_cycle_swap_mul_aux₁ n hb
663-
(show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b, by
664-
rw [← gpow_coe_nat, ← h, ← mul_apply, ← mul_apply, ← mul_apply, gpow_neg_succ_of_nat, ← inv_pow, pow_succ', mul_assoc,
665-
mul_assoc, inv_mul_self, mul_one, gpow_coe_nat, ← pow_succ', ← pow_succ]) in
666-
have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x, by rw [mul_apply, inv_apply_self, swap_apply_left],
667-
⟨-i, by rw [← add_sub_cancel i 1, neg_sub, sub_eq_add_neg, gpow_add, gpow_one, gpow_neg, ← inv_gpow,
668-
mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, gpow_add, gpow_one,
669-
mul_apply, mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (ne.symm hfbx')]⟩
670-
671-
lemma eq_swap_of_is_cycle_of_apply_apply_eq_self {α : Type*} [decidable_eq α]
672-
{f : perm α} (hf : is_cycle f) {x : α}
673-
(hfx : f x ≠ x) (hffx : f (f x) = x) : f = swap x (f x) :=
674-
equiv.ext $ λ y,
675-
let ⟨z, hz⟩ := hf in
676-
let ⟨i, hi⟩ := hz.2 x hfx in
677-
if hyx : y = x then by simp [hyx]
678-
else if hfyx : y = f x then by simp [hfyx, hffx]
679-
else begin
680-
rw [swap_apply_of_ne_of_ne hyx hfyx],
681-
refine by_contradiction (λ hy, _),
682-
cases hz.2 y hy with j hj,
683-
rw [← sub_add_cancel j i, gpow_add, mul_apply, hi] at hj,
684-
cases gpow_apply_eq_of_apply_apply_eq_self hffx (j - i) with hji hji,
685-
{ rw [← hj, hji] at hyx, cc },
686-
{ rw [← hj, hji] at hfyx, cc }
687-
end
688-
689-
lemma is_cycle_swap_mul {α : Type*} [decidable_eq α] {f : perm α} (hf : is_cycle f) {x : α}
690-
(hx : f x ≠ x) (hffx : f (f x) ≠ x) : is_cycle (swap x (f x) * f) :=
691-
⟨f x, by simp only [swap_apply_def, mul_apply];
692-
split_ifs; simp [injective.eq_iff f.injective] at *; cc,
693-
λ y hy,
694-
let ⟨i, hi⟩ := exists_gpow_eq_of_is_cycle hf hx (ne_and_ne_of_swap_mul_apply_ne_self hy).1 in
695-
have hi : (f ^ (i - 1)) (f x) = y, from
696-
calc (f ^ (i - 1)) (f x) = (f ^ (i - 1) * f ^ (1 : ℤ)) x : by rw [gpow_one, mul_apply]
697-
... = y : by rwa [← gpow_add, sub_add_cancel],
698-
is_cycle_swap_mul_aux₂ (i - 1) hy hi⟩
699-
700606
@[simp] lemma support_swap {x y : α} (hxy : x ≠ y) : (swap x y).support = {x, y} :=
701607
finset.ext $ λ a, by simp [swap_apply_def]; split_ifs; cc
702608

703609
lemma card_support_swap {x y : α} (hxy : x ≠ y) : (swap x y).support.card = 2 :=
704610
show (swap x y).support.card = finset.card ⟨x ::ₘ y ::ₘ 0, by simp [hxy]⟩,
705611
from congr_arg card $ by rw [support_swap hxy]; simp [*, finset.ext_iff]; cc
706612

707-
lemma sign_cycle : ∀ {f : perm α} (hf : is_cycle f),
708-
sign f = -(-1) ^ f.support.card
709-
| f := λ hf,
710-
let ⟨x, hx⟩ := hf in
711-
calc sign f = sign (swap x (f x) * (swap x (f x) * f)) :
712-
by rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]
713-
... = -(-1) ^ f.support.card :
714-
if h1 : f (f x) = x
715-
then
716-
have h : swap x (f x) * f = 1,
717-
begin
718-
rw eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1,
719-
simp only [perm.mul_def, perm.one_def, swap_apply_left, swap_swap]
720-
end,
721-
by rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
722-
eq_swap_of_is_cycle_of_apply_apply_eq_self hf hx.1 h1, card_support_swap hx.1.symm]; refl
723-
else
724-
have h : card (support (swap x (f x) * f)) + 1 = card (support f),
725-
by rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq h1,
726-
card_insert_of_not_mem (not_mem_erase _ _)],
727-
have wf : card (support (swap x (f x) * f)) < card (support f),
728-
from card_support_swap_mul hx.1,
729-
by rw [sign_mul, sign_swap hx.1.symm, sign_cycle (is_cycle_swap_mul hf hx.1 h1), ← h];
730-
simp only [pow_add, mul_one, units.neg_neg, one_mul, units.mul_neg, eq_self_iff_true,
731-
pow_one, units.neg_mul_neg]
732-
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ f, f.support.card)⟩]}
733-
734613
/-- If we apply `prod_extend_right a (σ a)` for all `a : α` in turn,
735614
we get `prod_congr_right σ`. -/
736615
lemma prod_prod_extend_right {α : Type*} [decidable_eq α] (σ : α → perm β)

0 commit comments

Comments
 (0)