From 1f65e42e46eb8d60f0e856c2d1bf78ae6e6b6391 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Thu, 22 Apr 2021 14:56:27 +0000 Subject: [PATCH] feat(category_theory/adjunction): reflective adjunction induces partial bijection (#7286) Co-authored-by: Scott Morrison --- .../adjunction/reflective.lean | 84 ++++++++++++++----- 1 file changed, 64 insertions(+), 20 deletions(-) diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean index ce0622537d1ad..c97294ca23cc6 100644 --- a/src/category_theory/adjunction/reflective.lean +++ b/src/category_theory/adjunction/reflective.lean @@ -16,15 +16,16 @@ Note properties of reflective functors relating to limits and colimits are inclu `category_theory.monad.limits`. -/ -universes v₁ v₂ u₁ u₂ +universes v₁ v₂ v₃ u₁ u₂ u₃ noncomputable theory namespace category_theory -open limits category +open category adjunction limits -variables {C : Type u₁} {D : Type u₂} [category.{v₁} C] [category.{v₂} D] +variables {C : Type u₁} {D : Type u₂} {E : Type u₃} +variables [category.{v₁} C] [category.{v₂} D] [category.{v₃} E] /-- A functor is *reflective*, or *a reflective inclusion*, if it is fully faithful and right adjoint. @@ -38,10 +39,10 @@ For a reflective functor `i` (with left adjoint `L`), with unit `η`, we have ` -/ -- TODO: This holds more generally for idempotent adjunctions, not just reflective adjunctions. lemma unit_obj_eq_map_unit [reflective i] (X : C) : - (adjunction.of_right_adjoint i).unit.app (i.obj ((left_adjoint i).obj X)) - = i.map ((left_adjoint i).map ((adjunction.of_right_adjoint i).unit.app X)) := + (of_right_adjoint i).unit.app (i.obj ((left_adjoint i).obj X)) + = i.map ((left_adjoint i).map ((of_right_adjoint i).unit.app X)) := begin - rw [←cancel_mono (i.map ((adjunction.of_right_adjoint i).counit.app ((left_adjoint i).obj X))), + rw [←cancel_mono (i.map ((of_right_adjoint i).counit.app ((left_adjoint i).obj X))), ←i.map_comp], simp, end @@ -53,12 +54,12 @@ More generally this applies to objects essentially in the reflective subcategory `functor.ess_image.unit_iso`. -/ instance is_iso_unit_obj [reflective i] {B : D} : - is_iso ((adjunction.of_right_adjoint i).unit.app (i.obj B)) := + is_iso ((of_right_adjoint i).unit.app (i.obj B)) := begin - have : (adjunction.of_right_adjoint i).unit.app (i.obj B) = - inv (i.map ((adjunction.of_right_adjoint i).counit.app B)), + have : (of_right_adjoint i).unit.app (i.obj B) = + inv (i.map ((of_right_adjoint i).counit.app B)), { rw ← comp_hom_eq_id, - apply (adjunction.of_right_adjoint i).right_triangle_components }, + apply (of_right_adjoint i).right_triangle_components }, rw this, exact is_iso.inv_is_iso, end @@ -71,10 +72,10 @@ reflection of `A`, with the isomorphism as `η_A`. (For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.) -/ lemma functor.ess_image.unit_is_iso [reflective i] {A : C} (h : A ∈ i.ess_image) : - is_iso ((adjunction.of_right_adjoint i).unit.app A) := + is_iso ((of_right_adjoint i).unit.app A) := begin - suffices : (adjunction.of_right_adjoint i).unit.app A = - h.get_iso.inv ≫ (adjunction.of_right_adjoint i).unit.app (i.obj h.witness) ≫ + suffices : (of_right_adjoint i).unit.app A = + h.get_iso.inv ≫ (of_right_adjoint i).unit.app (i.obj h.witness) ≫ (left_adjoint i ⋙ i).map h.get_iso.hom, { rw this, apply_instance }, @@ -84,14 +85,14 @@ end /-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`. -/ lemma mem_ess_image_of_unit_is_iso [is_right_adjoint i] (A : C) - [is_iso ((adjunction.of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := -⟨(left_adjoint i).obj A, ⟨(as_iso ((adjunction.of_right_adjoint i).unit.app A)).symm⟩⟩ + [is_iso ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := +⟨(left_adjoint i).obj A, ⟨(as_iso ((of_right_adjoint i).unit.app A)).symm⟩⟩ /-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/ lemma mem_ess_image_of_unit_split_mono [reflective i] {A : C} - [split_mono ((adjunction.of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := + [split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image := begin - let η : 𝟭 C ⟶ left_adjoint i ⋙ i := (adjunction.of_right_adjoint i).unit, + let η : 𝟭 C ⟶ left_adjoint i ⋙ i := (of_right_adjoint i).unit, haveI : is_iso (η.app (i.obj ((left_adjoint i).obj A))) := (i.obj_mem_ess_image _).unit_is_iso, have : epi (η.app A), { apply epi_of_epi (retraction (η.app A)) _, @@ -102,11 +103,54 @@ begin exact mem_ess_image_of_unit_is_iso A, end -universes v₃ u₃ -variables {E : Type u₃} [category.{v₃} E] - /-- Composition of reflective functors. -/ instance reflective.comp (F : C ⥤ D) (G : D ⥤ E) [Fr : reflective F] [Gr : reflective G] : reflective (F ⋙ G) := { to_faithful := faithful.comp F G, } +/-- (Implementation) Auxiliary definition for `unit_comp_partial_bijective`. -/ +def unit_comp_partial_bijective_aux [reflective i] (A : C) (B : D) : + (A ⟶ i.obj B) ≃ (i.obj ((left_adjoint i).obj A) ⟶ i.obj B) := +((adjunction.of_right_adjoint i).hom_equiv _ _).symm.trans (equiv_of_fully_faithful i) + +/-- The description of the inverse of the bijection `unit_comp_partial_bijective_aux`. -/ +lemma unit_comp_partial_bijective_aux_symm_apply [reflective i] {A : C} {B : D} + (f : i.obj ((left_adjoint i).obj A) ⟶ i.obj B) : + (unit_comp_partial_bijective_aux _ _).symm f = (of_right_adjoint i).unit.app A ≫ f := +by simp [unit_comp_partial_bijective_aux] + +/-- +If `i` has a reflector `L`, then the function `(i.obj (L.obj A) ⟶ B) → (A ⟶ B)` given by +precomposing with `η.app A` is a bijection provided `B` is in the essential image of `i`. +That is, the function `λ (f : i.obj (L.obj A) ⟶ B), η.app A ≫ f` is bijective, as long as `B` is in +the essential image of `i`. +This definition gives an equivalence: the key property that the inverse can be described +nicely is shown in `unit_comp_partial_bijective_symm_apply`. + +This establishes there is a natural bijection `(A ⟶ B) ≃ (i.obj (L.obj A) ⟶ B)`. In other words, +from the point of view of objects in `D`, `A` and `i.obj (L.obj A)` look the same: specifically +that `η.app A` is an isomorphism. +-/ +def unit_comp_partial_bijective [reflective i] (A : C) {B : C} (hB : B ∈ i.ess_image) : + (A ⟶ B) ≃ (i.obj ((left_adjoint i).obj A) ⟶ B) := +calc (A ⟶ B) ≃ (A ⟶ i.obj hB.witness) : iso.hom_congr (iso.refl _) hB.get_iso.symm + ... ≃ (i.obj _ ⟶ i.obj hB.witness) : unit_comp_partial_bijective_aux _ _ + ... ≃ (i.obj ((left_adjoint i).obj A) ⟶ B) : iso.hom_congr (iso.refl _) hB.get_iso + +@[simp] +lemma unit_comp_partial_bijective_symm_apply [reflective i] (A : C) {B : C} + (hB : B ∈ i.ess_image) (f) : + (unit_comp_partial_bijective A hB).symm f = (of_right_adjoint i).unit.app A ≫ f := +by simp [unit_comp_partial_bijective, unit_comp_partial_bijective_aux_symm_apply] + +lemma unit_comp_partial_bijective_symm_natural [reflective i] (A : C) {B B' : C} (h : B ⟶ B') + (hB : B ∈ i.ess_image) (hB' : B' ∈ i.ess_image) (f : i.obj ((left_adjoint i).obj A) ⟶ B) : + (unit_comp_partial_bijective A hB').symm (f ≫ h) = + (unit_comp_partial_bijective A hB).symm f ≫ h := +by simp + +lemma unit_comp_partial_bijective_natural [reflective i] (A : C) {B B' : C} (h : B ⟶ B') + (hB : B ∈ i.ess_image) (hB' : B' ∈ i.ess_image) (f : A ⟶ B) : + (unit_comp_partial_bijective A hB') (f ≫ h) = unit_comp_partial_bijective A hB f ≫ h := +by rw [←equiv.eq_symm_apply, unit_comp_partial_bijective_symm_natural A h, equiv.symm_apply_apply] + end category_theory