From c7fd29f854297699f997d956cbe7b9231be1fef9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 28 Sep 2015 00:38:35 -0400 Subject: [PATCH] feat(category): start with the introduction rule for equivalences --- hott/algebra/category/adjoint.hlean | 118 ++++++++++++++++-- .../category/constructions/functor.hlean | 20 +-- .../category/constructions/product.hlean | 2 +- hott/algebra/category/constructions/sum.hlean | 2 +- hott/algebra/category/iso.hlean | 12 +- hott/algebra/category/nat_trans.hlean | 5 + hott/algebra/e_closure.hlean | 3 +- src/emacs/lean-input.el | 4 +- 8 files changed, 141 insertions(+), 25 deletions(-) diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index 3ee13e4c1..9082391de 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -2,6 +2,10 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn + +Properties of functors such as adjoint functors, equivalences, faithful or full functors + +TODO: Split this file in different files -/ import algebra.category.constructions function arity @@ -225,16 +229,40 @@ namespace category theorem reflect_inverse (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c') [H : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ := inverse_eq_inverse (idp : to_hom (@(iso.mk f) (reflect_is_iso F f)) = f) +end category -/- +namespace category section - variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality - include η ε - --definition inverse_of_unit_counit + parameters {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) - private definition adj_η (c : C) : G (F c) ≅ c := - to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c - open iso + -- variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) + -- (pη : Π(c c' : C) (f : hom c c'), f ∘ to_hom (η c) = to_hom (η c') ∘ G (F f)) + -- (pε : Π⦃d d' : D⦄ (f : hom d d'), f ∘ to_hom (ε d) = to_hom (ε d') ∘ F (G f)) + + private definition ηn : 1 ⟹ G ∘f F := to_inv η + private definition εn : F ∘f G ⟹ 1 := to_hom ε + + private definition ηi (c : C) : G (F c) ≅ c := componentwise_iso η c + private definition εi (d : D) : F (G d) ≅ d := componentwise_iso ε d + + private definition ηi' (c : C) : G (F c) ≅ c := + to_fun_iso G (to_fun_iso F (ηi c)⁻¹ⁱ) ⬝i to_fun_iso G (εi (F c)) ⬝i ηi c +exit + set_option pp.implicit true + private theorem adj_η_natural {c c' : C} (f : hom c c') + : G (F f) ∘ to_inv (ηi' c) = to_inv (ηi c') ∘ f := + let ηi'_nat : G ∘f F ⟹ 1 := + /- 1 ⇐ G ∘f F :-/ to_hom η + ∘n /- ... ⇐ (G ∘f 1) ∘f F :-/ hom_of_eq !functor.id_right ∘nf F + ∘n /- ... ⇐ (G ∘f (F ∘f G)) ∘f F :-/ (G ∘fn εn) ∘nf F + ∘n /- ... ⇐ ((G ∘f F) ∘f G) ∘f F :-/ hom_of_eq !functor.assoc⁻¹ ∘nf F + ∘n /- ... ⇐ (G ∘f F) ∘f (G ∘f F) :-/ hom_of_eq !functor.assoc + ∘n /- ... ⇐ (G ∘f F) ∘f 1 :-/ (G ∘f F) ∘fn ηn + ∘n /- ... ⇐ G ∘f F :-/ hom_of_eq !functor.id_right⁻¹ + in + have ηi'_nat ~ ηi', begin intro c, fold [precategory_functor C C] + /-rewrite [+natural_map_hom_of_eq],-/ end, + _ private theorem adjointify_adjH (c : C) : to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id := @@ -248,16 +276,88 @@ namespace category exact sorry end + attribute functor.id [reducible] variables (F G) definition is_equivalence.mk : is_equivalence F := begin - fconstructor, + fapply is_equivalence.mk', { exact G}, - { } + { fapply nat_trans.mk, + { intro c, exact to_inv (adj_η η ε c)}, + { intro c c' f, exact adj_η_natural η ε pη pε f}}, + { fapply nat_trans.mk, + { exact λd, to_hom (ε d)}, + { exact pε}}, + { exact adjointify_adjH η ε pη pε}, + { exact adjointify_adjK η ε pη pε}, + { exact @(is_iso_nat_trans _) (λc, !is_iso_inverse)}, + { apply is_iso_nat_trans}, end end + definition is_equivalence.mk2 (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) : is_equivalence F := + is_equivalence.mk F G + (componentwise_iso η) (componentwise_iso ε) + begin intro c c' f, esimp, apply naturality (to_hom η) f end + begin intro c c' f, esimp, apply naturality (to_hom ε) f end + +exit + + section + variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) -- we need some kind of naturality + include η ε + + -- private definition adj_η : G ∘f F ≅ functor.id := + -- change_inv + -- ( calc + -- G ∘f F ≅ (G ∘f F) ∘f 1 : iso_of_eq !functor.id_right + -- ... ≅ (G ∘f F) ∘f (G ∘f F) : _ + -- ... ≅ G ∘f (F ∘f (G ∘f F)) : _ + -- ... ≅ G ∘f ((F ∘f G) ∘f F) : _ + -- ... ≅ G ∘f (1 ∘f F) : _ + -- ... ≅ G ∘f F : _ + -- ... ≅ 1 : η) + -- _ + -- _ --change_natural_map _ _ + --sorry --to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c + open iso + + -- definition nat_map_of_iso [reducible] {C D : Precategory} {F G : C ⇒ D} (η : F ≅ G) (c : C) + -- : F c ⟶ G c := + -- natural_map (to_hom η) c + + private theorem adjointify_adjH (c : C) : + natural_map (to_hom ε) (F c) ∘ F (natural_map (to_inv (adj_η η ε)) c) = id := + begin + exact sorry + end + + -- (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c)) + -- (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d)) + + private theorem adjointify_adjK (d : D) : + G (natural_map (to_hom ε) d) ∘ natural_map (to_inv (adj_η η ε)) (G d) = id := + begin + exact sorry + end + + variables (F G) + definition is_equivalence.mk : is_equivalence F := + begin + fapply is_equivalence.mk', + { exact G}, + { exact to_inv (adj_η η ε)}, + { exact to_hom ε}, + { exact adjointify_adjH η ε}, + { exact adjointify_adjK η ε}, + { unfold to_inv, apply is_iso_inverse}, + { apply iso.struct}, + end + + end +/- + definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] : fully_faithful F := begin diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index 2b5dd3c54..39260500b 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -35,14 +35,14 @@ namespace category nat_trans.mk (λc, (η c)⁻¹) (λc d f, - begin + abstract begin apply comp_inverse_eq_of_eq_comp, transitivity (natural_map η d)⁻¹ ∘ to_fun_hom G f ∘ natural_map η c, {apply eq_inverse_comp_of_comp_eq, symmetry, apply naturality}, {apply assoc} - end) + end end) - definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id := + definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = 1 := begin fapply (apd011 nat_trans.mk), apply eq_of_homotopy, intro c, apply left_inverse, @@ -50,7 +50,7 @@ namespace category apply is_hset.elim end - definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id := + definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = 1 := begin fapply (apd011 nat_trans.mk), apply eq_of_homotopy, intro c, apply right_inverse, @@ -69,9 +69,9 @@ namespace category section /- and conversely, if a natural transformation is an iso, it is componentwise an iso -/ - variables {A B C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C) + variables {A B C D : Precategory} {F G : C ⇒ D} (η : hom F G) [isoη : is_iso η] (c : C) include isoη - definition componentwise_is_iso [instance] : is_iso (η c) := + definition componentwise_is_iso [instance] [constructor] : is_iso (η c) := @is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c) (ap010 natural_map (right_inverse η) c) @@ -113,19 +113,19 @@ namespace category : natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ := eq.rec_on p idp - definition hom_of_eq_compose_right {H : C ^c B} (p : F = G) + definition hom_of_eq_compose_right {H : B ⇒ C} (p : F = G) : hom_of_eq (ap (λx, x ∘f H) p) = hom_of_eq p ∘nf H := eq.rec_on p idp - definition inv_of_eq_compose_right {H : C ^c B} (p : F = G) + definition inv_of_eq_compose_right {H : B ⇒ C} (p : F = G) : inv_of_eq (ap (λx, x ∘f H) p) = inv_of_eq p ∘nf H := eq.rec_on p idp - definition hom_of_eq_compose_left {H : B ^c D} (p : F = G) + definition hom_of_eq_compose_left {H : D ⇒ C} (p : F = G) : hom_of_eq (ap (λx, H ∘f x) p) = H ∘fn hom_of_eq p := by induction p; exact !fn_id⁻¹ - definition inv_of_eq_compose_left {H : B ^c D} (p : F = G) + definition inv_of_eq_compose_left {H : D ⇒ C} (p : F = G) : inv_of_eq (ap (λx, H ∘f x) p) = H ∘fn inv_of_eq p := by induction p; exact !fn_id⁻¹ diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean index 31cfe6c38..d475c79e6 100644 --- a/hott/algebra/category/constructions/product.hlean +++ b/hott/algebra/category/constructions/product.hlean @@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Jakob von Raumer -Functor product precategory and (TODO) category +Product precategory and (TODO) category -/ import ..category ..functor hit.trunc diff --git a/hott/algebra/category/constructions/sum.hlean b/hott/algebra/category/constructions/sum.hlean index 20601b815..2f0398347 100644 --- a/hott/algebra/category/constructions/sum.hlean +++ b/hott/algebra/category/constructions/sum.hlean @@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Jakob von Raumer -Functor product precategory and (TODO) category +Sum precategory and (TODO) category -/ import ..category ..functor types.sum diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index d04987a00..6af7abccd 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -50,7 +50,7 @@ namespace iso definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) := is_iso.mk !id_id !id_id - definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) [H : is_iso f] : is_iso f⁻¹ := + definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) {H : is_iso f} : is_iso f⁻¹ := is_iso.mk !right_inverse !left_inverse definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a} @@ -165,6 +165,12 @@ namespace iso infixl ` ⬝i `:75 := iso.trans postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm + definition change_hom (H : a ≅ b) (f : a ⟶ b) (p : to_hom H = f) : a ≅ b := + iso.MK f (to_inv H) (p ▸ to_left_inverse H) (p ▸ to_right_inverse H) + + definition change_inv (H : a ≅ b) (g : b ⟶ a) (p : to_inv H = g) : a ≅ b := + iso.MK (to_hom H) g (p ▸ to_left_inverse H) (p ▸ to_right_inverse H) + definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f') : iso.mk f = iso.mk f' := apd011 iso.mk p !is_hprop.elim @@ -279,6 +285,10 @@ namespace iso end iso +attribute iso.refl [refl] +attribute iso.symm [symm] +attribute iso.trans [trans] + namespace iso /- rewrite lemmas for inverses, modified from diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index 9a67bbeee..858554db2 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -175,4 +175,9 @@ namespace nat_trans nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c)) (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹)) + definition compose_rev (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ + end nat_trans + +attribute nat_trans.compose_rev [trans] -- TODO: this doesn't work +attribute nat_trans.id [refl] diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 9bcda26ef..725351cdc 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Floris van Doorn The "equivalence closure" of a type-valued relation. -Given a binary type-valued relation (fibration), we add reflexivity, symmetry and transitivity terms +A more appropriate intuition is the type of words formed from the relation, + and inverses, concatenations and reflexivity -/ import .relation eq2 arity diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index b335fdf87..ec81a60dd 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -412,10 +412,10 @@ order for the change to take effect." ("ur" . ,(lean-input-to-string-list "↗⇗ ➶➹➚ ")) ("dr" . ,(lean-input-to-string-list "↘⇘ ⇲ ➴➷➘ ")) ("dl" . ,(lean-input-to-string-list "↙⇙ ")) - ("==>" . ("⟹")) + ("==>" . ("⟹")) ("nattrans" . ("⟹")) ("nat_trans" . ("⟹")) ("l-" . ("←")) ("<-" . ("←")) ("l=" . ("⇐")) - ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) + ("r-" . ("→")) ("->" . ("→")) ("r=" . ("⇒")) ("=>" . ("⇒")) ("functor" . ("⇒")) ("u-" . ("↑")) ("u=" . ("⇑")) ("d-" . ("↓")) ("d=" . ("⇓")) ("ud-" . ("↕")) ("ud=" . ("⇕"))