Updates across Algebra, Naturals and Set

Author: kaleidawave

Mathematics.lean

@@ -2,3 +2,4 @@ import Mathematics.Logic
 import Mathematics.Structures.Numbers.Natural
 import Mathematics.Structures.Set
 import Mathematics.Algebra.Group
+import Mathematics.Algebra.Field

Mathematics/Algebra/Field.lean

@@ -0,0 +1,118 @@
+class Field (T: Type) extends Zero T, OfNat T 1, Add T, Sub T, Neg T, Mul T, Div T, LE T, LT T where
+different: (0: T) ≠ (1: T)
+add_zero: ∀x: T, x + 0 = x
+zero_add: ∀x: T, 0 + x = x
+add_associative: ∀a b c: T, a + (b + c) = (a + b) + c
+add_commutative: ∀a b: T, a + b = b + a
+zero_mul: ∀x: T, 0 * x = 0
+one_mul: ∀x: T, 1 * x = x
+mul_associative: ∀a b c: T, a * (b * c) = a * b * c
+mul_commutative: ∀a b: T, a * b = b * a
+neg_def: ∀x: T, -x = -1 * x
+sub_eq: ∀x y: T, x = y ↔ x - y = 0
+sub_def: ∀x y: T, x - y = x + (-1 * y)
+distributive: ∀a b c: T, a * c + b * c = (a + b) * c
+-- TODO can this one be proven from above?
+neg_neg: ∀x: T, - (-x) = x
+div_self : ∀a: T, (a / a) = 1
+add_neg_assoc : ∀a b c: T, a - (b + c) = a - b - c
+add_neg_rerrange : ∀a b c d: T, a + b - c - d = (a - c) + (b - d)
+-- Double check
+add_neg_rerrange₂ : ∀a b c d: T, a - b + (c - d) = (a - d) - (b - c)
+-- TODO can these be proven
+div_add: ∀a b c: T, (a / c) + (b / c) = (a + b) / c
+div_mul: ∀a b c: T, (a * b) / c = a * (b / c)
+
+theorem Field.sub_distributive {T: Type} [Field T] (a b c: T): a * b - a * c = a * (b - c) := by
+  rw [
+    sub_def,
+    mul_commutative a c,
+    mul_associative,
+    mul_commutative a _,
+    distributive,
+    ←sub_def,
+    mul_commutative a _,
+  ]
+
+theorem Field.distributive' {T: Type} [f: Field T] (a b c: T): a * b + a * c = a * (b + c) := by
+  rw [f.mul_commutative a (b + c), ←f.distributive, f.mul_commutative a b, f.mul_commutative c a]
+
+-- TODO via calc
+theorem Field.difference_of_squares {T: Type} [Field T] (a b: T) : (a * a - b * b) = (a + b) * (a - b) := by
+  rw [
+    ←distributive,
+    ←sub_distributive,
+    ←sub_distributive,
+    add_neg_rerrange₂,
+    -- This line is a little complex
+    (sub_eq (a * b) (b * a)).mp (mul_commutative a b),
+    -- TODO this can be extracted as their own theorems
+    sub_def _ 0,
+    mul_commutative _ 0,
+    zero_mul,
+    add_zero
+  ]
+
+theorem Field.sub_zero {T: Type} [Field T] (a: T) : a - 0 = a := by
+  rw [Field.sub_def, Field.mul_commutative, Field.zero_mul, Field.add_zero]
+
+theorem Field.mul_one {T: Type} [Field T] (a: T) : a * 1 = a := (Field.mul_commutative _ (1: T)) ▸ Field.one_mul a
+
+theorem Field.add_self {T: Type} [Field T] (a: T): a + a = (1 + 1) * a := by
+  conv => lhs; rw [←Field.one_mul a];
+  rw [Field.distributive]
+
+class OrderedField (T: Type) [Field T] extends LE T, LT T where
+eq_then_leq: ∀a: T, a = a → a <= a
+total: ∀a b: T, a < b ∨ a >= b
+le_def: ∀a b: T, a <= b ↔ (a = b ∨ a < b)
+gt_zero_one: 0 < (1: T)
+-- TODO this might need some work
+le_def₂: ∀a b: T, a <= b ↔ ∃c: T, c >= 0 ∧ a + c = b
+
+lt_lt_trans : ∀a b c: T, a < b → b < c → a < c
+ge_one_two: 1 <= (1 + 1: T)
+gt_zero_two: 0 < (1 + 1: T)
+gt_one_two: 1 < (1 + 1: T)
+lt_div : ∀a b: T, a > b → (a / (1 + 1)) > b
+lt_add: ∀a b c d: T, a < b → c < d → (a + c) < (b + d)
+lt_sub: ∀a b c: T, a - b > c → a > b + c
+lt_sub': ∀a b c: T, a - b < c → a < c + b
+lt_mul_cancel: ∀a b c: T, b > 0 → b * a < b * c → a < c
+
+theorem OrderedField.lt_implies_le {T: Type} [Field T] [OrderedField T] (a b: T) (h1: a < b) : a <= b := (OrderedField.le_def a b).mpr (Or.inr h1)
+
+theorem OrderedField.le_lt_trans {T: Type} [Field T] [OrderedField T] (a b c: T) (h1: a <= b) (h2: b < c): a < c := by
+  cases (OrderedField.le_def a b).mp h1 with
+  | inl h3 => rw [h3]; exact h2
+  | inr h3 => exact OrderedField.lt_lt_trans a b c h3 h2
+
+theorem OrderedField.lt_le_trans {T: Type} [Field T] [OrderedField T] (a b c: T) (h1: a < b) (h2: b <= c): a < c := by
+  cases (OrderedField.le_def b c).mp h2 with
+  | inl h3 => rw [←h3]; exact h1
+  | inr h3 => exact OrderedField.lt_lt_trans a b c h1 h3
+
+theorem OrderedField.ge_zero_one {T: Type} [Field T] [OrderedField T] : 0 <= (1: T) := (OrderedField.le_def 0 1).mpr (Or.inr OrderedField.gt_zero_one)
+
+theorem OrderedField.ge_zero_two {T: Type} [Field T] [OrderedField T] : 0 <= (1 + 1: T) := by
+  sorry
+  -- rw [OrderedField.le_def₂]
+  -- exists (1 + 1)
+
+def Real: Type := sorry
+
+-- variable {Real: Type} [Field Real] [OrderedField Real]
+-- variable [Field Real] [OrderedField Real]
+
+instance : Field Real := sorry
+instance : OrderedField Real := sorry
+
+-- TODO constraints
+class FieldWithAbsConjugate (T: Type) extends Field T where
+  abs: T → Real
+  conigate: T → T
+
+example : (0: Real) ≠ (1: Real) := Field.different
+
+-- class ConjugateField (T: Type) extends Field T
+-- conjugate: T → T

Mathematics/Algebra/Group.lean

@@ -1,16 +1,14 @@
-import Mathematics.Structures.Relation
-
 class Inverse (T : Type) where
-  inverse' : T → T
+  inverseOfElement : T → T
 
-postfix:max "⁻¹" => Inverse.inverse'
+postfix:max "⁻¹" => Inverse.inverseOfElement
 
-class Group (T: Type) extends Mul T, Inverse T, OfNat T 1 :=
+class Group (T: Type) extends Mul T, Inverse T, OfNat T 1 where
 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
 
-class AbelianGroup (T: Type) extends Group T :=
+class AbelianGroup (T: Type) extends Group T where
 commutativity : ∀ a b : T, a * b = b * a
 
 namespace groups
@@ -74,73 +72,3 @@ theorem one.unique_left (e: T) : ∀ x: T, e * x = x → e = 1 := by
   exact (multiply.right_cancel_iff x e 1).1 h1
 
 end groups
-
-def conjugation { T: Type } [Group T] (c: T) := fun (x: T) => c * x * c⁻¹
-
-namespace random
-
-variable {T: Type} [Group T]
-
-def are_conjugate (x x': T) : Prop := ∃g, x' = conjugation g x
-
-open groups in
-instance : Relation T are_conjugate := {
-  symmetric := by
-    intro a b h1
-    let ⟨g, h2⟩ := h1
-    apply Exists.intro g⁻¹
-    unfold conjugation at *
-    rw [
-      h2,
-      inv.double,
-      multiply.associative,
-      ←multiply.associative _ g⁻¹ g,
-      (Group.inverse g).1,
-      multiply.one,
-      multiply.associative,
-      (Group.inverse g).1,
-      one.multiply
-    ]
-  reflexivity := by
-    intro a
-    apply Exists.intro 1
-    unfold conjugation at *
-    rw [one.multiply, one.inverse, multiply.one]
-  transitivity := by
-    intro a b c h1
-    let ⟨⟨g1, h2⟩, ⟨g2, h3⟩⟩ := h1
-    apply Exists.intro (g2 * g1)
-    unfold conjugation at *
-    rw [h3, h2, inv.multiply, multiply.associative, multiply.associative, multiply.associative]
-}
-
-end random
-
-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] : 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
-theorem mul_inv (A B: Type) [Group A] [Group B] (a: Group.Product A B) : a⁻¹ = (a.1⁻¹, a.2⁻¹) := rfl
-theorem one_left (A B: Type) [Group A] [Group B] : (1: Group.Product A B) = (1, 1) := rfl
-
-instance (A B: Type) {ga: Group A} {gb: Group B} : Group (Group.Product A B) := {
-  associativity := by
-    intro a b c
-    rw [mul_eq, mul_eq, ga.associativity, gb.associativity]
-    rfl
-  inverse := by
-    intro a
-    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
-    rw [mul_eq, one_left, (ga.identity _).1, (gb.identity _).1, mul_eq, (ga.identity _).2, (gb.identity _).2]
-    exact ⟨rfl, rfl⟩
-}
-
-end product

Mathematics/Algebra/Group/Conjugation.lean

@@ -0,0 +1,39 @@
+import Mathematics.Algebra.Group
+import Mathematics.Relation.Relation
+
+def conjugation { T: Type } [Group T] (c: T) := fun (x: T) => c * x * c⁻¹
+
+variable {T: Type} [Group T]
+
+def are_conjugate (x x': T) : Prop := ∃g, x' = conjugation g x
+
+open groups in
+instance : Relation T are_conjugate := {
+  symmetric := by
+    intro a b h1
+    let ⟨g, h2⟩ := h1
+    exists g⁻¹
+    unfold conjugation at *
+    rw [
+      h2,
+      inv.double,
+      multiply.associative,
+      ←multiply.associative _ g⁻¹ g,
+      (Group.inverse g).1,
+      multiply.one,
+      multiply.associative,
+      (Group.inverse g).1,
+      one.multiply
+    ]
+  reflexivity := by
+    intro a
+    exists 1
+    unfold conjugation at *
+    rw [one.multiply, one.inverse, multiply.one]
+  transitivity := by
+    intro a b c h1
+    let ⟨⟨g1, h2⟩, ⟨g2, h3⟩⟩ := h1
+    exists (g2 * g1)
+    unfold conjugation at *
+    rw [h3, h2, inv.multiply, multiply.associative, multiply.associative, multiply.associative]
+}

Mathematics/Algebra/Group/Product.lean

@@ -0,0 +1,26 @@
+import Mathematics.Algebra.Group
+
+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] : 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
+theorem mul_inv (A B: Type) [Group A] [Group B] (a: Group.Product A B) : a⁻¹ = (a.1⁻¹, a.2⁻¹) := rfl
+theorem one_left (A B: Type) [Group A] [Group B] : (1: Group.Product A B) = (1, 1) := rfl
+
+instance (A B: Type) {ga: Group A} {gb: Group B} : Group (Group.Product A B) := {
+  associativity := by
+    intro a b c
+    rw [mul_eq, mul_eq, ga.associativity, gb.associativity]
+    rfl
+  inverse := by
+    intro a
+    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
+    rw [mul_eq, one_left, (ga.identity _).1, (gb.identity _).1, mul_eq, (ga.identity _).2, (gb.identity _).2]
+    exact ⟨rfl, rfl⟩
+}

Mathematics/Algebra/Group/Subgroup.lean

@@ -0,0 +1,22 @@
+import Mathematics.Algebra.Group
+import Mathematics.Structures.Set
+
+class Subgroup (T: Type) [Group T] (H: Set T) where
+closure: ∀a ∈ H, ∀b ∈ H, (a * b) ∈ H
+
+-- TODO contains 0 etc
+
+variable {T: Type} [Group T]
+
+-- TODO name wrong
+def Subgroup.unit : Subgroup T (Set.universal T) where
+closure := by
+  intro a _ b _
+  trivial
+
+-- TODO name wrong
+def Subgroup.identity : Subgroup T (Set.singleton 1) where
+closure := by
+  intro a h1 b h2
+  rw [h1, h2, groups.one.multiply]
+  rfl

Mathematics/Algebra/PartialOrder.lean

@@ -0,0 +1,23 @@
+import Mathematics.Algebra.Field
+
+class VectorSpace (X F: Type) [Field F] extends Zero X, OfNat X 1, Add X, Sub X, HMul F X X, Neg X where
+zero_mul: ∀x: X, (0: F) * x = (0: X)
+one_mul: ∀x: X, (1: F) * x = x
+add_zero: ∀x: X, x + (0: X) = x
+sub_eq: ∀x y: X, x = y ↔ x - y = 0
+sub_def: ∀x y: X, x - y = x + ((-1: F) * y)
+neg_def: ∀x: X, -x = (-1: F) * x
+mul_associative: ∀x: X, ∀a b: F, a * (b * x) = (a * b) * x
+add_commutative: ∀x y: X, x + y = y + x
+distributive: ∀b c: X, ∀a: F, a * b + a * c = a * (b + c)
+
+instance {T: Type} [f: Field T] : VectorSpace T T where
+zero_mul := f.zero_mul
+one_mul := f.one_mul
+add_zero := f.add_zero
+sub_eq := f.sub_eq
+sub_def := f.sub_def
+neg_def := f.neg_def
+add_commutative := f.add_commutative
+mul_associative := fun a b c => f.mul_associative b c a
+distributive := fun a b c => f.distributive' c a b

Mathematics/Algebra/VectorSpace.lean

@@ -0,0 +1,7 @@
+import Mathematics.Algebra.Field
+
+class Abs {F: Type} [Field F] [OrderedField F] (abs: F → Real) where
+positive: ∀a: F, abs a >= 0
+equal: ∀a: F, abs a = 0 ↔ a = 0
+multiplicative: ∀a b: F, abs (a * b) = (abs a) * (abs b)
+negative: ∀a: F, abs (-a) = abs a