[Merged by Bors] - feat(CategoryTheory/Triangulated): localizing subcategories

Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean

@@ -15,9 +15,9 @@ Let `C` be a pretriangulated category. If `A` and `B` are triangulated
 subcategories of `C`, we define predicates (typeclasses
 `IsVerdierRightLocalizing` and `IsVerdierLeftLocalizing`)
 saying that `A` is right `B`-localizing (or left `B`-localizing).
-When `B` is closed under isomorphisms, we shall show that this implies that
+When `B` is closed under isomorphisms, we show that this implies that
 the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully
-faithful (TODO @joelriou).
+faithful.
 
 ## References
 * [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*,
@@ -33,7 +33,7 @@ open Category Limits Pretriangulated Opposite
 
 namespace ObjectProperty
 
-variable {C D D' : Type*} [Category* C] [Category* D] [Category* D']
+variable {C D D₁ D₂ : Type*} [Category* C] [Category* D] [Category* D₁] [Category* D₂]
 
 /-- If `A` and `B` are triangulated subcategories of a (pre)triangulated
 category `C` (with `B` closed under isomorphisms), we say that `A` is
@@ -151,6 +151,197 @@ lemma IsVerdierLeftLocalizing.fac'
     ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' :=
   (isVerdierLeftLocalizing_iff A B).1 inferInstance s hY hs
 
+/-- If `A` is a triangulated subcategory of a pretriangulated category `C`,
+and `B : ObjectProperty C`, this is the inclusion functor
+`A.ι : A.FullSubcategory ⥤ C`, considered as a localizer morphism,
+where `C` is equipped with the property of morphisms `B.trW`
+and `A.FullSubcategory` with the property of morphisms `(B.inverseImage A.ι).trW`. -/
+@[implicit_reducible]
+def triangulatedLocalizerMorphism [A.IsTriangulated] :
+    LocalizerMorphism (B.inverseImage A.ι).trW B.trW where
+  functor := A.ι
+  map X Y f hf := by
+    simp only [MorphismProperty.inverseImage_iff, trW_iff] at hf ⊢
+    obtain ⟨Z, a, b, hT, hZ⟩ := hf
+    exact ⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩
+
+instance [A.IsTriangulated] :
+    (triangulatedLocalizerMorphism A B).functor.CommShift ℤ :=
+  inferInstanceAs (A.ι.CommShift ℤ)
+
+instance [A.IsTriangulated] :
+    (triangulatedLocalizerMorphism A B).functor.IsTriangulated :=
+  inferInstanceAs A.ι.IsTriangulated
+
+lemma trW_inverseImage_ι_iff [A.IsTriangulated] {X Y : A.FullSubcategory} (f : X ⟶ Y) :
+    (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom := by
+  simp only [trW_iff]
+  constructor
+  · rintro ⟨Z, a, b, h, hZ⟩
+    exact ⟨_, _, _, A.ι.map_distinguished _ h, Z.property, hZ⟩
+  · rintro ⟨Z, a, b, h, hZ⟩
+    refine ⟨⟨Z, hZ.1⟩, A.homMk a, A.homMk (b ≫ (A.ι.commShiftIso 1).inv.app _), ?_, hZ.2⟩
+    rw [← A.ι.map_distinguished_iff]
+    refine isomorphic_distinguished _ h _
+      (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_)
+    · cat_disch
+    · cat_disch
+    · simp [dsimp% (A.ι.commShiftIso (1 : ℤ)).inv_hom_id_app X]
+
+lemma inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op [A.IsTriangulated]
+    [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] :
+    (B.op.inverseImage A.op.ι).trW.inverseImage A.opEquivalence.inverse =
+      (B.inverseImage A.ι).op.trW := by
+  ext ⟨X₁⟩ ⟨X₂⟩ a
+  simp [trW_op, trW_inverseImage_ι_iff, ← op_inf]
+
+variable [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms]
+
+section
+
+variable [A.IsVerdierRightLocalizing B]
+  (L₁ : A.FullSubcategory ⥤ D₁) (L₂ : C ⥤ D₂)
+  [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW]
+
+instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full := by
+  let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
+  have : L₁.EssSurj := Localization.essSurj L₁ (B.inverseImage A.ι).trW
+  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso
+    (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
+  refine F.full_of_comp_essSurj L₁ (fun X₁ X₂ φ ↦ ?_)
+  obtain ⟨φ', hφ'⟩ : ∃ φ', φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂ :=
+    ⟨e.hom.app X₁ ≫ φ ≫ e.inv.app X₂, by
+      simp [dsimp% e.inv_hom_id_app_assoc, dsimp% e.inv_hom_id_app]⟩
+  obtain ⟨f, hf⟩ := Localization.exists_leftFraction L₂ B.trW φ'
+  obtain ⟨X₃, s', a, hX₃, hs', fac⟩ :=
+    IsVerdierRightLocalizing.fac' f.s X₂.property f.hs
+  let g : (B.inverseImage A.ι).trW.LeftFraction X₁ X₂ :=
+    { Y' := ⟨X₃, hX₃⟩
+      f := A.homMk (f.f ≫ a)
+      s := A.homMk s'
+      hs := by rwa [trW_inverseImage_ι_iff] }
+  have := Localization.inverts L₁ _ _ g.hs
+  refine ⟨g.map L₁ (Localization.inverts _ _), ?_⟩
+  rw [← cancel_mono (F.map (L₁.map g.s)), ← Functor.map_comp,
+    MorphismProperty.LeftFraction.map_comp_map_s]
+  simp [g, ← fac, hφ', hf, ← dsimp% NatIso.naturality_1 e,
+    dsimp% e.hom_inv_id_app_assoc]
+
+instance [Preadditive D₁] [Preadditive D₂] [L₁.Additive] [L₂.Additive] :
+    ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive := by
+  let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
+  rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
+  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso
+    (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
+  exact Functor.additive_of_iso e
+
+instance : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful := by
+  letI := Localization.preadditive L₁ (B.inverseImage A.ι).trW
+  letI := Localization.preadditive L₂ B.trW
+  have := Localization.functor_additive L₁ (B.inverseImage A.ι).trW
+  have := Localization.functor_additive L₂ B.trW
+  let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
+  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
+    CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
+  refine Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions L₁
+    (B.inverseImage A.ι).trW F (fun X₁ X₂ f hf ↦ ?_)
+  replace hf : L₂.map f.hom = L₂.map 0 := by
+    simp [← dsimp% NatIso.naturality_2 e f, hf]
+  rw [MorphismProperty.map_eq_iff_postcomp L₂ B.trW] at hf
+  obtain ⟨X₃, s, hs, fac⟩ := hf
+  obtain ⟨X₄, t, a, hX₄, ht, fac'⟩ :=
+    IsVerdierRightLocalizing.fac' s X₂.property hs
+  let t' : X₂ ⟶ ⟨X₄, hX₄⟩ := A.homMk t
+  have := Localization.inverts L₁ (B.inverseImage A.ι).trW t'
+    (by rwa [trW_inverseImage_ι_iff])
+  rw [← cancel_mono (L₁.map t'), zero_comp, ← L₁.map_comp, ← L₁.map_zero]
+  congr 1
+  ext
+  simp [t', ← fac', reassoc_of% fac]
+
+end
+
+instance [A.IsVerdierRightLocalizing B] :
+    (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful where
+  nonempty_fullyFaithful := ⟨.ofFullyFaithful _⟩
+
+instance [A.IsVerdierLeftLocalizing B] :
+    (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful := by
+  let L₁ := (B.inverseImage A.ι).trW.Q
+  let L₂ := B.trW.Q
+  let F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization :=
+    (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
+  letI : CatCommSq (A.op.triangulatedLocalizerMorphism B.op).functor
+    (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op :=
+    ⟨Functor.isoWhiskerLeft A.opEquivalence.functor
+      (NatIso.op (CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F).symm)⟩
+  have : L₂.op.IsLocalization B.op.trW := by rw [trW_op]; infer_instance
+  have : (A.opEquivalence.functor ⋙ L₁.op).IsLocalization (B.op.inverseImage A.op.ι).trW := by
+    refine Functor.IsLocalization.of_equivalence_source L₁.op (B.inverseImage A.ι).trW.op
+      _ _ A.opEquivalence.symm ?_ ?_
+      ((Functor.associator _ _ _).symm ≪≫
+        Functor.isoWhiskerRight A.opEquivalence.counitIso _ ≪≫ Functor.leftUnitor _)
+    · rw [← trW_op, ← inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op]
+      intro _ _ f hf
+      simp only [MorphismProperty.inverseImage_iff, Equivalence.symm_functor] at hf ⊢
+      exact MorphismProperty.le_isoClosure _ _ hf
+    · refine fun _ _ _ hf ↦ Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_
+      simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using hf
+  exact LocalizerMorphism.IsLocalizedFullyFaithful.mk' (A.triangulatedLocalizerMorphism B)
+    L₁ L₂ F (((A.op.triangulatedLocalizerMorphism B.op).fullyFaithful
+    (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op).unop)
+
+section
+
+variable [A.IsVerdierLeftLocalizing B] (L₁ : A.FullSubcategory ⥤ D₁) (L₂ : C ⥤ D₂)
+  [L₁.IsLocalization (B.inverseImage A.ι).trW]
+  [L₂.IsLocalization B.trW]
+
+example : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Full := by
+  infer_instance
+
+example : ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful := by
+  infer_instance
+
+instance [A.IsVerdierLeftLocalizing B] [Preadditive D₁] [Preadditive D₂]
+    [L₁.Additive] [L₂.Additive] :
+    ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Additive := by
+  let F := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
+  rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW]
+  let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso
+    (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
+  exact Functor.additive_of_iso e
+
+/-- If `A` is a left `B`-localizing triangulated subcategory in the sense of Verdier,
+then the induced functor between the localizations with respect to `(B.inverseImage A.ι).trW`
+and `B.trW` is fully faithful. -/
+@[no_expose]
+noncomputable def IsVerdierLeftLocalizing.fullyFaithful [A.IsVerdierLeftLocalizing B]
+    {L₁ : A.FullSubcategory ⥤ D₁} {L₂ : C ⥤ D₂} {F : D₁ ⥤ D₂}
+    [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW]
+    (e : L₁ ⋙ F ≅ A.ι ⋙ L₂) :
+    F.FullyFaithful :=
+  Functor.FullyFaithful.ofIso (.ofFullyFaithful
+    ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂))
+    (Localization.liftNatIso L₁ (B.inverseImage A.ι).trW
+      ((A.triangulatedLocalizerMorphism B).functor ⋙ L₂) (L₁ ⋙ F) _ _ e.symm)
+
+/-- If `A` is a right `B`-localizing triangulated subcategory in the sense of Verdier,
+then the induced functor between the localizations with respect to `(B.inverseImage A.ι).trW`
+and `B.trW` is fully faithful. -/
+@[no_expose]
+noncomputable def IsVerdierRightLocalizing.fullyFaithful [A.IsVerdierRightLocalizing B]
+    {L₁ : A.FullSubcategory ⥤ D₁} {L₂ : C ⥤ D₂} {F : D₁ ⥤ D₂}
+    [L₁.IsLocalization (B.inverseImage A.ι).trW] [L₂.IsLocalization B.trW]
+    (e : L₁ ⋙ F ≅ A.ι ⋙ L₂) :
+    F.FullyFaithful :=
+  Functor.FullyFaithful.ofIso (.ofFullyFaithful
+    ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂))
+    (Localization.liftNatIso L₁ (B.inverseImage A.ι).trW
+      ((A.triangulatedLocalizerMorphism B).functor ⋙ L₂) (L₁ ⋙ F) _ _ e.symm)
+
+end
+
 end ObjectProperty
 
 end CategoryTheory