diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean index 61c042e..f98c671 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour -/ import Mathlib.CategoryTheory.Comma.Over.Pullback -import Mathlib.CategoryTheory.ChosenFiniteProducts +import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic import Mathlib.CategoryTheory.Monad.Products import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic @@ -16,7 +16,9 @@ universe v₁ v₂ u₁ u₂ namespace CategoryTheory -open Category Limits Comonad MonoidalCategory +open Category Limits Comonad MonoidalCategory CartesianMonoidalCategory + +attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts variable {C : Type u₁} [Category.{v₁} C] @@ -87,7 +89,7 @@ end Reindex section BinaryProduct -open ChosenFiniteProducts Sigma Reindex +open Sigma Reindex variable [HasFiniteWidePullbacks C] {X : C} @@ -106,8 +108,6 @@ def isBinaryProductSigmaReindex (Y Z : Over X) : · exact congr_arg CommaMorphism.left (h ⟨ .right⟩) · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩) -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts - /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z` in `Over X`. -/ @[simps!] @@ -122,12 +122,12 @@ def sigmaReindexIsoProdMk {Y : C} (f : Y ⟶ X) (Z : Over X) : sigmaReindexIsoProd (Over.mk f) _ lemma sigmaReindexIsoProd_hom_comp_fst {Y Z : Over X} : - (sigmaReindexIsoProd Y Z).hom ≫ (fst Y Z) = (π_ Y Z) := + (sigmaReindexIsoProd Y Z).hom ≫ fst Y Z = (π_ Y Z) := IsLimit.conePointUniqueUpToIso_hom_comp (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.left⟩ lemma sigmaReindexIsoProd_hom_comp_snd {Y Z : Over X} : - (sigmaReindexIsoProd Y Z).hom ≫ (snd Y Z) = (μ_ Y Z) := + (sigmaReindexIsoProd Y Z).hom ≫ snd Y Z = (μ_ Y Z) := IsLimit.conePointUniqueUpToIso_hom_comp (isBinaryProductSigmaReindex Y Z) (Limits.prodIsProd Y Z) ⟨.right⟩ @@ -137,10 +137,7 @@ end Over section TensorLeft -open MonoidalCategory Over Functor ChosenFiniteProducts - -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts -attribute [local instance] monoidalOfChosenFiniteProducts +open Over Functor variable [HasFiniteWidePullbacks C] {X : C} @@ -150,16 +147,16 @@ def Over.sigmaReindexNatIsoTensorLeft (Y : Over X) : (pullback Y.hom) ⋙ (map Y.hom) ≅ tensorLeft Y := by fapply NatIso.ofComponents · intro Z - simp only [const_obj_obj, Functor.id_obj, comp_obj, tensorLeft_obj, tensorObj, Over.pullback] + simp only [const_obj_obj, Functor.id_obj, comp_obj, Over.pullback] exact sigmaReindexIsoProd Y Z · intro Z Z' f - simp + dsimp ext1 <;> simp_rw [assoc] - · simp_rw [whiskerLeft_fst] + · rw [whiskerLeft_fst] iterate rw [sigmaReindexIsoProd_hom_comp_fst] ext simp - · simp_rw [whiskerLeft_snd] + · rw [whiskerLeft_snd] iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd] ext simp [Reindex.sndProj] @@ -187,7 +184,7 @@ def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C := namespace Over -open MonoidalCategory +open CartesianMonoidalCategory variable {C} @@ -201,15 +198,14 @@ lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) : instance [HasBinaryProducts C] (X : C) : (forget X).IsLeftAdjoint := ⟨_, ⟨forgetAdjStar X⟩⟩ -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts -attribute [local instance] monoidalOfChosenFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts lemma whiskerLeftProdMapId [HasFiniteLimits C] {X : C} {A A' : C} {g : A ⟶ A'} : X ◁ g = prod.map (𝟙 X) g := by ext - · simp only [ChosenFiniteProducts.whiskerLeft_fst] + · simp only [whiskerLeft_fst] exact (Category.comp_id _).symm.trans (prod.map_fst (𝟙 X) g).symm - · simp only [ChosenFiniteProducts.whiskerLeft_snd] + · simp only [whiskerLeft_snd] exact (prod.map_snd (𝟙 X) g).symm def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) : diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean index 752a72c..e131353 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean @@ -21,14 +21,13 @@ universe v₁ v₂ u₁ u₂ namespace CategoryTheory -open Category Limits MonoidalCategory CartesianClosed Adjunction Over +open Category Limits MonoidalCategory CartesianMonoidalCategory CartesianClosed Adjunction Over variable {C : Type u₁} [Category.{v₁} C] attribute [local instance] hasBinaryProducts_of_hasTerminal_and_pullbacks attribute [local instance] hasFiniteProducts_of_has_binary_and_terminal -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts -attribute [local instance] monoidalOfChosenFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts section @@ -36,34 +35,34 @@ variable [HasFiniteProducts C] /-- The isomorphism between `X ⨯ Y` and `X ⊗ Y` for objects `X` and `Y` in `C`. This is tautological by the definition of the cartesian monoidal structure on `C`. -This isomorphism provides an interface between `prod.fst` and `ChosenFiniteProducts.fst` +This isomorphism provides an interface between `prod.fst` and `CartesianMonoidalCategory.fst` as well as between `prod.map` and `tensorHom`. -/ def prodIsoTensorObj (X Y : C) : X ⨯ Y ≅ X ⊗ Y := Iso.refl _ @[reassoc (attr := simp)] theorem prodIsoTensorObj_inv_fst {X Y : C} : - (prodIsoTensorObj X Y).inv ≫ prod.fst = ChosenFiniteProducts.fst X Y := + (prodIsoTensorObj X Y).inv ≫ prod.fst = fst X Y := Category.id_comp _ @[reassoc (attr := simp)] theorem prodIsoTensorObj_inv_snd {X Y : C} : - (prodIsoTensorObj X Y).inv ≫ prod.snd = ChosenFiniteProducts.snd X Y := + (prodIsoTensorObj X Y).inv ≫ prod.snd = snd X Y := Category.id_comp _ @[reassoc (attr := simp)] theorem prodIsoTensorObj_hom_fst {X Y : C} : - (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.fst X Y = prod.fst := + (prodIsoTensorObj X Y).hom ≫ fst X Y = prod.fst := Category.id_comp _ @[reassoc (attr := simp)] theorem prodIsoTensorObj_hom_snd {X Y : C} : - (prodIsoTensorObj X Y).hom ≫ ChosenFiniteProducts.snd X Y = prod.snd := + (prodIsoTensorObj X Y).hom ≫ snd X Y = prod.snd := Category.id_comp _ @[reassoc (attr := simp)] theorem prodMap_comp_prodIsoTensorObj_hom {X Y Z W : C} (f : X ⟶ Y) (g : Z ⟶ W) : - prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ g) := by - apply ChosenFiniteProducts.hom_ext <;> simp + prod.map f g ≫ (prodIsoTensorObj _ _).hom = (prodIsoTensorObj _ _).hom ≫ (f ⊗ₘ g) := by + apply hom_ext <;> simp end @@ -73,7 +72,7 @@ variable (I : C) [Exponentiable I] /-- The first leg of a cospan constructing a pullback diagram in `C` used to define `sections` . -/ def curryId : ⊤_ C ⟶ (I ⟹ I) := - CartesianClosed.curry (ChosenFiniteProducts.fst I (⊤_ C)) + CartesianClosed.curry (fst I (⊤_ C)) variable {I} diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean index e26775e..2111115 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean @@ -62,11 +62,12 @@ universe v u namespace CategoryTheory -open CategoryTheory Category MonoidalCategory Limits Functor Adjunction Over +open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction + Over variable {C : Type u} [Category.{v} C] -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts /-- A morphism `f : I ⟶ J` is exponentiable if the pullback functor `Over J ⥤ Over I` has a right adjoint. -/ @@ -223,7 +224,7 @@ end HasPushforwards namespace CartesianClosedOver -open Over Reindex IsIso ChosenFiniteProducts CartesianClosed HasPushforwards ExponentiableMorphism +open Over Reindex IsIso CartesianClosed HasPushforwards ExponentiableMorphism variable {C} [HasFiniteWidePullbacks C] {I J : C} [CartesianClosed (Over J)] diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index d2b7952..eca421e 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -129,8 +129,6 @@ def paste : cartesian (pasteCell f u) := by · unfold pasteCell2 apply cartesian.whiskerRight (cellLeftCartesian f u) -#check pushforwardPullbackTwoSquare - -- use `pushforwardPullbackTwoSquare` to construct this iso. def pentagonIso : map u ⋙ pushforward f ≅ pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean index 065ad49..2fad239 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Presheaf.lean @@ -22,7 +22,7 @@ abbrev Psh (C : Type u) [Category.{v} C] : Type (max u (v + 1)) := Cᵒᵖ ⥤ T variable {C : Type*} [SmallCategory C] [HasTerminal C] -attribute [local instance] ChosenFiniteProducts.ofFiniteProducts +attribute [local instance] CartesianMonoidalCategory.ofFiniteProducts instance cartesianClosedOver {C : Type u} [Category.{max u v} C] (P : Psh C) : CartesianClosed (Over P) := diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean index 6eb67a0..cd1f798 100644 --- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean +++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean @@ -18,6 +18,8 @@ variable {K : Type*} [Category K] {D : Type*} [Category D] namespace NatTrans +open Functor + /-- A natural transformation is cartesian if every commutative square of the following form is a pullback. ``` diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 77abc99..c4f1516 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -223,10 +223,10 @@ instance : Category (UvPoly.Total C) where id P := UvPoly.Hom.id P.poly comp := UvPoly.Hom.comp id_comp := by - simp [UvPoly.Hom.id, UvPoly.Hom.comp] + simp [UvPoly.Hom.comp] sorry comp_id := by - simp [UvPoly.Hom.id, UvPoly.Hom.comp] + simp [UvPoly.Hom.comp] sorry assoc := by simp [UvPoly.Hom.comp] diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean index 7e000fe..4ccc736 100644 --- a/Poly/UvPoly/UPFan.lean +++ b/Poly/UvPoly/UPFan.lean @@ -23,8 +23,7 @@ def equiv (P : UvPoly E B) (Γ : C) (X : C) : dsimp symm fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩ - · simp [partialProd.lift] - rfl + · simp; rfl · sorry right_inv := by intro ⟨b, e⟩ diff --git a/lake-manifest.json b/lake-manifest.json index d16603f..e7e3aaa 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b3fb998509f92a040e362f8a06f8ee2825ec8c10", + "rev": "75044446e214659fa9b0be92b1d6c1c1885ba245", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.22.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", - "rev": "75d7aea6c81efeb68701164edaaa9116f06b91ba", + "rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4", "name": "checkdecls", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "b6b76a5d7cc1c8b11c52f12a7bd90c460b7cba5a", + "rev": "7279fc299b10681b00aefe1edd0668766cead87c", "name": "seq", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fbe595fc740ee7a1789c6e6ebefa322e054a41c0", + "rev": "a00db62ed4abdcae081291eb892fa79c32ab1d76", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -45,27 +45,27 @@ "type": "git", "subDir": null, "scope": "", - "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925", + "rev": "a8733224c9aad9d372d82f208e32da1eed667875", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/jcommelin/lean4-unicode-basic", + {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "458e2d3feda3999490987eabee57b8bb88b1949c", + "rev": "1cf274454c624e4b94c79f14b6db70d9fe0bdd51", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", - "inputRev": "bump_to_v4.18.0-rc1", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/dupuisf/BibtexQuery", "type": "git", "subDir": null, "scope": "", - "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2", + "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb", + "rev": "b16338c5c66f57ef5510d4334eb6fa4e2c6c8cd8", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a", + "rev": "151892dbc73e6c6033ca33f5a63ae20e57ad75ea", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c", + "rev": "2bf782bac3fc773faf4aaab8c735a5a01c189a2d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,17 +115,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8", + "rev": "e33ec3e6393358e5764f6acd95a6227e2b9f10bd", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.53", + "inputRev": "v0.0.66", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ec060e0e10c685be8af65f288e23d026c9fde245", + "rev": "8f2d76dce940f1364878dd9b7fde299b607a71ba", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,7 +135,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73", + "rev": "0632bccc9007cb1c2baf275298f40b15a81fdc90", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -145,7 +145,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2fb9809751c4646c68c329b14f7d229a93176fd", + "rev": "14ac7be905d97a24c53a3247ebf5c5d9c00adc26", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 2e9f658..5811283 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -package «Poly» where +package Poly where -- Settings applied to both builds and interactive editing leanOptions := #[ ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b` @@ -14,11 +14,11 @@ require mathlib from git require seq from git "https://github.com/Vtec234/lean4-seq" @[default_target] -lean_lib «Poly» where +lean_lib Poly where -- add any library configuration options here require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git" meta if get_config? env = some "dev" then require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "main" \ No newline at end of file + "https://github.com/leanprover/doc-gen4" @ "v4.22.0-rc2" diff --git a/lean-toolchain b/lean-toolchain index ee45541..bfcebb1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0-rc1 \ No newline at end of file +leanprover/lean4:v4.22.0-rc2