From e019097fed03e0a474a9caf3f769365ef68d9139 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Sep 2018 16:03:59 +0200 Subject: [PATCH] update after changes in Lean --- cohomology/serre.hlean | 2 +- homotopy/EM.hlean | 10 +++---- homotopy/dsmash.hlean | 61 ++---------------------------------------- 3 files changed, 6 insertions(+), 67 deletions(-) diff --git a/cohomology/serre.hlean b/cohomology/serre.hlean index 235115e..8822393 100644 --- a/cohomology/serre.hlean +++ b/cohomology/serre.hlean @@ -31,7 +31,7 @@ begin { apply is_conn_fun_trunc_elim, apply is_conn_fun_tr }, { have is_trunc (n+1) (ptrunc n.+1 A), from !is_trunc_trunc, have is_trunc ((n+1).+1) (ptrunc n A), by do 2 apply is_trunc_succ, apply is_trunc_trunc, - apply is_trunc_pfiber } + exact is_trunc_pfiber _ _ _ _ } end end diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index ba94e0c..ee2fa6a 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -673,7 +673,7 @@ namespace EM open fiber definition is_trunc_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_trunc 1 (pfiber (EM1_functor φ)) := - !is_trunc_fiber + is_trunc_pfiber _ _ _ _ definition is_conn_fiber_EM1_functor {G H : Group} (φ : G →g H) : is_conn -1 (pfiber (EM1_functor φ)) := @@ -683,9 +683,7 @@ namespace EM definition is_trunc_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_trunc (n+1) (pfiber (EMadd1_functor φ n)) := - begin - apply is_trunc_fiber - end + is_trunc_pfiber _ _ _ _ definition is_conn_fiber_EMadd1_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_conn (n.-1) (pfiber (EMadd1_functor φ n)) := @@ -696,9 +694,7 @@ namespace EM definition is_trunc_fiber_EM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_trunc n (pfiber (EM_functor φ n)) := - begin - apply is_trunc_fiber - end + is_trunc_pfiber _ _ _ _ definition is_conn_fiber_EM_functor {G H : AbGroup} (φ : G →g H) (n : ℕ) : is_conn (n.-2) (pfiber (EM_functor φ n)) := diff --git a/homotopy/dsmash.hlean b/homotopy/dsmash.hlean index 7913519..bce9d10 100644 --- a/homotopy/dsmash.hlean +++ b/homotopy/dsmash.hlean @@ -1651,7 +1651,7 @@ open is_trunc sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (f pt))⁻¹ᵉ ⬝e sigma_equiv_sigma_right (λh₂, sigma_equiv_sigma_right (λr₂, - sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep) ⬝e !sigma_comm_equiv) ⬝e + sigma_equiv_sigma_right (λh₁, !comm_equiv_constant) ⬝e !sigma_comm_equiv) ⬝e !sigma_comm_equiv) ⬝e !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λr, @@ -1661,7 +1661,7 @@ open is_trunc sigma_equiv_sigma_left (pi_equiv_pi_right (λa, equiv_eq_closed_right _ r)) ⬝e sigma_equiv_sigma_right (λh₁, !eq_equiv_con_inv_eq_idp⁻¹ᵉ)) ⬝e !sigma_comm_equiv ⬝e - sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep)) ⬝e + sigma_equiv_sigma_right (λh₁, !comm_equiv_constant)) ⬝e !sigma_comm_equiv) ⬝e !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₁, !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₂, @@ -1675,63 +1675,6 @@ open is_trunc definition dsmash_pelim_equiv' (B : A → Type*) (C : Type*) : ppmap (⋀ B) C ≃ Π*a, B a →** C := dsmash_pelim_equiv B C ⬝e (ppi_equiv_dbpmap B (λa, C))⁻¹ᵉ -exit - definition dsmash_arrow_equiv2 [constructor] (B : A → Type*) (C : Type) : - (⋀ B → C) ≃ Σ(f : Πa, B a → C) (c₀ : C) (p : Πa, f a pt = c₀) (q : Πb, f pt b = c₀), p pt = q pt := - begin - fapply equiv.MK, - { intro f, exact ⟨λa b, f (dsmash.mk a b), f auxr, f auxl, (λa, ap f (gluel a), λb, ap f (gluer b))⟩ }, - { intro x, exact dsmash.elim x.1 x.2.2.1 x.2.1 x.2.2.2.1 x.2.2.2.2 }, - { intro x, induction x with f x, induction x with c₁ x, induction x with c₀ x, induction x with p₁ p₂, - apply ap (dpair _), apply ap (dpair _), apply ap (dpair _), esimp, - exact pair_eq (eq_of_homotopy (elim_gluel _ _)) (eq_of_homotopy (elim_gluer _ _)) }, - { intro f, apply eq_of_homotopy, intro x, induction x, reflexivity, reflexivity, reflexivity, - apply eq_pathover, apply hdeg_square, apply elim_gluel, - apply eq_pathover, apply hdeg_square, apply elim_gluer } - end - definition dsmash_arrow_equiv2_inv_pt [constructor] - (x : Σ(f : Πa, B a → C) (c₁ : C) (c₀ : C), (Πa, f a pt = c₀) × (Πb, f pt b = c₁)) : - to_inv (dsmash_arrow_equiv B C) x pt = x.1 pt pt := - by reflexivity - - open pi - - definition dsmash_pmap_equiv2 (B : A → Type*) (C : Type*) : - (⋀ B →* C) ≃ dbppmap B (λa, C) := - begin - refine !pmap.sigma_char ⬝e _, - refine sigma_equiv_sigma_left !dsmash_arrow_equiv ⬝e _, - refine sigma_equiv_sigma_right (λx, equiv_eq_closed_left _ (dsmash_arrow_equiv_inv_pt x)) ⬝e _, - refine !sigma_assoc_equiv ⬝e _, - refine sigma_equiv_sigma_right (λf, !sigma_assoc_equiv ⬝e - sigma_equiv_sigma_right (λc₁, !sigma_assoc_equiv ⬝e - sigma_equiv_sigma_right (λc₂, sigma_equiv_sigma_left !sigma.equiv_prod⁻¹ᵉ ⬝e - !sigma_assoc_equiv) ⬝e - sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (λa, f a pt))⁻¹ᵉ ⬝e - sigma_equiv_sigma_right (λh₁, !sigma_comm_equiv) ⬝e !sigma_comm_equiv) ⬝e - sigma_assoc_equiv_left _ (sigma_homotopy_constant_equiv pt (f pt))⁻¹ᵉ ⬝e - sigma_equiv_sigma_right (λh₂, - sigma_equiv_sigma_right (λr₂, - sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep) ⬝e !sigma_comm_equiv) ⬝e - !sigma_comm_equiv) ⬝e - !sigma_comm_equiv ⬝e - sigma_equiv_sigma_right (λr, - sigma_equiv_sigma_left (pi_equiv_pi_right (λb, equiv_eq_closed_right _ r)) ⬝e - sigma_equiv_sigma_right (λh₂, - sigma_equiv_sigma !eq_equiv_con_inv_eq_idp⁻¹ᵉ (λr₂, - sigma_equiv_sigma_left (pi_equiv_pi_right (λa, equiv_eq_closed_right _ r)) ⬝e - sigma_equiv_sigma_right (λh₁, !eq_equiv_con_inv_eq_idp⁻¹ᵉ)) ⬝e - !sigma_comm_equiv ⬝e - sigma_equiv_sigma_right (λh₁, !comm_equiv_nondep)) ⬝e - !sigma_comm_equiv) ⬝e - !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₁, - !sigma_comm_equiv ⬝e sigma_equiv_sigma_right (λh₂, - !sigma_sigma_eq_right))) ⬝e _, - refine !sigma_assoc_equiv' ⬝e _, - refine sigma_equiv_sigma_left (@sigma_pi_equiv_pi_sigma _ _ (λa f, f pt = pt) ⬝e - pi_equiv_pi_right (λa, !pmap.sigma_char⁻¹ᵉ)) ⬝e _, - exact !dbpmap.sigma_char⁻¹ᵉ - end end dsmash