preservesConnectedLimitsOfShape_of_hasLimitsOfShape

Author: sinhp

Poly/UvPoly/Limits.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Sina Hazratpour. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sina Hazratpour
+-/
+
+import Poly.UvPoly.Basic
+
+/-!  We show that the polynomial functor preserve connected limits. -/
+
+universe v₁ v₂ u₁ u₂
+
+open CategoryTheory Category Limits Functor Adjunction Over ExponentiableMorphism
+  LocallyCartesianClosed
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+instance forgetPreservesConnectedLimitsOfShape_of_hasLimitsOfShape {J : Type*} [SmallCategory J]
+    [IsConnected J] [HasLimitsOfShape J C] {B : C} :
+    PreservesLimitsOfShape J (forget B) := by
+  apply preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
+
+namespace UvPoly
+
+variable {C : Type u₁} [Category.{v₁} C] [HasPullbacks C] [HasTerminal C] {E B : C}
+
+instance foo : PreservesLimits (star E) :=
+  forgetAdjStar E |>.rightAdjoint_preservesLimits
+
+instance pushforward_preservesLimits (P : UvPoly E B) : PreservesLimits (pushforward P.p) :=
+  (adj P.p).rightAdjoint_preservesLimits
+
+instance preservesConnectedLimitsOfShape_of_hasLimitsOfShape {J : Type v₁} [SmallCategory J] [IsConnected J]
+    [HasLimitsOfShape J C] (P : UvPoly E B) :
+    PreservesLimitsOfShape J (P.functor) := by
+  refine @comp_preservesLimitsOfShape _ _ _ _ (J:= J) _ _ _ (Over.star E)
+    (pushforward P.p ⋙ forget B) ?_ ?_
+  · apply forgetAdjStar E |>.rightAdjoint_preservesLimits |>.preservesLimitsOfShape (J:= J)
+  · apply @comp_preservesLimitsOfShape _ _ _ _ (J:= J) _ _ _ (pushforward P.p) (forget B) ?_ ?_
+    · apply P.pushforward_preservesLimits |>.preservesLimitsOfShape (J:= J)
+    · apply forgetPreservesConnectedLimitsOfShape_of_hasLimitsOfShape
+
+instance preservesConnectedLimitsOfShape_of_hasLimitsOfShape' {J : Type v₁} [SmallCategory J]
+    [IsConnected J] [HasLimitsOfShape J C] (P : UvPoly E B) :
+    PreservesLimitsOfShape J (P.functor) := by
+  infer_instance
+
+end UvPoly

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/PatrickMassot/checkdecls.git",
+ [{"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "061dfa3b4207216f7c7a7f63e99421f551059687",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.22.0-rc3",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
    "type": "git",
    "subDir": null,
    "scope": "",
@@ -31,6 +41,46 @@
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bb6eb5b25892aa968e9d35f6ef9ca5c6b896c16d",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/acmepjz/md4lean",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
@@ -100,16 +150,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "leanprover",
-   "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
  "lakeDir": ".lake"}