diff --git a/Mathlib.lean b/Mathlib.lean index 8569d32bdc872..9dca17ca90852 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1921,6 +1921,7 @@ import Mathlib.CategoryTheory.Linear.FunctorCategory import Mathlib.CategoryTheory.Linear.LinearFunctor import Mathlib.CategoryTheory.Linear.Yoneda import Mathlib.CategoryTheory.Localization.Adjunction +import Mathlib.CategoryTheory.Localization.Bifunctor import Mathlib.CategoryTheory.Localization.Bousfield import Mathlib.CategoryTheory.Localization.CalculusOfFractions import Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows diff --git a/Mathlib/CategoryTheory/Functor/Category.lean b/Mathlib/CategoryTheory/Functor/Category.lean index 7288ae9ebc9fe..64d1a3f601533 100644 --- a/Mathlib/CategoryTheory/Functor/Category.lean +++ b/Mathlib/CategoryTheory/Functor/Category.lean @@ -142,6 +142,18 @@ protected def flip (F : C ⥤ D ⥤ E) : D ⥤ C ⥤ E where end Functor +variable (C D E) in +/-- The functor `(C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E` which flips the variables. -/ +@[simps] +def flipFunctor : (C ⥤ D ⥤ E) ⥤ D ⥤ C ⥤ E where + obj F := F.flip + map {F₁ F₂} φ := + { app := fun Y => + { app := fun X => (φ.app X).app Y + naturality := fun X₁ X₂ f => by + dsimp + simp only [← NatTrans.comp_app, naturality] } } + namespace Iso @[reassoc (attr := simp)] diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean index 5c8021e9a84c0..67683abeb8e5a 100644 --- a/Mathlib/CategoryTheory/Functor/Currying.lean +++ b/Mathlib/CategoryTheory/Functor/Currying.lean @@ -88,6 +88,26 @@ def currying : C ⥤ D ⥤ E ≌ C × D ⥤ E where dsimp at f₁ f₂ ⊢ simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp])) +/-- The functor `uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E` is fully faithful. -/ +def fullyFaithfulUncurry : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).FullyFaithful := + currying.fullyFaithfulFunctor + +instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Full := + fullyFaithfulUncurry.full + +instance : (uncurry : (C ⥤ D ⥤ E) ⥤ C × D ⥤ E).Faithful := + fullyFaithfulUncurry.faithful + +/-- Given functors `F₁ : C ⥤ D`, `F₂ : C' ⥤ D'` and `G : D × D' ⥤ E`, this is the isomorphism +between `curry.obj ((F₁.prod F₂).comp G)` and +`F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂` in the category `C ⥤ C' ⥤ E`. -/ +@[simps!] +def curryObjProdComp {C' D' : Type*} [Category C'] [Category D'] + (F₁ : C ⥤ D) (F₂ : C' ⥤ D') (G : D × D' ⥤ E) : + curry.obj ((F₁.prod F₂).comp G) ≅ + F₁ ⋙ curry.obj G ⋙ (whiskeringLeft C' D' E).obj F₂ := + NatIso.ofComponents (fun X₁ ↦ NatIso.ofComponents (fun X₂ ↦ Iso.refl _)) + /-- `F.flip` is isomorphic to uncurrying `F`, swapping the variables, and currying. -/ @[simps!] def flipIsoCurrySwapUncurry (F : C ⥤ D ⥤ E) : F.flip ≅ curry.obj (Prod.swap _ _ ⋙ uncurry.obj F) := diff --git a/Mathlib/CategoryTheory/Localization/Bifunctor.lean b/Mathlib/CategoryTheory/Localization/Bifunctor.lean new file mode 100644 index 0000000000000..e4556b6e608d8 --- /dev/null +++ b/Mathlib/CategoryTheory/Localization/Bifunctor.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2023 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.CategoryTheory.Localization.Prod +import Mathlib.CategoryTheory.Functor.Currying + +/-! +# Lifting of bifunctors + +In this file, in the context of the localization of categories, we extend the notion +of lifting of functors to the case of bifunctors. As the localization of categories +behaves well with respect to finite products of categories (when the classes of +morphisms contain identities), all the definitions for bifunctors `C₁ ⥤ C₂ ⥤ E` +are obtained by reducing to the case of functors `(C₁ × C₂) ⥤ E` by using +currying and uncurrying. + +Given morphism properties `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂`, +and a functor `F : C₁ ⥤ C₂ ⥤ E`, we define `MorphismProperty.IsInvertedBy₂ W₁ W₂ F` +as the condition that the functor `uncurry.obj F : C₁ × C₂ ⥤ E` inverts `W₁.prod W₂`. + +If `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` are localization functors for `W₁` and `W₂` +respectively, and `F : C₁ ⥤ C₂ ⥤ E` satisfies `MorphismProperty.IsInvertedBy₂ W₁ W₂ F`, +we introduce `Localization.lift₂ F hF L₁ L₂ : D₁ ⥤ D₂ ⥤ E` which is a bifunctor +which lifts `F`. + +-/ + +namespace CategoryTheory + +open Category + +variable {C₁ C₂ D₁ D₂ E E' : Type*} [Category C₁] [Category C₂] + [Category D₁] [Category D₂] [Category E] [Category E'] + +namespace MorphismProperty + +/-- Classes of morphisms `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` are said +to be inverted by `F : C₁ ⥤ C₂ ⥤ E` if `W₁.prod W₂` is inverted by +the functor `uncurry.obj F : C₁ × C₂ ⥤ E`. -/ +def IsInvertedBy₂ (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) + (F : C₁ ⥤ C₂ ⥤ E) : Prop := + (W₁.prod W₂).IsInvertedBy (uncurry.obj F) + +end MorphismProperty + +namespace Localization + +section + +variable (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂) + +/-- Given functors `L₁ : C₁ ⥤ D₁`, `L₂ : C₂ ⥤ D₂`, morphisms properties `W₁` on `C₁` +and `W₂` on `C₂`, and functors `F : C₁ ⥤ C₂ ⥤ E` and `F' : D₁ ⥤ D₂ ⥤ E`, we say +`Lifting₂ L₁ L₂ W₁ W₂ F F'` holds if `F` is induced by `F'`, up to an isomorphism. -/ +class Lifting₂ (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) + (F : C₁ ⥤ C₂ ⥤ E) (F' : D₁ ⥤ D₂ ⥤ E) where + /-- the isomorphism `(((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F` expressing + that `F` is induced by `F'` up to an isomorphism -/ + iso' : (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F + +variable (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) + (F : C₁ ⥤ C₂ ⥤ E) (F' : D₁ ⥤ D₂ ⥤ E) [Lifting₂ L₁ L₂ W₁ W₂ F F'] + +/-- The isomorphism `(((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F` when +`Lifting₂ L₁ L₂ W₁ W₂ F F'` holds. -/ +noncomputable def Lifting₂.iso : (((whiskeringLeft₂ E).obj L₁).obj L₂).obj F' ≅ F := + Lifting₂.iso' W₁ W₂ + +/-- If `Lifting₂ L₁ L₂ W₁ W₂ F F'` holds, then `Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁))` +holds for any `X₁ : C₁`. -/ +noncomputable def Lifting₂.fst (X₁ : C₁) : + Lifting L₂ W₂ (F.obj X₁) (F'.obj (L₁.obj X₁)) where + iso' := ((evaluation _ _).obj X₁).mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F') + +noncomputable instance Lifting₂.flip : Lifting₂ L₂ L₁ W₂ W₁ F.flip F'.flip where + iso' := (flipFunctor _ _ _).mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F') + +/-- If `Lifting₂ L₁ L₂ W₁ W₂ F F'` holds, then +`Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂))` holds for any `X₂ : C₂`. -/ +noncomputable def Lifting₂.snd (X₂ : C₂) : + Lifting L₁ W₁ (F.flip.obj X₂) (F'.flip.obj (L₂.obj X₂)) := + Lifting₂.fst L₂ L₁ W₂ W₁ F.flip F'.flip X₂ + +noncomputable instance Lifting₂.uncurry [Lifting₂ L₁ L₂ W₁ W₂ F F'] : + Lifting (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F) (uncurry.obj F') where + iso' := CategoryTheory.uncurry.mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ F F') + +end + +section + +variable (F : C₁ ⥤ C₂ ⥤ E) {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} + (hF : MorphismProperty.IsInvertedBy₂ W₁ W₂ F) + (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂) + [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] + [W₁.ContainsIdentities] [W₂.ContainsIdentities] + +/-- Given localization functor `L₁ : C₁ ⥤ D₁` and `L₂ : C₂ ⥤ D₂` with respect +to `W₁ : MorphismProperty C₁` and `W₂ : MorphismProperty C₂` respectively, +and a bifunctor `F : C₁ ⥤ C₂ ⥤ E` which inverts `W₁` and `W₂`, this is +the induced localized bifunctor `D₁ ⥤ D₂ ⥤ E`. -/ +noncomputable def lift₂ : D₁ ⥤ D₂ ⥤ E := + curry.obj (lift (uncurry.obj F) hF (L₁.prod L₂)) + +noncomputable instance : Lifting₂ L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂) where + iso' := (curryObjProdComp _ _ _).symm ≪≫ + curry.mapIso (fac (uncurry.obj F) hF (L₁.prod L₂)) ≪≫ + currying.unitIso.symm.app F + +noncomputable instance Lifting₂.liftingLift₂ (X₁ : C₁) : + Lifting L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁)) := + Lifting₂.fst _ _ W₁ _ _ _ _ + +noncomputable instance Lifting₂.liftingLift₂Flip (X₂ : C₂) : + Lifting L₁ W₁ (F.flip.obj X₂) ((lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂)) := + Lifting₂.snd _ _ _ W₂ _ _ _ + +lemma lift₂_iso_hom_app_app₁ (X₁ : C₁) (X₂ : C₂) : + ((Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)).hom.app X₁).app X₂ = + (Lifting.iso L₂ W₂ (F.obj X₁) ((lift₂ F hF L₁ L₂).obj (L₁.obj X₁))).hom.app X₂ := + rfl + +lemma lift₂_iso_hom_app_app₂ (X₁ : C₁) (X₂ : C₂) : + ((Lifting₂.iso L₁ L₂ W₁ W₂ F (lift₂ F hF L₁ L₂)).hom.app X₁).app X₂ = + (Lifting.iso L₁ W₁ (F.flip.obj X₂) ((lift₂ F hF L₁ L₂).flip.obj (L₂.obj X₂))).hom.app X₁ := + rfl + +end + +section + +variable (L₁ : C₁ ⥤ D₁) (L₂ : C₂ ⥤ D₂) + (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) + [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] + [W₁.ContainsIdentities] [W₂.ContainsIdentities] + (F₁ F₂ : C₁ ⥤ C₂ ⥤ E) (F₁' F₂' : D₁ ⥤ D₂ ⥤ E) + [Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] [Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] + +/-- The natural transformation `F₁' ⟶ F₂'` of bifunctors induced by a +natural transformation `τ : F₁ ⟶ F₂` when `Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'` +and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold. -/ +noncomputable def lift₂NatTrans (τ : F₁ ⟶ F₂) : F₁' ⟶ F₂' := + fullyFaithfulUncurry.preimage + (liftNatTrans (L₁.prod L₂) (W₁.prod W₂) (uncurry.obj F₁) + (uncurry.obj F₂) (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ)) + +@[simp] +theorem lift₂NatTrans_app_app (τ : F₁ ⟶ F₂) (X₁ : C₁) (X₂ : C₂) : + ((lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ).app (L₁.obj X₁)).app (L₂.obj X₂) = + ((Lifting₂.iso L₁ L₂ W₁ W₂ F₁ F₁').hom.app X₁).app X₂ ≫ (τ.app X₁).app X₂ ≫ + ((Lifting₂.iso L₁ L₂ W₁ W₂ F₂ F₂').inv.app X₁).app X₂ := by + dsimp [lift₂NatTrans, fullyFaithfulUncurry, Equivalence.fullyFaithfulFunctor] + simp only [currying_unitIso_hom_app_app_app, currying_unitIso_inv_app_app_app, comp_id, id_comp] + exact liftNatTrans_app _ _ _ _ (uncurry.obj F₁') (uncurry.obj F₂') (uncurry.map τ) ⟨X₁, X₂⟩ + +variable {F₁' F₂'} in +include W₁ W₂ in +theorem natTrans₂_ext {τ τ' : F₁' ⟶ F₂'} + (h : ∀ (X₁ : C₁) (X₂ : C₂), (τ.app (L₁.obj X₁)).app (L₂.obj X₂) = + (τ'.app (L₁.obj X₁)).app (L₂.obj X₂)) : τ = τ' := + uncurry.map_injective (natTrans_ext (L₁.prod L₂) (W₁.prod W₂) (fun _ ↦ h _ _)) + +/-- The natural isomorphism `F₁' ≅ F₂'` of bifunctors induced by a +natural isomorphism `e : F₁ ≅ F₂` when `Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'` +and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold. -/ +noncomputable def lift₂NatIso (e : F₁ ≅ F₂) : F₁' ≅ F₂' where + hom := lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom + inv := lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv + hom_inv_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat) + inv_hom_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat) + +end + +end Localization + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean index b56d44cf24b6c..bc2855fa278ac 100644 --- a/Mathlib/CategoryTheory/Localization/Predicate.lean +++ b/Mathlib/CategoryTheory/Localization/Predicate.lean @@ -266,7 +266,7 @@ lemma faithful_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) variable {E} -theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} (τ τ' : F₁ ⟶ F₂) +theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} {τ τ' : F₁ ⟶ F₂} (h : ∀ X : C, τ.app (L.obj X) = τ'.app (L.obj X)) : τ = τ' := by haveI := essSurj L W ext Y @@ -331,13 +331,13 @@ theorem comp_liftNatTrans (F₁ F₂ F₃ : C ⥤ E) (F₁' F₂' F₃' : D ⥤ [h₂ : Lifting L W F₂ F₂'] [h₃ : Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃) : liftNatTrans L W F₁ F₂ F₁' F₂' τ ≫ liftNatTrans L W F₂ F₃ F₂' F₃' τ' = liftNatTrans L W F₁ F₃ F₁' F₃' (τ ≫ τ') := - natTrans_ext L W _ _ fun X => by + natTrans_ext L W fun X => by simp only [NatTrans.comp_app, liftNatTrans_app, assoc, Iso.inv_hom_id_app_assoc] @[simp] theorem liftNatTrans_id (F : C ⥤ E) (F' : D ⥤ E) [h : Lifting L W F F'] : liftNatTrans L W F F F' F' (𝟙 F) = 𝟙 F' := - natTrans_ext L W _ _ fun X => by + natTrans_ext L W fun X => by simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app] rfl diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean index 2899c82c95db6..fcf0a2f963969 100644 --- a/Mathlib/CategoryTheory/NatIso.lean +++ b/Mathlib/CategoryTheory/NatIso.lean @@ -65,6 +65,16 @@ theorem inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) := congr_fun (congr_arg NatTrans.app α.inv_hom_id) X +@[reassoc (attr := simp)] +lemma hom_inv_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) : + (e.hom.app X₁).app X₂ ≫ (e.inv.app X₁).app X₂ = 𝟙 _ := by + rw [← NatTrans.comp_app, Iso.hom_inv_id_app, NatTrans.id_app] + +@[reassoc (attr := simp)] +lemma inv_hom_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) : + (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _ := by + rw [← NatTrans.comp_app, Iso.inv_hom_id_app, NatTrans.id_app] + end Iso namespace NatIso diff --git a/Mathlib/CategoryTheory/Whiskering.lean b/Mathlib/CategoryTheory/Whiskering.lean index 50cc4f617eec0..53feb19a7b2f9 100644 --- a/Mathlib/CategoryTheory/Whiskering.lean +++ b/Mathlib/CategoryTheory/Whiskering.lean @@ -302,4 +302,20 @@ theorem pentagon : end Functor +variable {C₁ C₂ D₁ D₂ : Type*} [Category C₁] [Category C₂] + [Category D₁] [Category D₂] (E : Type*) [Category E] + +/-- The obvious functor `(C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E)`. -/ +@[simps!] +def whiskeringLeft₂ : + (C₁ ⥤ D₁) ⥤ (C₂ ⥤ D₂) ⥤ (D₁ ⥤ D₂ ⥤ E) ⥤ (C₁ ⥤ C₂ ⥤ E) where + obj F₁ := + { obj := fun F₂ ↦ + (whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).obj ((whiskeringLeft C₂ D₂ E).obj F₂) ⋙ + (whiskeringLeft C₁ D₁ (C₂ ⥤ E)).obj F₁ + map := fun φ ↦ whiskerRight + ((whiskeringRight D₁ (D₂ ⥤ E) (C₂ ⥤ E)).map ((whiskeringLeft C₂ D₂ E).map φ)) _ } + map ψ := + { app := fun F₂ ↦ whiskerLeft _ ((whiskeringLeft C₁ D₁ (C₂ ⥤ E)).map ψ) } + end CategoryTheory