From 1e3da72526a9ad3e6b5b43197afc634f452fb283 Mon Sep 17 00:00:00 2001 From: Jason Yuen Date: Mon, 29 May 2023 05:02:18 +0000 Subject: [PATCH] feat: port CategoryTheory.Limits.Fubini (#4416) Co-authored-by: adomani --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Limits/Fubini.lean | 351 ++++++++++++++++++++++ 2 files changed, 352 insertions(+) create mode 100644 Mathlib/CategoryTheory/Limits/Fubini.lean diff --git a/Mathlib.lean b/Mathlib.lean index 59a0a61a4e44b..9df6a2612b67b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -711,6 +711,7 @@ import Mathlib.CategoryTheory.Limits.ExactFunctor import Mathlib.CategoryTheory.Limits.Filtered import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit import Mathlib.CategoryTheory.Limits.Final +import Mathlib.CategoryTheory.Limits.Fubini import Mathlib.CategoryTheory.Limits.FullSubcategory import Mathlib.CategoryTheory.Limits.FunctorCategory import Mathlib.CategoryTheory.Limits.HasLimits diff --git a/Mathlib/CategoryTheory/Limits/Fubini.lean b/Mathlib/CategoryTheory/Limits/Fubini.lean new file mode 100644 index 0000000000000..9e843cac14461 --- /dev/null +++ b/Mathlib/CategoryTheory/Limits/Fubini.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2020 Scott Morrison. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Scott Morrison + +! This file was ported from Lean 3 source module category_theory.limits.fubini +! leanprover-community/mathlib commit 59382264386afdbaf1727e617f5fdda511992eb9 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.Limits.HasLimits +import Mathlib.CategoryTheory.Products.Basic +import Mathlib.CategoryTheory.Functor.Currying + +/-! +# A Fubini theorem for categorical limits + +We prove that $lim_{J × K} G = lim_J (lim_K G(j, -))$ for a functor `G : J × K ⥤ C`, +when all the appropriate limits exist. + +We begin working with a functor `F : J ⥤ K ⥤ C`. We'll write `G : J × K ⥤ C` for the associated +"uncurried" functor. + +In the first part, given a coherent family `D` of limit cones over the functors `F.obj j`, +and a cone `c` over `G`, we construct a cone over the cone points of `D`. +We then show that if `c` is a limit cone, the constructed cone is also a limit cone. + +In the second part, we state the Fubini theorem in the setting where limits are +provided by suitable `HasLimit` classes. + +We construct +`limitUncurryIsoLimitCompLim F : limit (uncurry.obj F) ≅ limit (F ⋙ lim)` +and give simp lemmas characterising it. +For convenience, we also provide +`limitIsoLimitCurryCompLim G : limit G ≅ limit ((curry.obj G) ⋙ lim)` +in terms of the uncurried functor. + +## Future work + +The dual statement. +-/ + + +universe v u + +open CategoryTheory + +namespace CategoryTheory.Limits + +variable {J K : Type v} [SmallCategory J] [SmallCategory K] + +variable {C : Type u} [Category.{v} C] + +variable (F : J ⥤ K ⥤ C) + +-- We could try introducing a "dependent functor type" to handle this? +/-- A structure carrying a diagram of cones over the functors `F.obj j`. +-/ +structure DiagramOfCones where + obj : ∀ j : J, Cone (F.obj j) + map : ∀ {j j' : J} (f : j ⟶ j'), (Cones.postcompose (F.map f)).obj (obj j) ⟶ obj j' + id : ∀ j : J, (map (𝟙 j)).Hom = 𝟙 _ := by aesop_cat + comp : ∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃), + (map (f ≫ g)).Hom = (map f).Hom ≫ (map g).Hom := by aesop_cat +#align category_theory.limits.diagram_of_cones CategoryTheory.Limits.DiagramOfCones + +variable {F} + +/-- Extract the functor `J ⥤ C` consisting of the cone points and the maps between them, +from a `DiagramOfCones`. +-/ +@[simps] +def DiagramOfCones.conePoints (D : DiagramOfCones F) : J ⥤ C where + obj j := (D.obj j).pt + map f := (D.map f).Hom + map_id j := D.id j + map_comp f g := D.comp f g +#align category_theory.limits.diagram_of_cones.cone_points CategoryTheory.Limits.DiagramOfCones.conePoints + +/-- Given a diagram `D` of limit cones over the `F.obj j`, and a cone over `uncurry.obj F`, +we can construct a cone over the diagram consisting of the cone points from `D`. +-/ +@[simps] +def coneOfConeUncurry {D : DiagramOfCones F} (Q : ∀ j, IsLimit (D.obj j)) + (c : Cone (uncurry.obj F)) : Cone D.conePoints where + pt := c.pt + π := + { app := fun j => + (Q j).lift + { pt := c.pt + π := + { app := fun k => c.π.app (j, k) + naturality := fun k k' f => by + dsimp; simp only [Category.id_comp] + have := @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f) + dsimp at this + simp only [Category.id_comp, CategoryTheory.Functor.map_id, NatTrans.id_app] + at this + exact this } } + naturality := fun j j' f => + (Q j').hom_ext + (by + dsimp + intro k + simp only [Limits.ConeMorphism.w, Limits.Cones.postcompose_obj_π, + Limits.IsLimit.fac_assoc, Limits.IsLimit.fac, NatTrans.comp_app, Category.id_comp, + Category.assoc] + have := @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j', k) (f, 𝟙 k) + dsimp at this + simp only [Category.id_comp, Category.comp_id, CategoryTheory.Functor.map_id, + NatTrans.id_app] at this + exact this) } +#align category_theory.limits.cone_of_cone_uncurry CategoryTheory.Limits.coneOfConeUncurry + +/-- `coneOfConeUncurry Q c` is a limit cone when `c` is a limit cone. +-/ +def coneOfConeUncurryIsLimit {D : DiagramOfCones F} (Q : ∀ j, IsLimit (D.obj j)) + {c : Cone (uncurry.obj F)} (P : IsLimit c) : IsLimit (coneOfConeUncurry Q c) where + lift s := + P.lift + { pt := s.pt + π := + { app := fun p => s.π.app p.1 ≫ (D.obj p.1).π.app p.2 + naturality := fun p p' f => by + dsimp; simp only [Category.id_comp, Category.assoc] + rcases p with ⟨j, k⟩ + rcases p' with ⟨j', k'⟩ + rcases f with ⟨fj, fk⟩ + dsimp + slice_rhs 3 4 => rw [← NatTrans.naturality] + slice_rhs 2 3 => rw [← (D.obj j).π.naturality] + simp only [Functor.const_obj_map, Category.id_comp, Category.assoc] + have w := (D.map fj).w k' + dsimp at w + rw [← w] + have n := s.π.naturality fj + dsimp at n + simp only [Category.id_comp] at n + rw [n] + simp } } + fac s j := by + apply (Q j).hom_ext + intro k + simp + uniq s m w := by + refine' P.uniq + { pt := s.pt + π := _ } m _ + rintro ⟨j, k⟩ + dsimp + rw [← w j] + simp +#align category_theory.limits.cone_of_cone_uncurry_is_limit CategoryTheory.Limits.coneOfConeUncurryIsLimit + +section + +variable (F) + +variable [HasLimitsOfShape K C] + +/-- Given a functor `F : J ⥤ K ⥤ C`, with all needed limits, +we can construct a diagram consisting of the limit cone over each functor `F.obj j`, +and the universal cone morphisms between these. +-/ +@[simps] +noncomputable def DiagramOfCones.mkOfHasLimits : DiagramOfCones F where + obj j := limit.cone (F.obj j) + map f := { Hom := lim.map (F.map f) } +#align category_theory.limits.diagram_of_cones.mk_of_has_limits CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits + +-- Satisfying the inhabited linter. +noncomputable instance diagramOfConesInhabited : Inhabited (DiagramOfCones F) := + ⟨DiagramOfCones.mkOfHasLimits F⟩ +#align category_theory.limits.diagram_of_cones_inhabited CategoryTheory.Limits.diagramOfConesInhabited + +@[simp] +theorem DiagramOfCones.mkOfHasLimits_conePoints : + (DiagramOfCones.mkOfHasLimits F).conePoints = F ⋙ lim := + rfl +#align category_theory.limits.diagram_of_cones.mk_of_has_limits_cone_points CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_conePoints + +variable [HasLimit (uncurry.obj F)] + +variable [HasLimit (F ⋙ lim)] + +/-- The Fubini theorem for a functor `F : J ⥤ K ⥤ C`, +showing that the limit of `uncurry.obj F` can be computed as +the limit of the limits of the functors `F.obj j`. +-/ +noncomputable def limitUncurryIsoLimitCompLim : limit (uncurry.obj F) ≅ limit (F ⋙ lim) := by + let c := limit.cone (uncurry.obj F) + let P : IsLimit c := limit.isLimit _ + let G := DiagramOfCones.mkOfHasLimits F + let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _ + have Q' := coneOfConeUncurryIsLimit Q P + have Q'' := limit.isLimit (F ⋙ lim) + exact IsLimit.conePointUniqueUpToIso Q' Q'' +#align category_theory.limits.limit_uncurry_iso_limit_comp_lim CategoryTheory.Limits.limitUncurryIsoLimitCompLim + +@[simp, reassoc] +theorem limitUncurryIsoLimitCompLim_hom_π_π {j} {k} : + (limitUncurryIsoLimitCompLim F).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k) := by + dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso] + simp +#align category_theory.limits.limit_uncurry_iso_limit_comp_lim_hom_π_π CategoryTheory.Limits.limitUncurryIsoLimitCompLim_hom_π_π + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +@[simp, reassoc] +theorem limitUncurryIsoLimitCompLim_inv_π {j} {k} : + (limitUncurryIsoLimitCompLim F).inv ≫ limit.π _ (j, k) = + (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _) := by + rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom] + simp +#align category_theory.limits.limit_uncurry_iso_limit_comp_lim_inv_π CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π + +end + +section + +variable (F) [HasLimitsOfShape J C] [HasLimitsOfShape K C] + +-- With only moderate effort these could be derived if needed: +variable [HasLimitsOfShape (J × K) C] [HasLimitsOfShape (K × J) C] + +/-- The limit of `F.flip ⋙ lim` is isomorphic to the limit of `F ⋙ lim`. -/ +noncomputable def limitFlipCompLimIsoLimitCompLim : limit (F.flip ⋙ lim) ≅ limit (F ⋙ lim) := + (limitUncurryIsoLimitCompLim _).symm ≪≫ + HasLimit.isoOfNatIso (uncurryObjFlip _) ≪≫ + HasLimit.isoOfEquivalence (Prod.braiding _ _) + (NatIso.ofComponents (fun _ => by rfl) (by simp)) ≪≫ + limitUncurryIsoLimitCompLim _ +#align category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +@[simp, reassoc] +theorem limitFlipCompLimIsoLimitCompLim_hom_π_π (j) (k) : + (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π _ j ≫ limit.π _ k = + (limit.π _ k ≫ limit.π _ j : limit (_ ⋙ lim) ⟶ _) := by + dsimp [limitFlipCompLimIsoLimitCompLim] + simp +#align category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_hom_π_π CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +-- See note [dsimp, simp] +@[simp, reassoc] +theorem limitFlipCompLimIsoLimitCompLim_inv_π_π (k) (j) : + (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π _ k ≫ limit.π _ j = + (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _) := by + dsimp [limitFlipCompLimIsoLimitCompLim] + simp +#align category_theory.limits.limit_flip_comp_lim_iso_limit_comp_lim_inv_π_π CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_inv_π_π + +end + +section + +variable (G : J × K ⥤ C) + +section + +variable [HasLimitsOfShape K C] + +variable [HasLimit G] + +variable [HasLimit (curry.obj G ⋙ lim)] + +/-- The Fubini theorem for a functor `G : J × K ⥤ C`, +showing that the limit of `G` can be computed as +the limit of the limits of the functors `G.obj (j, _)`. +-/ +noncomputable def limitIsoLimitCurryCompLim : limit G ≅ limit (curry.obj G ⋙ lim) := by + have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G + haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimitOfIso i + trans limit (uncurry.obj ((@curry J _ K _ C _).obj G)) + apply HasLimit.isoOfNatIso i + exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G) +#align category_theory.limits.limit_iso_limit_curry_comp_lim CategoryTheory.Limits.limitIsoLimitCurryCompLim + +@[simp, reassoc] +theorem limitIsoLimitCurryCompLim_hom_π_π {j} {k} : + (limitIsoLimitCurryCompLim G).hom ≫ limit.π _ j ≫ limit.π _ k = limit.π _ (j, k) := by + simp [limitIsoLimitCurryCompLim, Trans.simple, HasLimit.isoOfNatIso, limitUncurryIsoLimitCompLim] +#align category_theory.limits.limit_iso_limit_curry_comp_lim_hom_π_π CategoryTheory.Limits.limitIsoLimitCurryCompLim_hom_π_π + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +@[simp, reassoc] +theorem limitIsoLimitCurryCompLim_inv_π {j} {k} : + (limitIsoLimitCurryCompLim G).inv ≫ limit.π _ (j, k) = + (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _) := by + rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom] + simp +#align category_theory.limits.limit_iso_limit_curry_comp_lim_inv_π CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π + +end + +section + +variable [HasLimits C] + +-- Certainly one could weaken the hypotheses here. +open CategoryTheory.prod + +/-- A variant of the Fubini theorem for a functor `G : J × K ⥤ C`, +showing that $\lim_k \lim_j G(j,k) ≅ \lim_j \lim_k G(j,k)$. +-/ +noncomputable def limitCurrySwapCompLimIsoLimitCurryCompLim : + limit (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) ≅ limit (curry.obj G ⋙ lim) := + calc + limit (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) ≅ limit (Prod.swap K J ⋙ G) := + (limitIsoLimitCurryCompLim _).symm + _ ≅ limit G := (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl _)) + _ ≅ limit (curry.obj G ⋙ lim) := limitIsoLimitCurryCompLim _ +#align category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +@[simp] +theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} : + (limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ limit.π _ j ≫ limit.π _ k = + (limit.π _ k ≫ limit.π _ j : limit (_ ⋙ lim) ⟶ _) := by + dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim] + simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_hom_π, + Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc] + erw [NatTrans.id_app] + -- Why can't `simp` do this`? + dsimp + -- porting note: the original proof only had `simp`. + -- However, now `CategoryTheory.Bifunctor.map_id` does not get used by `simp` + rw [CategoryTheory.Bifunctor.map_id] + simp + +#align category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_hom_π_π CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π + +-- Porting note: Added type annotation `limit (_ ⋙ lim) ⟶ _` +@[simp] +theorem limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π {j} {k} : + (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫ limit.π _ k ≫ limit.π _ j = + (limit.π _ j ≫ limit.π _ k : limit (_ ⋙ lim) ⟶ _) := by + dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim] + simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_inv_π, + Iso.refl_inv, limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc] + erw [NatTrans.id_app] + -- Why can't `simp` do this`? + dsimp; + simp +#align category_theory.limits.limit_curry_swap_comp_lim_iso_limit_curry_comp_lim_inv_π_π CategoryTheory.Limits.limitCurrySwapCompLimIsoLimitCurryCompLim_inv_π_π + +end + +end + +end CategoryTheory.Limits