feat(homotopy): add results about infty-connectedness and loops of EM-spaces
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
3213b1b3b0
commit
2cc8914874
6 changed files with 158 additions and 13 deletions
|
|
@ -199,16 +199,23 @@ namespace EM
|
|||
rexact add_mul_le_mul_add n 1 1
|
||||
end
|
||||
|
||||
local attribute EMadd1 [reducible]
|
||||
definition is_conn_EMadd1 (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _
|
||||
section
|
||||
local attribute EMadd1 [reducible]
|
||||
definition is_conn_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _
|
||||
|
||||
definition is_trunc_EMadd1 (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _
|
||||
definition is_trunc_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _
|
||||
end
|
||||
|
||||
/- K(G, n) -/
|
||||
definition EM (G : CommGroup) : ℕ → Type*
|
||||
| 0 := pType_of_Group G
|
||||
| (k+1) := EMadd1 G k
|
||||
|
||||
namespace ops
|
||||
abbreviation K := EM
|
||||
end ops
|
||||
open ops
|
||||
|
||||
definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G :=
|
||||
begin
|
||||
cases n with n,
|
||||
|
|
@ -277,11 +284,55 @@ namespace EM
|
|||
[is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
|
||||
begin
|
||||
apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
|
||||
intro p q, esimp, exact respect_mul e (tr p) (tr q)
|
||||
intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
|
||||
end
|
||||
|
||||
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)
|
||||
[is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X :=
|
||||
begin
|
||||
refine _ ⬝e* pEM1_pequiv e,
|
||||
apply ptrunc_pequiv,
|
||||
apply is_trunc_pEM1
|
||||
end
|
||||
|
||||
definition EMadd1_pequiv_pEM1 (G : CommGroup) : 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 :=
|
||||
EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e
|
||||
|
||||
definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y)
|
||||
[is_conn 0 X] [is_trunc 1 X] [is_conn 0 Y] [is_trunc 1 Y] : X ≃* Y :=
|
||||
(pEM1_pequiv e)⁻¹ᵉ* ⬝e* pEM1_pequiv !isomorphism.refl
|
||||
|
||||
open circle int
|
||||
definition EM_pequiv_circle : K agℤ 1 ≃* S¹. :=
|
||||
!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 :=
|
||||
begin
|
||||
cases n with n,
|
||||
{ symmetry, apply EM1add1_pequiv_0, rexact homotopy_group_EMadd1 G 1,
|
||||
-- apply is_conn_loop, apply is_conn_EMadd1,
|
||||
apply is_trunc_loop, apply is_trunc_EMadd1},
|
||||
{ refine loop_ptrunc_pequiv _ _ ⬝e* _,
|
||||
rewrite [add_one, succ_sub_two],
|
||||
have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1,
|
||||
symmetry, refine freudenthal_pequiv _ this, }
|
||||
end
|
||||
|
||||
definition loop_EM (G : CommGroup) (n : ℕ) : Ω (K G (succ n)) ≃* K G n :=
|
||||
begin
|
||||
cases n with n,
|
||||
{ refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_pEM1 G),
|
||||
refine loop_pequiv_loop (EMadd1_pequiv_pEM1 G) ⬝e* _,
|
||||
symmetry, apply ptrunc_pequiv, exact _},
|
||||
{ apply loop_EMadd1}
|
||||
end
|
||||
|
||||
end EM
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ import .sphere
|
|||
import types.int.hott
|
||||
import algebra.homotopy_group .connectedness
|
||||
|
||||
open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra
|
||||
open eq susp bool sphere_index is_equiv equiv is_trunc is_conn pi algebra pointed
|
||||
|
||||
definition circle : Type₀ := sphere 1
|
||||
|
||||
|
|
@ -337,6 +337,9 @@ namespace circle
|
|||
proposition is_conn_circle [instance] : is_conn 0 S¹ :=
|
||||
sphere.is_conn_sphere -1.+2
|
||||
|
||||
definition is_conn_pcircle [instance] : is_conn 0 S¹. := !is_conn_circle
|
||||
definition is_trunc_pcircle [instance] : is_trunc 1 S¹. := !is_trunc_circle
|
||||
|
||||
definition circle_mul [reducible] (x y : S¹) : S¹ :=
|
||||
circle.elim y (circle_turn y) x
|
||||
|
||||
|
|
|
|||
|
|
@ -2,16 +2,24 @@
|
|||
Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Ulrik Buchholtz, Floris van Doorn
|
||||
|
||||
Connectedness of types and functions
|
||||
-/
|
||||
import types.trunc types.arrow_2 types.lift
|
||||
|
||||
open eq is_trunc is_equiv nat equiv trunc function fiber funext pi
|
||||
open eq is_trunc is_equiv nat equiv trunc function fiber funext pi pointed
|
||||
|
||||
definition is_conn [reducible] (n : ℕ₋₂) (A : Type) : Type :=
|
||||
is_contr (trunc n A)
|
||||
|
||||
definition is_conn_fun [reducible] (n : ℕ₋₂) {A B : Type} (f : A → B) : Type :=
|
||||
Πb : B, is_conn n (fiber f b)
|
||||
|
||||
definition is_conn_inf [reducible] (A : Type) : Type := Πn, is_conn n A
|
||||
definition is_conn_fun_inf [reducible] {A B : Type} (f : A → B) : Type := Πn, is_conn_fun n f
|
||||
|
||||
namespace is_conn
|
||||
|
||||
definition is_conn [reducible] (n : ℕ₋₂) (A : Type) : Type :=
|
||||
is_contr (trunc n A)
|
||||
|
||||
definition is_conn_equiv_closed (n : ℕ₋₂) {A B : Type}
|
||||
: A ≃ B → is_conn n A → is_conn n B :=
|
||||
begin
|
||||
|
|
@ -21,9 +29,6 @@ namespace is_conn
|
|||
assumption
|
||||
end
|
||||
|
||||
definition is_conn_fun [reducible] (n : ℕ₋₂) {A B : Type} (f : A → B) : Type :=
|
||||
Πb : B, is_conn n (fiber f b)
|
||||
|
||||
theorem is_conn_of_le (A : Type) {n k : ℕ₋₂} (H : n ≤ k) [is_conn k A] : is_conn n A :=
|
||||
begin
|
||||
apply is_contr_equiv_closed,
|
||||
|
|
@ -34,6 +39,9 @@ namespace is_conn
|
|||
[is_conn_fun k f] : is_conn_fun n f :=
|
||||
λb, is_conn_of_le _ H
|
||||
|
||||
definition is_conn_of_is_conn_succ (n : ℕ₋₂) (A : Type) [is_conn (n.+1) A] : is_conn n A :=
|
||||
is_trunc_trunc_of_le A -2 (trunc_index.self_le_succ n)
|
||||
|
||||
namespace is_conn_fun
|
||||
section
|
||||
parameters (n : ℕ₋₂) {A B : Type} {h : A → B}
|
||||
|
|
@ -267,6 +275,15 @@ namespace is_conn
|
|||
apply is_trunc_equiv_closed, apply trunc_trunc_equiv_trunc_trunc
|
||||
end
|
||||
|
||||
definition is_conn_eq [instance] (n : ℕ₋₂) {A : Type} (a a' : A) [is_conn (n.+1) A] :
|
||||
is_conn n (a = a') :=
|
||||
begin
|
||||
apply is_trunc_equiv_closed, apply tr_eq_tr_equiv,
|
||||
end
|
||||
|
||||
definition is_conn_loop [instance] (n : ℕ₋₂) (A : Type*) [is_conn (n.+1) A] : is_conn n (Ω A) :=
|
||||
!is_conn_eq
|
||||
|
||||
open pointed
|
||||
definition is_conn_ptrunc [instance] (A : Type*) (n k : ℕ₋₂) [H : is_conn n A]
|
||||
: is_conn n (ptrunc k A) :=
|
||||
|
|
@ -330,4 +347,22 @@ namespace is_conn
|
|||
{ apply trunc_equiv_trunc, apply fiber_lift_functor}
|
||||
end
|
||||
|
||||
open trunc_index
|
||||
definition is_conn_fun_inf.mk_nat {A B : Type} {f : A → B} (H : Π(n : ℕ), is_conn_fun n f)
|
||||
: is_conn_fun_inf f :=
|
||||
begin
|
||||
intro n,
|
||||
cases n with n, { exact _},
|
||||
cases n with n, { have -1 ≤ of_nat 0, from dec_star, apply is_conn_fun_of_le f this},
|
||||
rewrite -of_nat_add_two, exact _
|
||||
end
|
||||
|
||||
definition is_conn_inf.mk_nat {A : Type} (H : Π(n : ℕ), is_conn n A) : is_conn_inf A :=
|
||||
begin
|
||||
intro n,
|
||||
cases n with n, { exact _},
|
||||
cases n with n, { have -1 ≤ of_nat 0, from dec_star, apply is_conn_of_le A this},
|
||||
rewrite -of_nat_add_two, exact _
|
||||
end
|
||||
|
||||
end is_conn
|
||||
|
|
|
|||
|
|
@ -244,3 +244,25 @@ namespace is_trunc
|
|||
end
|
||||
|
||||
end is_trunc
|
||||
open is_trunc function
|
||||
/- applications to infty-connected types and maps -/
|
||||
namespace is_conn
|
||||
|
||||
definition is_conn_fun_inf_of_equiv_on_homotopy_groups.{u} {A B : Type.{u}} (f : A → B)
|
||||
[is_equiv (trunc_functor 0 f)]
|
||||
(H1 : Πa k, is_equiv (homotopy_group_functor k (pmap_of_map f a))) : is_conn_fun_inf f :=
|
||||
begin
|
||||
apply is_conn_fun_inf.mk_nat, intro n, apply is_conn_fun_of_equiv_on_homotopy_groups,
|
||||
{ intro a k H, exact H1 a k},
|
||||
{ intro a, apply is_surjective_of_is_equiv}
|
||||
end
|
||||
|
||||
definition is_equiv_trunc_functor_of_is_conn_fun_inf.{u} (n : ℕ₋₂) {A B : Type.{u}} (f : A → B)
|
||||
[is_conn_fun_inf f] : is_equiv (trunc_functor n f) :=
|
||||
_
|
||||
|
||||
definition is_equiv_homotopy_group_functor_of_is_conn_fun_inf.{u} {A B : pType.{u}} (f : A →* B)
|
||||
[is_conn_fun_inf f] (a : A) (k : ℕ) : is_equiv (homotopy_group_functor k f) :=
|
||||
is_equiv_π_of_is_connected f (le.refl k)
|
||||
|
||||
end is_conn
|
||||
|
|
|
|||
|
|
@ -18,6 +18,10 @@ namespace int
|
|||
Group.mk ℤ (group_of_add_group _)
|
||||
|
||||
notation `gℤ` := group_integers
|
||||
|
||||
definition CommGroup_int [constructor] : CommGroup :=
|
||||
CommGroup.mk ℤ ⦃comm_group, group_of_add_group ℤ, mul_comm := add.comm⦄
|
||||
notation `agℤ` := CommGroup_int
|
||||
end
|
||||
|
||||
definition is_equiv_succ [instance] : is_equiv succ :=
|
||||
|
|
|
|||
|
|
@ -182,6 +182,9 @@ namespace trunc_index
|
|||
definition sub_two_succ_succ (n : ℕ) : n.-2.+1.+1 = n := rfl
|
||||
definition succ_sub_two_succ (n : ℕ) : (nat.succ n).-2.+1 = n := rfl
|
||||
|
||||
definition of_nat_add_two (n : ℕ₋₂) : of_nat (add_two n) = n.+2 :=
|
||||
begin induction n with n IH, reflexivity, exact ap succ IH end
|
||||
|
||||
definition of_nat_le_of_nat {n m : ℕ} (H : n ≤ m) : (of_nat n ≤ of_nat m) :=
|
||||
begin
|
||||
induction H with m H IH,
|
||||
|
|
@ -224,6 +227,17 @@ namespace trunc_index
|
|||
{ exact succ_le_succ H2'}}
|
||||
end
|
||||
|
||||
definition trunc_index.decidable_le [instance] : Π(n m : ℕ₋₂), decidable (n ≤ m) :=
|
||||
begin
|
||||
intro n, induction n with n IH: intro m,
|
||||
{ left, apply minus_two_le},
|
||||
cases m with m,
|
||||
{ right, apply not_succ_le_minus_two},
|
||||
cases IH m with H H,
|
||||
{ left, apply succ_le_succ H},
|
||||
right, intro H2, apply H, exact le_of_succ_le_succ H2
|
||||
end
|
||||
|
||||
end trunc_index open trunc_index
|
||||
|
||||
namespace is_trunc
|
||||
|
|
@ -401,6 +415,7 @@ namespace is_trunc
|
|||
is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) :=
|
||||
iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn)
|
||||
|
||||
-- use loopn in name
|
||||
theorem is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type)
|
||||
: is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](pointed.Mk a)) :=
|
||||
begin
|
||||
|
|
@ -417,6 +432,7 @@ namespace is_trunc
|
|||
apply imp_iff, reflexivity}
|
||||
end
|
||||
|
||||
-- use loopn in name
|
||||
theorem is_trunc_iff_is_contr_loop (n : ℕ) (A : Type)
|
||||
: is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) :=
|
||||
begin
|
||||
|
|
@ -427,6 +443,7 @@ namespace is_trunc
|
|||
{ apply is_trunc_iff_is_contr_loop_succ},
|
||||
end
|
||||
|
||||
-- rename to is_contr_loopn_of_is_trunc
|
||||
theorem is_contr_loop_of_is_trunc (n : ℕ) (A : Type*) [H : is_trunc (n.-2.+1) A] :
|
||||
is_contr (Ω[n] A) :=
|
||||
begin
|
||||
|
|
@ -434,6 +451,7 @@ namespace is_trunc
|
|||
apply iff.mp !is_trunc_iff_is_contr_loop H
|
||||
end
|
||||
|
||||
-- rename to is_trunc_loopn_of_is_trunc
|
||||
theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] :
|
||||
is_trunc n (Ω[k] A) :=
|
||||
begin
|
||||
|
|
@ -442,6 +460,17 @@ namespace is_trunc
|
|||
{ apply is_trunc_eq}
|
||||
end
|
||||
|
||||
definition is_trunc_loopn (k : ℕ₋₂) (n : ℕ) (A : Type*) [H : is_trunc (k+n) A]
|
||||
: is_trunc k (Ω[n] A) :=
|
||||
begin
|
||||
revert k H, induction n with n IH: intro k H, exact _,
|
||||
apply is_trunc_eq, apply IH, rewrite [succ_add_nat, add_nat_succ at H], exact H
|
||||
end
|
||||
|
||||
definition is_set_loopn (n : ℕ) (A : Type*) [is_trunc n A] : is_set (Ω[n] A) :=
|
||||
have is_trunc (0+[ℕ₋₂]n) A, by rewrite [trunc_index.zero_add]; exact _,
|
||||
is_trunc_loopn 0 n A
|
||||
|
||||
end is_trunc open is_trunc
|
||||
|
||||
namespace trunc
|
||||
|
|
@ -496,7 +525,8 @@ namespace trunc
|
|||
intro p, induction p, induction aa with a, esimp, exact (tr idp)
|
||||
end
|
||||
|
||||
protected definition decode {n : ℕ₋₂} (aa aa' : trunc n.+1 A) : trunc.code n aa aa' → aa = aa' :=
|
||||
protected definition decode [unfold 3 4 5] {n : ℕ₋₂} (aa aa' : trunc n.+1 A) :
|
||||
trunc.code n aa aa' → aa = aa' :=
|
||||
begin
|
||||
induction aa' with a', induction aa with a,
|
||||
esimp [trunc.code, trunc.rec_on], intro x,
|
||||
|
|
|
|||
Loading…
Reference in a new issue