add pre-update

Author: Geoc2022

Game/Levels/Group/L01_MulLeft.lean

@@ -8,7 +8,7 @@ Title "Left Multiplication"
 
 namespace MyAlgebra
 
-Introduction "Just to get us warmed up, let's create some lemmas to make it easy to multiply."
+Introduction "Just to get us warmed up, let's create some lemmas for multiplication."
 
 /--
 `mul_left` is a proof that if `g1 = g2`, then `h * g1 = h * g2` - basically `h * _` is a function.

Game/Levels/Group/L02_MulRight.lean

@@ -10,7 +10,7 @@ namespace MyAlgebra
 Introduction "Here's a duel of that last level."
 
 /--
-`mul_right` is a proof that if `g1 = g2`, then `g1 * h = g2 * h` - basically `_ * h` is a function.
+`mul_right` is a proof that if `g1 = g2`, then `g1 * h = g2 * h` - based on `_ * h` is a well defined function.
 -/
 TheoremDoc MyAlgebra.mul_right as "mul_left" in "Group"
 @[to_additive]
@@ -19,4 +19,4 @@ Statement mul_right (g : G) [Group G] : g1 = g2 → g1 * g = g2 * g := by
   rw [h]
 
 
-Conclusion "Don't worry it going to get a bit more challenging (and a lot more fun)!"
+Conclusion "Don't worry it's going to get a bit more challenging (and a lot more fun)!"

Game/Levels/Group/L08_CombinedInv2.lean

@@ -39,8 +39,9 @@ NewDefinition MyAlgebra.prod_list MyAlgebra.prod_list_inv
 /--
 `inv_n_prod` is a proof that the inverse of a product of `n` elements is the product of the inverses in reverse order.
 -/
-TheoremDoc MyAlgebra.inv_n_prod as "inv_n_prod" in "Group"
-Statement inv_n_prod (l : List G) [Group G] : is_inv (prod_list l) (prod_list_inv l) := by
+-- TheoremDoc MyAlgebra.inv_n_prod as "inv_n_prod" in "Group"
+-- Statement inv_n_prod (l : List G) [Group G] : is_inv (prod_list l) (prod_list_inv l) := by
+Statement (l : List G) [Group G] : is_inv (prod_list l) (prod_list_inv l) := by
   Hint "Since we're working with a generalized number of elements, it might be helpful to use induction. It also helps that the functions `prod_list` and `prod_list_inv` are defined recursively."
   induction' l with fst rst
 
@@ -73,7 +74,7 @@ Statement inv_n_prod (l : List G) [Group G] : is_inv (prod_list l) (prod_list_in
 Conclusion "Congrats!"
 
 /--
-`induction l with fst rst` is a tactic that performs induction on the list `l`, with the first element of the list being called `fst` and the rest of the list being called `rst`.
+`induction' l with fst rst` is a tactic that performs induction on the list `l`, with the first element of the list being called `fst` and the rest of the list being called `rst`.
 -/
 TacticDoc induction'
 

Game/Levels/Group/L09_InvInv.lean

@@ -8,7 +8,7 @@ Title "Inverse of an Inverse"
 namespace MyAlgebra
 
 Introduction "
-  You would expect the inverse of an inverse to be the original element. Ex. `-(-2) = 2` or the composition of two flips is the identity. But let's formally prove it.
+  You should expect the inverse of an inverse to be the original element. Ex. `-(-2) = 2` or the composition of two flips is the identity. But let's formally prove it.
 "
 
 /--

Game/Levels/GroupExamples.lean

@@ -0,0 +1,11 @@
+import Game.Levels.GroupExamples.L01_Z_mod_mZ_Id
+import Game.Levels.GroupExamples.L02_Z_mod_mZ_Inv
+import Game.Levels.GroupExamples.L03_Dihedral_Id
+import Game.Levels.GroupExamples.L04_Dihedral_Inv
+
+World "Group Examples"
+Title "Group Examples World"
+
+Introduction "
+  In this world, we will explore some examples of groups. We will see how the axioms of groups apply to these examples and how they can be used to prove properties about the groups.
+"

Game/Levels/GroupExamples/L01_Z_mod_mZ_Id.lean

@@ -0,0 +1,32 @@
+import Game.MyAlgebra.Z_mod_mZ
+import Game.Levels.Group.L05_OneUnique
+
+World "Group Examples"
+Level 1
+
+Title "Z mod mZ Identity"
+
+namespace MyAlgebra
+
+Introduction "
+  The set of integers Z = {... , −2, −1, 0, 1, 2, . . .} is a group if we use addition as the group law. It is an example of group with infinitely many elements.
+
+  What goes wrong if we try to use multiplication as the group law?
+
+  The set of integers modulo m (denoted Z/mZ) forms a group with addition as the group law.
+
+  Ex. Z/12Z = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} is the group of integers modulo 12, which we use on clocks. If it's 11am and you add 1 hour, the clock wraps back to the start and it becomes 0pm (or 12pm).
+
+  In this level, we will prove that the identity element of the group Z_mod_mZ is 0.
+"
+
+/--
+`Z_mod_mZ_id` is a proof that the identity element of the group `Z_mod_mZ` is `0`.
+-/
+TheoremDoc MyAlgebra.Z_mod_mZ_id as "Z_mod_mZ_id" in "Group Examples"
+Statement Z_mod_mZ_id (m : ℕ) (a : ZMod m) : 0 + a = a ∧ a + 0 = a := by
+  Hint "We can use `add_zero` and `zero_add` from the Natural numbers."
+  rw [add_zero, zero_add]
+  exact ⟨rfl, rfl⟩
+
+Conclusion "Congrats!"

Game/Levels/GroupExamples/L02_Z_mod_mZ_Inv.lean

@@ -0,0 +1,28 @@
+import Game.Levels.GroupExamples.L01_Z_mod_mZ_Id
+
+World "Group Examples"
+Level 2
+
+Title "Z mod mZ Inverses"
+
+namespace MyAlgebra
+
+Introduction "
+  In this level, we will prove that every element in the group `Z_mod_mZ` has an inverse.
+
+  It might be helpful to use the `sub_eq_add_neg` and `sub_eq_neg_add` lemmas from the Natural numbers, which relate subtraction to addition with negation. Also, `sub_self` can be used to show that subtracting an element from itself gives zero.
+"
+
+/--
+`Z_mod_mZ_inv` is a proof that the group `Z_mod_mZ` has an inverse for every element `a`.
+-/
+TheoremDoc MyAlgebra.Z_mod_mZ_inv as "Z_mod_mZ_inv" in "Group Examples"
+Statement Z_mod_mZ_inv (m : ℕ) (a : ZMod m) : ∃ b : ZMod m, a + b = 0 ∧ b + a = 0 := by
+  Hint "What is the inverse of an element in `Z_mod_mZ`?"
+  use (-a : ZMod m)
+  rw [← sub_eq_add_neg]
+  rw [← sub_eq_neg_add]
+  rw [sub_self]
+  exact ⟨rfl, rfl⟩
+
+Conclusion "Congrats!"

Game/Levels/GroupExamples/L03_Dihedral_Id.lean

@@ -0,0 +1,64 @@
+import Game.MyAlgebra.Dihedral
+import Game.Levels.GroupExamples.L02_Z_mod_mZ_Inv
+
+open MyAlgebra
+
+
+World "Group Examples"
+Level 3
+
+Title "Dihedral Group Identity"
+
+namespace MyAlgebra
+
+Introduction "
+  We can consider n-gons and their symmetries, which form a group called the dihedral group. The dihedral group of order 2n, denoted D_n, consists of n rotations and n reflections.
+
+  Here is a square with its vertices labeled (1,2,3,4) and its symmetries (rotations and reflections):
+
+    1-----2
+    |     |
+    4-----3
+
+  Rotations:
+    0° (identity)      90°                180°               270°
+    1-----2            4-----1            3-----4            2-----3
+    |     |            |     |            |     |            |     |
+    4-----3            3-----2            2-----1            1-----4
+
+  Reflections:
+    Vertical           Horizontal         Diagonal (\\)        Diagonal (/)
+    2-----1            4-----3            1-----4             3-----2
+    |     |            |     |            |     |             |     |
+    3-----4            1-----2            2-----3             4-----1
+
+  Each symmetry is an element of the dihedral group D₄.
+
+
+  We define the dihedral group D_n as follows:
+  ```
+  inductive Dihedral (n : ℕ) : Type
+    | r : ZMod n → Dihedral n
+    | sr : ZMod n → Dihedral n
+  ```
+  The elements of D_n are either rotations (`r i`) or reflections (`sr i`), where i is an integer modulo n. `r` stands for rotation and `s` stands for reflection.
+
+  In this level, we will prove that the identity element of the dihedral group D_n is the identity rotation, which does not change the polygon.
+"
+
+namespace Dihedral
+
+variable {n : ℕ}
+
+/--
+`Dihedral_id` is a proof that the identity element of the dihedral group `D_n` is `r 0`.
+-/
+TheoremDoc MyAlgebra.Dihedral_id as "Dihedral_id" in "Group Examples"
+Statement Dihedral_id (n : ℕ) (a : Dihedral n) : ∃ b : Dihedral n, mul a (r 0) = a ∧ mul (r 0) a = a := by
+  use r 0
+  Hint "Use the definition of multiplication in the dihedral group."
+  induction a with
+  | r i => simp [mul]
+  | sr i => simp [mul]
+
+Conclusion "Congrats!"

Game/Levels/GroupExamples/L04_Dihedral_Inv.lean

@@ -0,0 +1,31 @@
+import Game.Levels.GroupExamples.L03_Dihedral_Id
+
+World "Group Examples"
+Level 4
+
+Title "Z mod mZ Inverses"
+
+namespace MyAlgebra
+
+Introduction "
+  In this level, we will prove that every element in the dihedral group has an inverse.
+"
+
+namespace Dihedral
+
+
+/--
+`Dihedral_inv` is a proof that the group `Z_mod_mZ` has an inverse for every element `a`.
+-/
+TheoremDoc MyAlgebra.Dihedral_inv as "Dihedral_inv" in "Group Examples"
+Statement Dihedral_inv (n : ℕ) (a : Dihedral n) : ∃ b : Dihedral n, mul a b = (r 0) ∧ mul b a = (r 0) := by
+  Hint "What is the inverse of an element in `Dihedral`? Dihedral elements are either rotations or reflections."
+  induction a with
+  | r i =>
+    use (r (- i))
+    simp [mul]
+  | sr i =>
+    use (sr i)
+    simp [mul]
+
+Conclusion "Congrats!"

Game/Levels/GroupHom.lean

@@ -8,7 +8,7 @@ World "GroupHom"
 Title "Group Homomorphisms"
 
 Introduction "
-  After creating groups, it's probably a good idea to define a function between groups. There can be a lot of different functions between groups, but we only care about the ones that preserve the group structure. These functions are called homomorphisms.
+  After creating groups, it's a good idea to define a function between them. There can be a lot of different functions between groups, but we only care about the ones that preserve the group structure (becasue they are the only interesting ones). These functions are called homomorphisms.
 
   So what makes up the group structure? Well, we have a set `α`, a binary operation `*`, an identity element `1`, and inverses. Therefore, we need to define a function that preserves these aspects.