diff --git a/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean b/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean index 9863fc8ae..6484168b9 100644 --- a/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean +++ b/LeanEval/Combinatorics/HoneycombConnectiveConstant.lean @@ -93,10 +93,12 @@ three-step self-avoiding walks from a fixed honeycomb vertex. -/ theorem walkCount_three : walkCount 3 = 12 := by decide -set_option maxRecDepth 10000 in -/-- At six steps the first hexagonal cycle appears; the standard count is `90`. -/ +/-- At six steps the first hexagonal cycle appears; the standard count is `90`. +The `+kernel` evaluation keeps the enumeration of all `3 ^ 6` direction words in +the kernel; reducing it in the elaborator costs several times the default +heartbeat budget. -/ theorem walkCount_six : walkCount 6 = 90 := by - decide + decide +kernel /-- **Duminil-Copin-Smirnov honeycomb connective-constant theorem.** The exponential growth rate of the number of self-avoiding walks is diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index d6facad1a..b850fac39 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -369,14 +369,14 @@ abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb := abelian group. -/ abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := (LightCondensed.discrete (ModuleCat ℤ)).obj - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) /-- The integral singular chain complex of a topological space, viewed as a cochain complex of light condensed abelian groups by applying the discrete functor degreewise and placing homological chain degree `n` in cohomological degree `-n`. -/ abbrev singularChainsLightCondAbComplexFunctor : TopCat ⥤ CochainComplex LightCondAb ℤ := - ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ + ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ (LightCondensed.discrete (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.down ℕ) ⋙ ComplexShape.embeddingDownNat.extendFunctor LightCondAb diff --git a/LeanEval/Geometry/MorseInequalities.lean b/LeanEval/Geometry/MorseInequalities.lean index 0c7606c15..c043b60c9 100644 --- a/LeanEval/Geometry/MorseInequalities.lean +++ b/LeanEval/Geometry/MorseInequalities.lean @@ -90,7 +90,7 @@ noncomputable def morseCount coefficients. -/ noncomputable def bettiNumber (M : Type) [TopologicalSpace M] (k : ℕ) : ℕ := Module.finrank ℝ - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℝ) k).obj + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℝ) k).obj (ModuleCat.of ℝ ℝ)).obj (TopCat.of M)) /-- The alternating partial sum `∑_{j=0}^{k} (−1)^{k−j} a_j`. -/ diff --git a/LeanEval/Geometry/WeakMorseInequality.lean b/LeanEval/Geometry/WeakMorseInequality.lean index 5aea130c5..5a70bcffe 100644 --- a/LeanEval/Geometry/WeakMorseInequality.lean +++ b/LeanEval/Geometry/WeakMorseInequality.lean @@ -87,7 +87,7 @@ noncomputable def morseCount /-- `b_k(M) := dim_ℝ H_k(M; ℝ)`. -/ noncomputable def bettiNumber (M : Type) [TopologicalSpace M] (k : ℕ) : ℕ := Module.finrank ℝ - (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℝ) k).obj + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℝ) k).obj (ModuleCat.of ℝ ℝ)).obj (TopCat.of M)) /-- **Weak Morse inequalities.** For a Morse function `f` on a closed diff --git a/LeanEval/Topology/AsphericalHomologySphere.lean b/LeanEval/Topology/AsphericalHomologySphere.lean index fbe2972cb..a4875d741 100644 --- a/LeanEval/Topology/AsphericalHomologySphere.lean +++ b/LeanEval/Topology/AsphericalHomologySphere.lean @@ -59,7 +59,7 @@ attribute [instance] Closed4Manifold.topology Closed4Manifold.t2 /-- `Hₖ(X; ℤ)`, the `k`-th singular homology with integer coefficients, as an object of `ModuleCat ℤ`. -/ noncomputable def intHomology (k : ℕ) (X : TopCat) : ModuleCat ℤ := - ((singularHomologyFunctor (ModuleCat ℤ) k).obj (ModuleCat.of ℤ ℤ)).obj X + ((singularHomologyFunctor (ModuleCat.{0} ℤ) k).obj (ModuleCat.of ℤ ℤ)).obj X /-- `M` is **aspherical**: every higher homotopy group vanishes at every basepoint. -/ diff --git a/LeanEval/Topology/Hurewicz.lean b/LeanEval/Topology/Hurewicz.lean index fa7860f74..42eded5d4 100644 --- a/LeanEval/Topology/Hurewicz.lean +++ b/LeanEval/Topology/Hurewicz.lean @@ -18,7 +18,7 @@ open CategoryTheory AlgebraicTopology /-- Integral singular homology in degree `n`, as an additive group. -/ noncomputable abbrev IntegralHomology (n : ℕ) (X : Type) [TopologicalSpace X] : AddCommGrpCat := - ((singularHomologyFunctor AddCommGrpCat n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) + ((singularHomologyFunctor AddCommGrpCat.{0} n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X) /-- **Hurewicz (n = 1).** For a path-connected space `X`, `H₁(X;ℤ)` is the abelianization of `π₁(X, x)`. -/ diff --git a/lake-manifest.json b/lake-manifest.json index 6e78c9e96..af237b8db 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,51 +1,41 @@ -{"version": "1.2.0", +{"version": "1.3.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover/lean-eval-generator.git", "type": "git", "subDir": null, "scope": "", - "rev": "2de74049bd91d2c592e7009df8f5e5968599a272", + "rev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6", "name": "«lean-eval-generator»", "manifestFile": "lake-manifest.json", - "inputRev": "2de74049bd91d2c592e7009df8f5e5968599a272", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "inputRev": "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99", + "rev": "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99", + "inputRev": "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/TauCetiProject/TauCeti", "type": "git", "subDir": null, "scope": "", - "rev": "23bfe9bc742f8713b58ce40b155f994848ae8a5e", + "rev": "522706e83ca349c3d6bde045e56778d17354ae8d", "name": "TauCeti", "manifestFile": "lake-manifest.json", - "inputRev": "23bfe9bc742f8713b58ce40b155f994848ae8a5e", + "inputRev": "522706e83ca349c3d6bde045e56778d17354ae8d", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "rev": "29ff470276c725ae01505d55b17148c18fc7dfd3", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e928b72544873815af278d38681b31c0293588e3", + "rev": "7e81a29bda33a6b257bd37557a6aa6aebe175d96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "rev": "c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "rev": "a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "rev": "37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -105,11 +95,21 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "rev": "33131f4fb10067cb3009bf4db615d9680c1ccd6b", "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": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.35.0-rc3", + "inherited": true, "configFile": "lakefile.toml"}], "name": "«lean-eval»", "lakeDir": ".lake", diff --git a/lakefile.toml b/lakefile.toml index 3f7f8af5c..cfb065b72 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -13,22 +13,17 @@ autoImplicit = false [[require]] name = "TauCeti" git = "https://github.com/TauCetiProject/TauCeti" -rev = "23bfe9bc742f8713b58ce40b155f994848ae8a5e" +rev = "522706e83ca349c3d6bde045e56778d17354ae8d" [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "db1c5741da0acf96c97584de6ccf0e3bfbc0ae99" - -[[require]] -name = "Cli" -git = "https://github.com/leanprover/lean4-cli" -rev = "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204" +rev = "5e0c4e5239cb0a2d86d68a884bf52cfd963fce22" [[require]] name = "lean-eval-generator" git = "https://github.com/leanprover/lean-eval-generator.git" -rev = "2de74049bd91d2c592e7009df8f5e5968599a272" +rev = "a61cd80bc45b16c4f8f900a15f5c80f32e75aad6" [[lean_lib]] name = "LeanEval" diff --git a/lean-toolchain b/lean-toolchain index 12359f928..f0e00b333 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.34.0 +leanprover/lean4:v4.35.0-rc3