From e79063970d62229ad4d9843b6a037474749de693 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 4 Aug 2016 14:58:45 +0200 Subject: [PATCH] feat(hott) finish proof of lemma 9.9.4 --- .../category/constructions/functor.hlean | 74 +++++++++++++++---- 1 file changed, 59 insertions(+), 15 deletions(-) diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 052216554..0537f8d0a 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -412,6 +412,7 @@ namespace functor exact ap (λ x, G x ∘ γ a) Ek⁻¹ ⬝ naturality γ k ⬝ ap (λ x, γ a0 ∘ F x) Ek end + --TODO speed this up private definition fully_faithful_precomposition_naturality {b b' : carrier D} (f : hom b b') : to_fun_hom G f ∘ (fully_faithful_precomposition_functor_pair γ b).1 = (fully_faithful_precomposition_functor_pair γ b').1 ∘ to_fun_hom F f := @@ -471,7 +472,10 @@ namespace functor (k_coh : Π {a a'} h h' (f : hom a a'), to_hom h' ∘ (to_fun_hom H f) = to_hom h → to_hom (k a' h') ∘ to_fun_hom F f = to_hom (k a h)) local abbreviation X := essentially_surj_precomp_X - local abbreviation X.mk := @essentially_surj_precomp_X.mk + local abbreviation X.mk [constructor] := @essentially_surj_precomp_X.mk + local abbreviation X.c [unfold 7] := @essentially_surj_precomp_X.c + local abbreviation X.k [unfold 7] := @essentially_surj_precomp_X.k + local abbreviation X.k_coh [unfold 7] := @essentially_surj_precomp_X.k_coh section variables {c c' : carrier C} (p : c = c') @@ -523,18 +527,44 @@ namespace functor begin induction He.2 b with Hb, cases Hb with a0 Ha0, fconstructor, exact F a0, - { intro a h, apply to_fun_iso, apply iso_of_F_iso_F H, + { intro a h, apply to_fun_iso F, apply reflect_iso H, exact h ⬝i Ha0⁻¹ⁱ }, - { intros a a' h h' f HH, esimp[iso_of_F_iso_F], + { intros a a' h h' f HH, apply concat, apply !respect_comp⁻¹, apply ap (to_fun_hom F), - rewrite [-HH], + esimp, rewrite [-HH], apply concat, apply ap (λ x, _ ∘ x), apply inverse, apply left_inv (to_fun_hom H), apply concat, apply !hom_inv_respect_comp⁻¹, apply ap (hom_inv H), apply !assoc⁻¹ } end - local abbreviation G0 := λ (b), essentially_surj_precomp_X.c (X_inh b) - local abbreviation k := λ b, essentially_surj_precomp_X.k (X_inh b) - local abbreviation k_coh := λ b, @essentially_surj_precomp_X.k_coh b (X_inh b) + definition G0 [reducible] := λ (b), X.c (X_inh b) + definition k := λ b, X.k (X_inh b) + definition k_coh := λ b, @X.k_coh b (X_inh b) + + private definition X_c_eq_of_eq {b} (t t' : X b) (p : t = t') : X.c t = X.c t' := + by cases p; reflexivity + + private definition X_k_eq_of_eq {b} (t t' : X b) (p : t = t') (a : carrier A) (h : H a ≅ b) : + X_c_eq_of_eq t t' p ▸ X.k t a h = X.k t' a h:= + by cases p; reflexivity + + private definition X_phi {b} (t : X b) : X.c t = X.c (X_inh b) := + X_c_eq_of_eq _ _ !is_prop.elim + + private definition X_phi_transp {b} (t : X b) (a : carrier A) (h : H a ≅ b) : + (X_phi t) ▸ (X.k t a h) = k b a h := + by apply X_k_eq_of_eq t _ !is_prop.elim + + private definition X_phi_hom_of_eq' {b} (t t' : X b) (p : t = t') (a : carrier A) (h : H a ≅ b) : + X.k t' a h ⬝i (iso_of_eq (X_c_eq_of_eq t t' p)⁻¹) = X.k t a h := + begin + cases p, apply iso_eq, apply id_left + end + + private definition X_phi_hom_of_eq {b} (t : X b) (a : carrier A) (h : H a ≅ b) : + to_hom (k b a h ⬝i (iso_of_eq (X_phi t)⁻¹)) = to_hom (X.k t a h) := + begin + apply ap to_hom, apply X_phi_hom_of_eq' + end structure essentially_surj_precomp_Y {b b' : carrier B} (f : hom b b') : Type := (g : hom (G0 b) (G0 b')) @@ -666,31 +696,45 @@ namespace functor { intro a b c g f, apply G_hom_comp } end - private theorem G0_H_eq_F (a0 : carrier A) : G0 (H a0) = F a0 := + private definition XF (a0 : carrier A) : X (H a0) := begin - apply concat, apply ap essentially_surj_precomp_X.c, apply is_prop.elim, fconstructor, - { apply F a0 }, + { exact F a0 }, { intro a h, apply to_fun_iso F, apply reflect_iso, apply He.1, exact h }, { intro a a' h h' f l, esimp, apply concat, apply !respect_comp⁻¹, apply ap (to_fun_hom F), apply inverse, apply concat, apply ap (hom_inv H) l⁻¹, - apply concat, apply hom_inv_respect_comp, apply ap (λ x, _ ∘ x), apply left_inv }, - reflexivity + apply concat, apply hom_inv_respect_comp, apply ap (λ x, _ ∘ x), apply left_inv } + end + + private definition G0_H_eq_F (a0 : carrier A) : G0 (H a0) = F a0 := + begin + apply inverse, apply X_phi (XF a0) end private theorem G_hom_H_eq_F {a0 a0' : carrier A} (f0 : hom a0 a0') : - hom_of_eq (G0_H_eq_F a0') ∘ G_hom (to_fun_hom H f0) ∘ inv_of_eq (G0_H_eq_F a0) + hom_of_eq (G0_H_eq_F a0') ∘ G_hom (to_fun_hom H f0) ∘ inv_of_eq (G0_H_eq_F a0) = to_fun_hom F f0 := begin apply comp_eq_of_eq_inverse_comp, apply comp_inverse_eq_of_eq_comp, apply concat, apply ap essentially_surj_precomp_Y.g, apply is_prop.elim, fconstructor, { exact (inv_of_eq (G0_H_eq_F a0') ∘ to_fun_hom F f0) ∘ hom_of_eq (G0_H_eq_F a0) }, - { intros a a' h h' f l, }, + { intros a a' h h' l α, esimp[G0_H_eq_F], apply inverse, + apply concat, apply !assoc⁻¹, + apply concat, apply ap (λ x, _ ∘ x), apply X_phi_hom_of_eq, + apply concat, apply !assoc⁻¹, + apply inverse_comp_eq_of_eq_comp, apply inverse, + apply concat, apply assoc, + apply concat, apply ap (λ x, x ∘ _), apply X_phi_hom_of_eq, esimp[XF], + refine !respect_comp⁻¹ ⬝ ap (to_fun_hom F) _ ⬝ !respect_comp, + apply eq_of_fn_eq_fn' (to_fun_hom H), + refine !respect_comp ⬝ _ ⬝ !respect_comp⁻¹, + apply concat, apply ap (λ x, x ∘ _) !(right_inv (to_fun_hom H)), + apply concat, rotate 1, apply ap (λ x, _ ∘ x) !(right_inv (to_fun_hom H))⁻¹, + exact α }, reflexivity end - check k_coh end essentially_surjective_precomposition