feat: port CategoryTheory.Localization.Opposite (#2949)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib.lean

@@ -440,6 +440,7 @@ import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Linear.FunctorCategory
 import Mathlib.CategoryTheory.Linear.LinearFunctor
 import Mathlib.CategoryTheory.Localization.Construction
+import Mathlib.CategoryTheory.Localization.Opposite
 import Mathlib.CategoryTheory.Localization.Predicate
 import Mathlib.CategoryTheory.Monad.Basic
 import Mathlib.CategoryTheory.Monoidal.Category

Mathlib/CategoryTheory/Localization/Opposite.lean

@@ -0,0 +1,67 @@
+/-
+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
+
+! This file was ported from Lean 3 source module category_theory.localization.opposite
+! leanprover-community/mathlib commit 8efef279998820353694feb6ff5631ed0d309ecc
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Localization.Predicate
+
+/-!
+
+# Localization of the opposite category
+
+If a functor `L : C ⥤ D` is a localization functor for `W : MorphismProperty C`, it
+is shown in this file that `L.op : Cᵒᵖ ⥤ Dᵒᵖ` is also a localization functor.
+
+-/
+
+
+noncomputable section
+
+open CategoryTheory CategoryTheory.Category
+
+namespace CategoryTheory
+
+variable {C D : Type _} [Category C] [Category D] {L : C ⥤ D} {W : MorphismProperty 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 StrictUniversalPropertyFixedTarget.op {E : Type _} [Category E]
+    (h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ) :
+    StrictUniversalPropertyFixedTarget L.op W.op E
+    where
+  inverts := h.inverts.op
+  lift F hF := (h.lift F.rightOp hF.rightOp).leftOp
+  fac F hF := by
+    convert congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)
+  uniq F₁ F₂ eq :=
+    by
+    suffices F₁.rightOp = F₂.rightOp by
+      rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
+    have eq' := congr_arg Functor.rightOp eq
+    exact h.uniq _ _ eq'
+#align category_theory.localization.strict_universal_property_fixed_target.op CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.op
+
+instance isLocalization_op : W.Q.op.IsLocalization W.op :=
+  Functor.IsLocalization.mk' W.Q.op W.op (strictUniversalPropertyFixedTargetQ W _).op
+    (strictUniversalPropertyFixedTargetQ W _).op
+#align category_theory.localization.is_localization_op CategoryTheory.Localization.isLocalization_op
+
+end Localization
+
+namespace Functor
+
+instance IsLocalization.op [L.IsLocalization W] : L.op.IsLocalization W.op :=
+  IsLocalization.of_equivalence_target W.Q.op W.op L.op (Localization.equivalenceFromModel L W).op
+    (NatIso.op (Localization.qCompEquivalenceFromModelFunctorIso L W).symm)
+#align category_theory.functor.is_localization.op CategoryTheory.Functor.IsLocalization.op
+
+end Functor
+
+end CategoryTheory