define atiyah-hirzebruch exact couple
this commit also defines str and strunc_elim proving that the exact couple is bounded, and that it converges to the right this is still todo
This commit is contained in:
Floris van Doorn
parent
d23466396d
commit
f54011335d
4 changed files with 177 additions and 116 deletions
|
|
@ -1,6 +1,6 @@
|
|||
import ..algebra.module_exact_couple .strunc
|
||||
|
||||
open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift
|
||||
open eq spectrum trunc is_trunc pointed int EM algebra left_module fiber lift equiv is_equiv
|
||||
|
||||
/- Eilenberg MacLane spaces are the fibers of the Postnikov system of a type -/
|
||||
|
||||
|
|
@ -37,6 +37,14 @@ definition postnikov_map_natural {A B : Type*} (f : A →* B) (n : ℕ₋₂) :
|
|||
(ptrunc_functor (n.+1) f) (ptrunc_functor n f) :=
|
||||
!ptrunc_functor_postnikov_map ⬝* !ptrunc_elim_ptrunc_functor⁻¹*
|
||||
|
||||
definition is_equiv_postnikov_map (A : Type*) {n k : ℕ₋₂} [HA : is_trunc k A] (H : k ≤ n) :
|
||||
is_equiv (postnikov_map A n) :=
|
||||
begin
|
||||
apply is_equiv_of_equiv_of_homotopy
|
||||
(ptrunc_pequiv_ptrunc_of_is_trunc (trunc_index.le.step H) H HA),
|
||||
intro x, induction x, reflexivity
|
||||
end
|
||||
|
||||
definition encode_ap1_gen_tr (n : ℕ₋₂) {A : Type*} {a a' : A} (p : a = a') :
|
||||
trunc.encode (ap1_gen tr idp idp p) = tr p :> trunc n (a = a') :=
|
||||
by induction p; reflexivity
|
||||
|
|
@ -54,63 +62,34 @@ begin
|
|||
end,
|
||||
this⁻¹ᵛ*
|
||||
|
||||
definition is_strunc_strunc_pred (X : spectrum) (k : ℤ) : is_strunc k (strunc (k - 1) X) :=
|
||||
λn, @(is_trunc_of_le _ (maxm2_monotone (add_le_add_right (sub_one_le k) n))) !is_strunc_strunc
|
||||
|
||||
-- definition postnikov_map_int (X : Type*) (k : ℤ) :
|
||||
-- ptrunc (maxm2 (k + 1)) X →* ptrunc (maxm2 k) X :=
|
||||
-- begin
|
||||
-- induction k with k k,
|
||||
-- exact postnikov_map X k,
|
||||
-- exact !pconst
|
||||
-- end
|
||||
definition postnikov_smap [constructor] (X : spectrum) (k : ℤ) :
|
||||
strunc k X →ₛ strunc (k - 1) X :=
|
||||
strunc_elim (str (k - 1) X) (is_strunc_strunc_pred X k)
|
||||
|
||||
-- definition postnikov_map_int_natural {A B : Type*} (f : A →* B) (k : ℤ) :
|
||||
-- psquare (postnikov_map_int A k) (postnikov_map_int B k)
|
||||
-- (ptrunc_int_functor (k+1) f) (ptrunc_int_functor k f) :=
|
||||
-- begin
|
||||
-- induction k with k k,
|
||||
-- exact postnikov_map_natural f k,
|
||||
-- apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
|
||||
-- end
|
||||
definition postnikov_smap_phomotopy [constructor] (X : spectrum) (k : ℤ) (n : ℤ) :
|
||||
postnikov_smap X k n ~* postnikov_map (X n) (maxm2 (k - 1 + n)) ∘*
|
||||
sorry :=
|
||||
sorry
|
||||
|
||||
-- definition postnikov_map_int_natural_pequiv {A B : Type*} (f : A ≃* B) (k : ℤ) :
|
||||
-- psquare (postnikov_map_int A k) (postnikov_map_int B k)
|
||||
-- (ptrunc_int_pequiv_ptrunc_int (k+1) f) (ptrunc_int_pequiv_ptrunc_int k f) :=
|
||||
-- begin
|
||||
-- induction k with k k,
|
||||
-- exact postnikov_map_natural f k,
|
||||
-- apply psquare_of_phomotopy, exact !pcompose_pconst ⬝* !pconst_pcompose⁻¹*
|
||||
-- end
|
||||
section atiyah_hirzebruch
|
||||
parameters {X : Type*} (Y : X → spectrum) (s₀ : ℤ) (H : Πx, is_strunc s₀ (Y x))
|
||||
|
||||
-- definition pequiv_ap_natural2 {X A : Type} (B C : X → A → Type*) {a a' : X → A}
|
||||
-- (p : a ~ a')
|
||||
-- (s : X → X) (f : Πx a, B x a →* C (s x) a) (x : X) :
|
||||
-- psquare (pequiv_ap (B x) (p x)) (pequiv_ap (C (s x)) (p x)) (f x (a x)) (f x (a' x)) :=
|
||||
-- begin induction p using homotopy.rec_on_idp, exact phrfl end
|
||||
definition atiyah_hirzebruch_exact_couple : exact_couple rℤ Z2 :=
|
||||
@exact_couple_sequence (λs, strunc s (spi X Y)) (postnikov_smap (spi X Y))
|
||||
|
||||
-- definition pequiv_ap_natural3 {X A : Type} (B C : X → A → Type*) {a a' : A}
|
||||
-- (p : a = a')
|
||||
-- (s : X → X) (x : X) (f : Πx a, B x a →* C (s x) a) :
|
||||
-- psquare (pequiv_ap (B x) p) (pequiv_ap (C (s x)) p) (f x a) (f x a') :=
|
||||
-- begin induction p, exact phrfl end
|
||||
definition is_bounded_atiyah_hirzebruch : is_bounded atiyah_hirzebruch_exact_couple :=
|
||||
is_bounded_sequence _ s₀ (λn, n - 1)
|
||||
begin
|
||||
intro s n H,
|
||||
exact sorry
|
||||
end
|
||||
begin
|
||||
intro s n H, apply trivial_shomotopy_group_of_is_strunc,
|
||||
apply is_strunc_strunc,
|
||||
exact lt_of_le_sub_one H,
|
||||
end
|
||||
|
||||
-- definition postnikov_smap (X : spectrum) (k : ℤ) :
|
||||
-- strunc (k+1) X →ₛ strunc k X :=
|
||||
-- smap.mk (λn, postnikov_map_int (X n) (k + n) ∘* ptrunc_int_change_int _ !norm_num.add_comm_middle)
|
||||
-- (λn, begin
|
||||
-- exact sorry
|
||||
-- -- exact (_ ⬝vp* !ap1_pequiv_ap) ⬝h* (!postnikov_map_int_natural_pequiv ⬝v* _ ⬝v* _) ⬝vp* !ap1_pcompose,
|
||||
-- end)
|
||||
|
||||
|
||||
-- section atiyah_hirzebruch
|
||||
-- parameters {X : Type*} (Y : X → spectrum)
|
||||
|
||||
-- definition atiyah_hirzebruch_exact_couple : exact_couple rℤ spectrum.I :=
|
||||
-- @exact_couple_sequence (λs, strunc s (spi X (λx, Y x)))
|
||||
-- (λs, !postnikov_smap ∘ₛ strunc_change_int _ !succ_pred⁻¹)
|
||||
|
||||
-- -- parameters (k : ℕ) (H : Π(x : X) (n : ℕ), is_trunc (k + n) (Y x n))
|
||||
|
||||
|
||||
|
||||
-- end atiyah_hirzebruch
|
||||
end atiyah_hirzebruch
|
||||
|
|
|
|||
|
|
@ -1,10 +1,9 @@
|
|||
import .spectrum .EM
|
||||
|
||||
-- TODO move this
|
||||
open trunc_index nat
|
||||
|
||||
namespace int
|
||||
|
||||
-- TODO move this
|
||||
open trunc_index nat algebra
|
||||
section
|
||||
private definition maxm2_le.lemma₁ {n k : ℕ} : n+(1:int) + -[1+ k] ≤ n :=
|
||||
le.intro (
|
||||
|
|
@ -39,13 +38,29 @@ open int trunc eq is_trunc lift unit pointed equiv is_equiv algebra EM
|
|||
|
||||
namespace spectrum
|
||||
|
||||
definition ptrunc_maxm2_change_int {k l : ℤ} (X : Type*) (p : k = l)
|
||||
definition ptrunc_maxm2_change_int {k l : ℤ} (p : k = l) (X : Type*)
|
||||
: ptrunc (maxm2 k) X ≃* ptrunc (maxm2 l) X :=
|
||||
pequiv_ap (λ n, ptrunc (maxm2 n) X) p
|
||||
|
||||
definition loop_ptrunc_maxm2_pequiv (k : ℤ) (X : Type*) :
|
||||
Ω (ptrunc (maxm2 (k+1)) X) ≃* ptrunc (maxm2 k) (Ω X) :=
|
||||
definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
|
||||
: is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
|
||||
by induction p; exact id
|
||||
|
||||
definition is_trunc_maxm2_loop {k : ℤ} {A : Type*} (H : is_trunc (maxm2 (k+1)) A) :
|
||||
is_trunc (maxm2 k) (Ω A) :=
|
||||
begin
|
||||
induction k with k k,
|
||||
apply is_trunc_loop, exact H,
|
||||
apply is_contr_loop,
|
||||
cases k with k,
|
||||
{ exact H },
|
||||
{ apply is_trunc_succ, apply is_trunc_succ, exact H }
|
||||
end
|
||||
|
||||
definition loop_ptrunc_maxm2_pequiv {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l) (X : Type*) :
|
||||
Ω (ptrunc l X) ≃* ptrunc (maxm2 k) (Ω X) :=
|
||||
begin
|
||||
induction p,
|
||||
induction k with k k,
|
||||
{ exact loop_ptrunc_pequiv k X },
|
||||
{ refine pequiv_of_is_contr _ _ _ !is_trunc_trunc,
|
||||
|
|
@ -55,6 +70,43 @@ begin
|
|||
{ change is_set (trunc -2 X), apply _ }}
|
||||
end
|
||||
|
||||
definition ptrunc_elim_phomotopy2 [constructor] (k : ℕ₋₂) {A B : Type*} {f g : A →* B} (H₁ : is_trunc k B)
|
||||
(H₂ : is_trunc k B) (p : f ~* g) : @ptrunc.elim k A B H₁ f ~* @ptrunc.elim k A B H₂ g :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro x, induction x with a, exact p a },
|
||||
{ exact to_homotopy_pt p }
|
||||
end
|
||||
|
||||
definition loop_ptrunc_maxm2_pequiv_ptrunc_elim' {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
|
||||
{A B : Type*} (f : A →* B) {H : is_trunc l B} :
|
||||
Ω→ (ptrunc.elim l f) ∘* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ~*
|
||||
@ptrunc.elim (maxm2 k) _ _ (is_trunc_maxm2_loop (is_trunc_of_eq p⁻¹ H)) (Ω→ f) :=
|
||||
begin
|
||||
induction p, induction k with k k,
|
||||
{ refine pwhisker_right _ (ap1_phomotopy _) ⬝* @(ap1_ptrunc_elim k f) H,
|
||||
apply ptrunc_elim_phomotopy2, reflexivity },
|
||||
{ apply phomotopy_of_is_contr_cod, exact is_trunc_maxm2_loop H }
|
||||
end
|
||||
|
||||
definition loop_ptrunc_maxm2_pequiv_ptrunc_elim {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l)
|
||||
{A B : Type*} (f : A →* B) {H1 : is_trunc ((maxm2 k).+1) B } {H2 : is_trunc l B} :
|
||||
Ω→ (ptrunc.elim l f) ∘* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ~* ptrunc.elim (maxm2 k) (Ω→ f) :=
|
||||
begin
|
||||
induction p, induction k with k k: esimp at H1,
|
||||
{ refine pwhisker_right _ (ap1_phomotopy _) ⬝* ap1_ptrunc_elim k f,
|
||||
apply ptrunc_elim_phomotopy2, reflexivity },
|
||||
{ apply phomotopy_of_is_contr_cod }
|
||||
end
|
||||
|
||||
definition loop_ptrunc_maxm2_pequiv_ptr {k : ℤ} {l : ℕ₋₂} (p : maxm2 (k+1) = l) (A : Type*) :
|
||||
Ω→ (ptr l A) ~* (loop_ptrunc_maxm2_pequiv p A)⁻¹ᵉ* ∘* ptr (maxm2 k) (Ω A) :=
|
||||
begin
|
||||
induction p, induction k with k k,
|
||||
{ exact ap1_ptr k A },
|
||||
{ apply phomotopy_pinv_left_of_phomotopy, apply phomotopy_of_is_contr_cod, apply is_trunc_trunc }
|
||||
end
|
||||
|
||||
definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
|
||||
: is_trunc (maxm2 k) X → is_trunc (max0 k) X :=
|
||||
λ H, @is_trunc_of_le X _ _ (maxm2_le_maxm0 k) H
|
||||
|
|
@ -62,24 +114,12 @@ definition is_trunc_of_is_trunc_maxm2 (k : ℤ) (X : Type)
|
|||
definition strunc [constructor] (k : ℤ) (E : spectrum) : spectrum :=
|
||||
spectrum.MK (λ(n : ℤ), ptrunc (maxm2 (k + n)) (E n))
|
||||
(λ(n : ℤ), ptrunc_pequiv_ptrunc (maxm2 (k + n)) (equiv_glue E n)
|
||||
⬝e* (loop_ptrunc_maxm2_pequiv (k + n) (E (n+1)))⁻¹ᵉ*
|
||||
⬝e* (loop_pequiv_loop
|
||||
(ptrunc_maxm2_change_int _ (add.assoc k n 1))))
|
||||
⬝e* (loop_ptrunc_maxm2_pequiv (ap maxm2 (add.assoc k n 1)) (E (n+1)))⁻¹ᵉ*)
|
||||
|
||||
definition strunc_change_int [constructor] {k l : ℤ} (E : spectrum) (p : k = l) :
|
||||
strunc k E →ₛ strunc l E :=
|
||||
begin induction p, reflexivity end
|
||||
|
||||
definition is_trunc_maxm2_loop (A : pType) (k : ℤ)
|
||||
: is_trunc (maxm2 (k + 1)) A → is_trunc (maxm2 k) (Ω A) :=
|
||||
begin
|
||||
intro H, induction k with k k,
|
||||
{ apply is_trunc_loop, exact H },
|
||||
{ apply is_contr_loop, cases k with k,
|
||||
{ exact H },
|
||||
{ have H2 : is_contr A, from H, apply _ } }
|
||||
end
|
||||
|
||||
definition is_strunc [reducible] (k : ℤ) (E : spectrum) : Type :=
|
||||
Π (n : ℤ), is_trunc (maxm2 (k + n)) (E n)
|
||||
|
||||
|
|
@ -98,13 +138,36 @@ definition is_strunc_strunc (k : ℤ) (E : spectrum)
|
|||
: is_strunc k (strunc k E) :=
|
||||
λ n, is_trunc_trunc (maxm2 (k + n)) (E n)
|
||||
|
||||
definition is_trunc_maxm2_change_int {k l : ℤ} (X : pType) (p : k = l)
|
||||
: is_trunc (maxm2 k) X → is_trunc (maxm2 l) X :=
|
||||
by induction p; exact id
|
||||
definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
|
||||
smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
|
||||
abstract begin
|
||||
intro n,
|
||||
apply psquare_of_phomotopy,
|
||||
refine !passoc ⬝* pwhisker_left _ !ptr_natural ⬝* _,
|
||||
refine !passoc⁻¹* ⬝* pwhisker_right _ !loop_ptrunc_maxm2_pequiv_ptr⁻¹*,
|
||||
end end
|
||||
|
||||
definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
|
||||
(H : is_strunc k F) : strunc k E →ₛ F :=
|
||||
smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
|
||||
abstract begin
|
||||
intro n,
|
||||
apply psquare_of_phomotopy,
|
||||
symmetry,
|
||||
refine !passoc⁻¹* ⬝* pwhisker_right _ !loop_ptrunc_maxm2_pequiv_ptrunc_elim' ⬝* _,
|
||||
refine @(ptrunc_elim_ptrunc_functor _ _ _) _ ⬝* _,
|
||||
refine _ ⬝* @(ptrunc_elim_pcompose _ _ _) _ _,
|
||||
apply is_trunc_maxm2_loop,
|
||||
refine is_trunc_of_eq _ (H (n+1)), exact ap maxm2 (add.assoc k n 1)⁻¹,
|
||||
apply ptrunc_elim_phomotopy2,
|
||||
apply phomotopy_of_psquare,
|
||||
apply ptranspose,
|
||||
apply smap.glue_square
|
||||
end end
|
||||
|
||||
definition strunc_functor [constructor] (k : ℤ) {E F : spectrum} (f : E →ₛ F) :
|
||||
strunc k E →ₛ strunc k F :=
|
||||
smap.mk (λn, ptrunc_functor (maxm2 (k + n)) (f n)) sorry
|
||||
strunc_elim (str k F ∘ₛ f) (is_strunc_strunc k F)
|
||||
|
||||
definition is_strunc_EM_spectrum (G : AbGroup)
|
||||
: is_strunc 0 (EM_spectrum G) :=
|
||||
|
|
@ -121,11 +184,6 @@ begin
|
|||
apply is_trunc_loop, apply is_trunc_succ, exact IH }}
|
||||
end
|
||||
|
||||
definition strunc_elim [constructor] {k : ℤ} {E F : spectrum} (f : E →ₛ F)
|
||||
(H : is_strunc k F) : strunc k E →ₛ F :=
|
||||
smap.mk (λn, ptrunc.elim (maxm2 (k + n)) (f n))
|
||||
(λn, sorry)
|
||||
|
||||
definition trivial_shomotopy_group_of_is_strunc (E : spectrum)
|
||||
{n k : ℤ} (K : is_strunc n E) (H : n < k)
|
||||
: is_contr (πₛ[k] E) :=
|
||||
|
|
@ -139,11 +197,6 @@ have I : m < 2, from
|
|||
(is_trunc_of_is_trunc_maxm2 m (E (2 - k)) (K (2 - k)))
|
||||
(nat.succ_le_succ (max0_le_of_le (le_sub_one_of_lt I)))
|
||||
|
||||
definition str [constructor] (k : ℤ) (E : spectrum) : E →ₛ strunc k E :=
|
||||
smap.mk (λ n, ptr (maxm2 (k + n)) (E n))
|
||||
(λ n, sorry)
|
||||
|
||||
|
||||
structure truncspectrum (n : ℤ) :=
|
||||
(carrier : spectrum)
|
||||
(struct : is_strunc n carrier)
|
||||
|
|
|
|||
|
|
@ -209,38 +209,24 @@ namespace int
|
|||
{ exact nat.zero_le m }
|
||||
end
|
||||
|
||||
section
|
||||
-- is there a way to get this from int.add_assoc?
|
||||
private definition maxm2_monotone.lemma₁ {n k : ℕ}
|
||||
: k + n + (1:int) = k + (1:int) + n :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ reflexivity },
|
||||
{ exact ap (λ z, z + 1) IH }
|
||||
end
|
||||
definition not_neg_succ_le_of_nat {n m : ℕ} : ¬m ≤ -[1+n] :=
|
||||
by cases m: exact id
|
||||
|
||||
private definition maxm2_monotone.lemma₂ {n k : ℕ} : ¬ n ≤ -[1+ k] :=
|
||||
int.not_le_of_gt (lt.intro
|
||||
(calc -[1+ k] + (succ (k + n))
|
||||
= -(k+1) + (k + n + 1) : by reflexivity
|
||||
... = -(k+1) + (k + 1 + n) : maxm2_monotone.lemma₁
|
||||
... = (-(k+1) + (k+1)) + n : int.add_assoc
|
||||
... = (0:int) + n : by rewrite int.add_left_inv
|
||||
... = n : int.zero_add))
|
||||
|
||||
definition maxm2_monotone {n k : ℤ} : n ≤ k → maxm2 n ≤ maxm2 k :=
|
||||
definition maxm2_monotone {n m : ℤ} (H : n ≤ m) : maxm2 n ≤ maxm2 m :=
|
||||
begin
|
||||
intro H,
|
||||
induction n with n n,
|
||||
{ induction k with k k,
|
||||
{ exact trunc_index.of_nat_monotone (le_of_of_nat_le_of_nat H) },
|
||||
{ exact empty.elim (maxm2_monotone.lemma₂ H) } },
|
||||
{ induction k with k k,
|
||||
{ apply minus_two_le },
|
||||
{ apply le.tr_refl } }
|
||||
end
|
||||
{ induction m with m m,
|
||||
{ apply of_nat_le_of_nat, exact le_of_of_nat_le_of_nat H },
|
||||
{ exfalso, exact not_neg_succ_le_of_nat H }},
|
||||
{ apply minus_two_le }
|
||||
end
|
||||
|
||||
definition sub_nat_le (n : ℤ) (m : ℕ) : n - m ≤ n :=
|
||||
le.intro !sub_add_cancel
|
||||
|
||||
definition sub_one_le (n : ℤ) : n - 1 ≤ n :=
|
||||
sub_nat_le n 1
|
||||
|
||||
end int
|
||||
|
||||
namespace pmap
|
||||
|
|
@ -286,6 +272,44 @@ namespace trunc
|
|||
{ apply idp_con }
|
||||
end
|
||||
|
||||
definition ptrunc_elim_ptr_phomotopy_pid (n : ℕ₋₂) (A : Type*):
|
||||
ptrunc.elim n (ptr n A) ~* pid (ptrunc n A) :=
|
||||
begin
|
||||
fapply phomotopy.mk,
|
||||
{ intro a, induction a with a, reflexivity },
|
||||
{ apply idp_con }
|
||||
end
|
||||
|
||||
definition is_trunc_of_eq {n m : ℕ₋₂} (p : n = m) {A : Type} (H : is_trunc n A) : is_trunc m A :=
|
||||
transport (λk, is_trunc k A) p H
|
||||
|
||||
definition is_trunc_ptrunc_of_is_trunc [instance] [priority 500] (A : Type*)
|
||||
(n m : ℕ₋₂) [H : is_trunc n A] : is_trunc n (ptrunc m A) :=
|
||||
is_trunc_trunc_of_is_trunc A n m
|
||||
|
||||
definition ptrunc_pequiv_ptrunc_of_is_trunc {n m k : ℕ₋₂} {A : Type*}
|
||||
(H1 : n ≤ m) (H2 : n ≤ k) (H : is_trunc n A) : ptrunc m A ≃* ptrunc k A :=
|
||||
have is_trunc m A, from is_trunc_of_le A H1,
|
||||
have is_trunc k A, from is_trunc_of_le A H2,
|
||||
pequiv.MK (ptrunc.elim _ (ptr k A)) (ptrunc.elim _ (ptr m A))
|
||||
abstract begin
|
||||
refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
|
||||
exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
|
||||
end end
|
||||
abstract begin
|
||||
refine !ptrunc_elim_pcompose⁻¹* ⬝* _,
|
||||
exact ptrunc_elim_phomotopy _ !ptrunc_elim_ptr ⬝* !ptrunc_elim_ptr_phomotopy_pid,
|
||||
end end
|
||||
|
||||
definition ptrunc_change_index {k l : ℕ₋₂} (p : k = l) (X : Type*)
|
||||
: ptrunc k X ≃* ptrunc l X :=
|
||||
pequiv_ap (λ n, ptrunc n X) p
|
||||
|
||||
definition ptrunc_functor_le {k l : ℕ₋₂} (p : l ≤ k) (X : Type*)
|
||||
: ptrunc k X →* ptrunc l X :=
|
||||
have is_trunc k (ptrunc l X), from is_trunc_of_le _ p,
|
||||
ptrunc.elim _ (ptr l X)
|
||||
|
||||
end trunc
|
||||
|
||||
namespace sigma
|
||||
|
|
|
|||
|
|
@ -204,10 +204,15 @@ namespace pointed
|
|||
definition loop_punit : Ω punit ≃* punit :=
|
||||
loop_pequiv_punit_of_is_set punit
|
||||
|
||||
definition phomotopy_of_is_contr [constructor] {X Y: Type*} (f g : X →* Y) [is_contr Y] :
|
||||
definition phomotopy_of_is_contr_cod [constructor] {X Y : Type*} (f g : X →* Y) [is_contr Y] :
|
||||
f ~* g :=
|
||||
phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr
|
||||
|
||||
definition phomotopy_of_is_contr_dom [constructor] {X Y : Type*} (f g : X →* Y) [is_contr X] :
|
||||
f ~* g :=
|
||||
phomotopy.mk (λa, ap f !is_prop.elim ⬝ respect_pt f ⬝ (respect_pt g)⁻¹ ⬝ ap g !is_prop.elim)
|
||||
begin rewrite [▸*, is_prop_elim_self, +ap_idp, idp_con, con_idp, inv_con_cancel_right] end
|
||||
|
||||
|
||||
|
||||
end pointed
|
||||
|
|
|
|||
Loading…
Reference in a new issue