From 2b6d5e293f2d959f1d3f0541a5fe9c16604ba427 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 16:30:23 +0200 Subject: [PATCH 01/26] feat(CategoryTheory): the opposite of a triangulated subcategory --- Mathlib.lean | 1 + .../Triangulated/Opposite/Subcategory.lean | 80 +++++++++++++++++++ 2 files changed, 81 insertions(+) create mode 100644 Mathlib/CategoryTheory/Triangulated/Opposite/Subcategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index f691b4027e6fe7..8c25336594b291 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3389,6 +3389,7 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor public import Mathlib.CategoryTheory.Triangulated.Opposite.OpOp public import Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated +public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangle public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated public import Mathlib.CategoryTheory.Triangulated.Orthogonal diff --git a/Mathlib/CategoryTheory/Triangulated/Opposite/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Opposite/Subcategory.lean new file mode 100644 index 00000000000000..d805386974e048 --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/Opposite/Subcategory.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.ObjectProperty.Opposite +public import Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated + +/-! +# The opposite of a triangulated subcategory + +In this file, we show that if `P : ObjectProperty C` is a triangulated +subcategory of a pretriangulated category `C`, then `P.op` is a +triangulated subcategory of `Cᵒᵖ`. + +-/ + +public section + +namespace CategoryTheory + +open Pretriangulated.Opposite Pretriangulated Limits + +namespace ObjectProperty + +variable {C : Type*} [Category* C] + [HasShift C ℤ] [HasZeroObject C] [Preadditive C] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + +instance (P : ObjectProperty C) [P.IsStableUnderShift ℤ] : + P.op.IsStableUnderShift ℤ where + isStableUnderShiftBy n := { le_shift _ hX := P.le_shift (-n) _ hX } + +instance (P : ObjectProperty Cᵒᵖ) [P.IsStableUnderShift ℤ] : + P.unop.IsStableUnderShift ℤ where + isStableUnderShiftBy n := + { le_shift X hX := by + obtain ⟨m, rfl⟩ : ∃ m, n = -m := ⟨-n , by simp⟩ + exact P.le_shift m _ hX } + +instance (P : ObjectProperty C) [P.IsTriangulatedClosed₂] : P.op.IsTriangulatedClosed₂ where + ext₂' T hT h₁ h₃ := by + rw [mem_distTriang_op_iff] at hT + obtain ⟨X, hX, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ hT h₃ h₁ + exact ⟨Opposite.op X, hX, ⟨e.symm.op⟩⟩ + +instance (P : ObjectProperty Cᵒᵖ) [P.IsTriangulatedClosed₂] : P.unop.IsTriangulatedClosed₂ where + ext₂' T hT h₁ h₃ := by + obtain ⟨X, hX, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ (op_distinguished _ hT) h₃ h₁ + exact ⟨Opposite.unop X, hX, ⟨e.symm.unop⟩⟩ + +instance (P : ObjectProperty C) [P.IsTriangulated] : P.op.IsTriangulated where + +instance (P : ObjectProperty Cᵒᵖ) [P.IsTriangulated] : P.unop.IsTriangulated where + +lemma trW_of_op (P : ObjectProperty C) [P.IsTriangulated] + {X Y : C} {f : X ⟶ Y} (hf : P.op.trW f.op) : P.trW f := by + obtain ⟨Z, a, b, h₁, h₂⟩ := hf + rw [ObjectProperty.trW_iff'] + exact ⟨_, _, _, Pretriangulated.unop_distinguished _ h₁, h₂⟩ + +lemma trW_of_unop (P : ObjectProperty Cᵒᵖ) [P.IsTriangulated] + {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : P.unop.trW f.unop) : P.trW f := by + obtain ⟨Z, a, b, h₁, h₂⟩ := hf + rw [ObjectProperty.trW_iff'] + exact ⟨_, _, _, Pretriangulated.op_distinguished _ h₁, h₂⟩ + +lemma trW_op_iff (P : ObjectProperty C) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y} : + P.op.trW f ↔ P.trW f.unop := + ⟨P.trW_of_op, P.op.trW_of_unop⟩ + +lemma trW_op (P : ObjectProperty C) [P.IsTriangulated] : P.op.trW = P.trW.op := by + ext X Y f + exact P.trW_op_iff + +end ObjectProperty + +end CategoryTheory From 3e2ae14f10e3558413b0bcf2f393287a91423ae6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 16:58:19 +0200 Subject: [PATCH 02/26] wip --- Mathlib/CategoryTheory/EssentialImage.lean | 20 ++ .../Triangulated/LocalizingSubcategory.lean | 270 ++++++++++++++++++ 2 files changed, 290 insertions(+) create mode 100644 Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean diff --git a/Mathlib/CategoryTheory/EssentialImage.lean b/Mathlib/CategoryTheory/EssentialImage.lean index bdc6187812f158..fcb7cb2e15881e 100644 --- a/Mathlib/CategoryTheory/EssentialImage.lean +++ b/Mathlib/CategoryTheory/EssentialImage.lean @@ -164,6 +164,8 @@ lemma essImage_comp_apply_of_essSurj : (F ⋙ G).essImage X ↔ G.essImage X whe end EssSurj +section + variable {J C D : Type*} [Category* J] [Category* C] [Category* D] (G : J ⥤ D) (F : C ⥤ D) [F.Full] [F.Faithful] (hG : ∀ j, F.essImage (G.obj j)) @@ -186,6 +188,8 @@ factor through `essImage.liftFunctor G F hG`. -/ NatIso.ofComponents (fun i ↦ F.essImage.ι.mapIso (F.toEssImage.objObjPreimageIso ⟨G.obj i, hG _⟩)) +end + lemma essImage_ι_comp (F : C ⥤ D) (P : ObjectProperty C) : (P.ι ⋙ F).essImage = P.map F := by ext Y @@ -195,6 +199,22 @@ lemma essImage_ι_comp (F : C ⥤ D) (P : ObjectProperty C) : · rintro ⟨X, hX, ⟨e⟩⟩ exact ⟨⟨X, hX⟩, ⟨e⟩⟩ +lemma full_of_precomp_essSurj (F : D ⥤ E) (L : C ⥤ D) [EssSurj L] + (h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), + ∃ (f : L.obj X₁ ⟶ L.obj X₂), F.map f = φ) : + Full F := ⟨by + intro X₁ X₂ ψ + obtain ⟨f, hf⟩ := h (F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫ + F.map (L.objObjPreimageIso X₂).inv) + exact ⟨(L.objObjPreimageIso X₁).inv ≫ f ≫ (L.objObjPreimageIso X₂).hom, by simp [hf]⟩⟩ + +lemma faithful_of_precomp_essSurj (F : D ⥤ E) (L : C ⥤ D) [EssSurj L] + (h : ∀ ⦃X₁ X₂ : C⦄ (f g : L.obj X₁ ⟶ L.obj X₂), F.map f = F.map g → f = g) : + Faithful F where + map_injective hfg := by + rw [← cancel_mono (L.objObjPreimageIso _).inv, ← cancel_epi (L.objObjPreimageIso _).hom] + exact h _ _ (by simp [hfg]) + end Functor end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean new file mode 100644 index 00000000000000..495e0512eb368a --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -0,0 +1,270 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory +public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor +public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated +public import Mathlib.CategoryTheory.Localization.Triangulated +--public import Mathlib.CategoryTheory.Localization.CalculusOfFractions.Lemmas + +/-! +# Localizing subcategories + +-/ + +@[expose] public section + +namespace CategoryTheory + +open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite + +namespace ObjectProperty + +variable {A C D D' : Type*} [Category* A] [Category* C] [Category* D] [Category* D'] + [HasZeroObject C] [HasShift C ℤ] [Preadditive C] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + (B : ObjectProperty C) (F : A ⥤ C) + +/-- Let `F : A ⥤ C` be a fully faithful triangulated functor and +`B` a triangulated subcategory of `C`, we say that `F` is +right `B`-localizing if any morphism `Y ⟶ F.obj X` with `hY : B Y` +factors as `a ≫ F.map b` with `a : Y ⟶ F.obj Y'` (such that +`B (F.obj Y')` holds) and `b : Y' ⟶ X`. -/ +class IsRightLocalizing [B.IsTriangulated] : Prop where + fac {Y : C} {X : A} (φ : Y ⟶ F.obj X) (hY : B Y) : + ∃ (Y' : A) (_ : B (F.obj Y')) (a : Y ⟶ F.obj Y') (b : Y' ⟶ X), + a ≫ F.map b = φ + +/-- Let `F : A ⥤ C` be a fully faithful triangulated functor and +`B` a triangulated subcategory of `C`, we say that `F` is +left `B`-localizing if any morphism `F.obj X ⟶ Y` with `hY : B Y` +factors as `F.map b ≫ a` with `b : X ⟶ Y'` and `a : F.obj Y' ⟶ Y` +such that `B (F.obj Y')` holds. -/ +class IsLeftLocalizing [B.IsTriangulated] : Prop where + fac {X : A} {Y : C} (φ : F.obj X ⟶ Y) (hY : B Y) : + ∃ (Y' : A) (_ : B (F.obj Y')) (a : F.obj Y' ⟶ Y) (b : X ⟶ Y'), + F.map b ≫ a = φ + +variable [B.IsTriangulated] + +lemma fac_of_isRightLocalizing [B.IsRightLocalizing F] + {Y : C} {X : A} (φ : Y ⟶ F.obj X) (hY : B Y) : + ∃ (Y' : A) (_ : B (F.obj Y')) (a : Y ⟶ F.obj Y') (b : Y' ⟶ X), + a ≫ F.map b = φ := + IsRightLocalizing.fac φ hY + +lemma fac_of_isLeftLocalizing [B.IsLeftLocalizing F] + {X : A} {Y : C} (φ : F.obj X ⟶ Y) (hY : B Y) : + ∃ (Y' : A) (_ : B (F.obj Y')) (a : F.obj Y' ⟶ Y) (b : X ⟶ Y'), + F.map b ≫ a = φ := + IsLeftLocalizing.fac φ hY + +open CategoryTheory.Pretriangulated.Opposite + +instance [B.IsLeftLocalizing F] : B.op.IsRightLocalizing F.op where + fac {Y X} φ hY := by + obtain ⟨Y', hY', a, b, fac⟩ := B.fac_of_isLeftLocalizing F φ.unop hY + exact ⟨Opposite.op Y', hY', a.op, b.op, Quiver.Hom.unop_inj fac⟩ + +lemma isLeftLocalizing_of_op [B.op.IsRightLocalizing F.op] : B.IsLeftLocalizing F where + fac {X Y} φ hY := by + obtain ⟨Y', hY', a, b, fac⟩ := B.op.fac_of_isRightLocalizing F.op φ.op hY + exact ⟨Y'.unop, hY', a.unop, b.unop, Quiver.Hom.op_inj fac⟩ + +variable [HasZeroObject A] + [HasShift A ℤ] + [Preadditive A] + [∀ (n : ℤ), (shiftFunctor A n).Additive] + [Pretriangulated A] + [F.CommShift ℤ] [F.IsTriangulated] + +section + +variable [B.IsClosedUnderIsomorphisms] + +/-- Factorization property of right localizing subcategories. -/ +lemma fac_of_isRightLocalizing' [B.IsRightLocalizing F] + {X : A} {Y : C} (s : F.obj X ⟶ Y) (hs : B.trW s) : + ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') (b : Y ⟶ F.obj X'), + s ≫ b = F.map s' := by + rw [ObjectProperty.trW_iff'] at hs + obtain ⟨W, a, b, hT, hW⟩ := hs + obtain ⟨W', hW', c, d, fac⟩ := B.fac_of_isRightLocalizing F a hW + obtain ⟨U, e, f, hT'⟩ := Pretriangulated.distinguished_cocone_triangle d + obtain ⟨β, hβ, _⟩ := complete_distinguished_triangle_morphism _ _ hT (F.map_distinguished _ hT') + c (𝟙 _) (by simpa using fac.symm) + dsimp at β hβ + refine ⟨U, e, ?_, β, by simpa using hβ⟩ + rw [ObjectProperty.trW_iff'] + exact ⟨_, _, _, hT', hW'⟩ + +/-- Factorization property of left localizing subcategories. -/ +lemma fac_of_isLeftLocalizing' [B.IsLeftLocalizing F] + {X : A} {Y : C} (s : Y ⟶ F.obj X) (hs : B.trW s) : + ∃ (X' : A) (s' : X' ⟶ X) (_ : (B.inverseImage F).trW s') (b : F.obj X' ⟶ Y), + b ≫ s = F.map s' := by + obtain ⟨X', s', hs', b, fac⟩ := B.op.fac_of_isRightLocalizing' F.op s.op + (by simpa only [ObjectProperty.trW_op_iff] using hs) + refine ⟨X'.unop, s'.unop, ?_, b.unop, Quiver.Hom.op_inj fac⟩ + rw [← trW_op_iff] + exact hs' + +variable {B F} in +/-- Constructor for right localizing categories. -/ +lemma IsRightLocalizing.mk' + (h : ∀ ⦃X : A⦄ ⦃Y : C⦄ (s : F.obj X ⟶ Y) (_ : B.trW s), + ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') + (b : Y ⟶ F.obj X'), s ≫ b = F.map s') : + B.IsRightLocalizing F where + fac {Y X} φ hY := by + obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle φ + have hs : B.trW s := by + rw [trW_iff'] + exact ⟨_, _, _, hT, hY⟩ + obtain ⟨W, s', hs', c, fac⟩ := h s hs + obtain ⟨U, d, e, hT'⟩ := distinguished_cocone_triangle₁ s' + obtain ⟨β, hβ, _⟩ := complete_distinguished_triangle_morphism₁ _ _ hT + (F.map_distinguished _ hT') (𝟙 _) c (by simpa using fac) + dsimp at β hβ + refine ⟨U, (B.trW_iff_of_distinguished' _ (F.map_distinguished _ hT')).1 ?_, + β, d, by simpa using hβ.symm⟩ + rw [trW_iff] at hs' ⊢ + obtain ⟨_, _, _, hT'', hV⟩ := hs' + exact ⟨_, _, _, F.map_distinguished _ hT'', hV⟩ + +variable {B F} in +/-- Constructor for left localizing categories. -/ +lemma IsLeftLocalizing.mk' + (h : ∀ ⦃Y : C⦄ ⦃X : A⦄ (s : Y ⟶ F.obj X) (_ : B.trW s), + ∃ (X' : A) (s' : X' ⟶ X) (_ : (B.inverseImage F).trW s') + (b : F.obj X' ⟶ Y), b ≫ s = F.map s') : + B.IsLeftLocalizing F := by + have : B.op.IsRightLocalizing F.op := IsRightLocalizing.mk' (fun X Y s hs => by + obtain ⟨X', s', h, b, fac⟩ := h s.unop (trW_of_op _ hs) + exact ⟨Opposite.op X', s'.op, trW_of_unop _ h, b.op, Quiver.Hom.unop_inj fac⟩) + exact B.isLeftLocalizing_of_op F + +end + +variable (L : C ⥤ D) [L.IsLocalization B.trW] + +section + +variable [B.IsClosedUnderIsomorphisms] + (L' : A ⥤ D') [L'.IsLocalization (B.inverseImage F).trW] + (F' : D' ⥤ D) [Localization.Lifting L' (B.inverseImage F).trW (F ⋙ L) F'] + [IsTriangulated C] + +include L L' F' in +set_option backward.isDefEq.respectTransparency false in +lemma full_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] : F'.Full := by + have := Localization.essSurj L' (B.inverseImage F).trW + apply F'.full_of_precomp_essSurj L' + intro X₁ X₂ φ + have e := Localization.Lifting.iso L' (B.inverseImage F).trW (F ⋙ L) F' + obtain ⟨φ', hφ'⟩ : ∃ φ', φ = e.hom.app X₁ ≫ φ' ≫ e.inv.app X₂ := + ⟨e.inv.app X₁ ≫ φ ≫ e.hom.app X₂, by simp⟩ + obtain ⟨f, hf⟩ := Localization.exists_leftFraction L B.trW φ' + obtain ⟨X₃, s', hs', t, fac⟩ := B.fac_of_isRightLocalizing' F f.s f.hs + let f' : (B.inverseImage F).trW.LeftFraction X₁ X₂ := + { f := F.preimage (f.f ≫ t) + s := F.preimage (f.s ≫ t) + hs := by + rw [B.inverseImage_trW_iff, F.map_preimage, fac, ← B.inverseImage_trW_iff F] + exact hs' } + have hf' : φ' ≫ L.map (F.map f'.s) = L.map (F.map f'.f) := by + replace hf := hf =≫ L.map (f.s) + rw [f.map_comp_map_s] at hf + dsimp + rw [F.map_preimage, F.map_preimage, L.map_comp, L.map_comp, reassoc_of% hf] + have : IsIso (F'.map (L'.map f'.s)) := + ((MorphismProperty.isomorphisms D).arrow_mk_iso_iff + ((Arrow.isoOfNatIso e) (Arrow.mk f'.s))).2 + (Localization.inverts _ B.trW _ + (by simpa only [← B.inverseImage_trW_iff F] using f'.hs)) + refine ⟨f'.map L' (Localization.inverts _ _), ?_⟩ + rw [hφ', ← cancel_mono (F'.map (L'.map f'.s)), ← F'.map_comp, f'.map_comp_map_s, + assoc, assoc] + erw [← e.inv.naturality] + rw [Functor.comp_map, reassoc_of% hf'] + erw [e.inv.naturality, e.hom_inv_id_app_assoc] + rfl + +set_option backward.isDefEq.respectTransparency false in +include L L' in +lemma faithful_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] [F.Faithful] : + F'.Faithful := by + have e := Localization.Lifting.iso L' (B.inverseImage F).trW (F ⋙ L) F' + have := IsTriangulated.of_fully_faithful_triangulated_functor F + letI := Localization.preadditive L' (B.inverseImage F).trW + letI := Localization.functor_additive L' (B.inverseImage F).trW + letI := Localization.preadditive L B.trW + letI := Localization.functor_additive L B.trW + have : (B.inverseImage F).trW.HasLeftCalculusOfFractions := inferInstance + have : F'.Additive := by + rw [Localization.functor_additive_iff L' (B.inverseImage F).trW] + exact Functor.additive_of_iso e.symm + sorry + /- + apply F'.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions L' (B.inverseImage F).trW + intro X₁ X₂ f hf + replace hf : L.map (F.map f) = L.map 0 := by + erw [L.map_zero, ← NatIso.naturality_1 e f, hf, zero_comp, comp_zero] + rw [MorphismProperty.map_eq_iff_postcomp L B.trW] at hf + obtain ⟨Z, s, hs, fac⟩ := hf + rw [zero_comp] at fac + obtain ⟨W, s', hs', t, fac'⟩ := B.fac_of_isRightLocalizing' F s hs + have hfs' : f ≫ s' = 0 := F.map_injective (by + rw [F.map_zero, F.map_comp, ← fac', reassoc_of% fac, zero_comp]) + have := Localization.inverts L' (B.inverseImage F).trW s' hs' + rw [← cancel_mono (L'.map s'), zero_comp, ← L'.map_comp, hfs', L'.map_zero]-/ + +end + +variable {L : C ⥤ D} {L' : A ⥤ D'} {H : D' ⥤ D} (e : L' ⋙ H ≅ F ⋙ L) + [L'.EssSurj] [H.Full] [H.Faithful] [L.IsLocalization B.trW] + [IsTriangulated C] [B.IsClosedUnderIsomorphisms] + +include e in +lemma isLocalization_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] [F.Faithful] : + L'.IsLocalization (B.inverseImage F).trW := by + have hL' : (B.inverseImage F).trW.IsInvertedBy L' := fun X₁ X₂ f hf => by + rw [B.inverseImage_trW_iff] at hf + have : IsIso (H.map (L'.map f)) := + ((MorphismProperty.isomorphisms D).arrow_mk_iso_iff + (Arrow.isoOfNatIso e f)).2 (Localization.inverts L B.trW _ hf) + apply isIso_of_fully_faithful H + let G := Localization.lift _ hL' (B.inverseImage F).trW.Q + have eG : (B.inverseImage F).trW.Q ⋙ G ≅ L' := + Localization.Lifting.iso _ (B.inverseImage F).trW _ _ + have : Localization.Lifting (B.inverseImage F).trW.Q (B.inverseImage F).trW + (F ⋙ L) (G ⋙ H) := + ⟨(Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight eG H ≪≫ e⟩ + have := full_of_isRightLocalizing B F L (B.inverseImage F).trW.Q (G ⋙ H) + have := faithful_of_isRightLocalizing B F L (B.inverseImage F).trW.Q (G ⋙ H) + have : G.EssSurj := + { mem_essImage := fun X => + ⟨_, ⟨eG.app (L'.objPreimage X) ≪≫ L'.objObjPreimageIso X⟩⟩ } + have : G.Full := Functor.Full.of_comp_faithful G H + have : G.Faithful := Functor.Faithful.of_comp_iso (Iso.refl (G ⋙ H)) + have : G.IsEquivalence := { } + exact Functor.IsLocalization.of_equivalence_target (B.inverseImage F).trW.Q _ _ + G.asEquivalence eG + +include e in +lemma isLocalization_of_isLeftLocalizing [B.IsLeftLocalizing F] [F.Full] [F.Faithful] : + L'.IsLocalization (B.inverseImage F).trW := by + rw [← Functor.IsLocalization.op_iff, ← trW_op] + have : Functor.IsLocalization L.op (B.op.trW) := by + rw [trW_op] + infer_instance + let e' : L'.op ⋙ H.op ≅ F.op ⋙ L.op := NatIso.op e.symm + exact B.op.isLocalization_of_isRightLocalizing F.op e' + +end ObjectProperty + +end CategoryTheory From ac4959e10f2623d5d275da45999f21ee5fbeec7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 18:31:39 +0200 Subject: [PATCH 03/26] wip --- .../Triangulated/LocalizingSubcategory.lean | 147 +++++++++++++----- .../Triangulated/Subcategory.lean | 31 ++++ 2 files changed, 140 insertions(+), 38 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 495e0512eb368a..1bedf1c48102a4 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -24,44 +24,114 @@ open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite namespace ObjectProperty -variable {A C D D' : Type*} [Category* A] [Category* C] [Category* D] [Category* D'] - [HasZeroObject C] [HasShift C ℤ] [Preadditive C] +variable {C : Type*} [Category* C] + +class IsRightLocalizing (A B : ObjectProperty C) : Prop where + fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) : + ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f + +class IsLeftLocalizing (A B : ObjectProperty C) : Prop where + fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) : + ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f + +instance (A B : ObjectProperty C) [A.IsLeftLocalizing B] : + A.op.IsRightLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsLeftLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsLeftLocalizing B] : + A.unop.IsRightLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsLeftLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +instance (A B : ObjectProperty C) [A.IsRightLocalizing B] : + A.op.IsLeftLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsRightLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsRightLocalizing B] : + A.unop.IsLeftLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsRightLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +variable (A B : ObjectProperty C) + +lemma isLeftLocalizing_op_iff : + A.op.IsLeftLocalizing B.op ↔ A.IsRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsRightLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +lemma isRightLocalizing_op_iff : + A.op.IsRightLocalizing B.op ↔ A.IsLeftLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsLeftLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] - (B : ObjectProperty C) (F : A ⥤ C) - -/-- Let `F : A ⥤ C` be a fully faithful triangulated functor and -`B` a triangulated subcategory of `C`, we say that `F` is -right `B`-localizing if any morphism `Y ⟶ F.obj X` with `hY : B Y` -factors as `a ≫ F.map b` with `a : Y ⟶ F.obj Y'` (such that -`B (F.obj Y')` holds) and `b : Y' ⟶ X`. -/ -class IsRightLocalizing [B.IsTriangulated] : Prop where - fac {Y : C} {X : A} (φ : Y ⟶ F.obj X) (hY : B Y) : - ∃ (Y' : A) (_ : B (F.obj Y')) (a : Y ⟶ F.obj Y') (b : Y' ⟶ X), - a ≫ F.map b = φ - -/-- Let `F : A ⥤ C` be a fully faithful triangulated functor and -`B` a triangulated subcategory of `C`, we say that `F` is -left `B`-localizing if any morphism `F.obj X ⟶ Y` with `hY : B Y` -factors as `F.map b ≫ a` with `b : X ⟶ Y'` and `a : F.obj Y' ⟶ Y` -such that `B (F.obj Y')` holds. -/ -class IsLeftLocalizing [B.IsTriangulated] : Prop where - fac {X : A} {Y : C} (φ : F.obj X ⟶ Y) (hY : B Y) : - ∃ (Y' : A) (_ : B (F.obj Y')) (a : F.obj Y' ⟶ Y) (b : X ⟶ Y'), - F.map b ≫ a = φ - -variable [B.IsTriangulated] - -lemma fac_of_isRightLocalizing [B.IsRightLocalizing F] - {Y : C} {X : A} (φ : Y ⟶ F.obj X) (hY : B Y) : - ∃ (Y' : A) (_ : B (F.obj Y')) (a : Y ⟶ F.obj Y') (b : Y' ⟶ X), - a ≫ F.map b = φ := - IsRightLocalizing.fac φ hY - -lemma fac_of_isLeftLocalizing [B.IsLeftLocalizing F] - {X : A} {Y : C} (φ : F.obj X ⟶ Y) (hY : B Y) : - ∃ (Y' : A) (_ : B (F.obj Y')) (a : F.obj Y' ⟶ Y) (b : X ⟶ Y'), - F.map b ≫ a = φ := - IsLeftLocalizing.fac φ hY + +lemma isRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsRightLocalizing B ↔ + ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A X) (_ : B.trW s), + ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := by + refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩ + · rw [ObjectProperty.trW_iff'] at hs + obtain ⟨W, a, b, hT, hW⟩ := hs + obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsRightLocalizing.fac a hW hX + obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX + obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT' + c (𝟙 _) (by cat_disch) + refine ⟨U, e, g, hU, ?_, by cat_disch⟩ + rw [ObjectProperty.trW_iff'] + exact ⟨_, _, _, hT', h₁, h₂⟩ + · obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle f + have hs : B.trW s := by + rw [trW_iff'] + exact ⟨_, _, _, hT, hX⟩ + obtain ⟨W, s', g, hW, hs', fac⟩ := hA s hY hs + obtain ⟨U, hU, a, c, hT'⟩ := A.distinguished_cocone_triangle₁ s' hY hW + obtain ⟨t, ht, ht'⟩ := + complete_distinguished_triangle_morphism₁ _ _ hT hT' (𝟙 Y) g (by cat_disch) + exact ⟨U, t, a, hU, (B.trW_iff_of_distinguished' _ hT').1 (trW_monotone (by simp) _ hs'), + by cat_disch⟩ + +-- to be moved +instance [A.ContainsZero] [B.ContainsZero] [B.IsClosedUnderIsomorphisms] : + (A ⊓ B).ContainsZero where + exists_zero := by + obtain ⟨Z, hZ, hA⟩ := A.exists_prop_of_containsZero + exact ⟨Z, hZ, hA, B.prop_of_isZero hZ⟩ + +-- to be moved +instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : + (A ⊓ B).IsTriangulated where + ext₂' T hT h₁ h₃ := by + obtain ⟨Y, hY, ⟨e⟩⟩ := A.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1 + exact ⟨Y, ⟨hY, B.prop_of_iso e (B.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩ + +lemma isLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsLeftLocalizing B ↔ + ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A Y) (_ : B.trW s), + ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := by + rw [← isRightLocalizing_op_iff, isRightLocalizing_iff] + refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX hs ↦ ?_⟩ + · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff]) + exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', by cat_disch⟩ + · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs) + exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ + +--lemma fac_of_isRightLocalizing' [B.IsRightLocalizing F] +-- {X : A} {Y : C} (s : F.obj X ⟶ Y) (hs : B.trW s) : +-- ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') (b : Y ⟶ F.obj X'), +-- s ≫ b = F.map s' := by +-- rw [ObjectProperty.trW_iff'] at hs + +/- open CategoryTheory.Pretriangulated.Opposite @@ -265,6 +335,7 @@ lemma isLocalization_of_isLeftLocalizing [B.IsLeftLocalizing F] [F.Full] [F.Fait let e' : L'.op ⋙ H.op ≅ F.op ⋙ L.op := NatIso.op e.symm exact B.op.isLocalization_of_isRightLocalizing F.op e' -end ObjectProperty +-/ +end ObjectProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean index 7392b7fdceb0d4..3dde43aae82633 100644 --- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean @@ -90,6 +90,30 @@ lemma ext_of_isTriangulatedClosed₃' (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃ := IsTriangulatedClosed₃.ext₃' T hT h₁ h₂ +protected lemma distinguished_cocone_triangle [P.IsTriangulatedClosed₃] + {X Y : C} (a : X ⟶ Y) (hX : P X) (hY : P Y) : + ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a + obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY + exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩ + +protected lemma distinguished_cocone_triangle₁ [P.IsTriangulatedClosed₁] + {Y Z : C} (b : Y ⟶ Z) (hY : P Y) (hZ : P Z) : + ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b + obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ + exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩ + +protected lemma distinguished_cocone_triangle₂ [P.IsTriangulatedClosed₂] + {X Z : C} (c : Z ⟶ X⟦(1 : ℤ)⟧) (hX : P X) (hZ : P Z) : + ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c + obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ + exact ⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩ + lemma ext_of_isTriangulatedClosed₁ [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms] (T : Triangle C) (hT : T ∈ distTriang C) @@ -447,6 +471,13 @@ lemma trW_isoClosure : P.isoClosure.trW = P.trW := by · rintro ⟨Z, g, h, mem, hZ⟩ exact ⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩ +variable {P} in +lemma trW_monotone {Q : ObjectProperty C} (h : P ≤ Q) : P.trW ≤ Q.trW := by + intro X Y f hf + rw [trW_iff] at hf ⊢ + obtain ⟨Z, a, b, hT, hZ⟩ := hf + exact ⟨Z, a, b, hT, h _ hZ⟩ + set_option backward.isDefEq.respectTransparency false in instance : P.trW.RespectsIso where precomp {X' X Y} e (he : IsIso e) := by From f167e3ad50fab00d177bf601118746e077fdbbfd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 18:50:37 +0200 Subject: [PATCH 04/26] wip --- .../Triangulated/LocalizingSubcategory.lean | 84 ++++++++++++------- 1 file changed, 56 insertions(+), 28 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 1bedf1c48102a4..88f52490939af5 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -9,11 +9,15 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated public import Mathlib.CategoryTheory.Localization.Triangulated ---public import Mathlib.CategoryTheory.Localization.CalculusOfFractions.Lemmas /-! # Localizing subcategories + + +## References +* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] + -/ @[expose] public section @@ -24,64 +28,75 @@ open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite namespace ObjectProperty -variable {C : Type*} [Category* C] +variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] -class IsRightLocalizing (A B : ObjectProperty C) : Prop where +/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated +category `C` (with `B` closed under isomorphisms), we say that `A` is +right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and +`Y` in `A` factors through an object that is in `A` and `B`. +See `isTriangulatedRightLocalizing_iff` for another characterization. -/ +class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f -class IsLeftLocalizing (A B : ObjectProperty C) : Prop where +/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated +category `C` (with `B` closed under isomorphisms), we say that `A` is +left `B`-localizing if any morphism `X ⟶ Y` with `X` in `A` and +`Y` in `B` factors through an object that is in `A` and `B`. +See `isTriangulatedLeftLocalizing_iff` for another characterization. -/ +class IsTriangulatedLeftLocalizing (A B : ObjectProperty C) : Prop where fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f -instance (A B : ObjectProperty C) [A.IsLeftLocalizing B] : - A.op.IsRightLocalizing B.op where +instance (A B : ObjectProperty C) [A.IsTriangulatedLeftLocalizing B] : + A.op.IsTriangulatedRightLocalizing B.op where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsLeftLocalizing.fac f.unop hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := + IsTriangulatedLeftLocalizing.fac f.unop hY hX exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ -instance (A B : ObjectProperty Cᵒᵖ) [A.IsLeftLocalizing B] : - A.unop.IsRightLocalizing B.unop where +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedLeftLocalizing B] : + A.unop.IsTriangulatedRightLocalizing B.unop where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsLeftLocalizing.fac f.op hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedLeftLocalizing.fac f.op hY hX exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ -instance (A B : ObjectProperty C) [A.IsRightLocalizing B] : - A.op.IsLeftLocalizing B.op where +instance (A B : ObjectProperty C) [A.IsTriangulatedRightLocalizing B] : + A.op.IsTriangulatedLeftLocalizing B.op where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsRightLocalizing.fac f.unop hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.unop hY hX exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ -instance (A B : ObjectProperty Cᵒᵖ) [A.IsRightLocalizing B] : - A.unop.IsLeftLocalizing B.unop where +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedRightLocalizing B] : + A.unop.IsTriangulatedLeftLocalizing B.unop where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsRightLocalizing.fac f.op hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.op hY hX exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ variable (A B : ObjectProperty C) -lemma isLeftLocalizing_op_iff : - A.op.IsLeftLocalizing B.op ↔ A.IsRightLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsRightLocalizing B.op.unop), +lemma isTriangulatedLeftLocalizing_op_iff : + A.op.IsTriangulatedLeftLocalizing B.op ↔ A.IsTriangulatedRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedRightLocalizing B.op.unop), fun _ ↦ inferInstance⟩ -lemma isRightLocalizing_op_iff : - A.op.IsRightLocalizing B.op ↔ A.IsLeftLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsLeftLocalizing B.op.unop), +lemma isTriangulatedRightLocalizing_op_iff : + A.op.IsTriangulatedRightLocalizing B.op ↔ A.IsTriangulatedLeftLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedLeftLocalizing B.op.unop), fun _ ↦ inferInstance⟩ variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] -lemma isRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsRightLocalizing B ↔ + A.IsTriangulatedRightLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A X) (_ : B.trW s), ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := by refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩ · rw [ObjectProperty.trW_iff'] at hs obtain ⟨W, a, b, hT, hW⟩ := hs - obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsRightLocalizing.fac a hW hX + obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac a hW hX obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT' c (𝟙 _) (by cat_disch) @@ -113,18 +128,31 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : obtain ⟨Y, hY, ⟨e⟩⟩ := A.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1 exact ⟨Y, ⟨hY, B.prop_of_iso e (B.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩ -lemma isLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsLeftLocalizing B ↔ + A.IsTriangulatedLeftLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A Y) (_ : B.trW s), ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := by - rw [← isRightLocalizing_op_iff, isRightLocalizing_iff] + rw [← isTriangulatedRightLocalizing_op_iff, isTriangulatedRightLocalizing_iff] refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX hs ↦ ?_⟩ · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff]) exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', by cat_disch⟩ · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs) exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ +variable [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + (L : C ⥤ D) [L.IsLocalization B.trW] + (L' : A.FullSubcategory ⥤ D') [L'.IsLocalization (B.inverseImage A.ι).trW] + (F' : D' ⥤ D) [Localization.Lifting L' (B.inverseImage A.ι).trW (A.ι ⋙ L) F'] + +lemma full_of_isTriangulatedRightLocalizing [A.IsTriangulatedRightLocalizing B] : + F'.Full := by + sorry + +lemma faithful_of_isTriangulatedRightLocalizing [A.IsTriangulatedRightLocalizing B] : + F'.Full := by + sorry + --lemma fac_of_isRightLocalizing' [B.IsRightLocalizing F] -- {X : A} {Y : C} (s : F.obj X ⟶ Y) (hs : B.trW s) : -- ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') (b : Y ⟶ F.obj X'), From 6f2158852937a9ae6c202b2ac59f59ab6413b959 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 22:32:04 +0200 Subject: [PATCH 05/26] wip --- .../Localization/LocalizerMorphism.lean | 73 +++++ .../Triangulated/LocalizingSubcategory.lean | 249 ++---------------- 2 files changed, 99 insertions(+), 223 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index aeb62f15b3f1bf..9c0da740687e39 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -136,6 +136,29 @@ lemma isEquivalence_iff : G.IsEquivalence ↔ G'.IsEquivalence := ⟨fun _ => Φ.isEquivalence_imp L₁ L₂ G L₁' L₂' G', fun _ => Φ.isEquivalence_imp L₁' L₂' G' L₁ L₂ G⟩ +/-- If a localizer morphism induces a fully faithful functor on some choice of +localized categories, it will be so for any choice of localized categories. -/ +noncomputable def fullyFaithfulImp (hG : G.FullyFaithful) : G'.FullyFaithful := + let E₁ := Localization.uniq L₁ L₁' W₁ + let E₂ := Localization.uniq L₂ L₂' W₂ + let e : L₁ ⋙ G ⋙ E₂.functor ≅ L₁ ⋙ E₁.functor ⋙ G' := + calc + L₁ ⋙ G ⋙ E₂.functor ≅ Φ.functor ⋙ L₂ ⋙ E₂.functor := + (associator _ _ _).symm ≪≫ + isoWhiskerRight (CatCommSq.iso Φ.functor L₁ L₂ G).symm E₂.functor ≪≫ + associator _ _ _ + _ ≅ Φ.functor ⋙ L₂' := isoWhiskerLeft Φ.functor (compUniqFunctor L₂ L₂' W₂) + _ ≅ L₁' ⋙ G' := CatCommSq.iso Φ.functor L₁' L₂' G' + _ ≅ L₁ ⋙ E₁.functor ⋙ G' := + isoWhiskerRight (compUniqFunctor L₁ L₁' W₁).symm G' ≪≫ associator _ _ _ + (E₁.fullyFaithfulInverse.comp (hG.comp E₂.fullyFaithfulFunctor)).ofIso + ((isoWhiskerLeft (E₁.inverse) (liftNatIso L₁ W₁ _ _ (G ⋙ E₂.functor) (E₁.functor ⋙ G') e) ≪≫ + (associator _ _ _).symm ≪≫ isoWhiskerRight E₁.counitIso G' ≪≫ G'.leftUnitor)) + +lemma nonempty_fullyFaithful_iff : Nonempty G.FullyFaithful ↔ Nonempty G'.FullyFaithful := + ⟨fun ⟨h⟩ => ⟨Φ.fullyFaithfulImp L₁ L₂ G L₁' L₂' G' h⟩, + fun ⟨h⟩ => ⟨Φ.fullyFaithfulImp L₁' L₂' G' L₁ L₂ G h⟩⟩ + end /-- Condition that a `LocalizerMorphism` induces an equivalence on the localized categories -/ @@ -234,6 +257,56 @@ instance IsLocalizedEquivalence.comp [Φ.IsLocalizedEquivalence] Functor.IsLocalization.of_iso _ (Functor.associator _ _ _).symm of_isLocalization_of_isLocalization _ W₃.Q +/-- Condition that a `LocalizerMorphism` induces a fully faithful functor +on the localized categories -/ +class IsLocalizedFullyFaithful : Prop where + /-- the induced functor on the constructed localized categories is fully faithful -/ + nonempty_fullyFaithful : Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful + +lemma IsLocalizedFullyFaithful.mk' [CatCommSq Φ.functor L₁ L₂ G] (hG : G.FullyFaithful) : + Φ.IsLocalizedFullyFaithful where + nonempty_fullyFaithful := by + rw [Φ.nonempty_fullyFaithful_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G] + exact ⟨hG⟩ + +instance [Φ.IsLocalizedEquivalence] : Φ.IsLocalizedFullyFaithful where + nonempty_fullyFaithful := ⟨Functor.FullyFaithful.ofFullyFaithful _⟩ + +/-- If a `LocalizerMorphism` becomes a fully faithful after localization, then any compatible +functor between the localized categories is fully faithful. -/ +noncomputable irreducible_def fullyFaithful + [h : Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] : + G.FullyFaithful := (Nonempty.some (by + rw [Φ.nonempty_fullyFaithful_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)] + exact h.nonempty_fullyFaithful)) + +lemma faithful [Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] : + G.Faithful := + (Φ.fullyFaithful L₁ L₂ G).faithful + +lemma full [Φ.IsLocalizedFullyFaithful] [CatCommSq Φ.functor L₁ L₂ G] : + G.Full := + (Φ.fullyFaithful L₁ L₂ G).full + +/-- If a `LocalizerMorphism` becomes fully faithful after localization, +then the induced functor on the localized categories is fully faithful. -/ +noncomputable irreducible_def fullyFaithfulLocalizedFunctor [Φ.IsLocalizedFullyFaithful] : + (Φ.localizedFunctor L₁ L₂).FullyFaithful := + Φ.fullyFaithful L₁ L₂ _ + +instance [Φ.IsLocalizedFullyFaithful] : (Φ.localizedFunctor L₁ L₂).Full := + Φ.full L₁ L₂ _ + +instance [Φ.IsLocalizedFullyFaithful] : (Φ.localizedFunctor L₁ L₂).Faithful := + Φ.faithful L₁ L₂ _ + +instance [Φ.IsLocalizedFullyFaithful] : Φ.op.IsLocalizedFullyFaithful := by + let G := Φ.localizedFunctor W₁.Q W₂.Q + letI : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op := + ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩ + exact IsLocalizedFullyFaithful.mk' Φ.op W₁.Q.op W₂.Q.op G.op + (Φ.fullyFaithful W₁.Q W₂.Q G).op + /-- The localizer morphism from `W₁.arrow` to `W₂.arrow` that is induced by `Φ : LocalizerMorphism W₁ W₂`. -/ @[simps] diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 88f52490939af5..db76c6498f69a6 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -140,230 +140,33 @@ lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs) exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ -variable [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - (L : C ⥤ D) [L.IsLocalization B.trW] - (L' : A.FullSubcategory ⥤ D') [L'.IsLocalization (B.inverseImage A.ι).trW] - (F' : D' ⥤ D) [Localization.Lifting L' (B.inverseImage A.ι).trW (A.ι ⋙ L) F'] +/-- 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 localized morphism, +where `C` is equipped with the property of morphisms `B.trW` +and `A.FullSubcategory` with the property of morphisms `(B.inverseImage A.ι).trW`. -/ +@[simps] +def triangulatedLocalizedMorphism [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⟩ -lemma full_of_isTriangulatedRightLocalizing [A.IsTriangulatedRightLocalizing B] : - F'.Full := by - sorry - -lemma faithful_of_isTriangulatedRightLocalizing [A.IsTriangulatedRightLocalizing B] : - F'.Full := by - sorry - ---lemma fac_of_isRightLocalizing' [B.IsRightLocalizing F] --- {X : A} {Y : C} (s : F.obj X ⟶ Y) (hs : B.trW s) : --- ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') (b : Y ⟶ F.obj X'), --- s ≫ b = F.map s' := by --- rw [ObjectProperty.trW_iff'] at hs - -/- - -open CategoryTheory.Pretriangulated.Opposite - -instance [B.IsLeftLocalizing F] : B.op.IsRightLocalizing F.op where - fac {Y X} φ hY := by - obtain ⟨Y', hY', a, b, fac⟩ := B.fac_of_isLeftLocalizing F φ.unop hY - exact ⟨Opposite.op Y', hY', a.op, b.op, Quiver.Hom.unop_inj fac⟩ - -lemma isLeftLocalizing_of_op [B.op.IsRightLocalizing F.op] : B.IsLeftLocalizing F where - fac {X Y} φ hY := by - obtain ⟨Y', hY', a, b, fac⟩ := B.op.fac_of_isRightLocalizing F.op φ.op hY - exact ⟨Y'.unop, hY', a.unop, b.unop, Quiver.Hom.op_inj fac⟩ - -variable [HasZeroObject A] - [HasShift A ℤ] - [Preadditive A] - [∀ (n : ℤ), (shiftFunctor A n).Additive] - [Pretriangulated A] - [F.CommShift ℤ] [F.IsTriangulated] - -section - -variable [B.IsClosedUnderIsomorphisms] - -/-- Factorization property of right localizing subcategories. -/ -lemma fac_of_isRightLocalizing' [B.IsRightLocalizing F] - {X : A} {Y : C} (s : F.obj X ⟶ Y) (hs : B.trW s) : - ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') (b : Y ⟶ F.obj X'), - s ≫ b = F.map s' := by - rw [ObjectProperty.trW_iff'] at hs - obtain ⟨W, a, b, hT, hW⟩ := hs - obtain ⟨W', hW', c, d, fac⟩ := B.fac_of_isRightLocalizing F a hW - obtain ⟨U, e, f, hT'⟩ := Pretriangulated.distinguished_cocone_triangle d - obtain ⟨β, hβ, _⟩ := complete_distinguished_triangle_morphism _ _ hT (F.map_distinguished _ hT') - c (𝟙 _) (by simpa using fac.symm) - dsimp at β hβ - refine ⟨U, e, ?_, β, by simpa using hβ⟩ - rw [ObjectProperty.trW_iff'] - exact ⟨_, _, _, hT', hW'⟩ - -/-- Factorization property of left localizing subcategories. -/ -lemma fac_of_isLeftLocalizing' [B.IsLeftLocalizing F] - {X : A} {Y : C} (s : Y ⟶ F.obj X) (hs : B.trW s) : - ∃ (X' : A) (s' : X' ⟶ X) (_ : (B.inverseImage F).trW s') (b : F.obj X' ⟶ Y), - b ≫ s = F.map s' := by - obtain ⟨X', s', hs', b, fac⟩ := B.op.fac_of_isRightLocalizing' F.op s.op - (by simpa only [ObjectProperty.trW_op_iff] using hs) - refine ⟨X'.unop, s'.unop, ?_, b.unop, Quiver.Hom.op_inj fac⟩ - rw [← trW_op_iff] - exact hs' - -variable {B F} in -/-- Constructor for right localizing categories. -/ -lemma IsRightLocalizing.mk' - (h : ∀ ⦃X : A⦄ ⦃Y : C⦄ (s : F.obj X ⟶ Y) (_ : B.trW s), - ∃ (X' : A) (s' : X ⟶ X') (_ : (B.inverseImage F).trW s') - (b : Y ⟶ F.obj X'), s ≫ b = F.map s') : - B.IsRightLocalizing F where - fac {Y X} φ hY := by - obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle φ - have hs : B.trW s := by - rw [trW_iff'] - exact ⟨_, _, _, hT, hY⟩ - obtain ⟨W, s', hs', c, fac⟩ := h s hs - obtain ⟨U, d, e, hT'⟩ := distinguished_cocone_triangle₁ s' - obtain ⟨β, hβ, _⟩ := complete_distinguished_triangle_morphism₁ _ _ hT - (F.map_distinguished _ hT') (𝟙 _) c (by simpa using fac) - dsimp at β hβ - refine ⟨U, (B.trW_iff_of_distinguished' _ (F.map_distinguished _ hT')).1 ?_, - β, d, by simpa using hβ.symm⟩ - rw [trW_iff] at hs' ⊢ - obtain ⟨_, _, _, hT'', hV⟩ := hs' - exact ⟨_, _, _, F.map_distinguished _ hT'', hV⟩ - -variable {B F} in -/-- Constructor for left localizing categories. -/ -lemma IsLeftLocalizing.mk' - (h : ∀ ⦃Y : C⦄ ⦃X : A⦄ (s : Y ⟶ F.obj X) (_ : B.trW s), - ∃ (X' : A) (s' : X' ⟶ X) (_ : (B.inverseImage F).trW s') - (b : F.obj X' ⟶ Y), b ≫ s = F.map s') : - B.IsLeftLocalizing F := by - have : B.op.IsRightLocalizing F.op := IsRightLocalizing.mk' (fun X Y s hs => by - obtain ⟨X', s', h, b, fac⟩ := h s.unop (trW_of_op _ hs) - exact ⟨Opposite.op X', s'.op, trW_of_unop _ h, b.op, Quiver.Hom.unop_inj fac⟩) - exact B.isLeftLocalizing_of_op F - -end - -variable (L : C ⥤ D) [L.IsLocalization B.trW] - -section - -variable [B.IsClosedUnderIsomorphisms] - (L' : A ⥤ D') [L'.IsLocalization (B.inverseImage F).trW] - (F' : D' ⥤ D) [Localization.Lifting L' (B.inverseImage F).trW (F ⋙ L) F'] - [IsTriangulated C] - -include L L' F' in -set_option backward.isDefEq.respectTransparency false in -lemma full_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] : F'.Full := by - have := Localization.essSurj L' (B.inverseImage F).trW - apply F'.full_of_precomp_essSurj L' - intro X₁ X₂ φ - have e := Localization.Lifting.iso L' (B.inverseImage F).trW (F ⋙ L) F' - obtain ⟨φ', hφ'⟩ : ∃ φ', φ = e.hom.app X₁ ≫ φ' ≫ e.inv.app X₂ := - ⟨e.inv.app X₁ ≫ φ ≫ e.hom.app X₂, by simp⟩ - obtain ⟨f, hf⟩ := Localization.exists_leftFraction L B.trW φ' - obtain ⟨X₃, s', hs', t, fac⟩ := B.fac_of_isRightLocalizing' F f.s f.hs - let f' : (B.inverseImage F).trW.LeftFraction X₁ X₂ := - { f := F.preimage (f.f ≫ t) - s := F.preimage (f.s ≫ t) - hs := by - rw [B.inverseImage_trW_iff, F.map_preimage, fac, ← B.inverseImage_trW_iff F] - exact hs' } - have hf' : φ' ≫ L.map (F.map f'.s) = L.map (F.map f'.f) := by - replace hf := hf =≫ L.map (f.s) - rw [f.map_comp_map_s] at hf - dsimp - rw [F.map_preimage, F.map_preimage, L.map_comp, L.map_comp, reassoc_of% hf] - have : IsIso (F'.map (L'.map f'.s)) := - ((MorphismProperty.isomorphisms D).arrow_mk_iso_iff - ((Arrow.isoOfNatIso e) (Arrow.mk f'.s))).2 - (Localization.inverts _ B.trW _ - (by simpa only [← B.inverseImage_trW_iff F] using f'.hs)) - refine ⟨f'.map L' (Localization.inverts _ _), ?_⟩ - rw [hφ', ← cancel_mono (F'.map (L'.map f'.s)), ← F'.map_comp, f'.map_comp_map_s, - assoc, assoc] - erw [← e.inv.naturality] - rw [Functor.comp_map, reassoc_of% hf'] - erw [e.inv.naturality, e.hom_inv_id_app_assoc] - rfl - -set_option backward.isDefEq.respectTransparency false in -include L L' in -lemma faithful_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] [F.Faithful] : - F'.Faithful := by - have e := Localization.Lifting.iso L' (B.inverseImage F).trW (F ⋙ L) F' - have := IsTriangulated.of_fully_faithful_triangulated_functor F - letI := Localization.preadditive L' (B.inverseImage F).trW - letI := Localization.functor_additive L' (B.inverseImage F).trW - letI := Localization.preadditive L B.trW - letI := Localization.functor_additive L B.trW - have : (B.inverseImage F).trW.HasLeftCalculusOfFractions := inferInstance - have : F'.Additive := by - rw [Localization.functor_additive_iff L' (B.inverseImage F).trW] - exact Functor.additive_of_iso e.symm - sorry - /- - apply F'.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions L' (B.inverseImage F).trW - intro X₁ X₂ f hf - replace hf : L.map (F.map f) = L.map 0 := by - erw [L.map_zero, ← NatIso.naturality_1 e f, hf, zero_comp, comp_zero] - rw [MorphismProperty.map_eq_iff_postcomp L B.trW] at hf - obtain ⟨Z, s, hs, fac⟩ := hf - rw [zero_comp] at fac - obtain ⟨W, s', hs', t, fac'⟩ := B.fac_of_isRightLocalizing' F s hs - have hfs' : f ≫ s' = 0 := F.map_injective (by - rw [F.map_zero, F.map_comp, ← fac', reassoc_of% fac, zero_comp]) - have := Localization.inverts L' (B.inverseImage F).trW s' hs' - rw [← cancel_mono (L'.map s'), zero_comp, ← L'.map_comp, hfs', L'.map_zero]-/ - -end - -variable {L : C ⥤ D} {L' : A ⥤ D'} {H : D' ⥤ D} (e : L' ⋙ H ≅ F ⋙ L) - [L'.EssSurj] [H.Full] [H.Faithful] [L.IsLocalization B.trW] - [IsTriangulated C] [B.IsClosedUnderIsomorphisms] - -include e in -lemma isLocalization_of_isRightLocalizing [B.IsRightLocalizing F] [F.Full] [F.Faithful] : - L'.IsLocalization (B.inverseImage F).trW := by - have hL' : (B.inverseImage F).trW.IsInvertedBy L' := fun X₁ X₂ f hf => by - rw [B.inverseImage_trW_iff] at hf - have : IsIso (H.map (L'.map f)) := - ((MorphismProperty.isomorphisms D).arrow_mk_iso_iff - (Arrow.isoOfNatIso e f)).2 (Localization.inverts L B.trW _ hf) - apply isIso_of_fully_faithful H - let G := Localization.lift _ hL' (B.inverseImage F).trW.Q - have eG : (B.inverseImage F).trW.Q ⋙ G ≅ L' := - Localization.Lifting.iso _ (B.inverseImage F).trW _ _ - have : Localization.Lifting (B.inverseImage F).trW.Q (B.inverseImage F).trW - (F ⋙ L) (G ⋙ H) := - ⟨(Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight eG H ≪≫ e⟩ - have := full_of_isRightLocalizing B F L (B.inverseImage F).trW.Q (G ⋙ H) - have := faithful_of_isRightLocalizing B F L (B.inverseImage F).trW.Q (G ⋙ H) - have : G.EssSurj := - { mem_essImage := fun X => - ⟨_, ⟨eG.app (L'.objPreimage X) ≪≫ L'.objObjPreimageIso X⟩⟩ } - have : G.Full := Functor.Full.of_comp_faithful G H - have : G.Faithful := Functor.Faithful.of_comp_iso (Iso.refl (G ⋙ H)) - have : G.IsEquivalence := { } - exact Functor.IsLocalization.of_equivalence_target (B.inverseImage F).trW.Q _ _ - G.asEquivalence eG - -include e in -lemma isLocalization_of_isLeftLocalizing [B.IsLeftLocalizing F] [F.Full] [F.Faithful] : - L'.IsLocalization (B.inverseImage F).trW := by - rw [← Functor.IsLocalization.op_iff, ← trW_op] - have : Functor.IsLocalization L.op (B.op.trW) := by - rw [trW_op] - infer_instance - let e' : L'.op ⋙ H.op ≅ F.op ⋙ L.op := NatIso.op e.symm - exact B.op.isLocalization_of_isRightLocalizing F.op e' - --/ +instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : + (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful where + nonempty_fullyFaithful := by + let L₁ := (B.inverseImage A.ι).trW.Q + let L₂ := B.trW.Q + let F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization := + (A.triangulatedLocalizedMorphism B).localizedFunctor L₁ L₂ + let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := + CatCommSq.iso (A.triangulatedLocalizedMorphism B).functor L₁ L₂ F + have : F.Full := sorry + have : F.Faithful := sorry + exact ⟨.ofFullyFaithful F⟩ end ObjectProperty + end CategoryTheory From f38643665494265e2f5328faac4b3454591bf6a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 28 Apr 2026 22:42:51 +0200 Subject: [PATCH 06/26] wip --- .../Triangulated/LocalizingSubcategory.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index db76c6498f69a6..59dec93f43235c 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -154,7 +154,8 @@ def triangulatedLocalizedMorphism [A.IsTriangulated] : obtain ⟨Z, a, b, hT, hZ⟩ := hf exact ⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩ -instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : +instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedRightLocalizing B] : (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful where nonempty_fullyFaithful := by let L₁ := (B.inverseImage A.ι).trW.Q @@ -167,6 +168,11 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : have : F.Faithful := sorry exact ⟨.ofFullyFaithful F⟩ +instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedLeftLocalizing B] : + (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful := by + sorry + end ObjectProperty end CategoryTheory From cf5ae46d5173ab03df2a77290f5a43d433e500bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 11:16:01 +0200 Subject: [PATCH 07/26] wip --- .../Triangulated/LocalizingSubcategory.lean | 34 ++++++++++++++++--- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 59dec93f43235c..81154565aaf030 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -114,6 +114,14 @@ lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] exact ⟨U, t, a, hU, (B.trW_iff_of_distinguished' _ hT').1 (trW_monotone (by simp) _ hs'), by cat_disch⟩ +variable {A B} in +lemma IsTriangulatedRightLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedRightLocalizing B] + {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) : + ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := + (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs + -- to be moved instance [A.ContainsZero] [B.ContainsZero] [B.IsClosedUnderIsomorphisms] : (A ⊓ B).ContainsZero where @@ -140,6 +148,14 @@ lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs) exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ +variable {A B} in +lemma IsTriangulatedLeftLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedLeftLocalizing B] + {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) : + ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := + (isTriangulatedLeftLocalizing_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 localized morphism, @@ -154,8 +170,9 @@ def triangulatedLocalizedMorphism [A.IsTriangulated] : obtain ⟨Z, a, b, hT, hZ⟩ := hf exact ⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩ -instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsTriangulatedRightLocalizing B] : +variable [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + +instance [A.IsTriangulatedRightLocalizing B] : (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful where nonempty_fullyFaithful := by let L₁ := (B.inverseImage A.ι).trW.Q @@ -164,8 +181,17 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] (A.triangulatedLocalizedMorphism B).localizedFunctor L₁ L₂ let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizedMorphism B).functor L₁ L₂ F - have : F.Full := sorry - have : F.Faithful := sorry + have : F.Full := + Functor.full_of_precomp_essSurj _ L₁ (fun X₁ X₂ φ ↦ by + 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]⟩ + dsimp at φ' hφ' + obtain ⟨f, hf⟩ := Localization.exists_leftFraction L₂ B.trW φ' + have := IsTriangulatedRightLocalizing.fac' f.s X₂.property f.hs + sorry ) + have : F.Faithful := by + sorry exact ⟨.ofFullyFaithful F⟩ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] From b318aaded3a392b1ea880a310f128437d9c74be1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 14:00:29 +0200 Subject: [PATCH 08/26] wip --- .../ObjectProperty/CompleteLattice.lean | 13 ++++ Mathlib/CategoryTheory/Opposites.lean | 5 ++ .../Triangulated/LocalizingSubcategory.lean | 73 ++++++++++++++++++- 3 files changed, 88 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean index 51dd57c087bcb7..d9885743f9b9eb 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean @@ -7,6 +7,7 @@ module public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory +public import Mathlib.CategoryTheory.ObjectProperty.Opposite public import Mathlib.Order.CompleteLattice.Basic /-! @@ -41,6 +42,18 @@ instance nonempty_sup_right [Q.Nonempty] : (P ⊔ Q).Nonempty := instance nonempty_top [Nonempty C] : (⊤ : ObjectProperty C).Nonempty := nonempty_of_prop (X := Classical.arbitrary C) (by trivial) +@[simp] +lemma op_inf : (P ⊓ Q).op = P.op ⊓ Q.op := rfl + +@[simp] +lemma op_sup : (P ⊔ Q).op = P.op ⊔ Q.op := rfl + +@[simp] +lemma unop_inf (P Q : ObjectProperty Cᵒᵖ) : (P ⊓ Q).unop = P.unop ⊓ Q.unop := rfl + +@[simp] +lemma unop_sup (P Q : ObjectProperty Cᵒᵖ) : (P ⊔ Q).unop = P.unop ⊔ Q.unop := rfl + lemma isoClosure_sup : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure := by ext X simp only [prop_sup_iff] diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 56ea73ea8546e8..1ebe3871954b75 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/Mathlib/CategoryTheory/Opposites.lean @@ -305,6 +305,11 @@ instance {F : C ⥤ D} [Faithful F] : Faithful F.op where protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where preimage {X Y} f := .op <| hF.preimage f.unop +/-- A functor is fully faithful when its opposite is fully faithful. -/ +protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) : + F.unop.FullyFaithful where + preimage {X Y} f := (hF.preimage f.op).unop + /-- If F is faithful then the `rightOp` of F is also faithful. -/ instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h)) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 81154565aaf030..1335014722a93e 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -30,6 +30,14 @@ namespace ObjectProperty variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] +@[simps] +def opEquivalence (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ where + functor := (P.lift P.op.ι.leftOp (fun X ↦ X.unop.property)).rightOp + inverse := P.op.lift P.ι.op (fun X ↦ X.unop.property) + unitIso := Iso.refl _ + counitIso := Iso.refl _ + functor_unitIso_comp X := Quiver.Hom.unop_inj (by cat_disch) + /-- If `A` and `B` are triangulated subcategories of a (pre)triangulated category `C` (with `B` closed under isomorphisms), we say that `A` is right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and @@ -170,6 +178,28 @@ def triangulatedLocalizedMorphism [A.IsTriangulated] : obtain ⟨Z, a, b, hT, hZ⟩ := hf exact ⟨_, _, _, A.ι.map_distinguished _ hT, hZ⟩ +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] instance [A.IsTriangulatedRightLocalizing B] : @@ -188,8 +218,22 @@ instance [A.IsTriangulatedRightLocalizing B] : simp [dsimp% e.inv_hom_id_app_assoc, dsimp% e.inv_hom_id_app]⟩ dsimp at φ' hφ' obtain ⟨f, hf⟩ := Localization.exists_leftFraction L₂ B.trW φ' - have := IsTriangulatedRightLocalizing.fac' f.s X₂.property f.hs - sorry ) + obtain ⟨X₃, s', a, hX₃, hs', fac⟩ := + IsTriangulatedRightLocalizing.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 : IsIso (L₁.map g.s) := + Localization.inverts L₁ (B.inverseImage A.ι).trW _ 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] + dsimp [g] + simp only [← fac, hφ', Category.assoc, hf, ← dsimp% NatIso.naturality_1 e, + homMk_hom, Functor.map_comp, assoc, dsimp% e.hom_inv_id_app_assoc, + MorphismProperty.LeftFraction.map_comp_map_s_assoc] ) have : F.Faithful := by sorry exact ⟨.ofFullyFaithful F⟩ @@ -197,7 +241,30 @@ instance [A.IsTriangulatedRightLocalizing B] : instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsTriangulatedLeftLocalizing B] : (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful := by - sorry + let L₁ := (B.inverseImage A.ι).trW.Q + let L₂ := B.trW.Q + let F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization := + (A.triangulatedLocalizedMorphism B).localizedFunctor L₁ L₂ + letI : CatCommSq (A.op.triangulatedLocalizedMorphism B.op).functor + (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op := + ⟨Functor.isoWhiskerLeft A.opEquivalence.functor + (NatIso.op (CatCommSq.iso (A.triangulatedLocalizedMorphism 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 + · intro _ _ f hf + refine Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_ + simpa [trW_inverseImage_ι_iff, ← op_inf, trW_op] using hf + exact LocalizerMorphism.IsLocalizedFullyFaithful.mk' (A.triangulatedLocalizedMorphism B) + L₁ L₂ F (((A.op.triangulatedLocalizedMorphism B.op).fullyFaithful + (A.opEquivalence.functor ⋙ L₁.op) L₂.op F.op).unop) end ObjectProperty From 33b5686fb79c6a8a962e00f4d8d586b6e7b780fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 16:25:12 +0200 Subject: [PATCH 09/26] sorry free --- .../Triangulated/LocalizingSubcategory.lean | 59 +++++++++++++++++-- 1 file changed, 55 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 1335014722a93e..e76fb1cc46c6ac 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -26,10 +26,42 @@ namespace CategoryTheory open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite +-- to be moved +lemma Functor.faithful_of_precomp_of_hasLeftCalculusOfFractions + {C D E : Type*} [Category* C] [Category* D] [Category* E] + (F : D ⥤ E) (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W] + [W.HasLeftCalculusOfFractions] + (h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g) : + Faithful F := by + have := Localization.essSurj L W + refine F.faithful_of_precomp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_) + obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g + have := Localization.inverts L W φ.s φ.hs + rw [← cancel_mono (L.map φ.s)] + erw [φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L] + apply h + simpa only [← F.map_comp, φ.fst.map_comp_map_s, φ.snd.map_comp_map_s] using + hfg =≫ F.map (L.map φ.s) + +-- to be moved +lemma Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions + {C D E : Type*} [Category* C] [Category* D] [Category* E] + (F : D ⥤ E) (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W] + [W.HasLeftCalculusOfFractions] + [Preadditive C] [Preadditive D] [Preadditive E] [L.Additive] [F.Additive] + (h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0) : + Faithful F := + faithful_of_precomp_of_hasLeftCalculusOfFractions F L W + (fun X₁ X₂ f g hfg => by + rw [← sub_eq_zero, ← L.map_sub] + exact h _ (by rw [L.map_sub, F.map_sub, hfg, sub_self])) + namespace ObjectProperty variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] +/-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory` +and `P.FullSubcategoryᵒᵖ`. -/ @[simps] def opEquivalence (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ where functor := (P.lift P.op.ι.leftOp (fun X ↦ X.unop.property)).rightOp @@ -234,8 +266,28 @@ instance [A.IsTriangulatedRightLocalizing B] : simp only [← fac, hφ', Category.assoc, hf, ← dsimp% NatIso.naturality_1 e, homMk_hom, Functor.map_comp, assoc, dsimp% e.hom_inv_id_app_assoc, MorphismProperty.LeftFraction.map_comp_map_s_assoc] ) - have : F.Faithful := by - sorry + have : F.Additive := by + rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW] + exact Functor.additive_of_iso e + have : F.Faithful := + Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions _ L₁ + (B.inverseImage A.ι).trW (fun X₁ X₂ f hf ↦ by + 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 + simp only [zero_comp] at fac + obtain ⟨X₄, t, a, hX₄, ht, fac'⟩ := + IsTriangulatedRightLocalizing.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 + dsimp [t'] + rw [← fac', reassoc_of% fac, zero_comp]) exact ⟨.ofFullyFaithful F⟩ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] @@ -259,8 +311,7 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] intro _ _ f hf simp only [MorphismProperty.inverseImage_iff, Equivalence.symm_functor] at hf ⊢ exact MorphismProperty.le_isoClosure _ _ hf - · intro _ _ f hf - refine Localization.inverts L₁.op (B.inverseImage A.ι).trW.op _ ?_ + · 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.triangulatedLocalizedMorphism B) L₁ L₂ F (((A.op.triangulatedLocalizedMorphism B.op).fullyFaithful From 2c22505f268027f673ccdd47e60b319d308f46c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 16:31:38 +0200 Subject: [PATCH 10/26] wip --- .../CalculusOfFractions/Fractions.lean | 15 ++++++++ .../CalculusOfFractions/Preadditive.lean | 11 ++++++ .../Triangulated/LocalizingSubcategory.lean | 34 ++----------------- 3 files changed, 28 insertions(+), 32 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean index fea1ca061ab25b..9685b1d724789d 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean @@ -319,4 +319,19 @@ lemma exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) : end Localization +lemma Functor.faithful_of_precomp_of_hasLeftCalculusOfFractions + {E : Type*} [Category* E] (F : D ⥤ E) + [W.HasLeftCalculusOfFractions] + (h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g) : + Faithful F := by + have := Localization.essSurj L W + refine F.faithful_of_precomp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_) + obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g + have := Localization.inverts L W φ.s φ.hs + rw [← cancel_mono (L.map φ.s)] + erw [φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L] + apply h + simpa only [← F.map_comp, φ.fst.map_comp_map_s, φ.snd.map_comp_map_s] using + hfg =≫ F.map (L.map φ.s) + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean index 75e5824a5a84b8..11852867843a4a 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean @@ -358,4 +358,15 @@ instance [HasZeroObject C] : HasZeroObject W.Localization' := W.Q'.hasZeroObject end Localization +lemma Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions + {E : Type*} [Category* E] (F : D ⥤ E) + [W.HasLeftCalculusOfFractions] + [Preadditive D] [Preadditive E] [L.Additive] [F.Additive] + (h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0) : + Faithful F := + faithful_of_precomp_of_hasLeftCalculusOfFractions L W F + (fun X₁ X₂ f g hfg => by + rw [← sub_eq_zero, ← L.map_sub] + exact h _ (by rw [L.map_sub, F.map_sub, hfg, sub_self])) + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index e76fb1cc46c6ac..4c1610a73cdf0c 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -26,36 +26,6 @@ namespace CategoryTheory open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite --- to be moved -lemma Functor.faithful_of_precomp_of_hasLeftCalculusOfFractions - {C D E : Type*} [Category* C] [Category* D] [Category* E] - (F : D ⥤ E) (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W] - [W.HasLeftCalculusOfFractions] - (h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g) : - Faithful F := by - have := Localization.essSurj L W - refine F.faithful_of_precomp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_) - obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g - have := Localization.inverts L W φ.s φ.hs - rw [← cancel_mono (L.map φ.s)] - erw [φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L] - apply h - simpa only [← F.map_comp, φ.fst.map_comp_map_s, φ.snd.map_comp_map_s] using - hfg =≫ F.map (L.map φ.s) - --- to be moved -lemma Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions - {C D E : Type*} [Category* C] [Category* D] [Category* E] - (F : D ⥤ E) (L : C ⥤ D) (W : MorphismProperty C) [L.IsLocalization W] - [W.HasLeftCalculusOfFractions] - [Preadditive C] [Preadditive D] [Preadditive E] [L.Additive] [F.Additive] - (h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0) : - Faithful F := - faithful_of_precomp_of_hasLeftCalculusOfFractions F L W - (fun X₁ X₂ f g hfg => by - rw [← sub_eq_zero, ← L.map_sub] - exact h _ (by rw [L.map_sub, F.map_sub, hfg, sub_self])) - namespace ObjectProperty variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] @@ -270,8 +240,8 @@ instance [A.IsTriangulatedRightLocalizing B] : rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW] exact Functor.additive_of_iso e have : F.Faithful := - Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions _ L₁ - (B.inverseImage A.ι).trW (fun X₁ X₂ f hf ↦ by + Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions L₁ + (B.inverseImage A.ι).trW _ (fun X₁ X₂ f hf ↦ by 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 From 9c51b9a2c48b48b123b6f3222a2de3ef3e28b9bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 19:48:00 +0200 Subject: [PATCH 11/26] wip --- .../Localization/LocalizerMorphism.lean | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index 9c0da740687e39..6b46e96db925ae 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -307,6 +307,38 @@ instance [Φ.IsLocalizedFullyFaithful] : Φ.op.IsLocalizedFullyFaithful := by exact IsLocalizedFullyFaithful.mk' Φ.op W₁.Q.op W₂.Q.op G.op (Φ.fullyFaithful W₁.Q W₂.Q G).op +lemma isLocalization_of_isLocalizedFullyFaithful + [Φ.IsLocalizedFullyFaithful] {L₂ : C₂ ⥤ D₂} [L₂.IsLocalization W₂] + {L₁ : C₁ ⥤ D₁} {F : D₁ ⥤ D₂} + (iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) + [F.Full] [F.Faithful] [L₁.EssSurj] : + L₁.IsLocalization W₁ := by + -- There is a better proof... + have := Localization.essSurj L₂ W₂ + let G' := Φ.localizedFunctor W₁.Q L₂ + let iso₂ : Φ.functor ⋙ L₂ ≅ W₁.Q ⋙ G' := + CatCommSq.iso Φ.functor W₁.Q L₂ (Φ.localizedFunctor W₁.Q L₂) + let G'' := ObjectProperty.lift F.essImage G' + (fun X ↦ ⟨L₁.obj (W₁.Q.objPreimage X), ⟨(iso.symm.trans iso₂).app _ ≪≫ + G'.mapIso (W₁.Q.objObjPreimageIso X)⟩⟩) + let iso₃ : G'' ⋙ F.essImage.ι ≅ G' := Iso.refl _ + have : G''.EssSurj := ⟨by + rintro ⟨X₂, X₁, ⟨e⟩⟩ + exact ⟨W₁.Q.obj (L₁.objPreimage X₁), ⟨ObjectProperty.isoMk _ + ((iso₂.symm.trans iso).app _ ≪≫ F.mapIso (L₁.objObjPreimageIso X₁) ≪≫ e)⟩⟩⟩ + have : G''.IsEquivalence := { } + let eq : W₁.Localization ≌ D₁ := + G''.asEquivalence.trans F.toEssImage.asEquivalence.symm + let iso₄ : W₁.Q ⋙ G'' ≅ L₁ ⋙ F.toEssImage := + ((whiskeringRight _ _ _).obj F.essImage.ι).preimageIso + (associator _ _ _ ≪≫ isoWhiskerLeft _ iso₃ ≪≫ iso₂.symm ≪≫ iso ≪≫ + isoWhiskerLeft L₁ F.toEssImageCompι.symm ≪≫ (associator _ _ _).symm) + let iso₅ : W₁.Q ⋙ eq.functor ≅ L₁ := + (associator _ _ _).symm ≪≫ isoWhiskerRight iso₄ _ ≪≫ + associator _ _ _ ≪≫ isoWhiskerLeft _ F.toEssImage.asEquivalence.unitIso.symm ≪≫ + L₁.rightUnitor + exact IsLocalization.of_equivalence_target W₁.Q W₁ L₁ eq iso₅ + /-- The localizer morphism from `W₁.arrow` to `W₂.arrow` that is induced by `Φ : LocalizerMorphism W₁ W₂`. -/ @[simps] From dc8e80c144727be9059b0618b95ed3fa533ed30e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 20:13:16 +0200 Subject: [PATCH 12/26] better proof --- .../Localization/LocalizerMorphism.lean | 41 ++++++++----------- 1 file changed, 16 insertions(+), 25 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index 6b46e96db925ae..3e3180af5e88c8 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -313,31 +313,22 @@ lemma isLocalization_of_isLocalizedFullyFaithful (iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) [F.Full] [F.Faithful] [L₁.EssSurj] : L₁.IsLocalization W₁ := by - -- There is a better proof... - have := Localization.essSurj L₂ W₂ - let G' := Φ.localizedFunctor W₁.Q L₂ - let iso₂ : Φ.functor ⋙ L₂ ≅ W₁.Q ⋙ G' := - CatCommSq.iso Φ.functor W₁.Q L₂ (Φ.localizedFunctor W₁.Q L₂) - let G'' := ObjectProperty.lift F.essImage G' - (fun X ↦ ⟨L₁.obj (W₁.Q.objPreimage X), ⟨(iso.symm.trans iso₂).app _ ≪≫ - G'.mapIso (W₁.Q.objObjPreimageIso X)⟩⟩) - let iso₃ : G'' ⋙ F.essImage.ι ≅ G' := Iso.refl _ - have : G''.EssSurj := ⟨by - rintro ⟨X₂, X₁, ⟨e⟩⟩ - exact ⟨W₁.Q.obj (L₁.objPreimage X₁), ⟨ObjectProperty.isoMk _ - ((iso₂.symm.trans iso).app _ ≪≫ F.mapIso (L₁.objObjPreimageIso X₁) ≪≫ e)⟩⟩⟩ - have : G''.IsEquivalence := { } - let eq : W₁.Localization ≌ D₁ := - G''.asEquivalence.trans F.toEssImage.asEquivalence.symm - let iso₄ : W₁.Q ⋙ G'' ≅ L₁ ⋙ F.toEssImage := - ((whiskeringRight _ _ _).obj F.essImage.ι).preimageIso - (associator _ _ _ ≪≫ isoWhiskerLeft _ iso₃ ≪≫ iso₂.symm ≪≫ iso ≪≫ - isoWhiskerLeft L₁ F.toEssImageCompι.symm ≪≫ (associator _ _ _).symm) - let iso₅ : W₁.Q ⋙ eq.functor ≅ L₁ := - (associator _ _ _).symm ≪≫ isoWhiskerRight iso₄ _ ≪≫ - associator _ _ _ ≪≫ isoWhiskerLeft _ F.toEssImage.asEquivalence.unitIso.symm ≪≫ - L₁.rightUnitor - exact IsLocalization.of_equivalence_target W₁.Q W₁ L₁ eq iso₅ + have h : W₁.IsInvertedBy L₁ := fun _ _ f hf ↦ by + rw [← isIso_iff_of_reflects_iso _ F] + exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff + (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf)) + let G := Localization.lift L₁ h W₁.Q + let e : W₁.Q ⋙ G ≅ L₁ := Localization.fac L₁ h W₁.Q + letI : CatCommSq Φ.functor W₁.Q L₂ (G ⋙ F) := + ⟨iso ≪≫ isoWhiskerRight e.symm _ ≪≫ associator _ _ _⟩ + have hG : G.FullyFaithful := Functor.FullyFaithful.ofCompFaithful + (Φ.fullyFaithful W₁.Q L₂ (G ⋙ F)) + have := hG.full + have := hG.faithful + have : G.EssSurj := + ⟨fun X ↦ ⟨W₁.Q.obj (L₁.objPreimage X), ⟨e.app _ ≪≫ L₁.objObjPreimageIso X⟩⟩⟩ + have : G.IsEquivalence := { } + exact IsLocalization.of_equivalence_target W₁.Q W₁ L₁ G.asEquivalence e /-- The localizer morphism from `W₁.arrow` to `W₂.arrow` that is induced by `Φ : LocalizerMorphism W₁ W₂`. -/ From ee8c3730a1f27ceb6be5f49f406871c9547ff21c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 29 Apr 2026 21:47:55 +0200 Subject: [PATCH 13/26] cleaning up --- .../Localization/CalculusOfFractions.lean | 12 ++++++++---- .../CalculusOfFractions/Fractions.lean | 17 ++++++++++------- .../Triangulated/LocalizingSubcategory.lean | 3 +-- 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean index 910b287f3116b0..0c28286c73f2a5 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean @@ -66,6 +66,10 @@ variable {W} def ofInv (s : Y ⟶ X) (hs : W s) : W.LeftFraction X Y := mk (𝟙 X) s hs +instance {X Y : C} {L : C ⥤ D} [L.IsLocalization W] (z : W.LeftFraction X Y) : + IsIso (L.map z.s) := + Localization.inverts L W _ z.hs + /-- If `φ : W.LeftFraction X Y` and `L` is a functor which inverts `W`, this is the induced morphism `L.obj X ⟶ L.obj Y` -/ noncomputable def map (φ : W.LeftFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) : @@ -134,6 +138,10 @@ variable {W} def ofInv (s : Y ⟶ X) (hs : W s) : W.RightFraction X Y := mk s hs (𝟙 Y) +instance {X Y : C} {L : C ⥤ D} [L.IsLocalization W] (z : W.RightFraction X Y) : + IsIso (L.map z.s) := + Localization.inverts L W _ z.hs + /-- If `φ : W.RightFraction X Y` and `L` is a functor which inverts `W`, this is the induced morphism `L.obj X ⟶ L.obj Y` -/ noncomputable def map (φ : W.RightFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) : @@ -649,7 +657,6 @@ end lemma homMk_eq {X Y : C} (f : LeftFraction W X Y) : homMk f = f.map (Q W) (Localization.inverts _ W) := by - have := Localization.inverts (Q W) W f.s f.hs rw [← Q_map_comp_Qinv f.f f.s f.hs, ← cancel_mono ((Q W).map f.s), assoc, Qiso_inv_hom_id, comp_id, map_comp_map_s] @@ -683,7 +690,6 @@ lemma map_compatibility {W} {X Y : C} φ.map L₂ (Localization.inverts L₂ W) ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y := by let e := Localization.compUniqFunctor L₁ L₂ W - have := Localization.inverts L₂ W φ.s φ.hs rw [← cancel_mono (e.hom.app Y), assoc, assoc, e.inv_hom_id_app, comp_id, ← cancel_mono (L₂.map φ.s), assoc, assoc, map_comp_map_s, ← e.hom.naturality] simpa [← Functor.map_comp_assoc, map_comp_map_s] using e.hom.naturality φ.f @@ -701,8 +707,6 @@ lemma map_comp_map_eq_map {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.Left (L : C ⥤ D) [L.IsLocalization W] : z₁.map L (Localization.inverts L W) ≫ z₂.map L (Localization.inverts L W) = (z₁.comp₀ z₂ z₃).map L (Localization.inverts L W) := by - have := Localization.inverts L W _ z₂.hs - have := Localization.inverts L W _ z₃.hs have : IsIso (L.map (z₂.s ≫ z₃.s)) := by rw [L.map_comp] infer_instance diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean index 9685b1d724789d..2a131b7b359915 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean @@ -55,6 +55,9 @@ structure LeftFraction₂ (X Y : C) where /-- the condition that the denominator belongs to the given morphism property -/ hs : W s +instance {X Y : C} (z : W.LeftFraction₂ X Y) : IsIso (L.map z.s) := + Localization.inverts L W _ z.hs + /-- This structure contains the data of three left fractions for `W : MorphismProperty C` that have the same "denominator". -/ structure LeftFraction₃ (X Y : C) where @@ -71,6 +74,9 @@ structure LeftFraction₃ (X Y : C) where /-- the condition that the denominator belongs to the given morphism property -/ hs : W s +instance {X Y : C} (z : W.LeftFraction₃ X Y) : IsIso (L.map z.s) := + Localization.inverts L W _ z.hs + /-- This structure contains the data of two right fractions for `W : MorphismProperty C` that have the same "denominator". -/ structure RightFraction₂ (X Y : C) where @@ -85,6 +91,9 @@ structure RightFraction₂ (X Y : C) where /-- the numerator of the second right fraction -/ f' : X' ⟶ Y +instance {X Y : C} (z : W.RightFraction₂ X Y) : IsIso (L.map z.s) := + Localization.inverts L W _ z.hs + variable {W} /-- The equivalence relation on tuples of left fractions with the same denominator @@ -274,8 +283,6 @@ lemma exists_leftFraction₂ {X Y : C} (f f' : L.obj X ⟶ L.obj Y) : f' := φ'.f ≫ α.s s := φ'.s ≫ α.s hs := W.comp_mem _ _ φ'.hs α.hs } - have := inverts L W _ φ'.hs - have := inverts L W _ α.hs have : IsIso (L.map (φ'.s ≫ α.s)) := by rw [L.map_comp] infer_instance @@ -303,8 +310,6 @@ lemma exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) : f'' := β.f ≫ γ.s s := β.s ≫ γ.s hs := W.comp_mem _ _ β.hs γ.hs } - have := inverts L W _ β.hs - have := inverts L W _ γ.hs have : IsIso (L.map (β.s ≫ γ.s)) := by rw [L.map_comp] infer_instance @@ -327,9 +332,7 @@ lemma Functor.faithful_of_precomp_of_hasLeftCalculusOfFractions have := Localization.essSurj L W refine F.faithful_of_precomp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_) obtain ⟨φ, rfl, rfl⟩ := Localization.exists_leftFraction₂ L W f g - have := Localization.inverts L W φ.s φ.hs - rw [← cancel_mono (L.map φ.s)] - erw [φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L] + rw [← cancel_mono (L.map φ.s), φ.fst.map_comp_map_s L, φ.snd.map_comp_map_s L] apply h simpa only [← F.map_comp, φ.fst.map_comp_map_s, φ.snd.map_comp_map_s] using hfg =≫ F.map (L.map φ.s) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 4c1610a73cdf0c..a7a800fe249aa9 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -227,8 +227,7 @@ instance [A.IsTriangulatedRightLocalizing B] : f := A.homMk (f.f ≫ a) s := A.homMk s' hs := by rwa [trW_inverseImage_ι_iff] } - have : IsIso (L₁.map g.s) := - Localization.inverts L₁ (B.inverseImage A.ι).trW _ g.hs + have : IsIso (L₁.map g.s) := 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] From 2050130b82f7eac99fa39b5d525250ee179e421c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 30 Apr 2026 11:30:03 +0200 Subject: [PATCH 14/26] cleaning up --- Mathlib.lean | 1 + .../ObjectProperty/ContainsZero.lean | 6 +++++ .../ObjectProperty/Opposite.lean | 10 +++++++ .../Triangulated/LocalizingSubcategory.lean | 26 +------------------ .../Triangulated/Subcategory.lean | 6 +++++ 5 files changed, 24 insertions(+), 25 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 789113aab01f3d..9ff782fb9e66db 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3403,6 +3403,7 @@ public import Mathlib.CategoryTheory.Triangulated.Basic public import Mathlib.CategoryTheory.Triangulated.Functor public import Mathlib.CategoryTheory.Triangulated.Generators public import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor +public import Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor public import Mathlib.CategoryTheory.Triangulated.Opposite.OpOp diff --git a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean b/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean index ccee814b58d77a..c6b298d022d804 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean @@ -103,6 +103,12 @@ instance [P.ContainsZero] : HasZeroObject P.FullSubcategory where obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero exact ⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩ +instance [P.ContainsZero] [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] : + (P ⊓ Q).ContainsZero where + exists_zero := by + obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero + exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩ + end ObjectProperty /-- Given a functor `F : C ⥤ D`, this is the property of objects of `C` diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index 45dfa285be59cb..d22fb6225918f9 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -137,6 +137,16 @@ lemma unop_isoClosure (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure := by rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop] +/-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory` +and `P.FullSubcategoryᵒᵖ`. -/ +@[simps] +def opEquivalence (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ where + functor := (P.lift P.op.ι.leftOp (fun X ↦ X.unop.property)).rightOp + inverse := P.op.lift P.ι.op (fun X ↦ X.unop.property) + unitIso := Iso.refl _ + counitIso := Iso.refl _ + functor_unitIso_comp X := Quiver.Hom.unop_inj (by cat_disch) + end end CategoryTheory.ObjectProperty diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index a7a800fe249aa9..fb9ee373e92686 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -24,22 +24,12 @@ public import Mathlib.CategoryTheory.Localization.Triangulated namespace CategoryTheory -open Category Limits Pretriangulated Triangulated Pretriangulated.Opposite +open Category Limits Pretriangulated Opposite namespace ObjectProperty variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] -/-- Given `P : ObjectProperty C`, this is the equivalence between `P.op.FullSubcategory` -and `P.FullSubcategoryᵒᵖ`. -/ -@[simps] -def opEquivalence (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ where - functor := (P.lift P.op.ι.leftOp (fun X ↦ X.unop.property)).rightOp - inverse := P.op.lift P.ι.op (fun X ↦ X.unop.property) - unitIso := Iso.refl _ - counitIso := Iso.refl _ - functor_unitIso_comp X := Quiver.Hom.unop_inj (by cat_disch) - /-- If `A` and `B` are triangulated subcategories of a (pre)triangulated category `C` (with `B` closed under isomorphisms), we say that `A` is right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and @@ -132,20 +122,6 @@ lemma IsTriangulatedRightLocalizing.fac' ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs --- to be moved -instance [A.ContainsZero] [B.ContainsZero] [B.IsClosedUnderIsomorphisms] : - (A ⊓ B).ContainsZero where - exists_zero := by - obtain ⟨Z, hZ, hA⟩ := A.exists_prop_of_containsZero - exact ⟨Z, hZ, hA, B.prop_of_isZero hZ⟩ - --- to be moved -instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - (A ⊓ B).IsTriangulated where - ext₂' T hT h₁ h₃ := by - obtain ⟨Y, hY, ⟨e⟩⟩ := A.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1 - exact ⟨Y, ⟨hY, B.prop_of_iso e (B.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩ - lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : A.IsTriangulatedLeftLocalizing B ↔ diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean index 3dde43aae82633..20f61551c26639 100644 --- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean @@ -178,6 +178,12 @@ instance [P.IsTriangulated] : P.IsTriangulatedClosed₃ where instance [P.IsTriangulated] : P.isoClosure.IsTriangulated where +instance {Q : ObjectProperty C} [P.IsTriangulated] [Q.IsTriangulated] + [Q.IsClosedUnderIsomorphisms] : + (P ⊓ Q).IsTriangulated where + ext₂' T hT h₁ h₃ := by + obtain ⟨Y, hY, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1 + exact ⟨Y, ⟨hY, Q.prop_of_iso e (Q.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩ section From 824e35ab36a71203282864510246b8319762c2a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 30 Apr 2026 11:36:18 +0200 Subject: [PATCH 15/26] cleaning up --- .../ObjectProperty/CompleteLattice.lean | 13 ------------- Mathlib/CategoryTheory/ObjectProperty/Opposite.lean | 13 +++++++++++++ 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean index d9885743f9b9eb..51dd57c087bcb7 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean @@ -7,7 +7,6 @@ module public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory -public import Mathlib.CategoryTheory.ObjectProperty.Opposite public import Mathlib.Order.CompleteLattice.Basic /-! @@ -42,18 +41,6 @@ instance nonempty_sup_right [Q.Nonempty] : (P ⊔ Q).Nonempty := instance nonempty_top [Nonempty C] : (⊤ : ObjectProperty C).Nonempty := nonempty_of_prop (X := Classical.arbitrary C) (by trivial) -@[simp] -lemma op_inf : (P ⊓ Q).op = P.op ⊓ Q.op := rfl - -@[simp] -lemma op_sup : (P ⊔ Q).op = P.op ⊔ Q.op := rfl - -@[simp] -lemma unop_inf (P Q : ObjectProperty Cᵒᵖ) : (P ⊓ Q).unop = P.unop ⊓ Q.unop := rfl - -@[simp] -lemma unop_sup (P Q : ObjectProperty Cᵒᵖ) : (P ⊔ Q).unop = P.unop ⊔ Q.unop := rfl - lemma isoClosure_sup : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure := by ext X simp only [prop_sup_iff] diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index d22fb6225918f9..94170494697bbb 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -6,6 +6,7 @@ Authors: Joël Riou module public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms +public import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice public import Mathlib.CategoryTheory.Opposites /-! @@ -147,6 +148,18 @@ def opEquivalence (P : ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcat counitIso := Iso.refl _ functor_unitIso_comp X := Quiver.Hom.unop_inj (by cat_disch) +@[simp] +lemma op_inf (P Q : ObjectProperty C) : (P ⊓ Q).op = P.op ⊓ Q.op := rfl + +@[simp] +lemma op_sup (P Q : ObjectProperty C) : (P ⊔ Q).op = P.op ⊔ Q.op := rfl + +@[simp] +lemma unop_inf (P Q : ObjectProperty Cᵒᵖ) : (P ⊓ Q).unop = P.unop ⊓ Q.unop := rfl + +@[simp] +lemma unop_sup (P Q : ObjectProperty Cᵒᵖ) : (P ⊔ Q).unop = P.unop ⊔ Q.unop := rfl + end end CategoryTheory.ObjectProperty From c8de21c5fd2a5419d3413be949de099b14ad419d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sat, 2 May 2026 17:40:06 +0200 Subject: [PATCH 16/26] fix --- Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean index 3e3180af5e88c8..03a65f3ff07079 100644 --- a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean +++ b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean @@ -138,7 +138,7 @@ lemma isEquivalence_iff : G.IsEquivalence ↔ G'.IsEquivalence := /-- If a localizer morphism induces a fully faithful functor on some choice of localized categories, it will be so for any choice of localized categories. -/ -noncomputable def fullyFaithfulImp (hG : G.FullyFaithful) : G'.FullyFaithful := +private noncomputable def fullyFaithfulImp (hG : G.FullyFaithful) : G'.FullyFaithful := let E₁ := Localization.uniq L₁ L₁' W₁ let E₂ := Localization.uniq L₂ L₂' W₂ let e : L₁ ⋙ G ⋙ E₂.functor ≅ L₁ ⋙ E₁.functor ⋙ G' := From e7f2c011db167f183876430a6930955bdd7d6d73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 08:48:24 +0200 Subject: [PATCH 17/26] docstring --- .../Triangulated/LocalizingSubcategory.lean | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index fb9ee373e92686..58519fe999f6b7 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -6,14 +6,17 @@ Authors: Joël Riou module public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory -public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated -public import Mathlib.CategoryTheory.Localization.Triangulated /-! # Localizing subcategories - +Let `C` be a pretriangulated category. If `A` and `B` are triangulated +subcategories of `C`, we define predicates (typeclasses +`IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) +saying that `A` is right `B`-localizing (or left `B`-localizing). +When `B` is closed under isomorphisms, we show that the functor +from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful. ## References * [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] @@ -190,7 +193,7 @@ instance [A.IsTriangulatedRightLocalizing B] : let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizedMorphism B).functor L₁ L₂ F have : F.Full := - Functor.full_of_precomp_essSurj _ L₁ (fun X₁ X₂ φ ↦ by + Functor.full_of_comp_essSurj _ L₁ (fun X₁ X₂ φ ↦ by 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]⟩ @@ -215,7 +218,7 @@ instance [A.IsTriangulatedRightLocalizing B] : rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW] exact Functor.additive_of_iso e have : F.Faithful := - Functor.faithful_of_precomp_cancel_zero_of_hasLeftCalculusOfFractions L₁ + Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions L₁ (B.inverseImage A.ι).trW _ (fun X₁ X₂ f hf ↦ by replace hf : L₂.map f.hom = L₂.map 0 := by simp [← dsimp% NatIso.naturality_2 e f, hf] From 6f5fcab71b4959389a78679fcca8cbfbaed6d964 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 6 May 2026 08:58:13 +0200 Subject: [PATCH 18/26] feat(CategoryTheory/Triangulated): definition of localising subcategories --- Mathlib.lean | 1 + .../CalculusOfFractions/Fractions.lean | 1 - .../CalculusOfFractions/Preadditive.lean | 1 - .../ObjectProperty/ContainsZero.lean | 6 + Mathlib/CategoryTheory/Opposites.lean | 5 + .../Triangulated/LocalizingSubcategory.lean | 148 ++++++++++++++++++ .../Triangulated/Subcategory.lean | 37 +++++ 7 files changed, 197 insertions(+), 2 deletions(-) create mode 100644 Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3435a680bbbdec..3096be03ef5ef3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3411,6 +3411,7 @@ public import Mathlib.CategoryTheory.Triangulated.Basic public import Mathlib.CategoryTheory.Triangulated.Functor public import Mathlib.CategoryTheory.Triangulated.Generators public import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor +public import Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory public import Mathlib.CategoryTheory.Triangulated.Opposite.Basic public import Mathlib.CategoryTheory.Triangulated.Opposite.Functor public import Mathlib.CategoryTheory.Triangulated.Opposite.OpOp diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean index de916a3feec983..7909502d5b18fa 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean @@ -324,7 +324,6 @@ lemma exists_leftFraction₃ {X Y : C} (f f' f'' : L.obj X ⟶ L.obj Y) : end Localization - lemma Functor.faithful_of_comp_of_hasLeftCalculusOfFractions {E : Type*} [Category* E] (F : D ⥤ E) [W.HasLeftCalculusOfFractions] diff --git a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean index 85cb86a3344a8d..4373e02609c531 100644 --- a/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean +++ b/Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean @@ -355,7 +355,6 @@ instance [HasZeroObject C] : HasZeroObject W.Localization' := W.Q'.hasZeroObject end Localization - lemma Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions {E : Type*} [Category* E] (F : D ⥤ E) [W.HasLeftCalculusOfFractions] diff --git a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean b/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean index ccee814b58d77a..c6b298d022d804 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean @@ -103,6 +103,12 @@ instance [P.ContainsZero] : HasZeroObject P.FullSubcategory where obtain ⟨X, h₁, h₂⟩ := P.exists_prop_of_containsZero exact ⟨_, IsZero.of_full_of_faithful_of_isZero P.ι ⟨X, h₂⟩ h₁⟩ +instance [P.ContainsZero] [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] : + (P ⊓ Q).ContainsZero where + exists_zero := by + obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero + exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩ + end ObjectProperty /-- Given a functor `F : C ⥤ D`, this is the property of objects of `C` diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean index 56ea73ea8546e8..1ebe3871954b75 100644 --- a/Mathlib/CategoryTheory/Opposites.lean +++ b/Mathlib/CategoryTheory/Opposites.lean @@ -305,6 +305,11 @@ instance {F : C ⥤ D} [Faithful F] : Faithful F.op where protected def FullyFaithful.op {F : C ⥤ D} (hF : F.FullyFaithful) : F.op.FullyFaithful where preimage {X Y} f := .op <| hF.preimage f.unop +/-- A functor is fully faithful when its opposite is fully faithful. -/ +protected def FullyFaithful.unop {F : Cᵒᵖ ⥤ Dᵒᵖ} (hF : F.FullyFaithful) : + F.unop.FullyFaithful where + preimage {X Y} f := (hF.preimage f.op).unop + /-- If F is faithful then the `rightOp` of F is also faithful. -/ instance rightOp_faithful {F : Cᵒᵖ ⥤ D} [Faithful F] : Faithful F.rightOp where map_injective h := Quiver.Hom.op_inj (map_injective F (Quiver.Hom.op_inj h)) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean new file mode 100644 index 00000000000000..83dd63959b42ae --- /dev/null +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory +public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated + +/-! +# Localizing subcategories + +Let `C` be a pretriangulated category. If `A` and `B` are triangulated +subcategories of `C`, we define predicates (typeclasses +`IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) +saying that `A` is right `B`-localizing (or left `B`-localizing). + +## References +* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] + +-/ + +@[expose] public section + +namespace CategoryTheory + +open Category Limits Pretriangulated Opposite + +namespace ObjectProperty + +variable {C D D' : Type*} [Category* C] [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 +right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and +`Y` in `A` factors through an object that is in `A` and `B`. +See `isTriangulatedRightLocalizing_iff` for another characterization. -/ +class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where + fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) : + ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f + +/-- If `A` and `B` are triangulated subcategories of a (pre)triangulated +category `C` (with `B` closed under isomorphisms), we say that `A` is +left `B`-localizing if any morphism `X ⟶ Y` with `X` in `A` and +`Y` in `B` factors through an object that is in `A` and `B`. +See `isTriangulatedLeftLocalizing_iff` for another characterization. -/ +class IsTriangulatedLeftLocalizing (A B : ObjectProperty C) : Prop where + fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) : + ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f + +instance (A B : ObjectProperty C) [A.IsTriangulatedLeftLocalizing B] : + A.op.IsTriangulatedRightLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := + IsTriangulatedLeftLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedLeftLocalizing B] : + A.unop.IsTriangulatedRightLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedLeftLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +instance (A B : ObjectProperty C) [A.IsTriangulatedRightLocalizing B] : + A.op.IsTriangulatedLeftLocalizing B.op where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.unop hY hX + exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ + +instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedRightLocalizing B] : + A.unop.IsTriangulatedLeftLocalizing B.unop where + fac f hX hY := by + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.op hY hX + exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ + +variable (A B : ObjectProperty C) + +lemma isTriangulatedLeftLocalizing_op_iff : + A.op.IsTriangulatedLeftLocalizing B.op ↔ A.IsTriangulatedRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedRightLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +lemma isTriangulatedRightLocalizing_op_iff : + A.op.IsTriangulatedRightLocalizing B.op ↔ A.IsTriangulatedLeftLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedLeftLocalizing B.op.unop), + fun _ ↦ inferInstance⟩ + +variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C] + [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] + +lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsTriangulatedRightLocalizing B ↔ + ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A X) (_ : B.trW s), + ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := by + refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩ + · rw [ObjectProperty.trW_iff'] at hs + obtain ⟨W, a, b, hT, hW⟩ := hs + obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac a hW hX + obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX + obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT' + c (𝟙 _) (by cat_disch) + refine ⟨U, e, g, hU, ?_, by cat_disch⟩ + rw [ObjectProperty.trW_iff'] + exact ⟨_, _, _, hT', h₁, h₂⟩ + · obtain ⟨Z, s, b, hT⟩ := Pretriangulated.distinguished_cocone_triangle f + have hs : B.trW s := by + rw [trW_iff'] + exact ⟨_, _, _, hT, hX⟩ + obtain ⟨W, s', g, hW, hs', fac⟩ := hA s hY hs + obtain ⟨U, hU, a, c, hT'⟩ := A.distinguished_cocone_triangle₁ s' hY hW + obtain ⟨t, ht, ht'⟩ := + complete_distinguished_triangle_morphism₁ _ _ hT hT' (𝟙 Y) g (by cat_disch) + exact ⟨U, t, a, hU, (B.trW_iff_of_distinguished' _ hT').1 (trW_monotone (by simp) _ hs'), + by cat_disch⟩ + +variable {A B} in +lemma IsTriangulatedRightLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedRightLocalizing B] + {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) : + ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := + (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs + +lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] + [B.IsClosedUnderIsomorphisms] : + A.IsTriangulatedLeftLocalizing B ↔ + ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A Y) (_ : B.trW s), + ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := by + rw [← isTriangulatedRightLocalizing_op_iff, isTriangulatedRightLocalizing_iff] + refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX hs ↦ ?_⟩ + · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff]) + exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', by cat_disch⟩ + · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.unop hX (trW_of_op _ hs) + exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ + +variable {A B} in +lemma IsTriangulatedLeftLocalizing.fac' + [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] + [A.IsTriangulatedLeftLocalizing B] + {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) : + ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := + (isTriangulatedLeftLocalizing_iff A B).1 inferInstance s hY hs + +end ObjectProperty + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean index 7392b7fdceb0d4..20f61551c26639 100644 --- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean @@ -90,6 +90,30 @@ lemma ext_of_isTriangulatedClosed₃' (h₁ : P T.obj₁) (h₂ : P T.obj₂) : P.isoClosure T.obj₃ := IsTriangulatedClosed₃.ext₃' T hT h₁ h₂ +protected lemma distinguished_cocone_triangle [P.IsTriangulatedClosed₃] + {X Y : C} (a : X ⟶ Y) (hX : P X) (hY : P Y) : + ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a + obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY + exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩ + +protected lemma distinguished_cocone_triangle₁ [P.IsTriangulatedClosed₁] + {Y Z : C} (b : Y ⟶ Z) (hY : P Y) (hZ : P Z) : + ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b + obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ + exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩ + +protected lemma distinguished_cocone_triangle₂ [P.IsTriangulatedClosed₂] + {X Z : C} (c : Z ⟶ X⟦(1 : ℤ)⟧) (hX : P X) (hZ : P Z) : + ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z), Triangle.mk a b c ∈ distTriang _ := by + obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c + obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ + exact ⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _ + (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩ + lemma ext_of_isTriangulatedClosed₁ [P.IsTriangulatedClosed₁] [P.IsClosedUnderIsomorphisms] (T : Triangle C) (hT : T ∈ distTriang C) @@ -154,6 +178,12 @@ instance [P.IsTriangulated] : P.IsTriangulatedClosed₃ where instance [P.IsTriangulated] : P.isoClosure.IsTriangulated where +instance {Q : ObjectProperty C} [P.IsTriangulated] [Q.IsTriangulated] + [Q.IsClosedUnderIsomorphisms] : + (P ⊓ Q).IsTriangulated where + ext₂' T hT h₁ h₃ := by + obtain ⟨Y, hY, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.1 + exact ⟨Y, ⟨hY, Q.prop_of_iso e (Q.ext_of_isTriangulatedClosed₂ T hT h₁.2 h₃.2)⟩, ⟨e⟩⟩ section @@ -447,6 +477,13 @@ lemma trW_isoClosure : P.isoClosure.trW = P.trW := by · rintro ⟨Z, g, h, mem, hZ⟩ exact ⟨Z, g, h, mem, ObjectProperty.le_isoClosure _ _ hZ⟩ +variable {P} in +lemma trW_monotone {Q : ObjectProperty C} (h : P ≤ Q) : P.trW ≤ Q.trW := by + intro X Y f hf + rw [trW_iff] at hf ⊢ + obtain ⟨Z, a, b, hT, hZ⟩ := hf + exact ⟨Z, a, b, hT, h _ hZ⟩ + set_option backward.isDefEq.respectTransparency false in instance : P.trW.RespectsIso where precomp {X' X Y} e (he : IsIso e) := by From 17715c1c9955164bafbc9467df16b144aa5bc4b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 18:31:42 +0200 Subject: [PATCH 19/26] ref --- Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 83dd63959b42ae..885d89534d71ed 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -17,7 +17,8 @@ subcategories of `C`, we define predicates (typeclasses saying that `A` is right `B`-localizing (or left `B`-localizing). ## References -* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*][verdier1996] +* [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, + Proposition 2.3.5, Chapitre II][verdier1996] -/ From abd00d9dd02333f0beff9e6b7db26275e2e335c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 18:32:34 +0200 Subject: [PATCH 20/26] added TODO --- Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 885d89534d71ed..08f8c19394325e 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -15,6 +15,8 @@ Let `C` be a pretriangulated category. If `A` and `B` are triangulated subcategories of `C`, we define predicates (typeclasses `IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) saying that `A` is right `B`-localizing (or left `B`-localizing). +When `B` is closed under isomorphisms, we shall show that the functor +from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful (TODO @joelriou). ## References * [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, From a957b73e2aa80b8b95dc15ee70db447dcd57ee8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 19:07:42 +0200 Subject: [PATCH 21/26] IsVerdierLeft/RightLocalising --- .../Triangulated/LocalizingSubcategory.lean | 79 ++++++++++--------- 1 file changed, 42 insertions(+), 37 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 08f8c19394325e..05308db5f83fac 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -13,10 +13,11 @@ public import Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated Let `C` be a pretriangulated category. If `A` and `B` are triangulated subcategories of `C`, we define predicates (typeclasses -`IsTriangulatedRightLocalizing` and `IsTriangulatedLeftLocalizing`) +`IsVerdierRightLocalizing` and `IsVerdierLeftLocalizing`) saying that `A` is right `B`-localizing (or left `B`-localizing). -When `B` is closed under isomorphisms, we shall show that the functor -from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful (TODO @joelriou). +When `B` is closed under isomorphisms, we shall show that this implies that +the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully +faithful (TODO @joelriou). ## References * [Jean-Louis Verdier, *Des catégories dérivées des catégories abéliennes*, @@ -38,8 +39,10 @@ variable {C D D' : Type*} [Category* C] [Category* D] [Category* D'] category `C` (with `B` closed under isomorphisms), we say that `A` is right `B`-localizing if any morphism `X ⟶ Y` with `X` in `B` and `Y` in `A` factors through an object that is in `A` and `B`. -See `isTriangulatedRightLocalizing_iff` for another characterization. -/ -class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where +Note that the definition does not use the (pre)triangulated structure: +see `isVerdierRightLocalizing_iff` for a characterization which +relies on it. -/ +class IsVerdierRightLocalizing (A B : ObjectProperty C) : Prop where fac {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f @@ -47,60 +50,62 @@ class IsTriangulatedRightLocalizing (A B : ObjectProperty C) : Prop where category `C` (with `B` closed under isomorphisms), we say that `A` is left `B`-localizing if any morphism `X ⟶ Y` with `X` in `A` and `Y` in `B` factors through an object that is in `A` and `B`. -See `isTriangulatedLeftLocalizing_iff` for another characterization. -/ -class IsTriangulatedLeftLocalizing (A B : ObjectProperty C) : Prop where +Note that the definition does not use the (pre)triangulated structure: +see `isVerdierLeftLocalizing_iff` for a characterization which +relies on it. -/ +class IsVerdierLeftLocalizing (A B : ObjectProperty C) : Prop where fac {X Y : C} (f : X ⟶ Y) (hX : A X) (hY : B Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f -instance (A B : ObjectProperty C) [A.IsTriangulatedLeftLocalizing B] : - A.op.IsTriangulatedRightLocalizing B.op where +instance (A B : ObjectProperty C) [A.IsVerdierLeftLocalizing B] : + A.op.IsVerdierRightLocalizing B.op where fac f hX hY := by obtain ⟨Z, a, b, h₁, h₂, fac⟩ := - IsTriangulatedLeftLocalizing.fac f.unop hY hX + IsVerdierLeftLocalizing.fac f.unop hY hX exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ -instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedLeftLocalizing B] : - A.unop.IsTriangulatedRightLocalizing B.unop where +instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierLeftLocalizing B] : + A.unop.IsVerdierRightLocalizing B.unop where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedLeftLocalizing.fac f.op hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ -instance (A B : ObjectProperty C) [A.IsTriangulatedRightLocalizing B] : - A.op.IsTriangulatedLeftLocalizing B.op where +instance (A B : ObjectProperty C) [A.IsVerdierRightLocalizing B] : + A.op.IsVerdierLeftLocalizing B.op where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.unop hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩ -instance (A B : ObjectProperty Cᵒᵖ) [A.IsTriangulatedRightLocalizing B] : - A.unop.IsTriangulatedLeftLocalizing B.unop where +instance (A B : ObjectProperty Cᵒᵖ) [A.IsVerdierRightLocalizing B] : + A.unop.IsVerdierLeftLocalizing B.unop where fac f hX hY := by - obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac f.op hY hX + obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩ variable (A B : ObjectProperty C) -lemma isTriangulatedLeftLocalizing_op_iff : - A.op.IsTriangulatedLeftLocalizing B.op ↔ A.IsTriangulatedRightLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedRightLocalizing B.op.unop), +lemma isVerdierLeftLocalizing_op_iff : + A.op.IsVerdierLeftLocalizing B.op ↔ A.IsVerdierRightLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierRightLocalizing B.op.unop), fun _ ↦ inferInstance⟩ -lemma isTriangulatedRightLocalizing_op_iff : - A.op.IsTriangulatedRightLocalizing B.op ↔ A.IsTriangulatedLeftLocalizing B := - ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsTriangulatedLeftLocalizing B.op.unop), +lemma isVerdierRightLocalizing_op_iff : + A.op.IsVerdierRightLocalizing B.op ↔ A.IsVerdierLeftLocalizing B := + ⟨fun _ ↦ inferInstanceAs (A.op.unop.IsVerdierLeftLocalizing B.op.unop), fun _ ↦ inferInstance⟩ variable [HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] -lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isVerdierRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsTriangulatedRightLocalizing B ↔ + A.IsVerdierRightLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A X) (_ : B.trW s), ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := by refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩ · rw [ObjectProperty.trW_iff'] at hs obtain ⟨W, a, b, hT, hW⟩ := hs - obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsTriangulatedRightLocalizing.fac a hW hX + obtain ⟨W', c, d, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac a hW hX obtain ⟨U, hU, e, f, hT'⟩ := A.distinguished_cocone_triangle d h₁ hX obtain ⟨g, hg, _⟩ := complete_distinguished_triangle_morphism _ _ hT hT' c (𝟙 _) (by cat_disch) @@ -119,19 +124,19 @@ lemma isTriangulatedRightLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] by cat_disch⟩ variable {A B} in -lemma IsTriangulatedRightLocalizing.fac' +lemma IsVerdierRightLocalizing.fac' [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsTriangulatedRightLocalizing B] + [A.IsVerdierRightLocalizing B] {X Y : C} (s : X ⟶ Y) (hX : A X) (hs : B.trW s) : ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s' := - (isTriangulatedRightLocalizing_iff A B).1 inferInstance s hX hs + (isVerdierRightLocalizing_iff A B).1 inferInstance s hX hs -lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] +lemma isVerdierLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] : - A.IsTriangulatedLeftLocalizing B ↔ + A.IsVerdierLeftLocalizing B ↔ ∀ ⦃X Y : C⦄ (s : X ⟶ Y) (_ : A Y) (_ : B.trW s), ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := by - rw [← isTriangulatedRightLocalizing_op_iff, isTriangulatedRightLocalizing_iff] + rw [← isVerdierRightLocalizing_op_iff, isVerdierRightLocalizing_iff] refine ⟨fun hA X Y s hY hs ↦ ?_, fun hA X Y s hX hs ↦ ?_⟩ · obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff]) exact ⟨Z'.unop, s'.unop, b.unop, hZ', trW_of_op _ hs', by cat_disch⟩ @@ -139,12 +144,12 @@ lemma isTriangulatedLeftLocalizing_iff [A.IsTriangulated] [B.IsTriangulated] exact ⟨_, s'.op, b.op, hZ', trW_of_unop _ hs', by cat_disch⟩ variable {A B} in -lemma IsTriangulatedLeftLocalizing.fac' +lemma IsVerdierLeftLocalizing.fac' [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsTriangulatedLeftLocalizing B] + [A.IsVerdierLeftLocalizing B] {X Y : C} (s : X ⟶ Y) (hY : A Y) (hs : B.trW s) : ∃ (Z : C) (s' : Z ⟶ Y) (a : Z ⟶ X), A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s' := - (isTriangulatedLeftLocalizing_iff A B).1 inferInstance s hY hs + (isVerdierLeftLocalizing_iff A B).1 inferInstance s hY hs end ObjectProperty From 93f7b3af537ac65be5a1f265b7f085b2344e19f1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 20:35:04 +0200 Subject: [PATCH 22/26] fix --- .../Triangulated/LocalizingSubcategory.lean | 30 ++++++++++++------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 988f53c082c6dc..98e8ea841bd10f 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -156,8 +156,8 @@ and `B : ObjectProperty C`, this is the inclusion functor `A.ι : A.FullSubcategory ⥤ C`, considered as a localized morphism, where `C` is equipped with the property of morphisms `B.trW` and `A.FullSubcategory` with the property of morphisms `(B.inverseImage A.ι).trW`. -/ -@[simps] -def triangulatedLocalizedMorphism [A.IsTriangulated] : +@[implicit_reducible] +def triangulatedLocalizerMorphism [A.IsTriangulated] : LocalizerMorphism (B.inverseImage A.ι).trW B.trW where functor := A.ι map X Y f hf := by @@ -165,6 +165,14 @@ def triangulatedLocalizedMorphism [A.IsTriangulated] : 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] @@ -190,14 +198,14 @@ lemma inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op [A.IsTriangulate variable [IsTriangulated C] [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] instance [A.IsVerdierRightLocalizing B] : - (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful where + (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful where nonempty_fullyFaithful := by let L₁ := (B.inverseImage A.ι).trW.Q let L₂ := B.trW.Q let F : (B.inverseImage A.ι).trW.Localization ⥤ B.trW.Localization := - (A.triangulatedLocalizedMorphism B).localizedFunctor L₁ L₂ + (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂ let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := - CatCommSq.iso (A.triangulatedLocalizedMorphism B).functor L₁ L₂ F + CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F have : F.Full := Functor.full_of_comp_essSurj _ L₁ (fun X₁ X₂ φ ↦ by obtain ⟨φ', hφ'⟩ : ∃ φ', φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂ := @@ -240,15 +248,15 @@ instance [A.IsVerdierRightLocalizing B] : instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B] : - (A.triangulatedLocalizedMorphism B).IsLocalizedFullyFaithful := by + (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.triangulatedLocalizedMorphism B).localizedFunctor L₁ L₂ - letI : CatCommSq (A.op.triangulatedLocalizedMorphism B.op).functor + (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.triangulatedLocalizedMorphism B).functor L₁ L₂ F).symm)⟩ + (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 @@ -261,8 +269,8 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] 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.triangulatedLocalizedMorphism B) - L₁ L₂ F (((A.op.triangulatedLocalizedMorphism B.op).fullyFaithful + 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) end ObjectProperty From 3c54ece8394fd643e1022c66f1122b0bb06ea21c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 7 May 2026 22:12:02 +0200 Subject: [PATCH 23/26] auxiliary definitions and more API --- .../Triangulated/LocalizingSubcategory.lean | 169 ++++++++++++------ 1 file changed, 119 insertions(+), 50 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 98e8ea841bd10f..74080479c6e2c0 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -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 @@ -197,57 +197,75 @@ lemma inverseImage_opEquivalence_inverse_trW_inverseImage_ι_op [A.IsTriangulate 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 := 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₂ - let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := - CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F - have : F.Full := - Functor.full_of_comp_essSurj _ L₁ (fun X₁ X₂ φ ↦ by - 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]) - have : F.Additive := by - rw [Localization.functor_additive_iff L₁ (B.inverseImage A.ι).trW] - exact Functor.additive_of_iso e - have : F.Faithful := - Functor.faithful_of_comp_cancel_zero_of_hasLeftCalculusOfFractions L₁ - (B.inverseImage A.ι).trW _ (fun X₁ X₂ f hf ↦ by - 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]) - exact ⟨.ofFullyFaithful F⟩ - -instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] - [A.IsVerdierLeftLocalizing B] : + nonempty_fullyFaithful := ⟨.ofFullyFaithful _⟩ + +instance [A.IsVerdierLeftLocalizing B] : (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful := by let L₁ := (B.inverseImage A.ι).trW.Q let L₂ := B.trW.Q @@ -273,6 +291,57 @@ instance [A.IsTriangulated] [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] 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 From cbc15661261166fc811f7c2d1f0a0aebed0595a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Fri, 8 May 2026 13:22:41 +0200 Subject: [PATCH 24/26] Update Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Triangulated/LocalizingSubcategory.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 74080479c6e2c0..889e0fd05008ab 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -337,8 +337,8 @@ noncomputable def IsVerdierRightLocalizing.fullyFaithful [A.IsVerdierRightLocali 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) + (Localization.liftNatIso L₁ (B.inverseImage A.ι).trW + ((A.triangulatedLocalizerMorphism B).functor ⋙ L₂) (L₁ ⋙ F) _ _ e.symm) end From 67fb96635010ae227be13996a0cdf6eae6d8f052 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Fri, 8 May 2026 13:22:53 +0200 Subject: [PATCH 25/26] Update Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Triangulated/LocalizingSubcategory.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index 889e0fd05008ab..c5c5294a57c5b9 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -323,8 +323,8 @@ noncomputable def IsVerdierLeftLocalizing.fullyFaithful [A.IsVerdierLeftLocalizi 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) + (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` From 373aa033639de1312f0c11c2688999531868719a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Fri, 8 May 2026 13:23:04 +0200 Subject: [PATCH 26/26] Update Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean index c5c5294a57c5b9..9c8d3d42ec0c5b 100644 --- a/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean +++ b/Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean @@ -153,7 +153,7 @@ lemma IsVerdierLeftLocalizing.fac' /-- 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 localized morphism, +`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]