feat(hott): various additions
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
c6e628da12
commit
e515875464
12 changed files with 220 additions and 86 deletions
|
|
@ -6,7 +6,7 @@ Authors: Floris van Doorn
|
|||
homotopy groups of a pointed space
|
||||
-/
|
||||
|
||||
import types.pointed .trunc_group .hott types.trunc
|
||||
import .trunc_group .hott types.trunc
|
||||
|
||||
open nat eq pointed trunc is_trunc algebra
|
||||
|
||||
|
|
@ -45,6 +45,10 @@ namespace eq
|
|||
|
||||
prefix `π₁`:95 := fundamental_group
|
||||
|
||||
definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
|
||||
: π*[n] A ≃* π*[n] B :=
|
||||
ptrunc_pequiv 0 (iterated_loop_space_pequiv n H)
|
||||
|
||||
open equiv unit
|
||||
theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A = G0 :=
|
||||
begin
|
||||
|
|
@ -54,12 +58,17 @@ namespace eq
|
|||
apply is_trunc_succ_succ_of_is_set
|
||||
end
|
||||
|
||||
definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πg[ n +1] A = π₁ Ω[n] A := idp
|
||||
definition phomotopy_group_succ_out (A : Type*) (n : ℕ) : π*[n + 1] A = π₁ Ω[n] A := idp
|
||||
|
||||
definition homotopy_group_succ_in (A : Type*) (n : ℕ) : πg[succ n +1] A = πg[n +1] Ω A :=
|
||||
definition phomotopy_group_succ_in (A : Type*) (n : ℕ) : π*[n + 1] A = π*[n] Ω A :=
|
||||
ap (ptrunc 0) (loop_space_succ_eq_in A n)
|
||||
|
||||
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 :=
|
||||
begin
|
||||
fapply Group_eq,
|
||||
{ apply equiv_of_eq, exact ap (λ(X : Type*), trunc 0 X) (loop_space_succ_eq_in A (succ n))},
|
||||
{ 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},
|
||||
|
|
@ -69,18 +78,51 @@ namespace eq
|
|||
begin
|
||||
revert A, induction m with m IH: intro A,
|
||||
{ reflexivity},
|
||||
{ esimp [iterated_ploop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
|
||||
{ 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_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_set (Ω[n] A))
|
||||
: πg[m+n+1] A = G0 :=
|
||||
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)
|
||||
|
||||
notation `π→*[`:95 n:0 `] `:0 f:95 := phomotopy_group_functor n f
|
||||
definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B :=
|
||||
phomotopy_group_functor n f
|
||||
|
||||
notation `π→*[`:95 n:0 `] `:0 f:95 := phomotopy_group_functor n f
|
||||
notation `π→[`:95 n:0 `] `:0 f:95 := homotopy_group_functor n f
|
||||
|
||||
definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
|
||||
ptrunc_functor 0 pinverse
|
||||
|
||||
definition ptrunc_functor_pinverse [constructor] {X : Type*}
|
||||
: ptrunc_functor 0 (@pinverse X) ~* @tinverse X :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ reflexivity},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition phomotopy_group_functor_mul [constructor] (n : ℕ) {A B : Type*} (g : A →* B)
|
||||
(p q : πg[n+1] A) :
|
||||
(π→[n + 1] g) (p *[πg[n+1] A] q) = (π→[n + 1] g) p *[πg[n+1] B] (π→[n + 1] g) q :=
|
||||
begin
|
||||
unfold [ghomotopy_group, homotopy_group] at *,
|
||||
refine @trunc.rec _ _ _ (λq, !is_trunc_eq) _ p, clear p, intro p,
|
||||
refine @trunc.rec _ _ _ (λq, !is_trunc_eq) _ q, clear q, intro q,
|
||||
apply ap tr, apply apn_con
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
end eq
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ namespace algebra
|
|||
definition Trivial_group [constructor] : Group :=
|
||||
Group.mk _ trivial_group
|
||||
|
||||
notation `G0` := Trivial_group
|
||||
abbreviation G0 := Trivial_group
|
||||
|
||||
open Group has_mul has_inv
|
||||
-- we prove under which conditions two groups are equal
|
||||
|
|
@ -27,8 +27,8 @@ namespace algebra
|
|||
-- coercions between them anymore.
|
||||
-- So, an application such as (@mul A G g h) in the following definition
|
||||
-- is type incorrect if the coercion is not added (explicitly or implicitly).
|
||||
definition group.to_has_mul [coercion] {A : Type} (H : group A) : has_mul A := _
|
||||
local attribute group.to_has_inv [coercion]
|
||||
definition group.to_has_mul {A : Type} (H : group A) : has_mul A := _
|
||||
local attribute group.to_has_mul group.to_has_inv [coercion]
|
||||
|
||||
universe variable l
|
||||
variables {A B : Type.{l}}
|
||||
|
|
@ -39,7 +39,7 @@ namespace algebra
|
|||
from λg, !mul_inv_cancel_right⁻¹,
|
||||
cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4,
|
||||
cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4,
|
||||
rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul,foo)],
|
||||
rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul',foo)],
|
||||
have same_mul : Gm = Hm, from eq_of_homotopy2 same_mul',
|
||||
cases same_mul,
|
||||
have same_one : G1 = H1, from calc
|
||||
|
|
@ -58,24 +58,24 @@ namespace algebra
|
|||
cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity
|
||||
end
|
||||
|
||||
definition group_pathover {G : group A} {H : group B} {f : A ≃ B}
|
||||
: (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
|
||||
definition group_pathover {G : group A} {H : group B} {p : A = B}
|
||||
(resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H :=
|
||||
begin
|
||||
revert H,
|
||||
eapply (rec_on_ua_idp' f),
|
||||
intros H resp_mul,
|
||||
esimp [equiv.refl] at resp_mul, esimp,
|
||||
apply pathover_idp_of_eq, apply group_eq,
|
||||
exact resp_mul
|
||||
induction p,
|
||||
apply pathover_idp_of_eq, exact group_eq (resp_mul)
|
||||
end
|
||||
|
||||
definition Group_eq_of_eq {G H : Group} (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 (apo011 mk p),
|
||||
exact group_pathover resp_mul
|
||||
end
|
||||
|
||||
definition Group_eq {G H : Group} (f : carrier G ≃ carrier H)
|
||||
(resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
|
||||
begin
|
||||
cases G with Gc G, cases H with Hc H,
|
||||
apply (apo011 mk (ua f)),
|
||||
apply group_pathover, exact resp_mul
|
||||
end
|
||||
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
|
||||
|
|
|
|||
|
|
@ -57,13 +57,20 @@ namespace trunc
|
|||
definition trunc_functor [unfold 5] (f : X → Y) : trunc n X → trunc n Y :=
|
||||
λxx, trunc.rec_on xx (λx, tr (f x))
|
||||
|
||||
definition trunc_functor_compose (f : X → Y) (g : Y → Z)
|
||||
definition trunc_functor_compose [unfold 7] (f : X → Y) (g : Y → Z)
|
||||
: trunc_functor n (g ∘ f) ~ trunc_functor n g ∘ trunc_functor n f :=
|
||||
λxx, trunc.rec_on xx (λx, idp)
|
||||
|
||||
definition trunc_functor_id : trunc_functor n (@id A) ~ id :=
|
||||
λxx, trunc.rec_on xx (λx, idp)
|
||||
|
||||
definition trunc_functor_cast {X Y : Type} (n : ℕ₋₂) (p : X = Y) :
|
||||
trunc_functor n (cast p) ~ cast (ap (trunc n) p) :=
|
||||
begin
|
||||
intro x, induction x with x, esimp,
|
||||
exact fn_tr_eq_tr_fn p (λy, tr) x ⬝ !tr_compose
|
||||
end
|
||||
|
||||
definition is_equiv_trunc_functor [constructor] (f : X → Y) [H : is_equiv f]
|
||||
: is_equiv (trunc_functor n f) :=
|
||||
adjointify _
|
||||
|
|
@ -98,8 +105,11 @@ namespace trunc
|
|||
|
||||
/- Propositional truncation -/
|
||||
|
||||
definition ttrunc [constructor] (n : ℕ₋₂) (X : Type) : n-Type :=
|
||||
trunctype.mk (trunc n X) _
|
||||
|
||||
-- should this live in Prop?
|
||||
definition merely [reducible] [constructor] (A : Type) : Prop := trunctype.mk (trunc -1 A) _
|
||||
definition merely [reducible] [constructor] (A : Type) : Prop := ttrunc -1 A
|
||||
|
||||
notation `||`:max A `||`:0 := merely A
|
||||
notation `∥`:max A `∥`:0 := merely A
|
||||
|
|
|
|||
|
|
@ -254,7 +254,7 @@ namespace circle
|
|||
open nat
|
||||
definition homotopy_group_of_circle (n : ℕ) : πg[n+1 +1] S¹. = G0 :=
|
||||
begin
|
||||
refine @trivial_homotopy_of_is_set_loop_space S¹. 1 n _,
|
||||
refine @trivial_homotopy_add_of_is_set_loop_space S¹. 1 n _,
|
||||
apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -171,7 +171,7 @@ namespace homotopy
|
|||
(Πa : A, P a) (unit → P (Point A)) (P (Point A))
|
||||
(λs x, s (Point A)) (λf, f unit.star)
|
||||
(is_conn_map.rec (is_conn_map_from_unit n A (Point A)) P)
|
||||
(to_is_equiv (unit.unit_imp_equiv (P (Point A))))
|
||||
(to_is_equiv (arrow_unit_left (P (Point A))))
|
||||
|
||||
protected definition elim : P (Point A) → (Πa : A, P a) :=
|
||||
@is_equiv.inv _ _ (λs, s (Point A)) rec
|
||||
|
|
@ -191,7 +191,7 @@ namespace homotopy
|
|||
(fiber (λs x, s (Point A)) (λx, p))
|
||||
(fiber (λs, s (Point A)) p)
|
||||
k
|
||||
(equiv.symm (fiber.equiv_postcompose (to_fun (unit.unit_imp_equiv (P (Point A))))))
|
||||
(equiv.symm (fiber.equiv_postcompose (to_fun (arrow_unit_left (P (Point A))))))
|
||||
(is_conn_map.elim_general (is_conn_map_from_unit n A (Point A)) P (λx, p))
|
||||
end
|
||||
end is_conn
|
||||
|
|
|
|||
|
|
@ -328,7 +328,7 @@ namespace equiv
|
|||
equiv.mk (transport P p) !is_equiv_tr
|
||||
|
||||
definition equiv_of_eq [constructor] {A B : Type} (p : A = B) : A ≃ B :=
|
||||
equiv_ap (λX, X) p
|
||||
equiv.mk (cast p) !is_equiv_tr
|
||||
|
||||
definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y :=
|
||||
(left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
|
||||
|
|
|
|||
|
|
@ -499,7 +499,7 @@ namespace eq
|
|||
by induction r; exact !idp_con⁻¹
|
||||
|
||||
definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
|
||||
f y (p ▸ z) = (p ▸ (f x z)) :=
|
||||
f y (p ▸ z) = p ▸ f x z :=
|
||||
by induction p; reflexivity
|
||||
|
||||
/- Transporting in particular fibrations -/
|
||||
|
|
|
|||
|
|
@ -77,7 +77,7 @@ namespace pointed
|
|||
definition ploop_space [reducible] [constructor] (A : Type*) : Type* :=
|
||||
pointed.mk' (point A = point A)
|
||||
|
||||
definition iterated_ploop_space [unfold 1] [reducible] : ℕ → Type* → Type*
|
||||
definition iterated_ploop_space [reducible] : ℕ → Type* → Type*
|
||||
| iterated_ploop_space 0 X := X
|
||||
| iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X)
|
||||
|
||||
|
|
@ -357,39 +357,18 @@ namespace pointed
|
|||
{ esimp [iterated_ploop_space], exact ap1 IH}
|
||||
end
|
||||
|
||||
prefix `Ω→`:(max+5) := ap1
|
||||
notation `Ω→[`:95 n:0 `] `:0 f:95 := apn n f
|
||||
|
||||
definition apn_zero (f : map₊ A B) : Ω→[0] f = f := idp
|
||||
definition apn_succ (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp
|
||||
|
||||
definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
|
||||
proof pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) qed
|
||||
|
||||
definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
|
||||
pmap.mk eq.inverse idp
|
||||
|
||||
/- properties about these instances -/
|
||||
|
||||
definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
|
||||
begin
|
||||
induction B with B b, induction f with f pf, esimp at *, cases pf, esimp,
|
||||
apply is_equiv.homotopy_closed (ap f),
|
||||
intro p, exact !idp_con⁻¹
|
||||
end
|
||||
|
||||
definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
|
||||
begin
|
||||
induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
|
||||
induction pg, induction pf,
|
||||
fconstructor,
|
||||
{ intro p, esimp, apply whisker_left, exact ap_compose g f p ⬝ ap (ap g) !idp_con⁻¹},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
|
||||
begin
|
||||
fconstructor,
|
||||
{ intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
|
||||
refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
|
||||
exact !inv_inv⁻¹},
|
||||
{ induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
|
||||
end
|
||||
|
||||
/- categorical properties of pointed homotopies -/
|
||||
|
||||
protected definition phomotopy.refl [constructor] [refl] (f : A →* B) : f ~* f :=
|
||||
|
|
@ -420,6 +399,81 @@ namespace pointed
|
|||
infix ` ⬝* `:75 := phomotopy.trans
|
||||
postfix `⁻¹*`:(max+1) := phomotopy.symm
|
||||
|
||||
/- properties about the given pointed maps -/
|
||||
|
||||
definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) :=
|
||||
begin
|
||||
induction B with B b, induction f with f pf, esimp at *, cases pf, esimp,
|
||||
apply is_equiv.homotopy_closed (ap f),
|
||||
intro p, exact !idp_con⁻¹
|
||||
end
|
||||
|
||||
definition is_equiv_apn {A B : Type*} (n : ℕ) (f : A →* B) [H : is_equiv f]
|
||||
: is_equiv (apn n f) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ exact H},
|
||||
{ exact is_equiv_ap1 (apn n f)}
|
||||
end
|
||||
|
||||
definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro p, esimp, refine !idp_con ⬝ !ap_id},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition ap1_pinverse {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro p, esimp, refine !idp_con ⬝ _, exact !inverse_eq_inverse2⁻¹ },
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition ap1_compose (g : B →* C) (f : A →* B) : ap1 (g ∘* f) ~* ap1 g ∘* ap1 f :=
|
||||
begin
|
||||
induction B, induction C, induction g with g pg, induction f with f pf, esimp at *,
|
||||
induction pg, induction pf,
|
||||
fconstructor,
|
||||
{ intro p, esimp, apply whisker_left, exact ap_compose g f p ⬝ ap (ap g) !idp_con⁻¹},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition ap1_compose_pinverse (f : A →* B) : ap1 f ∘* pinverse ~* pinverse ∘* ap1 f :=
|
||||
begin
|
||||
fconstructor,
|
||||
{ intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
|
||||
refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
|
||||
exact !inv_inv⁻¹},
|
||||
{ induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
|
||||
end
|
||||
|
||||
theorem ap1_con (f : A →* B) (p q : Ω A) : ap1 f (p ⬝ q) = ap1 f p ⬝ ap1 f q :=
|
||||
begin
|
||||
rewrite [▸*,ap_con, +con.assoc, con_inv_cancel_left], repeat apply whisker_left
|
||||
end
|
||||
|
||||
theorem ap1_inv (f : A →* B) (p : Ω A) : ap1 f p⁻¹ = (ap1 f p)⁻¹ :=
|
||||
begin
|
||||
rewrite [▸*,ap_inv, +con_inv, inv_inv, +con.assoc], repeat apply whisker_left
|
||||
end
|
||||
|
||||
definition pcast_ap_loop_space {A B : Type*} (p : A = B)
|
||||
: pcast (ap ploop_space p) ~* Ω→ (pcast p) :=
|
||||
begin
|
||||
induction p, exact !ap1_id⁻¹*
|
||||
end
|
||||
|
||||
definition pinverse_con [constructor] {X : Type*} (p q : Ω X)
|
||||
: pinverse (p ⬝ q) = pinverse q ⬝ pinverse p :=
|
||||
!con_inv
|
||||
|
||||
definition pinverse_inv [constructor] {X : Type*} (p : Ω X)
|
||||
: pinverse p⁻¹ = (pinverse p)⁻¹ :=
|
||||
idp
|
||||
|
||||
/- more on pointed homotopies -/
|
||||
|
||||
definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g :=
|
||||
phomotopy.mk (ap010 pmap.to_fun p) begin induction p, apply idp_con end
|
||||
|
||||
|
|
@ -452,20 +506,6 @@ namespace pointed
|
|||
(q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g :=
|
||||
pwhisker_left _ p ⬝* pwhisker_right _ q
|
||||
|
||||
definition ap1_pinverse {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro p, esimp, refine !idp_con ⬝ _, exact !inverse_eq_inverse2⁻¹ },
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro p, esimp, refine !idp_con ⬝ !ap_id},
|
||||
{ reflexivity}
|
||||
end
|
||||
|
||||
definition eq_of_phomotopy (p : f ~* g) : f = g :=
|
||||
begin
|
||||
fapply pmap_eq,
|
||||
|
|
@ -497,6 +537,13 @@ namespace pointed
|
|||
{ refine ap1_phomotopy IH ⬝* _, apply ap1_compose}
|
||||
end
|
||||
|
||||
theorem apn_con (n : ℕ) (f : A →* B) (p q : Ω[n+1] A)
|
||||
: apn (n+1) f (p ⬝ q) = apn (n+1) f p ⬝ apn (n+1) f q :=
|
||||
by rewrite [+apn_succ, ap1_con]
|
||||
|
||||
theorem apn_inv (n : ℕ) (f : A →* B) (p : Ω[n+1] A) : apn (n+1) f p⁻¹ = (apn (n+1) f p)⁻¹ :=
|
||||
by rewrite [+apn_succ, ap1_inv]
|
||||
|
||||
infix ` ⬝*p `:75 := pconcat_eq
|
||||
infix ` ⬝p* `:75 := eq_pconcat
|
||||
|
||||
|
|
|
|||
|
|
@ -86,6 +86,9 @@ namespace pointed
|
|||
definition loop_space_pequiv [constructor] (p : A ≃* B) : Ω A ≃* Ω B :=
|
||||
pequiv_of_pmap (ap1 p) (is_equiv_ap1 p)
|
||||
|
||||
definition iterated_loop_space_pequiv [constructor] (n : ℕ) (p : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
|
||||
pequiv_of_pmap (apn n p) (is_equiv_apn n p)
|
||||
|
||||
definition pequiv_eq {p q : A ≃* B} (H : p = q :> (A →* B)) : p = q :=
|
||||
begin
|
||||
cases p with f Hf, cases q with g Hg, esimp at *,
|
||||
|
|
|
|||
|
|
@ -204,8 +204,8 @@ namespace sum
|
|||
A × (B + C) ≃ (A × B) + (A × C) :=
|
||||
calc A × (B + C) ≃ (B + C) × A : prod_comm_equiv
|
||||
... ≃ (B × A) + (C × A) : sum_prod_right_distrib
|
||||
... ≃ (A × B) + (C × A) : prod_comm_equiv
|
||||
... ≃ (A × B) + (A × C) : prod_comm_equiv
|
||||
... ≃ (A × B) + (C × A) : sum_equiv_sum_right !prod_comm_equiv
|
||||
... ≃ (A × B) + (A × C) : sum_equiv_sum_left !prod_comm_equiv
|
||||
|
||||
section
|
||||
variables (H : unit + A ≃ unit + B)
|
||||
|
|
|
|||
|
|
@ -356,6 +356,14 @@ namespace is_trunc
|
|||
apply iff.mp !is_trunc_iff_is_contr_loop H
|
||||
end
|
||||
|
||||
theorem is_trunc_loop_of_is_trunc (n : ℕ₋₂) (k : ℕ) (A : Type*) [H : is_trunc n A] :
|
||||
is_trunc n (Ω[k] A) :=
|
||||
begin
|
||||
induction k with k IH,
|
||||
{ exact H},
|
||||
{ apply is_trunc_eq}
|
||||
end
|
||||
|
||||
end is_trunc open is_trunc is_trunc.trunc_index
|
||||
|
||||
namespace trunc
|
||||
|
|
@ -452,6 +460,10 @@ namespace trunc
|
|||
: ptrunc n X →* ptrunc n Y :=
|
||||
pmap.mk (trunc_functor n f) (ap tr (respect_pt f))
|
||||
|
||||
definition ptrunc_pequiv [constructor] (n : ℕ₋₂) {X Y : Type*} (H : X ≃* Y)
|
||||
: ptrunc n X ≃* ptrunc n Y :=
|
||||
pequiv_of_equiv (trunc_equiv_trunc n H) (ap tr (respect_pt H))
|
||||
|
||||
definition loop_ptrunc_pequiv [constructor] (n : ℕ₋₂) (A : Type*) :
|
||||
Ω (ptrunc (n+1) A) ≃* ptrunc n (Ω A) :=
|
||||
pequiv_of_equiv !tr_eq_tr_equiv idp
|
||||
|
|
@ -467,12 +479,38 @@ namespace trunc
|
|||
rewrite succ_add_nat}
|
||||
end
|
||||
|
||||
definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z)
|
||||
(f : X →* Y) : ptrunc_functor n (g ∘* f) ~* ptrunc_functor n g ∘* ptrunc_functor n f :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ apply trunc_functor_compose},
|
||||
{ esimp, refine !idp_con ⬝ _, refine whisker_right !ap_compose'⁻¹ᵖ _ ⬝ _,
|
||||
esimp, refine whisker_right (ap_compose' tr g _) _ ⬝ _, exact !ap_con⁻¹},
|
||||
end
|
||||
|
||||
definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) :
|
||||
ptrunc_functor n (pid X) ~* pid (ptrunc n X) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ apply trunc_functor_id},
|
||||
{ reflexivity},
|
||||
end
|
||||
|
||||
definition ptrunc_functor_pcast [constructor] {X Y : Type*} (n : ℕ₋₂) (p : X = Y) :
|
||||
ptrunc_functor n (pcast p) ~* pcast (ap (ptrunc n) p) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro x, esimp, refine !trunc_functor_cast ⬝ _, refine ap010 cast _ x,
|
||||
refine !ap_compose'⁻¹ ⬝ !ap_compose'},
|
||||
{ induction p, reflexivity},
|
||||
end
|
||||
|
||||
end trunc open trunc
|
||||
|
||||
namespace function
|
||||
variables {A B : Type}
|
||||
definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
|
||||
λb, !center
|
||||
λb, begin esimp, apply center end
|
||||
|
||||
definition is_equiv_equiv_is_embedding_times_is_surjective [constructor] (f : A → B)
|
||||
: is_equiv f ≃ (is_embedding f × is_surjective f) :=
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ namespace unit
|
|||
protected definition eta : Π(u : unit), ⋆ = u
|
||||
| eta ⋆ := idp
|
||||
|
||||
definition unit_equiv_option_empty : unit ≃ option empty :=
|
||||
definition unit_equiv_option_empty [constructor] : unit ≃ option empty :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro u, exact none},
|
||||
|
|
@ -22,14 +22,8 @@ namespace unit
|
|||
{ intro u, cases u, reflexivity},
|
||||
end
|
||||
|
||||
definition unit_imp_equiv (A : Type) : (unit → A) ≃ A :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
{ intro f, exact f star},
|
||||
{ intro a u, exact a},
|
||||
{ intro a, reflexivity},
|
||||
{ intro f, apply eq_of_homotopy, intro u, cases u, reflexivity},
|
||||
end
|
||||
-- equivalences involving unit and other type constructors are in the file
|
||||
-- of the other constructor
|
||||
|
||||
end unit
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue