michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

higher groups: rename Grp to GType

Browse source
This commit is contained in:
Floris van Doorn 2018-01-31 13:01:17 -05:00
parent 9914352e10
commit fbad62541b
2 changed files with 101 additions and 96 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

195
higher_groups.hlean
View file

@ -26,58 +26,59 @@ definition is_conn_fun_prod_of_wedge (n m : ℕ) (A B : Type*)
is_conn_fun_prod_of_wedge n m A B is_conn_fun_prod_of_wedge n m A B
end hide end hide
/- We require that the carrier has a point (preserved by the equivalence) -/ /- The k-groupal n-types.
We require that the carrier has a point (preserved by the equivalence) -/
structure Grp (n k : ℕ) : Type := /- (n,k)Grp, denoted here as [n;k]Grp -/ structure GType (n k : ℕ) : Type := /- (n,k)GType, denoted here as [n;k]GType -/
(car : ptrunctype.{u} n) (car : ptrunctype.{u} n)
(B : pconntype.{u} (k.-1)) /- this is Bᵏ -/ (B : pconntype.{u} (k.-1)) /- this is Bᵏ -/
(e : car ≃* Ω[k] B) (e : car ≃* Ω[k] B)
structure InfGrp (k : ℕ) : Type := /- (∞,k)Grp, denoted here as [∞;k]Grp -/ structure InfGType (k : ℕ) : Type := /- (∞,k)GType, denoted here as [∞;k]GType -/
(car : pType.{u}) (car : pType.{u})
(B : pconntype.{u} (k.-1)) /- this is Bᵏ -/ (B : pconntype.{u} (k.-1)) /- this is Bᵏ -/
(e : car ≃* Ω[k] B) (e : car ≃* Ω[k] B)
structure ωGrp (n : ℕ) := /- (n,ω)Grp, denoted here as [n;ω]Grp -/ structure ωGType (n : ℕ) := /- (n,ω)GType, denoted here as [n;ω]GType -/
(B : Π(k : ℕ), (n+k)-Type*[k.-1]) (B : Π(k : ℕ), (n+k)-Type*[k.-1])
(e : Π(k : ℕ), B k ≃* Ω (B (k+1))) (e : Π(k : ℕ), B k ≃* Ω (B (k+1)))
attribute InfGrp.car Grp.car [coercion] attribute InfGType.car GType.car [coercion]
variables {n k l : ℕ} variables {n k l : ℕ}
notation `[`:95 n:0 `; ` k `]Grp`:0 := Grp n k notation `[`:95 n:0 `; ` k `]GType`:0 := GType n k
notation `[∞; `:95 k:0 `]Grp`:0 := InfGrp k notation `[∞; `:95 k:0 `]GType`:0 := InfGType k
notation `[`:95 n:0 `;ω]Grp`:0 := ωGrp n notation `[`:95 n:0 `;ω]GType`:0 := ωGType n
open Grp open GType
open InfGrp (renaming B→iB e→ie) open InfGType (renaming B→iB e→ie)
open ωGrp (renaming B→oB e→oe) open ωGType (renaming B→oB e→oe)
/- some basic properties -/ /- some basic properties -/
lemma is_trunc_B' (G : [n;k]Grp) : is_trunc (k+n) (B G) := lemma is_trunc_B' (G : [n;k]GType) : is_trunc (k+n) (B G) :=
begin begin
apply is_trunc_of_is_trunc_loopn, apply is_trunc_of_is_trunc_loopn,
exact is_trunc_equiv_closed _ (e G), exact is_trunc_equiv_closed _ (e G),
exact _ exact _
end end
lemma is_trunc_B (G : [n;k]Grp) : is_trunc (n+k) (B G) := lemma is_trunc_B (G : [n;k]GType) : is_trunc (n+k) (B G) :=
transport (λm, is_trunc m (B G)) (add.comm k n) (is_trunc_B' G) transport (λm, is_trunc m (B G)) (add.comm k n) (is_trunc_B' G)
local attribute [instance] is_trunc_B local attribute [instance] is_trunc_B
definition Grp.sigma_char (n k : ℕ) : definition GType.sigma_char (n k : ℕ) :
Grp.{u} n k ≃ Σ(B : pconntype.{u} (k.-1)), Σ(X : ptrunctype.{u} n), X ≃* Ω[k] B := GType.{u} n k ≃ Σ(B : pconntype.{u} (k.-1)), Σ(X : ptrunctype.{u} n), X ≃* Ω[k] B :=
begin begin
fapply equiv.MK, fapply equiv.MK,
{ intro G, exact ⟨B G, G, e G⟩ }, { intro G, exact ⟨B G, G, e G⟩ },
{ intro v, exact Grp.mk v.2.1 v.1 v.2.2 }, { intro v, exact GType.mk v.2.1 v.1 v.2.2 },
{ intro v, induction v with v₁ v₂, induction v₂, reflexivity }, { intro v, induction v with v₁ v₂, induction v₂, reflexivity },
{ intro G, induction G, reflexivity }, { intro G, induction G, reflexivity },
end end
definition Grp_equiv (n k : ℕ) : [n;k]Grp ≃ (n+k)-Type*[k.-1] := definition GType_equiv (n k : ℕ) : [n;k]GType ≃ (n+k)-Type*[k.-1] :=
Grp.sigma_char n k ⬝e GType.sigma_char n k ⬝e
sigma_equiv_of_is_embedding_left_contr sigma_equiv_of_is_embedding_left_contr
ptruncconntype.to_pconntype ptruncconntype.to_pconntype
(is_embedding_ptruncconntype_to_pconntype (n+k) (k.-1)) (is_embedding_ptruncconntype_to_pconntype (n+k) (k.-1))
@ -92,63 +93,63 @@ sigma_equiv_of_is_embedding_left_contr
apply lem } apply lem }
end end
begin begin
intro B' H, apply fiber.mk (ptruncconntype.mk B' (is_trunc_B (Grp.mk H.1 B' H.2)) pt _), intro B' H, apply fiber.mk (ptruncconntype.mk B' (is_trunc_B (GType.mk H.1 B' H.2)) pt _),
induction B' with G' B' e', reflexivity induction B' with G' B' e', reflexivity
end end
definition Grp_equiv_pequiv {n k : ℕ} (G : [n;k]Grp) : Grp_equiv n k G ≃* B G := definition GType_equiv_pequiv {n k : ℕ} (G : [n;k]GType) : GType_equiv n k G ≃* B G :=
by reflexivity by reflexivity
definition Grp_eq_equiv {n k : ℕ} (G H : [n;k]Grp) : (G = H :> [n;k]Grp) ≃ (B G ≃* B H) := definition GType_eq_equiv {n k : ℕ} (G H : [n;k]GType) : (G = H :> [n;k]GType) ≃ (B G ≃* B H) :=
eq_equiv_fn_eq_of_equiv (Grp_equiv n k) _ _ ⬝e !ptruncconntype_eq_equiv eq_equiv_fn_eq_of_equiv (GType_equiv n k) _ _ ⬝e !ptruncconntype_eq_equiv
definition Grp_eq {n k : ℕ} {G H : [n;k]Grp} (e : B G ≃* B H) : G = H := definition GType_eq {n k : ℕ} {G H : [n;k]GType} (e : B G ≃* B H) : G = H :=
(Grp_eq_equiv G H)⁻¹ᵉ e (GType_eq_equiv G H)⁻¹ᵉ e
/- similar properties for [∞;k]Grp -/ /- similar properties for [∞;k]GType -/
definition InfGrp.sigma_char (k : ℕ) : definition InfGType.sigma_char (k : ℕ) :
InfGrp.{u} k ≃ Σ(B : pconntype.{u} (k.-1)), Σ(X : pType.{u}), X ≃* Ω[k] B := InfGType.{u} k ≃ Σ(B : pconntype.{u} (k.-1)), Σ(X : pType.{u}), X ≃* Ω[k] B :=
begin begin
fapply equiv.MK, fapply equiv.MK,
{ intro G, exact ⟨iB G, G, ie G⟩ }, { intro G, exact ⟨iB G, G, ie G⟩ },
{ intro v, exact InfGrp.mk v.2.1 v.1 v.2.2 }, { intro v, exact InfGType.mk v.2.1 v.1 v.2.2 },
{ intro v, induction v with v₁ v₂, induction v₂, reflexivity }, { intro v, induction v with v₁ v₂, induction v₂, reflexivity },
{ intro G, induction G, reflexivity }, { intro G, induction G, reflexivity },
end end
definition InfGrp_equiv (k : ℕ) : [∞;k]Grp ≃ Type*[k.-1] := definition InfGType_equiv (k : ℕ) : [∞;k]GType ≃ Type*[k.-1] :=
InfGrp.sigma_char k ⬝e InfGType.sigma_char k ⬝e
@sigma_equiv_of_is_contr_right _ _ @sigma_equiv_of_is_contr_right _ _
(λX, is_trunc_equiv_closed_rev -2 (sigma_equiv_sigma_right (λB', !pType_eq_equiv⁻¹ᵉ))) (λX, is_trunc_equiv_closed_rev -2 (sigma_equiv_sigma_right (λB', !pType_eq_equiv⁻¹ᵉ)))
definition InfGrp_equiv_pequiv {k : ℕ} (G : [∞;k]Grp) : InfGrp_equiv k G ≃* iB G := definition InfGType_equiv_pequiv {k : ℕ} (G : [∞;k]GType) : InfGType_equiv k G ≃* iB G :=
by reflexivity by reflexivity
definition InfGrp_eq_equiv {k : ℕ} (G H : [∞;k]Grp) : (G = H :> [∞;k]Grp) ≃ (iB G ≃* iB H) := definition InfGType_eq_equiv {k : ℕ} (G H : [∞;k]GType) : (G = H :> [∞;k]GType) ≃ (iB G ≃* iB H) :=
eq_equiv_fn_eq_of_equiv (InfGrp_equiv k) _ _ ⬝e !pconntype_eq_equiv eq_equiv_fn_eq_of_equiv (InfGType_equiv k) _ _ ⬝e !pconntype_eq_equiv
definition InfGrp_eq {k : ℕ} {G H : [∞;k]Grp} (e : iB G ≃* iB H) : G = H := definition InfGType_eq {k : ℕ} {G H : [∞;k]GType} (e : iB G ≃* iB H) : G = H :=
(InfGrp_eq_equiv G H)⁻¹ᵉ e (InfGType_eq_equiv G H)⁻¹ᵉ e
-- maybe to do: ωGrp ≃ Σ(X : spectrum), is_sconn n X -- maybe to do: ωGType ≃ Σ(X : spectrum), is_sconn n X
/- Constructions on higher groups -/ /- Constructions on higher groups -/
definition Decat (G : [n+1;k]Grp) : [n;k]Grp := definition Decat (G : [n+1;k]GType) : [n;k]GType :=
Grp.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (B G)) _ pt) GType.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (B G)) _ pt)
abstract begin abstract begin
refine ptrunc_pequiv_ptrunc n (e G) ⬝e* _, refine ptrunc_pequiv_ptrunc n (e G) ⬝e* _,
symmetry, exact !loopn_ptrunc_pequiv_nat symmetry, exact !loopn_ptrunc_pequiv_nat
end end end end
definition Disc (G : [n;k]Grp) : [n+1;k]Grp := definition Disc (G : [n;k]GType) : [n+1;k]GType :=
Grp.mk (ptrunctype.mk G (show is_trunc (n.+1) G, from _) pt) (B G) (e G) GType.mk (ptrunctype.mk G (show is_trunc (n.+1) G, from _) pt) (B G) (e G)
definition Decat_adjoint_Disc (G : [n+1;k]Grp) (H : [n;k]Grp) : definition Decat_adjoint_Disc (G : [n+1;k]GType) (H : [n;k]GType) :
ppmap (B (Decat G)) (B H) ≃* ppmap (B G) (B (Disc H)) := ppmap (B (Decat G)) (B H) ≃* ppmap (B G) (B (Disc H)) :=
pmap_ptrunc_pequiv (n + k) (B G) (B H) pmap_ptrunc_pequiv (n + k) (B G) (B H)
definition Decat_adjoint_Disc_natural {G G' : [n+1;k]Grp} {H H' : [n;k]Grp} definition Decat_adjoint_Disc_natural {G G' : [n+1;k]GType} {H H' : [n;k]GType}
(g : B G' →* B G) (h : B H →* B H') : (g : B G' →* B G) (h : B H →* B H') :
psquare (Decat_adjoint_Disc G H) psquare (Decat_adjoint_Disc G H)
(Decat_adjoint_Disc G' H') (Decat_adjoint_Disc G' H')
@ -156,46 +157,46 @@ definition Decat_adjoint_Disc_natural {G G' : [n+1;k]Grp} {H H' : [n;k]Grp}
(ppcompose_left h ∘* ppcompose_right g) := (ppcompose_left h ∘* ppcompose_right g) :=
pmap_ptrunc_pequiv_natural (n + k) g h pmap_ptrunc_pequiv_natural (n + k) g h
definition Decat_Disc (G : [n;k]Grp) : Decat (Disc G) = G := definition Decat_Disc (G : [n;k]GType) : Decat (Disc G) = G :=
Grp_eq !ptrunc_pequiv GType_eq !ptrunc_pequiv
definition InfDecat (n : ℕ) (G : [∞;k]Grp) : [n;k]Grp := definition InfDecat (n : ℕ) (G : [∞;k]GType) : [n;k]GType :=
Grp.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (iB G)) _ pt) GType.mk (ptrunctype.mk (ptrunc n G) _ pt) (pconntype.mk (ptrunc (n + k) (iB G)) _ pt)
abstract begin abstract begin
refine ptrunc_pequiv_ptrunc n (ie G) ⬝e* _, refine ptrunc_pequiv_ptrunc n (ie G) ⬝e* _,
symmetry, exact !loopn_ptrunc_pequiv_nat symmetry, exact !loopn_ptrunc_pequiv_nat
end end end end
definition InfDisc (n : ℕ) (G : [n;k]Grp) : [∞;k]Grp := definition InfDisc (n : ℕ) (G : [n;k]GType) : [∞;k]GType :=
InfGrp.mk G (B G) (e G) InfGType.mk G (B G) (e G)
definition InfDecat_adjoint_InfDisc (G : [∞;k]Grp) (H : [n;k]Grp) : definition InfDecat_adjoint_InfDisc (G : [∞;k]GType) (H : [n;k]GType) :
ppmap (B (InfDecat n G)) (B H) ≃* ppmap (iB G) (iB (InfDisc n H)) := ppmap (B (InfDecat n G)) (B H) ≃* ppmap (iB G) (iB (InfDisc n H)) :=
pmap_ptrunc_pequiv (n + k) (iB G) (B H) pmap_ptrunc_pequiv (n + k) (iB G) (B H)
/- To do: naturality -/ /- To do: naturality -/
definition InfDecat_InfDisc (G : [n;k]Grp) : InfDecat n (InfDisc n G) = G := definition InfDecat_InfDisc (G : [n;k]GType) : InfDecat n (InfDisc n G) = G :=
Grp_eq !ptrunc_pequiv GType_eq !ptrunc_pequiv
definition Deloop (G : [n;k+1]Grp) : [n+1;k]Grp := definition Deloop (G : [n;k+1]GType) : [n+1;k]GType :=
have is_conn k (B G), from is_conn_pconntype (B G), have is_conn k (B G), from is_conn_pconntype (B G),
have is_trunc (n + (k + 1)) (B G), from is_trunc_B G, have is_trunc (n + (k + 1)) (B G), from is_trunc_B G,
have is_trunc ((n + 1) + k) (B G), from transport (λ(n : ℕ), is_trunc n _) (succ_add n k)⁻¹ this, have is_trunc ((n + 1) + k) (B G), from transport (λ(n : ℕ), is_trunc n _) (succ_add n k)⁻¹ this,
Grp.mk (ptrunctype.mk (Ω[k] (B G)) !is_trunc_loopn_nat pt) GType.mk (ptrunctype.mk (Ω[k] (B G)) !is_trunc_loopn_nat pt)
(pconntype.mk (B G) !is_conn_of_is_conn_succ pt) (pconntype.mk (B G) !is_conn_of_is_conn_succ pt)
(pequiv_of_equiv erfl idp) (pequiv_of_equiv erfl idp)
definition Loop (G : [n+1;k]Grp) : [n;k+1]Grp := definition Loop (G : [n+1;k]GType) : [n;k+1]GType :=
Grp.mk (ptrunctype.mk (Ω G) !is_trunc_loop_nat pt) GType.mk (ptrunctype.mk (Ω G) !is_trunc_loop_nat pt)
(connconnect k (B G)) (connconnect k (B G))
(loop_pequiv_loop (e G) ⬝e* (loopn_connect k (B G))⁻¹ᵉ*) (loop_pequiv_loop (e G) ⬝e* (loopn_connect k (B G))⁻¹ᵉ*)
definition Deloop_adjoint_Loop (G : [n;k+1]Grp) (H : [n+1;k]Grp) : definition Deloop_adjoint_Loop (G : [n;k+1]GType) (H : [n+1;k]GType) :
ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) := ppmap (B (Deloop G)) (B H) ≃* ppmap (B G) (B (Loop H)) :=
(connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ* (connect_intro_pequiv _ !is_conn_pconntype)⁻¹ᵉ*
definition Deloop_adjoint_Loop_natural {G G' : [n;k+1]Grp} {H H' : [n+1;k]Grp} definition Deloop_adjoint_Loop_natural {G G' : [n;k+1]GType} {H H' : [n+1;k]GType}
(g : B G' →* B G) (h : B H →* B H') : (g : B G' →* B G) (h : B H →* B H') :
psquare (Deloop_adjoint_Loop G H) psquare (Deloop_adjoint_Loop G H)
(Deloop_adjoint_Loop G' H') (Deloop_adjoint_Loop G' H')
@ -205,20 +206,20 @@ definition Deloop_adjoint_Loop_natural {G G' : [n;k+1]Grp} {H H' : [n+1;k]Grp}
/- to do: naturality -/ /- to do: naturality -/
definition Loop_Deloop (G : [n;k+1]Grp) : Loop (Deloop G) = G := definition Loop_Deloop (G : [n;k+1]GType) : Loop (Deloop G) = G :=
Grp_eq (connect_pequiv (is_conn_pconntype (B G))) GType_eq (connect_pequiv (is_conn_pconntype (B G)))
definition Forget (G : [n;k+1]Grp) : [n;k]Grp := definition Forget (G : [n;k+1]GType) : [n;k]GType :=
have is_conn k (B G), from !is_conn_pconntype, have is_conn k (B G), from !is_conn_pconntype,
Grp.mk G (pconntype.mk (Ω (B G)) !is_conn_loop pt) GType.mk G (pconntype.mk (Ω (B G)) !is_conn_loop pt)
abstract begin abstract begin
refine e G ⬝e* !loopn_succ_in refine e G ⬝e* !loopn_succ_in
end end end end
definition Stabilize (G : [n;k]Grp) : [n;k+1]Grp := definition Stabilize (G : [n;k]GType) : [n;k+1]GType :=
have is_conn k (susp (B G)), from !is_conn_susp, have is_conn k (susp (B G)), from !is_conn_susp,
have Hconn : is_conn k (ptrunc (n + k + 1) (susp (B G))), from !is_conn_ptrunc, have Hconn : is_conn k (ptrunc (n + k + 1) (susp (B G))), from !is_conn_ptrunc,
Grp.mk (ptrunctype.mk (ptrunc n (Ω[k+1] (susp (B G)))) _ pt) GType.mk (ptrunctype.mk (ptrunc n (Ω[k+1] (susp (B G)))) _ pt)
(pconntype.mk (ptrunc (n+k+1) (susp (B G))) Hconn pt) (pconntype.mk (ptrunc (n+k+1) (susp (B G))) Hconn pt)
abstract begin abstract begin
refine !loopn_ptrunc_pequiv⁻¹ᵉ* ⬝e* _, refine !loopn_ptrunc_pequiv⁻¹ᵉ* ⬝e* _,
@ -226,12 +227,12 @@ Grp.mk (ptrunctype.mk (ptrunc n (Ω[k+1] (susp (B G)))) _ pt)
exact ptrunc_change_index !of_nat_add_of_nat _ exact ptrunc_change_index !of_nat_add_of_nat _
end end end end
definition Stabilize_adjoint_Forget (G : [n;k]Grp) (H : [n;k+1]Grp) : definition Stabilize_adjoint_Forget (G : [n;k]GType) (H : [n;k+1]GType) :
ppmap (B (Stabilize G)) (B H) ≃* ppmap (B G) (B (Forget H)) := ppmap (B (Stabilize G)) (B H) ≃* ppmap (B G) (B (Forget H)) :=
have is_trunc (n + k + 1) (B H), from !is_trunc_B, have is_trunc (n + k + 1) (B H), from !is_trunc_B,
pmap_ptrunc_pequiv (n + k + 1) (⅀ (B G)) (B H) ⬝e* susp_adjoint_loop (B G) (B H) pmap_ptrunc_pequiv (n + k + 1) (⅀ (B G)) (B H) ⬝e* susp_adjoint_loop (B G) (B H)
definition Stabilize_adjoint_Forget_natural {G G' : [n;k]Grp} {H H' : [n;k+1]Grp} definition Stabilize_adjoint_Forget_natural {G G' : [n;k]GType} {H H' : [n;k+1]GType}
(g : B G' →* B G) (h : B H →* B H') : (g : B G' →* B G) (h : B H →* B H') :
psquare (Stabilize_adjoint_Forget G H) psquare (Stabilize_adjoint_Forget G H)
(Stabilize_adjoint_Forget G' H') (Stabilize_adjoint_Forget G' H')
@ -246,17 +247,17 @@ end
/- to do: naturality -/ /- to do: naturality -/
definition ωForget (k : ℕ) (G : [n;ω]Grp) : [n;k]Grp := definition ωForget (k : ℕ) (G : [n;ω]GType) : [n;k]GType :=
have is_trunc (n + k) (oB G k), from _, have is_trunc (n + k) (oB G k), from _,
have is_trunc n (Ω[k] (oB G k)), from !is_trunc_loopn_nat, have is_trunc n (Ω[k] (oB G k)), from !is_trunc_loopn_nat,
Grp.mk (ptrunctype.mk (Ω[k] (oB G k)) _ pt) (oB G k) (pequiv_of_equiv erfl idp) GType.mk (ptrunctype.mk (Ω[k] (oB G k)) _ pt) (oB G k) (pequiv_of_equiv erfl idp)
definition nStabilize (H : k ≤ l) (G : Grp.{u} n k) : Grp.{u} n l := definition nStabilize (H : k ≤ l) (G : GType.{u} n k) : GType.{u} n l :=
begin begin
induction H with l H IH, exact G, exact Stabilize IH induction H with l H IH, exact G, exact Stabilize IH
end end
definition Forget_Stabilize (H : k ≥ n + 2) (G : [n;k]Grp) : B (Forget (Stabilize G)) ≃* B G := definition Forget_Stabilize (H : k ≥ n + 2) (G : [n;k]GType) : B (Forget (Stabilize G)) ≃* B G :=
loop_ptrunc_pequiv _ _ ⬝e* loop_ptrunc_pequiv _ _ ⬝e*
begin begin
cases k with k, cases k with k,
@ -268,12 +269,12 @@ begin
end⁻¹ᵉ* ⬝e* end⁻¹ᵉ* ⬝e*
ptrunc_pequiv (n + k) _ ptrunc_pequiv (n + k) _
definition Stabilize_Forget (H : k ≥ n + 1) (G : [n;k+1]Grp) : B (Stabilize (Forget G)) ≃* B G := definition Stabilize_Forget (H : k ≥ n + 1) (G : [n;k+1]GType) : B (Stabilize (Forget G)) ≃* B G :=
begin begin
assert lem1 : n + succ k ≤ 2 * k, assert lem1 : n + succ k ≤ 2 * k,
{ rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right H k }, { rewrite [two_mul, add_succ, -succ_add], exact nat.add_le_add_right H k },
have is_conn k (B G), from !is_conn_pconntype, have is_conn k (B G), from !is_conn_pconntype,
have Π(G' : [n;k+1]Grp), is_trunc (n + k + 1) (B G'), from is_trunc_B, have Π(G' : [n;k+1]GType), is_trunc (n + k + 1) (B G'), from is_trunc_B,
note z := is_conn_fun_loop_susp_counit (B G) (nat.le_refl (2 * k)), note z := is_conn_fun_loop_susp_counit (B G) (nat.le_refl (2 * k)),
refine ptrunc_pequiv_ptrunc_of_le (of_nat_le_of_nat lem1) (@(ptrunc_pequiv_ptrunc_of_is_conn_fun _ _) z) ⬝e* refine ptrunc_pequiv_ptrunc_of_le (of_nat_le_of_nat lem1) (@(ptrunc_pequiv_ptrunc_of_is_conn_fun _ _) z) ⬝e*
!ptrunc_pequiv, !ptrunc_pequiv,
@ -283,13 +284,13 @@ definition stabilization (H : k ≥ n + 2) : is_equiv (@Stabilize n k) :=
begin begin
fapply adjointify, fapply adjointify,
{ exact Forget }, { exact Forget },
{ intro G, apply Grp_eq, exact Stabilize_Forget (le.trans !self_le_succ H) _ }, { intro G, apply GType_eq, exact Stabilize_Forget (le.trans !self_le_succ H) _ },
{ intro G, apply Grp_eq, exact Forget_Stabilize H G } { intro G, apply GType_eq, exact Forget_Stabilize H G }
end end
definition ωGrp.mk_le {n : ℕ} (k₀ : ℕ) definition ωGType.mk_le {n : ℕ} (k₀ : ℕ)
(C : Π⦃k : ℕ⦄, k₀ ≤ k → ((n+k)-Type*[k.-1] : Type.{u+1})) (C : Π⦃k : ℕ⦄, k₀ ≤ k → ((n+k)-Type*[k.-1] : Type.{u+1}))
(e : Π⦃k : ℕ⦄ (H : k₀ ≤ k), C H ≃* Ω (C (le.step H))) : ([n;ω]Grp : Type.{u+1}) := (e : Π⦃k : ℕ⦄ (H : k₀ ≤ k), C H ≃* Ω (C (le.step H))) : ([n;ω]GType : Type.{u+1}) :=
begin begin
fconstructor, fconstructor,
{ apply rec_down_le _ k₀ C, intro n' D, { apply rec_down_le _ k₀ C, intro n' D,
@ -302,11 +303,11 @@ end
/- for l ≤ k we want to define it as Ω[k-l] (B G), /- for l ≤ k we want to define it as Ω[k-l] (B G),
for H : l ≥ k we want to define it as nStabilize H G -/ for H : l ≥ k we want to define it as nStabilize H G -/
definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]Grp) : [n;ω]Grp := definition ωStabilize_of_le (H : k ≥ n + 2) (G : [n;k]GType) : [n;ω]GType :=
ωGrp.mk_le k (λl H', Grp_equiv n l (nStabilize H' G)) ωGType.mk_le k (λl H', GType_equiv n l (nStabilize H' G))
(λl H', (Forget_Stabilize (le.trans H H') (nStabilize H' G))⁻¹ᵉ*) (λl H', (Forget_Stabilize (le.trans H H') (nStabilize H' G))⁻¹ᵉ*)
definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp := definition ωStabilize (G : [n;k]GType) : [n;ω]GType :=
ωStabilize_of_le !le_max_left (nStabilize !le_max_right G) ωStabilize_of_le !le_max_left (nStabilize !le_max_right G)
definition ωstabilization (H : k ≥ n + 2) : is_equiv (@ωStabilize n k) := definition ωstabilization (H : k ≥ n + 2) : is_equiv (@ωStabilize n k) :=
@ -314,44 +315,48 @@ sorry
/- to do: adjunction (and ωStabilize ∘ ωForget =?= id) -/ /- to do: adjunction (and ωStabilize ∘ ωForget =?= id) -/
definition Grp_hom (G H : [n;k]Grp) : Type := definition GType_hom (G H : [n;k]GType) : Type :=
B G →* B H B G →* B H
definition is_trunc_Grp_hom (G H : [n;k]Grp) : is_trunc n (Grp_hom G H) := definition is_trunc_GType_hom (G H : [n;k]GType) : is_trunc n (GType_hom G H) :=
is_trunc_pmap_of_is_conn _ (k.-2) _ (k + n) _ (le_of_eq (sub_one_add_plus_two_sub_one k n)⁻¹) is_trunc_pmap_of_is_conn _ (k.-2) _ (k + n) _ (le_of_eq (sub_one_add_plus_two_sub_one k n)⁻¹)
(is_trunc_B' H) (is_trunc_B' H)
definition is_set_Grp_hom (G H : [0;k]Grp) : is_set (Grp_hom G H) := definition is_set_GType_hom (G H : [0;k]GType) : is_set (GType_hom G H) :=
is_trunc_Grp_hom G H is_trunc_GType_hom G H
definition is_trunc_Grp (n k : ℕ) : is_trunc (n + 1) [n;k]Grp := definition is_trunc_GType (n k : ℕ) : is_trunc (n + 1) [n;k]GType :=
begin begin
apply @is_trunc_equiv_closed_rev _ _ (n + 1) (Grp_equiv n k), apply @is_trunc_equiv_closed_rev _ _ (n + 1) (GType_equiv n k),
apply is_trunc_succ_intro, intros X Y, apply is_trunc_succ_intro, intros X Y,
apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y), apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y),
apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_pmap X Y), apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_pmap X Y),
apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)), apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)),
exact is_trunc_Grp_hom ((Grp_equiv n k)⁻¹ᵉ X) ((Grp_equiv n k)⁻¹ᵉ Y) exact is_trunc_GType_hom ((GType_equiv n k)⁻¹ᵉ X) ((GType_equiv n k)⁻¹ᵉ Y)
end end
local attribute [instance] is_set_Grp_hom local attribute [instance] is_set_GType_hom
definition cGrp [constructor] (k : ℕ) : Precategory := definition cGType [constructor] (k : ℕ) : Precategory :=
pb_Precategory (cptruncconntype' (k.-1)) pb_Precategory (cptruncconntype' (k.-1))
(Grp_equiv 0 k ⬝e equiv_ap (λx, x-Type*[k.-1]) (ap of_nat (zero_add k)) ⬝e (GType_equiv 0 k ⬝e equiv_ap (λx, x-Type*[k.-1]) (ap of_nat (zero_add k)) ⬝e
(ptruncconntype'_equiv_ptruncconntype (k.-1))⁻¹ᵉ) (ptruncconntype'_equiv_ptruncconntype (k.-1))⁻¹ᵉ)
example (k : ℕ) : Precategory.carrier (cGrp k) = [0;k]Grp := by reflexivity example (k : ℕ) : Precategory.carrier (cGType k) = [0;k]GType := by reflexivity
-- TODO
-- example (k : ℕ) (G H : cGType k) : (G ⟶ H) = (B G →* B H) :=
-- begin esimp [cGType] end
--by induction G, induction H, reflexivity
definition cGrp_equivalence_cType [constructor] (k : ℕ) : cGrp k ≃c cType*[k.-1] := definition cGType_equivalence_cType [constructor] (k : ℕ) : cGType k ≃c cType*[k.-1] :=
!pb_Precategory_equivalence_of_equiv !pb_Precategory_equivalence_of_equiv
definition cGrp_equivalence_Grp [constructor] : cGrp.{u} 1 ≃c category.Grp.{u} := definition cGType_equivalence_Grp [constructor] : cGType.{u} 1 ≃c Grp.{u} :=
equivalence.trans !pb_Precategory_equivalence_of_equiv equivalence.trans !pb_Precategory_equivalence_of_equiv
(equivalence.trans (equivalence.symm Grp_equivalence_cptruncconntype') (equivalence.trans (equivalence.symm Grp_equivalence_cptruncconntype')
proof equivalence.refl _ qed) proof equivalence.refl _ qed)
definition cGrp_equivalence_AbGrp [constructor] (k : ℕ) : cGrp.{u} (k+2) ≃c category.AbGrp.{u} := definition cGType_equivalence_AbGrp [constructor] (k : ℕ) : cGType.{u} (k+2) ≃c AbGrp.{u} :=
equivalence.trans !pb_Precategory_equivalence_of_equiv equivalence.trans !pb_Precategory_equivalence_of_equiv
(equivalence.trans (equivalence.symm (AbGrp_equivalence_cptruncconntype' k)) (equivalence.trans (equivalence.symm (AbGrp_equivalence_cptruncconntype' k))
proof equivalence.refl _ qed) proof equivalence.refl _ qed)
@ -367,8 +372,8 @@ print axioms Deloop_adjoint_Loop_natural
print axioms Stabilize_adjoint_Forget print axioms Stabilize_adjoint_Forget
print axioms Stabilize_adjoint_Forget_natural print axioms Stabilize_adjoint_Forget_natural
print axioms stabilization print axioms stabilization
print axioms is_trunc_Grp print axioms is_trunc_GType
print axioms cGrp_equivalence_Grp print axioms cGType_equivalence_Grp
print axioms cGrp_equivalence_AbGrp print axioms cGType_equivalence_AbGrp
end higher_group end higher_group

2
homotopy/EM.hlean
View file

@ -399,7 +399,7 @@ namespace EM
attribute ptruncconntype'.A [coercion] attribute ptruncconntype'.A [coercion]
attribute ptruncconntype'.H1 ptruncconntype'.H2 [instance] attribute ptruncconntype'.H1 ptruncconntype'.H2 [instance]
definition ptruncconntype'_equiv_ptruncconntype (n : ℕ₋₂) : definition ptruncconntype'_equiv_ptruncconntype [constructor] (n : ℕ₋₂) :
(ptruncconntype' n : Type.{u+1}) ≃ ((n+1)-Type*[n] : Type.{u+1}) := (ptruncconntype' n : Type.{u+1}) ≃ ((n+1)-Type*[n] : Type.{u+1}) :=
begin begin
fapply equiv.MK, fapply equiv.MK,