feat(hott): use group isomorphisms instead of equality between groups

This commit is contained in:
Floris van Doorn 2016-04-20 11:51:56 -04:00 committed by Leonardo de Moura
parent 8db4676c46
commit 1135d80266
4 changed files with 303 additions and 44 deletions

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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