From 1135d80266af764b3f1af7aea2e7550509d5a039 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 20 Apr 2016 11:51:56 -0400 Subject: [PATCH] feat(hott): use group isomorphisms instead of equality between groups --- hott/algebra/group_theory.hlean | 260 ++++++++++++++++++++++++++++++ hott/algebra/homotopy_group.hlean | 68 ++++---- hott/algebra/hott.hlean | 7 - hott/homotopy/circle.hlean | 12 +- 4 files changed, 303 insertions(+), 44 deletions(-) create mode 100644 hott/algebra/group_theory.hlean diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean new file mode 100644 index 000000000..cd742a1de --- /dev/null +++ b/hott/algebra/group_theory.hlean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +Basic group theory + +This file will be rewritten in the future, when we develop are more systematic notation for +describing homomorphisms +-/ + +import algebra.category.category algebra.hott + +open eq algebra pointed function is_trunc pi category equiv is_equiv +set_option class.force_new true + +namespace group + + definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one + definition pType_of_Group [reducible] (G : Group) : Type* := pointed.mk' G + definition Set_of_Group (G : Group) : Set := trunctype.mk G _ + + definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := + Group.mk G _ + + definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup) + : comm_group (Group_of_CommGroup G) := + begin esimp, exact _ end + + definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) := + Group.struct G + + /- group homomorphisms -/ + + definition is_homomorphism [class] [reducible] + {G₁ G₂ : Type} [group G₁] [group G₂] (φ : G₁ → G₂) : Type := + Π(g h : G₁), φ (g * h) = φ g * φ h + + section + variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂) + [group G] [group G₁] [group G₂] [group G₃] + [is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ] + + definition respect_mul /- φ -/ : Π(g h : G₁), φ (g * h) = φ g * φ h := + by assumption + + theorem respect_one /- φ -/ : φ 1 = 1 := + mul.right_cancel + (calc + φ 1 * φ 1 = φ (1 * 1) : respect_mul φ + ... = φ 1 : ap φ !one_mul + ... = 1 * φ 1 : one_mul) + + theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := + eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one) + + definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ := + begin + apply function.is_embedding_of_is_injective, + intro g g' p, + apply eq_of_mul_inv_eq_one, + apply H, + refine !respect_mul ⬝ _, + rewrite [respect_inv φ, p], + apply mul.right_inv + end + + definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂} + (H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) := + λg h, ap ψ !respect_mul ⬝ !respect_mul + + definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) := + λg h, idp + + end + + structure homomorphism (G₁ G₂ : Group) : 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₂) + : is_homomorphism φ := + homomorphism.p φ + + variables {G G₁ G₂ G₃ : Group} {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 + + theorem to_respect_one /- φ -/ : φ 1 = 1 := + respect_one φ + + theorem to_respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := + respect_inv φ g + + 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₂) := + begin + have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂, + begin + fapply equiv.MK, + { intro φ, induction φ, constructor, assumption}, + { intro v, induction v, constructor, assumption}, + { intro v, induction v, reflexivity}, + { intro φ, induction φ, reflexivity} + end, + apply is_trunc_equiv_closed_rev, exact H + end + + local attribute group_pType_of_Group pointed.mk' [reducible] + definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ := + pmap.mk φ (respect_one φ) + + definition homomorphism_eq (p : group_fun φ₁ ~ group_fun φ₂) : φ₁ = φ₂ := + begin + induction φ₁ with φ₁ q₁, induction φ₂ with φ₂ q₂, esimp at p, induction p, + exact ap (homomorphism.mk φ₁) !is_prop.elim + end + + /- categorical structure of groups + homomorphisms -/ + + 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 := + homomorphism.mk (@id G) (is_homomorphism_id G) + + infixr ` ∘g `:75 := homomorphism_compose + notation 1 := homomorphism_id _ + + structure isomorphism (A B : Group) := + (to_hom : A →g B) + (is_equiv_to_hom : is_equiv to_hom) + + infix ` ≃g `:25 := isomorphism + attribute isomorphism.to_hom [coercion] + attribute isomorphism.is_equiv_to_hom [instance] + + definition equiv_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ ≃ G₂ := + equiv.mk φ _ + + definition isomorphism_of_equiv [constructor] (φ : G₁ ≃ G₂) + (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₂ := + Group_eq (equiv_of_isomorphism φ) (respect_mul φ) + + definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ := + isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ)) + begin intros, induction φ, reflexivity end + + definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ := + homomorphism.mk φ⁻¹ + abstract begin + intro g₁ g₂, apply eq_of_fn_eq_fn' φ, + rewrite [respect_mul φ, +right_inv φ] + end end + + definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G := + isomorphism.mk 1 !is_equiv_id + + definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ := + isomorphism.mk (to_ginv φ) !is_equiv_inv + + definition isomorphism.trans [trans] [constructor] (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := + isomorphism.mk (ψ ∘g φ) !is_equiv_compose + + postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm + infixl ` ⬝g `:75 := isomorphism.trans + + -- TODO + -- definition Group_univalence (G₁ G₂ : Group) : (G₁ ≃g G₂) ≃ (G₁ = G₂) := + -- begin + -- fapply equiv.MK, + -- { exact eq_of_isomorphism}, + -- { intro p, apply transport _ p, reflexivity}, + -- { intro p, induction p, esimp, }, + -- { } + -- end + + /- category of groups -/ + + definition precategory_group [constructor] : precategory Group := + precategory.mk homomorphism + @homomorphism_compose + @homomorphism_id + (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp)) + (λG₁ G₂ φ, homomorphism_eq (λg, idp)) + (λG₁ G₂ φ, homomorphism_eq (λg, idp)) + + -- TODO + -- definition category_group : category Group := + -- category.mk precategory_group + -- begin + -- intro G₁ G₂, + -- fapply adjointify, + -- { intro φ, fapply Group_eq, }, + -- { }, + -- { } + -- end + + /- given an equivalence A ≃ B we can transport a group structure on A to a group structure on B -/ + + section + + parameters {A B : Type} (f : A ≃ B) [group A] + + definition group_equiv_mul (b b' : B) : B := f (f⁻¹ᶠ b * f⁻¹ᶠ b') + + definition group_equiv_one : B := f one + + definition group_equiv_inv (b : B) : B := f (f⁻¹ᶠ b)⁻¹ + + local infix * := group_equiv_mul + local postfix ^ := group_equiv_inv + local notation 1 := group_equiv_one + + theorem group_equiv_mul_assoc (b₁ b₂ b₃ : B) : (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) := + by rewrite [↑group_equiv_mul, +left_inv f, mul.assoc] + + theorem group_equiv_one_mul (b : B) : 1 * b = b := + by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, one_mul, right_inv f] + + theorem group_equiv_mul_one (b : B) : b * 1 = b := + by rewrite [↑group_equiv_mul, ↑group_equiv_one, left_inv f, mul_one, right_inv f] + + theorem group_equiv_mul_left_inv (b : B) : b^ * b = 1 := + by rewrite [↑group_equiv_mul, ↑group_equiv_one, ↑group_equiv_inv, + +left_inv f, mul.left_inv] + + definition group_equiv_closed : group B := + ⦃group, + mul := group_equiv_mul, + mul_assoc := group_equiv_mul_assoc, + one := group_equiv_one, + one_mul := group_equiv_one_mul, + mul_one := group_equiv_mul_one, + inv := group_equiv_inv, + mul_left_inv := group_equiv_mul_left_inv, + is_set_carrier := is_trunc_equiv_closed 0 f⦄ + + end + + definition trivial_group_of_is_contr (G : Group) [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 := + eq_of_isomorphism (trivial_group_of_is_contr G) + +end group diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 36f050eec..067191599 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -8,7 +8,7 @@ homotopy groups of a pointed space import .trunc_group types.trunc .group_theory -open nat eq pointed trunc is_trunc algebra +open nat eq pointed trunc is_trunc algebra group function equiv unit namespace eq @@ -64,8 +64,7 @@ namespace eq exact loopn_pequiv_loopn k (pequiv_of_eq begin rewrite [trunc_index.zero_add] end) end - open equiv unit - theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 := + theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 := begin apply trivial_group_of_is_contr, apply is_trunc_trunc_of_is_trunc, @@ -80,32 +79,15 @@ namespace eq definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n +1] A = π₁ Ω[n] A := idp - definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A := + definition ghomotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A ≃g πg[n +1] Ω A := begin - fapply Group_eq, + fapply isomorphism_of_equiv, { apply equiv_of_eq, exact ap (ptrunc 0) (loop_space_succ_eq_in A (succ n))}, { exact abstract [irreducible] begin refine trunc.rec _, intro p, refine trunc.rec _, intro q, rewrite [▸*,-+tr_eq_cast_ap, +trunc_transport], refine !trunc_transport ⬝ _, apply ap tr, apply loop_space_succ_eq_in_concat end end}, end - definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A = πg[n +1] Ω[m] A := - begin - revert A, induction m with m IH: intro A, - { reflexivity}, - { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝ _, refine !IH ⬝ _, - exact ap (ghomotopy_group n) !loop_space_succ_eq_in⁻¹} - end - - theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) - (H : is_set (Ω[n] A)) : πg[m+n+1] A = G0 := - !homotopy_group_add ⬝ !trivial_homotopy_of_is_set - - theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m) - (H2 : is_set (Ω[n] A)) : πg[m+1] A = G0 := - obtain (k : ℕ) (p : n + k = m), from le.elim H1, - ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k) ⬝ trivial_homotopy_add_of_is_set_loop_space k H2 - definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) : π*[n] A →* π*[n] B := ptrunc_functor 0 (apn n f) @@ -140,7 +122,39 @@ namespace eq apply ap tr, apply apn_con end - open group function + definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B) + : πg[n+1] A →g πg[n+1] B := + begin + fconstructor, + { exact phomotopy_group_functor (n+1) f}, + { apply phomotopy_group_functor_mul} + end + + definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B) + : πg[n+1] A ≃g πg[n+1] B := + begin + apply isomorphism.mk (homotopy_group_homomorphism n f), + esimp, apply is_equiv_trunc_functor, apply is_equiv_apn, + end + + definition homotopy_group_add (A : Type*) (n m : ℕ) : πg[n+m +1] A ≃g πg[n +1] Ω[m] A := + begin + revert A, induction m with m IH: intro A, + { reflexivity}, + { esimp [iterated_ploop_space, nat.add], refine !ghomotopy_group_succ_in ⬝g _, refine !IH ⬝g _, + apply homotopy_group_isomorphism_of_pequiv, + exact pequiv_of_eq !loop_space_succ_eq_in⁻¹} + end + + theorem trivial_homotopy_add_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) + (H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 := + !homotopy_group_add ⬝g !trivial_homotopy_of_is_set + + theorem trivial_homotopy_le_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m) + (H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 := + obtain (k : ℕ) (p : n + k = m), from le.elim H1, + isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g + trivial_homotopy_add_of_is_set_loop_space k H2 /- some homomorphisms -/ @@ -162,14 +176,6 @@ namespace eq exact ap tr !con_inv end - definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B) - : πg[n+1] A →g πg[n+1] B := - begin - fconstructor, - { exact phomotopy_group_functor (n+1) f}, - { apply phomotopy_group_functor_mul} - end - notation `π→g[`:95 n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f end eq diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index a4b81d20e..fdf1f0076 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -77,11 +77,4 @@ namespace algebra (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⁻¹) - definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G = G0 := - begin - fapply Group_eq, - { apply equiv_unit_of_is_contr}, - { intros, reflexivity} - end - end algebra diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index e257d97be..df8a14ce0 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -7,8 +7,8 @@ Declaration of the circle -/ import .sphere -import types.bool types.int.hott types.equiv -import algebra.homotopy_group algebra.hott .connectedness +import types.int.hott +import algebra.homotopy_group .connectedness open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra @@ -293,7 +293,7 @@ namespace circle preserve_binary_of_inv_preserve base_eq_base_equiv concat (@add ℤ _) decode_add p q --the carrier of π₁(S¹) is the set-truncation of base = base. - open algebra trunc + open algebra trunc group definition fg_carrier_equiv_int : π[1](S¹.) ≃ ℤ := trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed @@ -301,16 +301,16 @@ namespace circle definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p := eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm]) - definition fundamental_group_of_circle : π₁(S¹.) = gℤ := + definition fundamental_group_of_circle : π₁(S¹.) ≃g gℤ := begin - apply (Group_eq fg_carrier_equiv_int), + apply (isomorphism_of_equiv fg_carrier_equiv_int), intros g h, induction g with g', induction h with h', apply encode_con, end open nat - definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. = G0 := + definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. ≃g G0 := begin refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _, apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv