diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean index c42123763..cb4b04196 100644 --- a/hott/algebra/category/adjoint.hlean +++ b/hott/algebra/category/adjoint.hlean @@ -11,10 +11,10 @@ open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_ namespace category variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C} - -- do we want to have a structure "is_adjoint" and define + -- TODO: define a structure "adjoint" and then define -- structure is_left_adjoint (F : C ⇒ D) := - -- (right_adjoint : D ⇒ C) -- G - -- (is_adjoint : adjoint F right_adjoint) + -- (G : D ⇒ C) -- G + -- (is_adjoint : adjoint F G) structure is_left_adjoint [class] (F : C ⇒ D) := (G : D ⇒ C) @@ -27,13 +27,6 @@ namespace category abbreviation unit := @is_left_adjoint.η abbreviation counit := @is_left_adjoint.ε - -- structure is_left_adjoint [class] (F : C ⇒ D) := - -- (right_adjoint : D ⇒ C) -- G - -- (unit : functor.id ⟹ right_adjoint ∘f F) -- η - -- (counit : F ∘f right_adjoint ⟹ functor.id) -- ε - -- (H : Π(c : C), (counit (F c)) ∘ (F (unit c)) = ID (F c)) - -- (K : Π(d : D), (right_adjoint (counit d)) ∘ (unit (right_adjoint d)) = ID (right_adjoint d)) - structure is_equivalence [class] (F : C ⇒ D) extends is_left_adjoint F := mk' :: (is_iso_unit : is_iso η) @@ -44,10 +37,6 @@ namespace category --a second notation for the inverse, which is not overloaded postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse - structure equivalence (C D : Precategory) := - (to_functor : C ⇒ D) - (struct : is_equivalence to_functor) - --TODO: review and change definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f' definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c') @@ -57,6 +46,10 @@ namespace category definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F definition is_isomorphism [class] (F : C ⇒ D) := fully_faithful F × is_equiv (to_fun_ob F) + structure equivalence (C D : Precategory) := + (to_functor : C ⇒ D) + (struct : is_equivalence to_functor) + structure isomorphism (C D : Precategory) := (to_functor : C ⇒ D) (struct : is_isomorphism to_functor) @@ -69,10 +62,10 @@ namespace category : is_equiv (@(to_fun_hom F) c c') := !H - definition is_iso_unit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (unit F) := + definition is_iso_unit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (unit F) := !is_equivalence.is_iso_unit - definition is_iso_counit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (counit F) := + definition is_iso_counit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (counit F) := !is_equivalence.is_iso_counit -- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D) @@ -127,19 +120,6 @@ namespace category -- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]}, -- end - section - variables (F G) - variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) - include η ε - --definition inverse_of_unit_counit - - definition is_equivalence.mk : is_equivalence F := - begin - exact sorry - end - - end - definition full_of_fully_faithful (H : fully_faithful F) : full F := λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)) @@ -155,16 +135,6 @@ namespace category { apply K} end - definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] - : fully_faithful F := - begin - intro c c', - fapply adjointify, - { intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c}, - { intro g, rewrite [+respect_comp], exact sorry}, - { exact sorry}, - end - definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] : split_essentially_surjective F := begin @@ -175,6 +145,32 @@ namespace category /- + definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F] + : fully_faithful F := + begin + intro c c', + fapply adjointify, + { intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c}, + { intro g, rewrite [+respect_comp,▸*], + krewrite [natural_map_inverse], xrewrite [respect_inv'], + apply inverse_comp_eq_of_eq_comp, + exact sorry /-this is basically the naturality of the counit-/ }, + { exact sorry}, + end + + section + variables (F G) + variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1) + include η ε + --definition inverse_of_unit_counit + + definition is_equivalence.mk : is_equivalence F := + begin + exact sorry + end + + end + definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) := sorry diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index c6dea2931..f2aceee50 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -77,7 +77,9 @@ namespace category local attribute componentwise_is_iso [instance] + variable {isoη} definition natural_map_inverse : natural_map η⁻¹ c = (η c)⁻¹ := idp + variable [isoη] definition naturality_iso {c c' : C} (f : c ⟶ c') : G f = η c' ∘ F f ∘ (η c)⁻¹ := calc diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index 88a24654d..23877991a 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -323,29 +323,32 @@ namespace iso H⁻¹ ▸ comp_inverse_cancel_left q g definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ inverse_comp_cancel_right f q - definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p := - H⁻¹ ▸ inverse_comp_cancel_left q p - definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r := - H⁻¹ ▸ comp_inverse_cancel_right r q definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y := (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹ definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q := (comp_eq_of_eq_comp_inverse H⁻¹)⁻¹ + variable {Hq} + definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p := + H⁻¹ ▸ inverse_comp_cancel_left q p + definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r := + H⁻¹ ▸ comp_inverse_cancel_right r q definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z := (inverse_comp_eq_of_eq_comp H⁻¹)⁻¹ definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ := (comp_inverse_eq_of_eq_comp H⁻¹)⁻¹ + definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹ definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹ + definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h := + (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹ + definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h := + (eq_inverse_of_comp_eq_id H⁻¹)⁻¹ + variable [Hq] definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q := eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q := eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹ definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹ - definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h := - (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹ - definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h := - (eq_inverse_of_comp_eq_id H⁻¹)⁻¹ end end iso diff --git a/hott/hit/torus.hlean b/hott/hit/torus.hlean index 266885572..c7dbdabca 100644 --- a/hott/hit/torus.hlean +++ b/hott/hit/torus.hlean @@ -76,7 +76,7 @@ namespace torus (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 := !elim_incl1 - definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) + theorem elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf) Ps diff --git a/hott/init/path.hlean b/hott/init/path.hlean index fda7b380a..bf08efe49 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -208,13 +208,14 @@ namespace eq infix ~ := homotopy - protected definition homotopy.refl [refl] [reducible] (f : Πx, P x) : f ~ f := + protected definition homotopy.refl [refl] [reducible] [unfold-full] (f : Πx, P x) : f ~ f := λ x, idp - protected definition homotopy.symm [symm] [reducible] {f g : Πx, P x} (H : f ~ g) : g ~ f := + protected definition homotopy.symm [symm] [reducible] [unfold-full] {f g : Πx, P x} (H : f ~ g) + : g ~ f := λ x, (H x)⁻¹ - protected definition homotopy.trans [trans] [reducible] {f g h : Πx, P x} + protected definition homotopy.trans [trans] [reducible] [unfold-full] {f g h : Πx, P x} (H1 : f ~ g) (H2 : g ~ h) : f ~ h := λ x, H1 x ⬝ H2 x @@ -287,12 +288,12 @@ namespace eq definition ap_id (p : x = y) : ap id p = p := eq.rec_on p idp - definition ap_compose (g : B → C) (f : A → B) {x y : A} (p : x = y) : + definition ap_compose [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) : ap (g ∘ f) p = ap g (ap f p) := eq.rec_on p idp -- Sometimes we don't have the actual function [compose]. - definition ap_compose' (g : B → C) (f : A → B) {x y : A} (p : x = y) : + definition ap_compose' [unfold 8] (g : B → C) (f : A → B) {x y : A} (p : x = y) : ap (λa, g (f a)) p = ap g (ap f p) := eq.rec_on p idp diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index 356917026..077c93b51 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -429,7 +429,7 @@ order for the change to take effect." ("d==" . ("⟱")) ("d-2" . ("⇊")) ("d-u-" . ("⇵")) ("l--" . ("⟵")) ("<--" . ("⟵")) ("l~" . ("↜" "⇜")) - ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) + ("r--" . ("⟶")) ("-->" . ("⟶")) ("r~" . ("↝" "⇝" "⟿")) ("hom" . ("⟶")) ("lr--" . ("⟷")) ("<-->" . ("⟷")) ("lr~" . ("↭")) ("l-n" . ("↚")) ("<-n" . ("↚")) ("l=n" . ("⇍"))