feat(category_theory/localization): localization of the opposite cate…

…gory (#17199)

If a functor `L : C ⥤ D` is a localization functor for `W : morphism_property C`, it is shown in this PR that `L.op : Cᵒᵖ ⥤ Dᵒᵖ` is also a localization functor.

src/category_theory/localization/opposite.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import category_theory.localization.predicate
+
+/-!
+
+# Localization of the opposite category
+
+If a functor `L : C ⥤ D` is a localization functor for `W : morphism_property C`, it
+is shown in this file that `L.op : Cᵒᵖ ⥤ Dᵒᵖ` is also a localization functor.
+
+-/
+
+noncomputable theory
+
+open category_theory category_theory.category
+
+namespace category_theory
+
+variables {C D : Type*} [category C] [category D] {L : C ⥤ D} {W : morphism_property C}
+
+namespace localization
+
+/-- If `L : C ⥤ D` satisfies the universal property of the localisation
+for `W : morphism_property C`, then `L.op` also does. -/
+def strict_universal_property_fixed_target.op {E : Type*} [category E]
+  (h : strict_universal_property_fixed_target L W Eᵒᵖ):
+  strict_universal_property_fixed_target L.op W.op E :=
+{ inverts := h.inverts.op,
+  lift := λ F hF, (h.lift F.right_op hF.right_op).left_op,
+  fac := λ F hF, begin
+    convert congr_arg functor.left_op (h.fac F.right_op hF.right_op),
+    exact F.right_op_left_op_eq.symm,
+  end,
+  uniq := λ F₁ F₂ eq, begin
+    suffices : F₁.right_op = F₂.right_op,
+    { rw [← F₁.right_op_left_op_eq, ← F₂.right_op_left_op_eq, this], },
+    have eq' := congr_arg functor.right_op eq,
+    exact h.uniq _ _ eq',
+  end, }
+
+instance is_localization_op : W.Q.op.is_localization W.op :=
+functor.is_localization.mk' W.Q.op W.op
+  (strict_universal_property_fixed_target_Q W _).op
+  (strict_universal_property_fixed_target_Q W _).op
+
+end localization
+
+namespace functor
+
+instance is_localization.op [h : L.is_localization W] : L.op.is_localization W.op :=
+is_localization.of_equivalence_target W.Q.op W.op L.op
+  (localization.equivalence_from_model L W).op
+  (nat_iso.op (localization.Q_comp_equivalence_from_model_functor_iso L W).symm)
+
+end functor
+
+end category_theory

src/category_theory/localization/predicate.lean

@@ -325,4 +325,42 @@ end lifting
 
 end localization
 
+namespace functor
+
+namespace is_localization
+
+open localization
+
+lemma of_iso {L₁ L₂ : C ⥤ D} (e : L₁ ≅ L₂) [L₁.is_localization W] : L₂.is_localization W :=
+begin
+  have h := localization.inverts L₁ W,
+  rw morphism_property.is_inverted_by.iff_of_iso W e at h,
+  let F₁ := localization.construction.lift L₁ (localization.inverts L₁ W),
+  let F₂ := localization.construction.lift L₂ h,
+  exact
+  { inverts := h,
+    nonempty_is_equivalence := nonempty.intro
+      (is_equivalence.of_iso (lift_nat_iso W.Q W L₁ L₂ F₁ F₂ e) infer_instance), },
+end
+
+/-- If `L : C ⥤ D` is a localization for `W : morphism_property C`, then it is also
+the case of a functor obtained by post-composing `L` with an equivalence of categories. -/
+lemma of_equivalence_target {E : Type*} [category E] (L' : C ⥤ E) (eq : D ≌ E)
+  [L.is_localization W] (e : L ⋙ eq.functor ≅ L') : L'.is_localization W :=
+begin
+  have h : W.is_inverted_by L',
+  { rw ← morphism_property.is_inverted_by.iff_of_iso W e,
+    exact morphism_property.is_inverted_by.of_comp W L (localization.inverts L W) eq.functor, },
+  let F₁ := localization.construction.lift L (localization.inverts L W),
+  let F₂ := localization.construction.lift L' h,
+  let e' : F₁ ⋙ eq.functor ≅ F₂ := lift_nat_iso W.Q W (L ⋙ eq.functor) L' _ _ e,
+  exact
+  { inverts := h,
+    nonempty_is_equivalence := nonempty.intro (is_equivalence.of_iso e' infer_instance) },
+end
+
+end is_localization
+
+end functor
+
 end category_theory

src/category_theory/morphism_property.lean

@@ -254,11 +254,31 @@ to isomorphisms in `D`. -/
 def is_inverted_by (P : morphism_property C) (F : C ⥤ D) : Prop :=
 ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : P f), is_iso (F.map f)
 
-lemma is_inverted_by.of_comp {C₁ C₂ C₃ : Type*} [category C₁] [category C₂] [category C₃]
+namespace is_inverted_by
+
+lemma of_comp {C₁ C₂ C₃ : Type*} [category C₁] [category C₂] [category C₃]
   (W : morphism_property C₁) (F : C₁ ⥤ C₂) (hF : W.is_inverted_by F) (G : C₂ ⥤ C₃) :
   W.is_inverted_by (F ⋙ G) :=
 λ X Y f hf, by { haveI := hF f hf, dsimp, apply_instance, }
 
+lemma op {W : morphism_property C} {L : C ⥤ D} (h : W.is_inverted_by L) :
+  W.op.is_inverted_by L.op :=
+λ X Y f hf, by { haveI := h f.unop hf, dsimp, apply_instance, }
+
+lemma right_op {W : morphism_property C} {L : Cᵒᵖ ⥤ D} (h : W.op.is_inverted_by L) :
+  W.is_inverted_by L.right_op :=
+λ X Y f hf, by { haveI := h f.op hf, dsimp, apply_instance, }
+
+lemma left_op {W : morphism_property C} {L : C ⥤ Dᵒᵖ} (h : W.is_inverted_by L) :
+  W.op.is_inverted_by L.left_op :=
+λ X Y f hf, by { haveI := h f.unop hf, dsimp, apply_instance, }
+
+lemma unop {W : morphism_property C} {L : Cᵒᵖ ⥤ Dᵒᵖ} (h : W.op.is_inverted_by L) :
+  W.is_inverted_by L.unop :=
+λ X Y f hf, by { haveI := h f.op hf, dsimp, apply_instance, }
+
+end is_inverted_by
+
 /-- Given `app : Π X, F₁.obj X ⟶ F₂.obj X` where `F₁` and `F₂` are two functors,
 this is the `morphism_property C` satisfied by the morphisms in `C` with respect
 to whom `app` is natural. -/
@@ -373,6 +393,18 @@ full_subcategory (λ (F : C ⥤ D), W.is_inverted_by F)
 def functors_inverting.mk {W : morphism_property C} {D : Type*} [category D]
 (F : C ⥤ D) (hF : W.is_inverted_by F) : W.functors_inverting D := ⟨F, hF⟩
 
+lemma is_inverted_by.iff_of_iso (W : morphism_property C) {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) :
+  W.is_inverted_by F₁ ↔ W.is_inverted_by F₂ :=
+begin
+  suffices : ∀ (X Y : C) (f : X ⟶ Y), is_iso (F₁.map f) ↔ is_iso (F₂.map f),
+  { split,
+    exact λ h X Y f hf, by { rw ← this, exact h f hf, },
+    exact λ h X Y f hf, by { rw this, exact h f hf, }, },
+  intros X Y f,
+  exact (respects_iso.isomorphisms D).arrow_mk_iso_iff
+    (arrow.iso_mk (e.app X) (e.app Y) (by simp)),
+end
+
 section diagonal
 
 variables [has_pullbacks C] {P : morphism_property C}

src/category_theory/natural_isomorphism.lean

@@ -196,6 +196,18 @@ begin
   ext, rw [←nat_trans.exchange], simp, refl
 end
 
+lemma is_iso_map_iff {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) {X Y : C} (f : X ⟶ Y) :
+  is_iso (F₁.map f) ↔ is_iso (F₂.map f) :=
+begin
+  revert F₁ F₂,
+  suffices : ∀ {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) (hf : is_iso (F₁.map f)), is_iso (F₂.map f),
+  { exact λ F₁ F₂ e, ⟨this e, this e.symm⟩, },
+  introsI F₁ F₂ e hf,
+  refine is_iso.mk ⟨e.inv.app Y ≫ inv (F₁.map f) ≫ e.hom.app X, _, _⟩,
+  { simp only [nat_trans.naturality_assoc, is_iso.hom_inv_id_assoc, iso.inv_hom_id_app], },
+  { simp only [assoc, ← e.hom.naturality, is_iso.inv_hom_id_assoc, iso.inv_hom_id_app], },
+end
+
 end nat_iso
 
 end category_theory

src/category_theory/opposites.lean

@@ -222,6 +222,10 @@ nat_iso.of_components (λ X, iso.refl _) (by tidy)
 def right_op_left_op_iso (F : Cᵒᵖ ⥤ D) : F.right_op.left_op ≅ F :=
 nat_iso.of_components (λ X, iso.refl _) (by tidy)
 
+/-- Whenever possible, it is advisable to use the isomorphism `right_op_left_op_iso`
+instead of this equality of functors. -/
+lemma right_op_left_op_eq (F : Cᵒᵖ ⥤ D) : F.right_op.left_op = F := by { cases F, refl, }
+
 end
 
 end functor