From 2f150dce1fc91702cea875a6b0f500aff687becc Mon Sep 17 00:00:00 2001 From: Clive Newstead Date: Thu, 4 Feb 2016 15:31:41 -0500 Subject: [PATCH] Playing with groups --- homotopy/clive.hlean | 37 +++++++++++++++++++++++++++++++++++-- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/homotopy/clive.hlean b/homotopy/clive.hlean index 1c01358..a602661 100644 --- a/homotopy/clive.hlean +++ b/homotopy/clive.hlean @@ -1,9 +1,42 @@ -import types.trunc types.arrow_2 types.fiber homotopy.susp homotopy.circle +/----- +This is Clive's file for playing around with (h)Lean/Git/Emacs +------/ + +import types.trunc types.arrow_2 types.fiber homotopy.circle + +open eq is_trunc is_equiv nat equiv trunc function circle + -open eq is_trunc is_equiv nat equiv trunc function fiber circle namespace clive +/-- Very easy goal: prove (loop⁻¹)⁻¹ = loop : base = base --/ +theorem symm_symm_loop_eq_loop : (loop⁻¹)⁻¹ = loop := +eq.rec_on loop idp + +/-- Another easy goal: define a group and prove that the left inverse law follows form the right inverse law --/ +structure group (X : Type) := +gpstr :: (unit : X) + (mult : X → X → X) + (inv : X → X) + (assoc_law : Π(a b c : X), mult (mult a b) c = mult a (mult b c)) + (inv_law : Π(a : X), mult a (inv a) = unit) + (unit_law : Π(a : X), mult a unit = a) + +constants (X : Type) (G : group X) +open group + +theorem group_cancel_right : Π(X : Type), Π(G : group X), Π(a b c : X), (mult G a c = mult G b c) → a = b := sorry + +theorem inv_mul_left_eq_unit : Π(X : Type), Π(G : group X), Π(a : X), mult G (inv G a) a = unit G := + take (X : Type) (G : group X) (a : X), + have q : mult G (mult G (inv G a) a) (inv G a) = mult G (unit G) (inv G a), from + calc + mult G (mult G (inv G a) a) (inv G a) = mult G (inv G a) (mult G a (inv G a)) : assoc_law + ... = mult G (inv G a) (unit G) : sorry + ... = inv G a : unit_law + ... = mult G (unit G) (inv G a) : sorry, + group_cancel_right X G (mult G (inv G a) a) (unit G) (inv G a) q end clive