From 18804b20bf5c73526837765e3c8ee38591acfb18 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 28 Feb 2021 20:56:20 +0000 Subject: [PATCH] chore(category/equivalence): remove functor.fun_inv_id (#6450) `F.fun_inv_id` was just a confusing alternative way to write `F.as_equivalence.unit_iso.symm`, and meant that many lemmas couldn't fire. Deletes the definitions `functor.fun_inv_id` and `functor.inv_hom_id`, and the lemmas `is_equivalence.functor_unit_comp` and `is_equivalence.inv_fun_id_inv_comp`. Co-authored-by: Scott Morrison --- src/category_theory/adjunction/lifting.lean | 3 +- src/category_theory/adjunction/limits.lean | 8 +++--- src/category_theory/equivalence.lean | 32 ++++----------------- 3 files changed, 12 insertions(+), 31 deletions(-) diff --git a/src/category_theory/adjunction/lifting.lean b/src/category_theory/adjunction/lifting.lean index be406c39c8c72..3e0e6f4f13914 100644 --- a/src/category_theory/adjunction/lifting.lean +++ b/src/category_theory/adjunction/lifting.lean @@ -205,7 +205,8 @@ begin { resetI, apply_instance }, { let : R' ⋙ (monad.comparison (adjunction.of_right_adjoint U)).inv ≅ R := - (iso_whisker_left R (monad.comparison _).fun_inv_id : _) ≪≫ R.right_unitor, + (iso_whisker_left R (monad.comparison _).as_equivalence.unit_iso.symm : _) ≪≫ + R.right_unitor, exactI adjunction.right_adjoint_of_nat_iso this } }, let : is_right_adjoint (R' ⋙ monad.forget (adjunction.of_right_adjoint U).to_monad) := adjunction.right_adjoint_of_nat_iso diff --git a/src/category_theory/adjunction/limits.lean b/src/category_theory/adjunction/limits.lean index 6f3548987a93a..ee665e749cb84 100644 --- a/src/category_theory/adjunction/limits.lean +++ b/src/category_theory/adjunction/limits.lean @@ -85,7 +85,7 @@ instance is_equivalence_reflects_colimits (E : D ⥤ C) [is_equivalence E] : ref { reflects_colimit := λ K, { reflects := λ c t, begin - have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.fun_inv_id, + have l := (is_colimit_of_preserves E.inv t).map_cocone_equiv E.as_equivalence.unit_iso.symm, refine (((is_colimit.precompose_inv_equiv K.right_unitor _).symm) l).of_iso_colimit _, tidy, end } } } @@ -113,7 +113,7 @@ lemma has_colimit_of_comp_equivalence (E : C ⥤ D) [is_equivalence E] [has_coli has_colimit K := @has_colimit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K (@adjunction.has_colimit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _) -((functor.right_unitor _).symm ≪≫ (iso_whisker_left K (fun_inv_id E)).symm) +((functor.right_unitor _).symm ≪≫ iso_whisker_left K (E.as_equivalence.unit_iso)) end preservation_colimits @@ -182,7 +182,7 @@ instance is_equivalence_reflects_limits (E : D ⥤ C) [is_equivalence E] : refle { reflects_limit := λ K, { reflects := λ c t, begin - have := (is_limit_of_preserves E.inv t).map_cone_equiv E.fun_inv_id, + have := (is_limit_of_preserves E.inv t).map_cone_equiv E.as_equivalence.unit_iso.symm, refine (((is_limit.postcompose_hom_equiv K.left_unitor _).symm) this).of_iso_limit _, tidy, end } } } @@ -210,7 +210,7 @@ lemma has_limit_of_comp_equivalence (E : D ⥤ C) [is_equivalence E] [has_limit has_limit K := @has_limit_of_iso _ _ _ _ (K ⋙ E ⋙ inv E) K (@adjunction.has_limit_comp_equivalence _ _ _ _ _ _ (K ⋙ E) (inv E) _ _) -((iso_whisker_left K (fun_inv_id E)) ≪≫ (functor.right_unitor _)) +((iso_whisker_left K E.as_equivalence.unit_iso.symm) ≪≫ (functor.right_unitor _)) end preservation_limits diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean index 379969a533cf3..c5fb20d8763d8 100644 --- a/src/category_theory/equivalence.lean +++ b/src/category_theory/equivalence.lean @@ -432,16 +432,6 @@ is_equivalence.of_equivalence F.as_equivalence.symm @[simp] lemma inv_inv (F : C ⥤ D) [is_equivalence F] : inv (inv F) = F := rfl -/-- The composition of functor that is an equivalence with its inverse is naturally isomorphic to - the identity functor. -/ -def fun_inv_id (F : C ⥤ D) [is_equivalence F] : F ⋙ F.inv ≅ 𝟭 C := -is_equivalence.unit_iso.symm - -/-- The composition of functor that is an equivalence with its inverse is naturally isomorphic to - the identity functor. -/ -def inv_fun_id (F : C ⥤ D) [is_equivalence F] : F.inv ⋙ F ≅ 𝟭 D := -is_equivalence.counit_iso - variables {E : Type u₃} [category.{v₃} E] instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] : @@ -471,28 +461,18 @@ end equivalence namespace is_equivalence @[simp] lemma fun_inv_map (F : C ⥤ D) [is_equivalence F] (X Y : D) (f : X ⟶ Y) : - F.map (F.inv.map f) = F.inv_fun_id.hom.app X ≫ f ≫ F.inv_fun_id.inv.app Y := + F.map (F.inv.map f) = F.as_equivalence.counit.app X ≫ f ≫ F.as_equivalence.counit_inv.app Y := begin erw [nat_iso.naturality_2], refl end @[simp] lemma inv_fun_map (F : C ⥤ D) [is_equivalence F] (X Y : C) (f : X ⟶ Y) : - F.inv.map (F.map f) = F.fun_inv_id.hom.app X ≫ f ≫ F.fun_inv_id.inv.app Y := + F.inv.map (F.map f) = F.as_equivalence.unit_inv.app X ≫ f ≫ F.as_equivalence.unit.app Y := begin - erw [nat_iso.naturality_2], + erw [nat_iso.naturality_1], refl end --- We should probably restate many of the lemmas about `equivalence` for `is_equivalence`, --- but these are the only ones I need for now. -@[simp] lemma functor_unit_comp (E : C ⥤ D) [is_equivalence E] (Y) : - E.map (E.fun_inv_id.inv.app Y) ≫ E.inv_fun_id.hom.app (E.obj Y) = 𝟙 _ := -equivalence.functor_unit_comp E.as_equivalence Y - -@[simp] lemma inv_fun_id_inv_comp (E : C ⥤ D) [is_equivalence E] (Y) : - E.inv_fun_id.inv.app (E.obj Y) ≫ E.map (E.fun_inv_id.hom.app Y) = 𝟙 _ := -eq_of_inv_eq_inv (functor_unit_comp _ _) - end is_equivalence namespace equivalence @@ -503,7 +483,7 @@ An equivalence is essentially surjective. See https://stacks.math.columbia.edu/tag/02C3. -/ lemma ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F := -⟨λ Y, ⟨F.inv.obj Y, ⟨F.inv_fun_id.app Y⟩⟩⟩ +⟨λ Y, ⟨F.inv.obj Y, ⟨F.as_equivalence.counit_iso.app Y⟩⟩⟩ /-- An equivalence is faithful. @@ -525,9 +505,9 @@ See https://stacks.math.columbia.edu/tag/02C3. -/ @[priority 100] -- see Note [lower instance priority] instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F := -{ preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y, +{ preimage := λ X Y f, F.as_equivalence.unit.app X ≫ F.inv.map f ≫ F.as_equivalence.unit_inv.app Y, witness' := λ X Y f, F.inv.map_injective $ - by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app] + by simpa only [is_equivalence.inv_fun_map, assoc, iso.inv_hom_id_app_assoc, iso.inv_hom_id_app] using comp_id _ } @[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F]