From 5548aa68fc93a510c0e30bc5a06b23494224fc1b Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 26 Jun 2025 17:29:18 -0400 Subject: [PATCH] feat: bump to v4.21.0-rc3 Main difference: ChosenFiniteProducts is now CartesianMonoidalCategory. --- .../CategoryTheory/Comma/Over/Pullback.lean | 36 ++++----- .../CategoryTheory/Comma/Over/Sections.lean | 21 +++-- .../LocallyCartesianClosed/Basic.lean | 7 +- .../LocallyCartesianClosed/Presheaf.lean | 2 +- lake-manifest.json | 80 +++++-------------- lakefile.lean | 2 +- lean-toolchain | 2 +- 7 files changed, 53 insertions(+), 97 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean index 61c042e..9955483 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, tensorObj, 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/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/lake-manifest.json b/lake-manifest.json index d16603f..d2b249b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,17 +1,7 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b3fb998509f92a040e362f8a06f8ee2825ec8c10", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/PatrickMassot/checkdecls.git", + [{"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, "scope": "", @@ -35,57 +25,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fbe595fc740ee7a1789c6e6ebefa322e054a41c0", + "rev": "7260822b747892e2a72b6f2a6c530c398e4d1adf", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/mhuisi/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/jcommelin/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "458e2d3feda3999490987eabee57b8bb88b1949c", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "bump_to_v4.18.0-rc1", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "c07de335d35ed6b118e084ec48cffc39b40d29d2", - "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": "7cf25ec0edf7a72830379ee227eefdaa96c48cfb", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a", + "rev": "1603151ac0db4e822908e18094f16acc250acaff", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ba020ed434b9c5877eb62ff072a28f5ec56eb871", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c", + "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -115,17 +65,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8", + "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.53", + "inputRev": "v0.0.62", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ec060e0e10c685be8af65f288e23d026c9fde245", + "rev": "1b1abe64060b3e3250218646023e47950d8cd396", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -135,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73", + "rev": "d6afe6744246a799a3564dc84a878dab0c4a56d8", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -145,11 +95,21 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2fb9809751c4646c68c329b14f7d229a93176fd", + "rev": "d12fdadd81cb96980327cc02587fc14dea65a6e0", "name": "batteries", "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": "a0abd472348dd725adbb26732e79b26e7e220913", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, "configFile": "lakefile.toml"}], "name": "Poly", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 2e9f658..52b7061 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -21,4 +21,4 @@ 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" @ "main" diff --git a/lean-toolchain b/lean-toolchain index ee45541..1efd365 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.18.0-rc1 \ No newline at end of file +leanprover/lean4:v4.21.0-rc3