From 5be8c2b6fb975825c603e6f62c8ac06d5dd154aa Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 23 Oct 2025 15:09:10 -0400 Subject: [PATCH] feat: bump to v4.25.0-rc2 --- Poly.lean | 8 ++--- Poly/Bifunctor/Sigma.lean | 5 +-- Poly/ForMathlib/CategoryTheory/Elements.lean | 2 +- .../LocallyCartesianClosed/BeckChevalley.lean | 6 ++-- Poly/ForMathlib/CategoryTheory/Types.lean | 2 +- Poly/Type/Univariate.lean | 2 +- Poly/UvPoly/UPIso.lean | 9 +++--- lake-manifest.json | 32 +++++++------------ lakefile.lean | 4 +-- lean-toolchain | 2 +- 10 files changed, 27 insertions(+), 45 deletions(-) diff --git a/Poly.lean b/Poly.lean index 2851889..f626468 100644 --- a/Poly.lean +++ b/Poly.lean @@ -2,9 +2,7 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Distributivity import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf --- import Poly.LCCC.BeckChevalley --- import Poly.LCCC.Presheaf --- import Poly.Type.Univariate --- import Poly.Exponentiable -import Poly.UvPoly.Basic +import Poly.Type.Univariate +import Poly.UvPoly.Limits +import Poly.UvPoly.UPIso import Poly.MvPoly.Basic diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean index 6740cb5..d453d2d 100644 --- a/Poly/Bifunctor/Sigma.lean +++ b/Poly/Bifunctor/Sigma.lean @@ -5,8 +5,7 @@ Authors: Wojciech Nawrocki -/ import Mathlib.CategoryTheory.Comma.Over.Basic import Mathlib.CategoryTheory.Functor.Currying - -import SEq.Tactic.DepRewrite +import Mathlib.Tactic.DepRewrite import Poly.ForMathlib.CategoryTheory.Elements import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic @@ -178,5 +177,3 @@ def forget_iso_Sigma (A : 𝒞) : simp end CategoryTheory.Over - -#min_imports diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean index 98eee42..b19ae69 100644 --- a/Poly/ForMathlib/CategoryTheory/Elements.lean +++ b/Poly/ForMathlib/CategoryTheory/Elements.lean @@ -22,7 +22,7 @@ theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) : theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq : G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) = G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫ - G.map (Subtype.mk (α := Y ⟶ Z) g (rfl)) := by + G.map (Subtype.mk g rfl) := by set X : F.Elements := ⟨X, a⟩ set Y : F.Elements := ⟨Y, F.map f a⟩ set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩ diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index f80e02d..fe6cdee 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -315,12 +315,12 @@ theorem pullbackMapTwoSquare_app : aesop theorem forget_map_pullbackMapTwoSquare : - (forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) = + (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) = pullback.map _ _ _ _ (𝟙 _) h k (id_comp _).symm sq.w.symm := by simp only [forget_map, pullbackMapTwoSquare_app, homMk_left] theorem isIso_forgetMappullbackMapTwoSquare_of_isPullback (pb : IsPullback h f g k) : - IsIso ((forget Z).map ((pullbackMapTwoSquare h f g k pb.toCommSq).app A)) := by + IsIso ((Over.forget Z).map ((pullbackMapTwoSquare h f g k pb.toCommSq).app A)) := by rw [forget_map_pullbackMapTwoSquare (sq:= pb.toCommSq)] let paste_horiz_pb := paste_horiz (IsPullback.of_hasPullback f A.hom) pb apply pullback.map_isIso_of_pullback_right_of_comm_cube @@ -333,7 +333,7 @@ instance pullbackMapTwoSquare_of_isPullback_isIso (pb : IsPullback h f g k) : apply (config := { allowSynthFailures:= true}) NatIso.isIso_of_isIso_app intro A have := isIso_forgetMappullbackMapTwoSquare_of_isPullback A pb - exact ReflectsIsomorphisms.reflects (forget Z) + exact ReflectsIsomorphisms.reflects (Over.forget Z) ((pullbackMapTwoSquare h f g k pb.toCommSq).app A) /-- The pullback-map exchange isomorphism. -/ diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean index b221290..3eb6659 100644 --- a/Poly/ForMathlib/CategoryTheory/Types.lean +++ b/Poly/ForMathlib/CategoryTheory/Types.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ -import Mathlib.CategoryTheory.Types +import Mathlib.CategoryTheory.Types.Basic namespace CategoryTheory.FunctorToTypes diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index 804cb07..988caad 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sina Hazratpour -/ -import Mathlib.CategoryTheory.Types +import Mathlib.CategoryTheory.Types.Basic open CategoryTheory Category Functor diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean index d6d9eb6..4843fd9 100644 --- a/Poly/UvPoly/UPIso.lean +++ b/Poly/UvPoly/UPIso.lean @@ -20,7 +20,7 @@ This is equivalent to the type of partial product cones with apex `Γ` over `X`. def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v := Functor.Sigma ((Over.equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ - (forget E).op ⋙ coyoneda (C := C)) + (Over.forget E).op ⋙ coyoneda (C := C)) @[simp] theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.partProdsOver.obj Γ).obj X) : @@ -40,7 +40,7 @@ def iso_Sigma (P : UvPoly E B) : P.functor ⋙₂ coyoneda (C := C) ≅ P.partProdsOver := calc P.functor ⋙₂ coyoneda (C := C) ≅ - (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) := + (star E ⋙ pushforward P.p) ⋙₂ (Over.forget B ⋙₂ coyoneda (C := C)) := Iso.refl _ _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma @@ -63,7 +63,7 @@ def iso_Sigma (P : UvPoly E B) : _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := Iso.refl _ - _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := + _ ≅ (Over.pullback P.p).op ⋙ (Over.forget E).op ⋙ coyoneda (C := C) := isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm; Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) @@ -75,7 +75,6 @@ theorem equiv_app (Γ X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by dsimp [equiv] --- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s! lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv Δ X (σ ≫ be) = let p := P.equiv Γ X be @@ -84,7 +83,7 @@ lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P. conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app] simp --- TODO(WN): Kernel typechecking takes 10s! +-- NOTE(WN): As of Lean 4.25, kernel typechecking time is down to 1s from 10s?! lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : equiv P Γ Y (be ≫ P.functor.map f) = let p := equiv P Γ X be diff --git a/lake-manifest.json b/lake-manifest.json index 1b4505a..34c0405 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -11,21 +11,11 @@ "inputRev": null, "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/Vtec234/lean4-seq", - "type": "git", - "subDir": null, - "scope": "", - "rev": "7279fc299b10681b00aefe1edd0668766cead87c", - "name": "seq", - "manifestFile": "lake-manifest.json", - "inputRev": null, - "inherited": false, - "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "839e741740619e20759a7153fd93b5c7d8df13e0", + "rev": "32bd6c7c8ca4a4be1c71bc04df0c9cf929d04818", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, @@ -35,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "240eddc1bb31420fbbc57fe5cc579435c2522493", + "rev": "8864a73bf79aad549e34eff972c606343935106d", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7c02243c07b61d493d7607ede432026781a3e47c", + "rev": "451499ea6e97cee4c8979b507a9af5581a849161", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,17 +55,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.71", + "inputRev": "v0.0.77", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3b779e9d1c73837a3764d516d81f942de391b6f0", + "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f85ad59c9b60647ef736719c23edd4578f723806", + "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a9a0cb7672b7134497c9d813e53999c9311f4037", + "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf", + "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.25.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "Poly", diff --git a/lakefile.lean b/lakefile.lean index 42e298b..066d6d0 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,8 +11,6 @@ package Poly where require mathlib from git "https://github.com/leanprover-community/mathlib4.git" -require seq from git "https://github.com/Vtec234/lean4-seq" - @[default_target] lean_lib Poly where -- add any library configuration options here @@ -21,4 +19,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" @ "v4.23.0-rc2" + "https://github.com/leanprover/doc-gen4" @ "v4.25.0-rc2" diff --git a/lean-toolchain b/lean-toolchain index 27770b5..137937a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.23.0-rc2 \ No newline at end of file +leanprover/lean4:v4.25.0-rc2 \ No newline at end of file