diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 05308db5f83fac..9c8d3d42ec0c5b 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/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