Updates

- Split things between files
- Added a few new things

Author: kaleidawave

.gitignore

@@ -3,4 +3,5 @@
 /private
 .lake
 TODO.md
-.vscode
+.vscode
+**/*/private_*.lean

Mathematics.lean

@@ -1 +1,4 @@
--- TODO what goes here
+import Mathematics.Logic
+import Mathematics.Structures.Numbers.Natural
+import Mathematics.Structures.Set
+import Mathematics.Algebra.Group

Mathematics/Algebra/Group.lean

@@ -1,12 +1,11 @@
 import Mathematics.Structures.Relation
 
-class Inv (T : Type) where
-  inv : T → T
+class Inverse (T : Type) where
+  inverse' : T → T
 
-postfix:max "⁻¹" => Inv.inverse
+postfix:max "⁻¹" => Inverse.inverse'
 
--- TODO to_additive
-class Group (T: Type) extends Mul T, Inv T, OfNat T 1 :=
+class Group (T: Type) extends Mul T, Inverse T, OfNat T 1 :=
 associativity : ∀ a b c: T, a * (b * c) = (a * b) * c
 identity : ∀ a: T, a * 1 = a ∧ 1 * a = a
 inverse : ∀ a: T, a⁻¹ * a = 1 ∧ a * a⁻¹ = 1
@@ -26,24 +25,24 @@ theorem one.multiply (a: T) : 1 * a = a := (Group.identity a).right
 theorem multiply.associative: ∀ a b c: T, a * (b * c) = (a * b) * c := Group.associativity
 
 theorem inv.double : (a⁻¹)⁻¹ = a := by
-  rw [←multiply.one (a⁻¹)⁻¹, ←(Group.inverseerse a).left, Group.associativity, (Group.inverseerse _).left, one.multiply]
+  rw [←multiply.one (a⁻¹)⁻¹, ←(Group.inverse a).left, Group.associativity, (Group.inverse _).left, one.multiply]
 
-theorem one.inverseerse : (1⁻¹) = (1: T) := by
-  rw [←multiply.one 1⁻¹, (Group.inverseerse 1).1]
+theorem one.inverse : (1⁻¹) = (1: T) := by
+  rw [←multiply.one 1⁻¹, (Group.inverse 1).1]
 
 theorem multiply.eq_one_implies_eq (h : a * b = 1) : a⁻¹ = b := by
-  rw [←multiply.one a⁻¹, ←h, Group.associativity, (Group.inverseerse a).left, one.multiply]
+  rw [←multiply.one a⁻¹, ←h, Group.associativity, (Group.inverse a).left, one.multiply]
 
 theorem inv.multiply : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
   apply multiply.eq_one_implies_eq
-  rw [←Group.associativity, Group.associativity b, (Group.inverseerse _).right, one.multiply, (Group.inverseerse a).right]
+  rw [←Group.associativity, Group.associativity b, (Group.inverse _).right, one.multiply, (Group.inverse a).right]
 
 theorem multiply.left_cancel (h : a * b = a * c) : b = c := by
-  rw [←one.multiply b, ←(Group.inverseerse a).left, ←Group.associativity, h, Group.associativity, (Group.inverseerse a).left, one.multiply c]
+  rw [←one.multiply b, ←(Group.inverse a).left, ←Group.associativity, h, Group.associativity, (Group.inverse a).left, one.multiply c]
 
 -- Note the symmetry with above
 theorem multiply.right_cancel (h : b * a = c * a) : b = c := by
-  rw [←multiply.one b, ←(Group.inverseerse a).right, Group.associativity, h, ←Group.associativity, (Group.inverseerse a).right, multiply.one c]
+  rw [←multiply.one b, ←(Group.inverse a).right, Group.associativity, h, ←Group.associativity, (Group.inverse a).right, multiply.one c]
 
 theorem multiply.injective_inverse : a⁻¹ = b⁻¹ ↔ a = b := by
   apply Iff.intro
@@ -78,70 +77,6 @@ end groups
 
 def conjugation { T: Type } [Group T] (c: T) := fun (x: T) => c * x * c⁻¹
 
-class GroupHomomorphism (T U: Type) [Group T] [Group U] (f: T -> U) :=
-map_mul : ∀ a b: T, f (a * b) = f a * f b
-
-namespace group_homomorphism
-
-def in_kernel {T U: Type} [Group T] [Group U] (f: T -> U) (a: T): Prop := f a = 1
-def in_image {T U: Type} [Group T] [Group U] (f: T -> U) (b: U): Prop := ∃ a: T, f a = b
-
-open groups
-
-variable {T U: Type} [Group T] [Group U] (f: T -> U) [GroupHomomorphism T U f]
-
-theorem map.multiply : ∀ a b: T, f (a * b) = f a * f b := GroupHomomorphism.map_mul
-
-theorem map.one : f 1 = 1 := by
-  apply groups.multiplytiply.left_cancel
-  show f 1 * f 1 = f 1 * 1
-  rw [←GroupHomomorphism.map_mul, multiply.one, multiply.one]
-
-def id := fun (x: T) => x
-
-theorem id.homomorphism : GroupHomomorphism T T id := {
-  map_mul := by intros a b; exact rfl
-}
-
-theorem conjugation.homomorphism (c: T) : GroupHomomorphism T T (conjugation c) := {
-  map_mul := by
-    intros a b
-    unfold conjugation
-    rw [
-      ←multiply.associative c b,
-      multiply.associative _ c,
-      ←multiply.associative _ _ c,
-      (Group.inverseerse c).left,
-      multiply.one,
-      multiply.associative,
-      multiply.associative
-    ]
-}
-
-theorem homomorphism.compose { V: Type } [Group V] (f: T -> U) (g: U -> V) [GroupHomomorphism _ _ f] [GroupHomomorphism _ _ g]
-  : GroupHomomorphism T V (g ∘ f) := {
-    map_mul := by
-      intros a b
-      unfold Function.comp
-      rw [←map.multiply, ←map.multiply]
-}
-
-theorem map.inverse (a : T) : f a⁻¹ = (f a)⁻¹ := by
-  apply (multiply.left_cancel_iff (f a) (f a⁻¹) (f a)⁻¹).mp
-  rw [←map.multiply, (Group.inverseerse a).right, (Group.inverseerse (f a)).right]
-  exact @map.one T U _ _ f _
-
-theorem map.multiplytiply.inverse (a b : T) : (f (a * b))⁻¹ = f b⁻¹ * f a⁻¹ := by
-  rw [←map.multiply, ←inv.multiply, ←map.inverse]
-
--- TODO exponents
--- theorem map_pow (a : T) (n : Natural) : f a ^ n = (f a) ^ n := by
---   induction n with
---   | zero => rw [power.zero]
---   | successor n ih => rw [power.successor, ih]
-
-end group_homomorphism
-
 namespace random
 
 variable {T: Type} [Group T]
@@ -153,24 +88,24 @@ instance : Relation T are_conjugate := {
   symmetric := by
     intro a b h1
     let ⟨g, h2⟩ := h1
-    apply Exists.intro (Inv.inverse g)
+    apply Exists.intro g⁻¹
     unfold conjugation at *
     rw [
       h2,
       inv.double,
       multiply.associative,
       ←multiply.associative _ g⁻¹ g,
-      (Group.inverseerse g).1,
+      (Group.inverse g).1,
       multiply.one,
       multiply.associative,
-      (Group.inverseerse g).1,
+      (Group.inverse g).1,
       one.multiply
     ]
   reflexivity := by
     intro a
     apply Exists.intro 1
     unfold conjugation at *
-    rw [one.multiply, one.inverseerse, multiply.one]
+    rw [one.multiply, one.inverse, multiply.one]
   transitivity := by
     intro a b c h1
     let ⟨⟨g1, h2⟩, ⟨g2, h3⟩⟩ := h1
@@ -186,7 +121,7 @@ namespace product
 def Group.Product (A B: Type) [Group A] [Group B] : Type := A × B
 
 instance (A B: Type) [Group A] [Group B] : Mul (Group.Product A B) := ⟨fun (g1, g2) (h1, h2) => (g1 * h1, g2 * h2)⟩
-instance (A B: Type) [Group A] [Group B] : Inv (Group.Product A B) := ⟨fun (g1, g2) => (g1⁻¹, g2⁻¹)⟩
+instance (A B: Type) [Group A] [Group B] : Inverse (Group.Product A B) := ⟨fun (g1, g2) => (g1⁻¹, g2⁻¹)⟩
 instance (A B: Type) [Group A] [Group B] : OfNat (Group.Product A B) 1 := ⟨(1, 1)⟩
 
 theorem mul_eq (A B: Type) [Group A] [Group B] (a b: Group.Product A B) : a * b = (a.1 * b.1, a.2 * b.2) := rfl
@@ -200,7 +135,7 @@ instance (A B: Type) {ga: Group A} {gb: Group B} : Group (Group.Product A B) :=
     rfl
   inverse := by
     intro a
-    rw [mul_inv, mul_eq, (ga.inverseerse _).1, (gb.inverseerse _).1, mul_eq, (ga.inverseerse _).2, (gb.inverseerse _).2]
+    rw [mul_inv, mul_eq, (ga.inverse _).1, (gb.inverse _).1, mul_eq, (ga.inverse _).2, (gb.inverse _).2]
     exact ⟨one_left _ _, one_left _ _⟩
   identity := by
     intro a

Mathematics/Algebra/Group/Homomorphism.lean

@@ -0,0 +1,63 @@
+import Mathematics.Algebra.Group
+
+class GroupHomomorphism (T U: Type) [Group T] [Group U] (f: T -> U) :=
+map_mul : ∀ a b: T, f (a * b) = f a * f b
+
+def in_kernel {T U: Type} [Group T] [Group U] (f: T -> U) (a: T): Prop := f a = 1
+def in_image {T U: Type} [Group T] [Group U] (f: T -> U) (b: U): Prop := ∃ a: T, f a = b
+
+open groups
+
+variable {T U: Type} [Group T] [Group U] (f: T -> U) [GroupHomomorphism T U f]
+
+theorem map.multiply : ∀ a b: T, f (a * b) = f a * f b := GroupHomomorphism.map_mul
+
+theorem map.one : f 1 = 1 := by
+  apply groups.multiply.left_cancel
+  show f 1 * f 1 = f 1 * 1
+  rw [←GroupHomomorphism.map_mul, multiply.one, multiply.one]
+
+-- def id := fun (x: T) => x
+
+instance : GroupHomomorphism T T id := {
+  map_mul := by intros a b; exact rfl
+}
+
+instance (c: T) : GroupHomomorphism T T (conjugation c) := {
+  map_mul := by
+    intros a b
+    unfold conjugation
+    rw [
+      ←multiply.associative c b,
+      multiply.associative _ c,
+      ←multiply.associative _ _ c,
+      (Group.inverse c).left,
+      multiply.one,
+      multiply.associative,
+      multiply.associative
+    ]
+}
+
+instance homomorphism.compose { V: Type } [Group V] (f: T -> U) (g: U -> V) [GroupHomomorphism _ _ f] [GroupHomomorphism _ _ g]
+  : GroupHomomorphism T V (g ∘ f) := {
+    map_mul := by
+      intros a b
+      unfold Function.comp
+      rw [←map.multiply, ←map.multiply]
+}
+
+theorem map.inverse (a : T) : f a⁻¹ = (f a)⁻¹ := by
+  apply (multiply.left_cancel_iff (f a) (f a⁻¹) (f a)⁻¹).mp
+  rw [←map.multiply, (Group.inverse a).right, (Group.inverse (f a)).right]
+  exact @map.one T U _ _ f _
+
+theorem map.multiply.inverse (a b : T) : (f (a * b))⁻¹ = f b⁻¹ * f a⁻¹ := by
+  rw [←map.multiply, ←inv.multiply, ←map.inverse]
+
+-- TODO exponents
+-- theorem map_pow (a : T) (n : Natural) : f a ^ n = (f a) ^ n := by
+--   induction n with
+--   | zero => rw [power.zero]
+--   | successor n ih => rw [power.successor, ih]
+
+def AutomorphismOf (T: Type) [Group T] := GroupHomomorphism T T

Mathematics/Algebra/Group/Order.lean

@@ -1,9 +1,11 @@
 import Mathematics.Algebra.Group
 import Mathematics.Structures.Numbers.Natural
+import Mathematics.Structures.Numbers.Natural.Addition
+import Mathematics.Structures.Numbers.Natural.Multiplication
 
 def Group.power {T: Type} [Group T] (a: T) (n: Natural) : T := match n with
 | Natural.zero => 1
-| Natural.successor n => (pow a n) * a
+| Natural.successor n => (Group.power a n) * a
 
 instance {T: Type} [Group T] : Pow T Natural where
   pow := Group.power
@@ -21,44 +23,42 @@ theorem power.successor (n: Natural) : a ^ Natural.successor n = a ^ n * a := rf
 theorem power.successor' (n: Natural) : a ^ Natural.successor n = a * a ^ n := by
   rw [power.successor]
   induction n with
-  | zero => rw [power.zero, one.multiply, multiply.one]
+  | zero => rw [power.zero, groups.one.multiply, groups.multiply.one]
   | successor n ih => rw [power.successor, Group.associativity, multiply.right_cancel_iff, ih]
 
 theorem power.one : a ^ (1: Natural) = a := by
-  rw [←successor.zero_eq_one, power.successor, power.zero, one.multiply]
+  rw [←successor.zero_eq_one, power.successor, power.zero, groups.one.multiply]
 
 theorem one.power (n: Natural) : (1 : T) ^ n = 1 := by
   induction n with
   | zero => exact power.zero 1
-  | successor n ih => rw [power.successor, ih, multiply.one]
+  | successor n ih => rw [power.successor, ih, groups.multiply.one]
 
-open addition in
 theorem power.add (m n : Natural) : a ^ (m + n) = a^m * a^n := by
   induction n with
-  | zero => rw [zero.eq_zero, add.zero, ←zero.eq_zero, power.zero, multiply.one]
-  | successor n ih => rw [add.successor, power.successor, power.successor, multiply.associative, multiply.right_cancel_iff, ih]
+  | zero => rw [Natural.zero_def, Natural.add.zero, ←Natural.zero_def, power.zero, groups.multiply.one]
+  | successor n ih => rw [add.successor, power.successor, power.successor, groups.multiply.associative, multiply.right_cancel_iff, ih]
 
-open multiplication in
 theorem power.multiply (m n : Natural) : a ^ (m * n) = (a ^ m) ^ n := by
   induction n with
-  | zero => rw [zero.eq_zero, multiply.zero, ←zero.eq_zero, power.zero, power.zero]
+  | zero => rw [Natural.zero_def, multiply.zero, ←Natural.zero_def, power.zero, power.zero]
   | successor n ih => rw [power.successor, ←ih, ←power.add, multiply.successor]
 
 theorem multiply.power {U : Type} [AbelianGroup U] (a b: U) (n : Natural) : (a * b) ^ n = a ^ n * b ^ n := by
   induction n with
-  | zero => rw [power.zero, power.zero, power.zero, multiply.one]
+  | zero => rw [power.zero, power.zero, power.zero, groups.multiply.one]
   | successor n ih => {
     rw [power.successor,
       power.successor,
       power.successor,
-      ←multiply.associative (a ^ n) a,
+      ←groups.multiply.associative (a ^ n) a,
       AbelianGroup.commutativity a (b ^ n * b),
       ih,
       AbelianGroup.commutativity a b,
-      ←multiply.associative (b ^ n) b a,
-      multiply.associative,
-      multiply.associative,
-      multiply.associative
+      ←groups.multiply.associative (b ^ n) b a,
+      groups.multiply.associative,
+      groups.multiply.associative,
+      groups.multiply.associative
     ]
   }
 

Mathematics/Algebra/PartialOrder.lean

@@ -0,0 +1,4 @@
+class PartialOrder (T: Type) (relation: T → T → Prop) :=
+reflexivity : ∀ a: T, relation a a
+antisymmetric : ∀ a b: T, (relation a b) ∧ (relation b a) → a = b
+transitivity : ∀ a b c: T, (relation a b) ∧ (relation b c) → (relation a c)

Mathematics/Random/README.md

@@ -9,3 +9,7 @@ def repeated_apply { T: Type } (f: T → T) (n: Natural) (a: T) : T := match n w
 
 /- adding three four times to 2 results in 14 -/
 example : repeated_apply (. + 3) 4 2 = 14 := rfl
+
+def function.point_free { T: Type } (f: T → T) : Prop := ∀t: T, f t ≠ t
+
+def function.is_involution { T: Type } (f: T → T) : Prop := ∀t: T, f (f t) = t