From d70334d1009847894062e1828c8969bba892e233 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 17 Sep 2016 18:37:49 -0400 Subject: [PATCH] feat(hott/algebra/bundled): add a parameter to Group to specify whether it's an additive or multiplicative group --- hott/algebra/bundled.hlean | 92 +++++++++++----- .../algebra/category/functor/attributes.hlean | 3 + .../category/functor/equivalence.hlean | 3 - hott/algebra/category/groupoid.hlean | 2 +- hott/algebra/group.hlean | 27 +++++ hott/algebra/group_theory.hlean | 63 ++++++----- hott/algebra/homotopy_group.hlean | 10 +- hott/algebra/hott.hlean | 10 +- hott/homotopy/EM.hlean | 102 ++++++++++-------- hott/homotopy/LES_of_homotopy_groups.hlean | 12 +-- hott/types/int/hott.hlean | 9 +- library/algebra/group.lean | 27 +++++ 12 files changed, 236 insertions(+), 124 deletions(-) diff --git a/hott/algebra/bundled.hlean b/hott/algebra/bundled.hlean index 120262135..9467e0634 100644 --- a/hott/algebra/bundled.hlean +++ b/hott/algebra/bundled.hlean @@ -5,7 +5,7 @@ Authors: Jeremy Avigad Bundled structures -/ -import algebra.group +import algebra.group homotopy.interval open algebra namespace algebra @@ -33,51 +33,85 @@ structure CommMonoid := attribute CommMonoid.carrier [coercion] attribute CommMonoid.struct [instance] -structure Group := +abbreviation signature := interval +structure Group (i : signature) := (carrier : Type) (struct : group carrier) +definition MulGroup [reducible] : Type := Group interval.zero +definition AddGroup [reducible] : Type := Group interval.one attribute Group.carrier [coercion] -attribute Group.struct [instance] -structure CommGroup := +definition MulGroup.mk [constructor] (G : Type) (H : group G) : MulGroup := Group.mk _ G _ +definition AddGroup.mk [constructor] (G : Type) (H : add_group G) : AddGroup := +Group.mk _ G add_group.to_group + +section +local attribute group.to_add_group Group.struct [instance] + +definition MulGroup.struct (G : MulGroup) : group G := _ +definition AddGroup.struct (G : AddGroup) : add_group G := _ +end + +attribute MulGroup.struct AddGroup.struct [instance] [priority 2000] +attribute Group.struct [instance] [priority 800] + +structure CommGroup (i : signature) := (carrier : Type) (struct : comm_group carrier) +definition MulCommGroup [reducible] : Type := CommGroup interval.zero +definition AddCommGroup [reducible] : Type := CommGroup interval.one attribute CommGroup.carrier [coercion] -attribute CommGroup.struct [instance] -structure AddSemigroup := -(carrier : Type) (struct : add_semigroup carrier) +definition MulCommGroup.mk [constructor] (G : Type) (H : comm_group G) : MulCommGroup := +CommGroup.mk _ G _ +definition AddCommGroup.mk [constructor] (G : Type) (H : add_comm_group G) : AddCommGroup := +CommGroup.mk _ G add_comm_group.to_comm_group -attribute AddSemigroup.carrier [coercion] -attribute AddSemigroup.struct [instance] +section +local attribute comm_group.to_add_comm_group CommGroup.struct [instance] -structure AddCommSemigroup := -(carrier : Type) (struct : add_comm_semigroup carrier) +definition MulCommGroup.struct (G : MulCommGroup) : comm_group G := _ +definition AddCommGroup.struct (G : AddCommGroup) : add_comm_group G := _ +end -attribute AddCommSemigroup.carrier [coercion] -attribute AddCommSemigroup.struct [instance] +attribute MulCommGroup.struct AddCommGroup.struct [instance] [priority 2000] +attribute CommGroup.struct [instance] [priority 800] -structure AddMonoid := -(carrier : Type) (struct : add_monoid carrier) -attribute AddMonoid.carrier [coercion] -attribute AddMonoid.struct [instance] -structure AddCommMonoid := -(carrier : Type) (struct : add_comm_monoid carrier) +-- structure AddSemigroup := +-- (carrier : Type) (struct : add_semigroup carrier) -attribute AddCommMonoid.carrier [coercion] -attribute AddCommMonoid.struct [instance] +-- attribute AddSemigroup.carrier [coercion] +-- attribute AddSemigroup.struct [instance] -structure AddGroup := -(carrier : Type) (struct : add_group carrier) +-- structure AddCommSemigroup := +-- (carrier : Type) (struct : add_comm_semigroup carrier) -attribute AddGroup.carrier [coercion] -attribute AddGroup.struct [instance] +-- attribute AddCommSemigroup.carrier [coercion] +-- attribute AddCommSemigroup.struct [instance] -structure AddCommGroup := -(carrier : Type) (struct : add_comm_group carrier) +-- structure AddMonoid := +-- (carrier : Type) (struct : add_monoid carrier) -attribute AddCommGroup.carrier [coercion] -attribute AddCommGroup.struct [instance] +-- attribute AddMonoid.carrier [coercion] +-- attribute AddMonoid.struct [instance] + +-- structure AddCommMonoid := +-- (carrier : Type) (struct : add_comm_monoid carrier) + +-- attribute AddCommMonoid.carrier [coercion] +-- attribute AddCommMonoid.struct [instance] + +-- structure AddGroup := +-- (carrier : Type) (struct : add_group carrier) + +-- attribute AddGroup.carrier [coercion] +-- attribute AddGroup.struct [instance] + +-- structure AddCommGroup := +-- (carrier : Type) (struct : add_comm_group carrier) + +-- attribute AddCommGroup.carrier [coercion] +-- attribute AddCommGroup.struct [instance] end algebra diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean index 5f25a64c8..b42cb9f08 100644 --- a/hott/algebra/category/functor/attributes.hlean +++ b/hott/algebra/category/functor/attributes.hlean @@ -21,6 +21,9 @@ namespace category definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d + definition is_weak_equivalence [class] (F : C ⇒ D) := + fully_faithful F × essentially_surjective F + definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') := !H diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index e10a2a5f7..f0c02fe13 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -18,9 +18,6 @@ namespace category (is_iso_unit : is_iso η) (is_iso_counit : is_iso ε) - definition is_weak_equivalence [class] (F : C ⇒ D) := - fully_faithful F × essentially_surjective F - abbreviation inverse := @is_equivalence.G postfix ⁻¹ := inverse --a second notation for the inverse, which is not overloaded (there is no unicode superscript F) diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index e7b0a7421..a1e14f402 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -79,7 +79,7 @@ namespace category definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C := Groupoid.rec (λob c, idp) C - definition Groupoid_of_Group [constructor] (G : Group) : Groupoid := + definition Groupoid_of_Group [constructor] {i : signature} (G : Group i) : Groupoid := Groupoid.mk unit (groupoid_of_group G) end category diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index f8d34e8b9..c51da8850 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -137,6 +137,22 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : c mul_comm := add_comm_monoid.add_comm ⦄ +definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A := +⦃ add_monoid, + add := monoid.mul, + add_assoc := monoid.mul_assoc, + zero := monoid.one A, + add_zero := monoid.mul_one, + zero_add := monoid.one_mul, + is_set_carrier := _ +⦄ + +definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A := +⦃ add_comm_monoid, + monoid.to_add_monoid, + add_comm := comm_monoid.mul_comm +⦄ + section add_comm_monoid variables [s : add_comm_monoid A] include s @@ -337,6 +353,9 @@ definition add_group.to_group {A : Type} [s : add_group A] : group A := ⦃ group, add_monoid.to_monoid, mul_left_inv := add_group.add_left_inv ⦄ +definition group.to_add_group {A : Type} [s : group A] : add_group A := +⦃ add_group, monoid.to_add_monoid, + add_left_inv := group.mul_left_inv ⦄ section add_group @@ -528,6 +547,14 @@ end add_group structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A +definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A := +⦃ comm_group, add_group.to_group, + mul_comm := add_comm_group.add_comm ⦄ + +definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A := +⦃ add_comm_group, group.to_add_group, + add_comm := comm_group.mul_comm ⦄ + section add_comm_group variable [s : add_comm_group A] include s diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 211d36266..c6483a7b1 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -15,19 +15,22 @@ open eq algebra pointed function is_trunc pi category equiv is_equiv set_option class.force_new true namespace group + definition pointed_Group [instance] [constructor] {i : signature} (G : Group i) : pointed G := + pointed.mk 1 + definition pType_of_Group [constructor] [reducible] {i : signature} (G : Group i) : Type* := + pointed.MK G 1 + definition Set_of_Group [constructor] {i : signature} (G : Group i) : Set := trunctype.mk G _ - definition pointed_Group [instance] [constructor] (G : Group) : pointed G := pointed.mk 1 - definition pType_of_Group [constructor] [reducible] (G : Group) : Type* := pointed.MK G 1 - definition Set_of_Group [constructor] (G : Group) : Set := trunctype.mk G _ + definition Group_of_CommGroup [coercion] [constructor] {i : signature} (G : CommGroup i) : + Group i := + Group.mk i G _ - definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := - Group.mk G _ - - definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup) + definition comm_group_Group_of_CommGroup [instance] [constructor] {i : signature} (G : CommGroup i) : comm_group (Group_of_CommGroup G) := begin esimp, exact _ end - definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) := + definition group_pType_of_Group [instance] {i : signature} (G : Group i) : + group (pType_of_Group G) := Group.struct G /- group homomorphisms -/ @@ -74,18 +77,20 @@ namespace group end - structure homomorphism (G₁ G₂ : Group) : Type := + structure homomorphism {i j : signature} (G₁ : Group i) (G₂ : Group j) : Type := (φ : G₁ → G₂) (p : is_homomorphism φ) infix ` →g `:55 := homomorphism - definition group_fun [unfold 3] [coercion] := @homomorphism.φ - definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂) + definition group_fun [unfold 5] [coercion] := @homomorphism.φ + definition homomorphism.struct [instance] [priority 2000] {i j : signature} + {G₁ : Group i} {G₂ : Group j} (φ : G₁ →g G₂) : is_homomorphism φ := homomorphism.p φ - variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂) + variables {i j k l : signature} {G : Group i} {G₁ : Group j} {G₂ : Group k} {G₃ : Group l} + {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂) definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h := respect_mul φ g h @@ -99,7 +104,8 @@ namespace group definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ := is_embedding_homomorphism φ @H - definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) := + variables (G₁ G₂) + definition is_set_homomorphism [instance] : is_set (G₁ →g G₂) := begin have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂, begin @@ -112,6 +118,7 @@ namespace group apply is_trunc_equiv_closed_rev, exact H end + variables {G₁ G₂} definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ := pmap.mk φ begin esimp, exact respect_one φ end @@ -126,13 +133,15 @@ namespace group definition homomorphism_compose [constructor] [trans] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ := homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _) - definition homomorphism_id [constructor] [refl] (G : Group) : G →g G := + variable (G) + definition homomorphism_id [constructor] [refl] : G →g G := homomorphism.mk (@id G) (is_homomorphism_id G) + variable {G} infixr ` ∘g `:75 := homomorphism_compose notation 1 := homomorphism_id _ - structure isomorphism (A B : Group) := + structure isomorphism {i j : signature} (A : Group i) (B : Group j) := (to_hom : A →g B) (is_equiv_to_hom : is_equiv to_hom) @@ -151,10 +160,10 @@ namespace group (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ := isomorphism.mk (homomorphism.mk φ p) !to_is_equiv - definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ := + definition eq_of_isomorphism {G₁ G₂ : Group i} (φ : G₁ ≃g G₂) : G₁ = G₂ := Group_eq (equiv_of_isomorphism φ) (respect_mul φ) - definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ := + definition isomorphism_of_eq {G₁ G₂ : Group i} (φ : G₁ = G₂) : G₁ ≃g G₂ := isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ)) begin intros, induction φ, reflexivity end @@ -165,8 +174,10 @@ namespace group rewrite [respect_mul φ, +right_inv φ] end end - definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G := + variable (G) + definition isomorphism.refl [refl] [constructor] : G ≃g G := isomorphism.mk 1 !is_equiv_id + variable {G} definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ := isomorphism.mk (to_ginv φ) !is_equiv_inv @@ -175,11 +186,11 @@ namespace group isomorphism.mk (ψ ∘g φ) !is_equiv_compose definition isomorphism.eq_trans [trans] [constructor] - {G₁ G₂ G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := + {G₁ G₂ : Group i} {G₃ : Group j} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := proof isomorphism.trans (isomorphism_of_eq φ) ψ qed definition isomorphism.trans_eq [trans] [constructor] - {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ := + {G₁ : Group i} {G₂ G₃ : Group j} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ := isomorphism.trans φ (isomorphism_of_eq ψ) postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm @@ -199,10 +210,10 @@ namespace group /- category of groups -/ - definition precategory_group [constructor] : precategory Group := + definition precategory_group [constructor] (i : signature) : precategory (Group i) := precategory.mk homomorphism - @homomorphism_compose - @homomorphism_id + (@homomorphism_compose _ _ _) + (@homomorphism_id _) (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp)) (λG₁ G₂ φ, homomorphism_eq (λg, idp)) (λG₁ G₂ φ, homomorphism_eq (λg, idp)) @@ -260,15 +271,17 @@ namespace group end - definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G ≃g G0 := + variable (G) + definition trivial_group_of_is_contr [H : is_contr G] : G ≃g G0 := begin fapply isomorphism_of_equiv, { apply equiv_unit_of_is_contr}, { intros, reflexivity} end - definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 := + definition trivial_group_of_is_contr' (G : MulGroup) [H : is_contr G] : G = G0 := eq_of_isomorphism (trivial_group_of_is_contr G) + variable {G} /- A group where the point in the pointed type corresponds with 1 in the group. diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 54ed467f6..450e63a4f 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -36,13 +36,13 @@ namespace eq local attribute comm_group_homotopy_group [instance] - definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : Group := - Group.mk (π[succ n] A) _ + definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulGroup := + MulGroup.mk (π[succ n] A) _ - definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup := - CommGroup.mk (π[succ (succ n)] A) _ + definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulCommGroup := + MulCommGroup.mk (π[succ (succ n)] A) _ - definition fundamental_group [constructor] (A : Type*) : Group := + definition fundamental_group [constructor] (A : Type*) : MulGroup := ghomotopy_group zero A notation `πg[`:95 n:0 ` +1] `:0 A:95 := ghomotopy_group n A diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index c5e8570dc..2e0a60659 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -15,8 +15,8 @@ namespace algebra definition trivial_group [constructor] : group unit := group.mk (λx y, star) _ (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) - definition Trivial_group [constructor] : Group := - Group.mk _ trivial_group + definition Trivial_group [constructor] : MulGroup := + MulGroup.mk _ trivial_group abbreviation G0 := Trivial_group @@ -65,15 +65,15 @@ namespace algebra apply pathover_idp_of_eq, exact group_eq (resp_mul) end - definition Group_eq_of_eq {G H : Group} (p : carrier G = carrier H) + definition Group_eq_of_eq {i : signature} {G H : Group i} (p : carrier G = carrier H) (resp_mul : Π(g h : G), cast p (g * h) = cast p g * cast p h) : G = H := begin cases G with Gc G, cases H with Hc H, - apply (apd011 mk p), + apply (apd011 (Group.mk i) p), exact group_pathover resp_mul end - definition Group_eq {G H : Group} (f : carrier G ≃ carrier H) + definition Group_eq {i : signature} {G H : Group i} (f : carrier G ≃ carrier H) (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H := Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index c5dd63d55..4dadf2dfc 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -14,10 +14,10 @@ open algebra pointed nat eq category group algebra is_trunc iso pointed unit tru namespace EM open groupoid_quotient - variable {G : Group} - definition EM1 (G : Group) : Type := + variables {i : signature} {G : Group i} + definition EM1 {i : signature} (G : Group i) : Type := groupoid_quotient (Groupoid_of_Group G) - definition pEM1 [constructor] (G : Group) : Type* := + definition pEM1 [constructor] {i : signature} (G : Group i) : Type* := pointed.MK (EM1 G) (elt star) definition base : EM1 G := elt star @@ -95,18 +95,19 @@ namespace EM end EM attribute EM.base [constructor] -attribute EM.rec EM.elim [unfold 7] [recursor 7] -attribute EM.rec_on EM.elim_on [unfold 4] -attribute EM.set_rec EM.set_elim [unfold 6] -attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5] +attribute EM.rec EM.elim [unfold 8] [recursor 8] +attribute EM.rec_on EM.elim_on [unfold 5] +attribute EM.set_rec EM.set_elim [unfold 7] +attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 6] namespace EM open groupoid_quotient - definition base_eq_base_equiv [constructor] (G : Group) : (base = base :> pEM1 G) ≃ G := + variables {i : signature} (G : Group i) + definition base_eq_base_equiv [constructor] : (base = base :> pEM1 G) ≃ G := !elt_eq_elt_equiv - definition fundamental_group_pEM1 (G : Group) : π₁ (pEM1 G) ≃g G := + definition fundamental_group_pEM1 : π₁ (pEM1 G) ≃g G := begin fapply isomorphism_of_equiv, { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G}, @@ -114,19 +115,20 @@ namespace EM exact encode_con p q} end - proposition is_trunc_pEM1 [instance] (G : Group) : is_trunc 1 (pEM1 G) := + proposition is_trunc_pEM1 [instance] : is_trunc 1 (pEM1 G) := !is_trunc_groupoid_quotient - proposition is_trunc_EM1 [instance] (G : Group) : is_trunc 1 (EM1 G) := + proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) := !is_trunc_groupoid_quotient - proposition is_conn_EM1 [instance] (G : Group) : is_conn 0 (EM1 G) := + proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) := by apply @is_conn_groupoid_quotient; esimp; exact _ - proposition is_conn_pEM1 [instance] (G : Group) : is_conn 0 (pEM1 G) := + proposition is_conn_pEM1 [instance] : is_conn 0 (pEM1 G) := is_conn_EM1 G + variable {G} - definition EM1_map [unfold 7] {G : Group} {X : Type*} (e : Ω X ≃ G) + definition EM1_map [unfold 7] {X : Type*} (e : Ω X ≃ G) (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X := begin intro x, induction x using EM.elim, @@ -140,9 +142,9 @@ end EM open hopf susp namespace EM -- The K(G,n+1): - variables (G : CommGroup) (n : ℕ) + variables {i : signature} {G : CommGroup i} (n : ℕ) - definition EM1_mul [unfold 2 3] {G : CommGroup} (x x' : EM1 G) : EM1 G := + definition EM1_mul [unfold 2 3] (x x' : EM1 G) : EM1 G := begin induction x, { exact x'}, @@ -154,14 +156,15 @@ namespace EM { refine EM.prop_rec _ x', apply resp_mul} end - definition EM1_mul_one (G : CommGroup) (x : EM1 G) : EM1_mul x base = x := + variable (G) + definition EM1_mul_one (x : EM1 G) : EM1_mul x base = x := begin induction x using EM.set_rec, { reflexivity}, { apply eq_pathover_id_right, apply hdeg_square, refine EM.elim_pth _ g} end - definition h_space_EM1 [constructor] [instance] (G : CommGroup) : h_space (pEM1 G) := + definition h_space_EM1 [constructor] [instance] : h_space (pEM1 G) := begin fapply h_space.mk, { exact EM1_mul}, @@ -171,22 +174,22 @@ namespace EM end /- K(G, n+1) -/ - definition EMadd1 (G : CommGroup) (n : ℕ) : Type* := + definition EMadd1 (n : ℕ) : Type* := ptrunc (n+1) (iterate_psusp n (pEM1 G)) - definition loop_EM2 (G : CommGroup) : Ω[1] (EMadd1 G 1) ≃* pEM1 G := + definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* pEM1 G := begin apply hopf.delooping, reflexivity end - definition homotopy_group_EM2 (G : CommGroup) : πg[1+1] (EMadd1 G 1) ≃g G := + definition homotopy_group_EM2 : πg[1+1] (EMadd1 G 1) ≃g G := begin refine ghomotopy_group_succ_in _ 0 ⬝g _, refine homotopy_group_isomorphism_of_pequiv 0 (loop_EM2 G) ⬝g _, apply fundamental_group_pEM1 end - definition homotopy_group_EMadd1 (G : CommGroup) (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := + definition homotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G := begin cases n with n, { refine homotopy_group_isomorphism_of_pequiv 0 _ ⬝g fundamental_group_pEM1 G, @@ -201,42 +204,43 @@ namespace EM section local attribute EMadd1 [reducible] - definition is_conn_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _ + definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := _ - definition is_trunc_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _ + definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := + _ end /- K(G, n) -/ - definition EM (G : CommGroup) : ℕ → Type* + definition EM {i : signature} (G : CommGroup i) : ℕ → Type* | 0 := pType_of_Group G | (k+1) := EMadd1 G k namespace ops - abbreviation K := EM + abbreviation K := @EM end ops open ops - definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G := + definition phomotopy_group_EM (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G := begin cases n with n, { rexact ptrunc_pequiv 0 (pType_of_Group G) _}, { apply pequiv_of_isomorphism (homotopy_group_EMadd1 G n)} end - definition ghomotopy_group_EM (G : CommGroup) (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := + definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G := homotopy_group_EMadd1 G n - definition is_conn_EM [instance] (G : CommGroup) (n : ℕ) : is_conn (n.-1) (EM G n) := + definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) := begin cases n with n, { apply is_conn_minus_one, apply tr, unfold [EM], exact 1}, { apply is_conn_EMadd1} end - definition is_conn_EM_succ [instance] (G : CommGroup) (n : ℕ) : is_conn n (EM G (succ n)) := + definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) := is_conn_EM G (succ n) - definition is_trunc_EM [instance] (G : CommGroup) (n : ℕ) : is_trunc n (EM G n) := + definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) := begin cases n with n, { unfold [EM], apply semigroup.is_set_carrier}, @@ -244,26 +248,29 @@ namespace EM end /- Uniqueness of K(G, 1) -/ - definition pEM1_pmap [constructor] {G : Group} {X : Type*} (e : Ω X ≃ G) - (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G →* X := + variable {H : Group i} + definition pEM1_pmap [constructor] {X : Type*} (e : Ω X ≃ H) + (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 H →* X := begin apply pmap.mk (EM1_map e r), reflexivity, end - definition loop_pEM1 [constructor] (G : Group) : Ω (pEM1 G) ≃* pType_of_Group G := - pequiv_of_equiv (base_eq_base_equiv G) idp + variable (H) + definition loop_pEM1 [constructor] : Ω (pEM1 H) ≃* pType_of_Group H := + pequiv_of_equiv (base_eq_base_equiv H) idp - definition loop_pEM1_pmap {G : Group} {X : Type*} (e : Ω X ≃ G) + variable {H} + definition loop_pEM1_pmap {X : Type*} (e : Ω X ≃ H) (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : - Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv G := + Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv H := begin - apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv G), + apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv H), intro g, exact !idp_con ⬝ !elim_pth end open trunc_index - definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G) + definition pEM1_pequiv'.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : Ω X ≃ G) (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X := begin apply pequiv_of_pmap (pEM1_pmap e r), @@ -280,7 +287,7 @@ namespace EM do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}} end - definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G) + definition pEM1_pequiv.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X := begin apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), @@ -290,7 +297,7 @@ namespace EM definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X := pEM1_pequiv !isomorphism.refl - definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) + definition EM_pequiv_1.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X := begin refine _ ⬝e* pEM1_pequiv e, @@ -298,11 +305,12 @@ namespace EM apply is_trunc_pEM1 end - definition EMadd1_pequiv_pEM1 (G : CommGroup) : EMadd1 G 0 ≃* pEM1 G := + variable (G) + definition EMadd1_pequiv_pEM1 : EMadd1 G 0 ≃* pEM1 G := begin apply ptrunc_pequiv, apply is_trunc_pEM1 end - definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) - [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X := + definition EM1add1_pequiv_0.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} + (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X := EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y) @@ -314,7 +322,8 @@ namespace EM !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle /- loops of EM-spaces -/ - definition loop_EMadd1 {G : CommGroup} (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n := + variable {G} + definition loop_EMadd1 (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n := begin cases n with n, { symmetry, apply EM1add1_pequiv_0, rexact homotopy_group_EMadd1 G 1, @@ -326,7 +335,8 @@ namespace EM symmetry, refine freudenthal_pequiv _ this, } end - definition loop_EM (G : CommGroup) (n : ℕ) : Ω (K G (succ n)) ≃* K G n := + variable (G) + definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n := begin cases n with n, { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_pEM1 G), diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 19e7e6bfb..b99f06ccc 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -729,13 +729,13 @@ namespace chain_complex | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := - Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) - (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) + definition Group_LES_of_homotopy_groups (x : +3ℕ) : MulGroup.{u} := + MulGroup.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) + (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) - definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} := - CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) - (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) + definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : MulCommGroup.{u} := + MulCommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) + (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ), Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 65bd2b566..f9bbc3079 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -14,13 +14,14 @@ namespace int section open algebra - definition group_integers [constructor] : Group := - Group.mk ℤ (group_of_add_group _) + definition group_integers [constructor] : AddGroup := + AddGroup.mk ℤ _ notation `gℤ` := group_integers - definition CommGroup_int [constructor] : CommGroup := - CommGroup.mk ℤ ⦃comm_group, group_of_add_group ℤ, mul_comm := add.comm⦄ + definition CommGroup_int [constructor] : AddCommGroup := + AddCommGroup.mk ℤ _ + notation `agℤ` := CommGroup_int end diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 26ec5d090..5f7052cbe 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -127,6 +127,21 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [add_comm_monoid A] : comm_ mul_comm := add_comm_monoid.add_comm ⦄ +definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A := +⦃ add_monoid, + add := monoid.mul, + add_assoc := monoid.mul_assoc, + zero := monoid.one A, + add_zero := monoid.mul_one, + zero_add := monoid.one_mul +⦄ + +definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A := +⦃ add_comm_monoid, + monoid.to_add_monoid, + add_comm := comm_monoid.mul_comm +⦄ + section add_comm_monoid variables [add_comm_monoid A] @@ -314,6 +329,9 @@ definition add_group.to_group {A : Type} [add_group A] : group A := ⦃ group, add_monoid.to_monoid, mul_left_inv := add_group.add_left_inv ⦄ +definition group.to_add_group {A : Type} [s : group A] : add_group A := +⦃ add_group, monoid.to_add_monoid, + add_left_inv := group.mul_left_inv ⦄ section add_group variables [s : add_group A] @@ -541,6 +559,15 @@ end add_group structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A +definition add_comm_group.to_comm_group (A : Type) [s : add_comm_group A] : comm_group A := +⦃ comm_group, add_group.to_group, + mul_comm := add_comm_group.add_comm ⦄ + +definition comm_group.to_add_comm_group (A : Type) [s : comm_group A] : add_comm_group A := +⦃ add_comm_group, group.to_add_group, + add_comm := comm_group.mul_comm ⦄ + + section add_comm_group variable [s : add_comm_group A] include s