Skip to content

Commit c5ab8fa

Browse files
Geoc2022Geoc2022
committed
Add PowMonoid PowGroup
1 parent caf3d2a commit c5ab8fa

2 files changed

Lines changed: 228 additions & 0 deletions

File tree

‎Game/MyAlgebra/PowGroup.lean‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
import Game.Levels.Group
2+
import Game.MyAlgebra.PowMonoid
3+
4+
namespace MyAlgebra
5+
6+
/-- The power function for groups -/
7+
def gpow {G : Type} [Group G] (x : G) : ℤ → G
8+
| Int.ofNat n => mpow x n
9+
| Int.negSucc n => mpow (x⁻¹) (n+1)
10+
11+
instance {G : Type} [Group G] : HPow G ℤ G where
12+
hPow := gpow
13+
14+
-- Basic lemmas
15+
@[simp]
16+
lemma gpow_eq_hpow (g : G) (n : ℤ) [Group G] : gpow g n = g ^ n := rfl
17+
18+
@[simp]
19+
lemma gpow_ofNat (g : G) (n : ℕ) [Group G] : g ^ ↑n = g ^ n := rfl
20+
21+
lemma gpow_negSucc (g : G) (n : ℕ) [Group G] : g ^ (Int.negSucc n) = (g⁻¹) ^ (n+1) := rfl
22+
23+
lemma inv_mpow (g : G) (n : ℕ) [Group G] : (g ^ n)⁻¹ = (g⁻¹) ^ n := by
24+
induction n with
25+
| zero =>
26+
simp
27+
rw [← inv_id]
28+
| succ n ih =>
29+
simp
30+
simp [mpow_add, ← inv_anticomm, ih, mpow_one, mpow_comm_mul]
31+
done
32+
33+
@[simp]
34+
lemma gpow_zero (g : G) [Group G] : g ^ (0 : ℤ) = 1 := rfl
35+
36+
@[simp]
37+
lemma gpow_one (g : G) [Group G] : g ^ (1 : ℤ) = g := by
38+
norm_cast
39+
exact mpow_one g
40+
41+
-- Start of Group Order Levels
42+
lemma gpow_neg_mpow (g : G) (x : ℕ) [Group G] : g ^ (-(x : ℤ)) = (g ^ x)⁻¹ := by
43+
cases x with
44+
| zero =>
45+
rw [Int.ofNat_zero]
46+
rw [Int.neg_zero]
47+
rw [gpow_zero g]
48+
rw [inv_id]
49+
rfl
50+
| succ x =>
51+
have h: -↑(x + 1) = Int.negSucc x := rfl
52+
rw [h]
53+
rw [gpow_negSucc]
54+
simp [inv_mpow, mpow_add, ← inv_anticomm, mpow_one, mpow_comm_mul]
55+
56+
57+
@[simp]
58+
lemma gpow_neg_one (g : G) [Group G] : g ^ (-1) = g⁻¹ := by
59+
rw [←Int.ofNat_one, gpow_neg_mpow]
60+
simp [mpow_one g]
61+
62+
63+
@[simp]
64+
lemma gpow_succ (g : G) (x : ℤ) [Group G] : g ^ (x + 1) = (g ^ x) * g := by
65+
induction x using Int.induction_on with
66+
| hz => rfl
67+
| hp x _ih =>
68+
repeat rw [←Int.ofNat_one]
69+
repeat rw [Int.ofNat_add_out]
70+
repeat rw [gpow_ofNat]
71+
rfl
72+
| hn x _ih =>
73+
rw [←Int.negSucc_coe', gpow_negSucc, mpow_succ_right, mul_assoc, inv_mul, mul_one]
74+
rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right, gpow_neg_mpow]
75+
exact inv_mpow g x
76+
77+
78+
lemma gpow_pred (g : G) (x : ℤ) [Group G] : (g ^ x) * (g⁻¹) = g ^ (x - 1) := by
79+
induction x with
80+
| ofNat x =>
81+
simp only [Int.ofNat_eq_coe]
82+
cases x with
83+
| zero =>
84+
rw [Int.ofNat_zero, gpow_zero]
85+
rw [one_mul, Int.zero_sub, gpow_neg_one]
86+
| succ x =>
87+
simp [gpow, Nat.cast_add, Nat.cast_one]
88+
rw [mul_assoc, mul_inv, mul_one]
89+
| negSucc x =>
90+
rw [Int.negSucc_sub_one, gpow_negSucc, gpow_negSucc]
91+
repeat rw [mpow_succ_right]
92+
93+
lemma gpow_add (g : G) (x y : ℤ) [Group G] : (g ^ x) * (g ^ y) = g ^ (x + y) := by
94+
induction y using Int.induction_on with
95+
| hz => rw [add_zero, gpow_zero, mul_one]
96+
| hp x ihn =>
97+
simp only [←Int.add_assoc, gpow_succ, mul_assoc]
98+
rw [←ihn]
99+
repeat rw [←mul_assoc]
100+
| hn x ihn =>
101+
rw [←gpow_pred, ←mul_assoc, ihn, gpow_pred, Int.add_sub_assoc]
102+
103+
lemma gpow_neg (g : G) (x : ℤ) [Group G] : g ^ (-x) = (g ^ x)⁻¹ := by
104+
induction x using Int.induction_on with
105+
| hz => rw [neg_zero, gpow_zero, ←inv_id]
106+
| hp x ih =>
107+
rw [Int.neg_add, ←Int.sub_eq_add_neg, ←gpow_pred, ih, inv_anticomm, ←Int.add_comm]
108+
rw [←gpow_add]
109+
rw [gpow_one]
110+
| hn x ih =>
111+
simp at *
112+
rw [Int.add_comm, gpow_succ, ih, ←gpow_pred, gpow_neg_mpow, inv_anticomm]
113+
repeat rw [← inv_inv]
114+
rw [← mpow_succ_right, mpow_succ_left]
115+
116+
@[simp]
117+
lemma gpow_sub (g : G) (x y : ℤ) [Group G] : (g ^ x) * ((g ^ y)⁻¹) = g ^ (x - y) := by
118+
rw [sub_eq_add_neg, ←gpow_add, gpow_neg]
119+
120+
121+
lemma gpow_mul (g : G) (x y : ℤ) [Group G] : g ^ (x * y) = (g ^ x) ^ y := by
122+
induction y using Int.induction_on with
123+
| hz => rw [mul_zero, gpow_zero, gpow_zero]
124+
| hp n ih => rw [mul_add, mul_one, ←gpow_add, gpow_succ, ih]
125+
| hn n ih => rw [Int.mul_sub, mul_one, ←gpow_sub, ←gpow_pred, ih]
126+
127+
-- theorem gpow_closure {H : Subgroup G} {n : ℤ}: x ∈ H → gpow x n ∈ H := by
128+
-- intro h
129+
-- induction n using Int.induction_on with
130+
-- | hz => exact H.one_mem
131+
-- | hp n ih =>
132+
-- rw [gpow_succ]
133+
-- apply H.mul_closure
134+
-- · exact ih
135+
-- · exact h
136+
-- | hn n ih =>
137+
-- rw [←gpow_pred, gpow_neg]
138+
-- apply H.mul_closure
139+
-- · rw [←gpow_neg]
140+
-- exact ih
141+
-- · apply H.inv_closure
142+
-- exact h

‎Game/MyAlgebra/PowMonoid.lean‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
import Game.Levels.Monoid
2+
3+
namespace MyAlgebra
4+
5+
/-- The power function for monoids -/
6+
def mpow {M : Type} [Monoid M] (x : M) : ℕ → M
7+
| Nat.zero => 1
8+
| Nat.succ n => (mpow x n) * x
9+
10+
instance {M : Type} [Monoid M] : HPow M ℕ M where
11+
hPow := mpow
12+
13+
-- Basic lemmas
14+
@[simp]
15+
lemma mpow_eq_hpow (m : M) (n : ℕ) [Monoid M] : mpow m n = m ^ n := rfl
16+
17+
@[simp]
18+
lemma mpow_zero (m : M) [Monoid M] : m ^ 0 = 1 := rfl
19+
20+
/-- m ^ (n + 1) = m ^ n * m -/
21+
@[simp]
22+
lemma mpow_succ_right (m : M) [Monoid M] : m ^ (n+1) = (m ^ n) * m := rfl
23+
24+
25+
-- Start of Monoid Order Levels
26+
/-- m¹ = m -/
27+
@[simp]
28+
lemma mpow_one (m : M) [Monoid M] : m ^ 1 = m := by
29+
rw [mpow_succ_right, mpow_zero, one_mul]
30+
31+
/-- m ^ (n + 1) = m * m ^ n-/
32+
lemma mpow_succ_left (m : M) [Monoid M] : m ^ (n + 1) = m * (m ^ n) := by
33+
induction n with
34+
| zero =>
35+
rw [mpow_zero, mpow_one]
36+
rw [mul_one]
37+
| succ n ih =>
38+
rw [mpow_succ_right]
39+
nth_rw 2 [mpow_succ_right]
40+
rw [ih, mul_assoc]
41+
42+
/-- m ^ (x + y) = m ^ x * m ^ y -/
43+
lemma mpow_add (m : M) (x y : ℕ) [Monoid M]: m ^ (x + y) = (m ^ x) * (m ^ y) := by
44+
induction y with
45+
| zero => rw [mpow_zero, mul_one, Nat.add_zero]
46+
| succ y ih =>
47+
rw [Nat.add_succ, mpow_succ_right, ih]
48+
rw [mpow_succ_right]
49+
rw [mul_assoc]
50+
51+
/-- m ^ (x * y) = (m ^ x) ^ y-/
52+
lemma mpow_mul (m : M) (x y : ℕ) [Monoid M] : m ^ (x * y) = (m ^ x) ^ y := by
53+
induction y with
54+
| zero =>
55+
rw [Nat.mul_zero, mpow_zero, mpow_zero]
56+
| succ y ih =>
57+
simp only [mpow_succ_right]
58+
rw [Nat.mul_succ, mpow_add, ih]
59+
60+
/-- 1 ^ x = 1 -/
61+
@[simp]
62+
lemma mpow_id (x : ℕ) [Monoid M] : 1 ^ x = (1 : M) := by
63+
induction x with
64+
| zero => rfl
65+
| succ x ih => rw [mpow_succ_right, ih, mul_one]
66+
67+
/-- m ^ x * m = m * m ^ x -/
68+
lemma mpow_comm_mul (m: M) (x : ℕ) [Monoid M] : (m ^ x) * m = m * (m ^ x) := by
69+
induction x with
70+
| zero => rw [mpow_zero, mul_one, one_mul]
71+
| succ x ih =>
72+
nth_rw 1 [mpow_succ_left, mpow_succ_right]
73+
rw [mul_assoc, ih]
74+
done
75+
76+
/-- m ^ x * m ^ y = m ^ y * m ^ x -/
77+
lemma mpow_comm_mpow (m : M) (x y : ℕ) [Monoid M] : (m ^ x) * (m ^ y) = (m ^ y) * (m ^ x) := by
78+
induction y with
79+
| zero => rw [mpow_zero, mul_one, one_mul]
80+
| succ y ih =>
81+
rw [mpow_succ_left]
82+
rw [mul_assoc]
83+
rw [← ih]
84+
rw [← mul_assoc m _ _]
85+
rw [← mul_assoc _ m _]
86+
rw [mpow_comm_mul]

0 commit comments

Comments
 (0)