Merge branch 'exteriorPower-basis' of https://github.com/morrison-daniel/mathlib4 into exteriorPower-basis

Author: morrison-daniel

.github/workflows/commit_verification.yml

@@ -22,7 +22,9 @@ permissions:
 
 env:
   TRANSIENT_PREFIX: "transient: "
-  AUTO_PREFIX: "x: "
+  # Support both "x " and "x: " (legacy) prefixes
+  AUTO_PREFIX_COLON: "x: "
+  AUTO_PREFIX_SPACE: "x "
 
 jobs:
   verify:
@@ -46,8 +48,9 @@ jobs:
           HEAD_SHA="${{ github.event.pull_request.head.sha }}"
 
           # Check if any commits have transient or auto prefix
+          # Auto prefix can be "x " or "x: " (legacy)
           HAS_SPECIAL=$(git log --format="%s" "$BASE_SHA..$HEAD_SHA" | \
-            grep -E "^(${TRANSIENT_PREFIX}|${AUTO_PREFIX})" || true)
+            grep -E "^(${TRANSIENT_PREFIX}|${AUTO_PREFIX_COLON}|${AUTO_PREFIX_SPACE})" || true)
 
           if [[ -n "$HAS_SPECIAL" ]]; then
             echo "has_special=true" >> "$GITHUB_OUTPUT"

.github/workflows/nightly_bump_and_merge.yml

@@ -230,7 +230,7 @@ jobs:
           }
 
           # Find tags that are ancestors of this branch with the right format
-          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}" | sort -r | head -n 1)
+          LATEST_TAG=$(git tag --merged HEAD | grep "nightly-testing-[0-9]\{4\}-[0-9]\{2\}-[0-9]\{2\}\(-rev[0-9]\+\)\?" | sort -rV | head -n 1)
           echo "Latest tag found for $BRANCH: ${LATEST_TAG:-none}"
 
           # Return to nightly-testing branch

.github/workflows/nightly_detect_failure.yml

@@ -274,7 +274,7 @@ jobs:
           core.setOutput('toolchain_content', content);
           core.setOutput('branch_name', branchName);
 
-          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2})/);
+          const match = content.match(/leanprover\/lean4:nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)/);
           if (!match) {
             core.setFailed('Toolchain pattern did not match');
             return null;
@@ -292,7 +292,7 @@ jobs:
         type: 'stream'
         topic: 'Mathlib status updates'
         content: |
-          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD'.
+          ⚠️ Warning: The lean-toolchain file in bump branch `${{ steps.bump_version.outputs.branch_name }}` does not match the expected pattern 'leanprover/lean4:nightly-YYYY-MM-DD(-revK)'.
 
           **Branch:** `${{ steps.bump_version.outputs.branch_name }}`
           **File URL:** https://github.com/${{ github.repository }}/blob/${{ steps.bump_version.outputs.branch_sha }}/lean-toolchain
@@ -418,7 +418,7 @@ jobs:
             if last_bot_message:
                 last_content = last_bot_message['content']
                 # Extract nightly date and bump branch from last bot message
-                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2})', last_content)
+                date_match = re.search(r'bump/nightly-(\d{4}-\d{2}-\d{2}(?:-rev\d+)?)', last_content)
                 branch_match = re.search(r'PR that to (bump/v[\d.]+)', last_content)
                 if date_match and branch_match:
                     last_date = date_match.group(1)

.github/workflows/nolints.yml

@@ -36,6 +36,8 @@ jobs:
       - name: Create Pull Request
         uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
+          # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+          author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
           token: ${{ steps.app-token.outputs.token }}
           commit-message: "chore(scripts): update nolints.json"
           branch: "nolints"
@@ -44,5 +46,7 @@ jobs:
           body: |
             I am happy to remove some nolints for you!
 
+            ---
+
             [workflow run for this PR](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }})
           labels: "auto-merge-after-CI"

.github/workflows/remove_deprecated_decls.yml

@@ -218,6 +218,8 @@ jobs:
       if: ${{ steps.process_dates.outputs.from_date && toJson(inputs.dry_run) != 'true' && steps.find-pr.outputs.pr_found != 'true' }}
       uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
       with:
+        # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+        author: "mathlib-nolints[bot] <258989889+mathlib-nolints[bot]@users.noreply.github.com>"
         token: ${{ steps.app-token.outputs.token }}
         commit-message: "chore: remove declarations deprecated between ${{ steps.process_dates.outputs.from_date }} and ${{ steps.process_dates.outputs.to_date }}"
         branch: ${{ env.BRANCH_NAME }}

.github/workflows/update_dependencies.yml

@@ -124,6 +124,8 @@ jobs:
         if: ${{ steps.pr-title.outcome == 'success' }}
         uses: peter-evans/create-pull-request@c0f553fe549906ede9cf27b5156039d195d2ece0 # v8.1.0
         with:
+          # this needs to be set, otherwise the last person who edited the `cron` line may get tagged
+          author: "mathlib-update-dependencies[bot] <258990618+mathlib-update-dependencies[bot]@users.noreply.github.com>"
           token: ${{ steps.app-token.outputs.token }}
           commit-message: "chore: update Mathlib dependencies ${{ env.timestamp }}"
           # this branch is referenced in update_dependencies_zulip.yml

Cache/Requests.lean

@@ -374,39 +374,38 @@ def monitorCurl (args : Array String) (size : Nat)
   return s
 
 /-- Call `curl` to download files from the server to `CACHEDIR` (`.cache`).
-Exit the process with exit code 1 if any files failed to download. -/
+Return the number of files which failed to download. -/
 def downloadFiles
     (repo : String) (hashMap : IO.ModuleHashMap)
-    (forceDownload : Bool) (parallel : Bool) (warnOnMissing : Bool): IO Unit := do
+    (forceDownload : Bool) (parallel : Bool) (warnOnMissing : Bool): IO Nat := do
   let hashMap ← if forceDownload then pure hashMap else hashMap.filterExists false
+  if hashMap.isEmpty then IO.println "No files to download"; return 0
   let size := hashMap.size
-  if size > 0 then
-    IO.FS.createDirAll IO.CACHEDIR
-    IO.println s!"Attempting to download {size} file(s) from {repo} cache"
-    let failed ← if parallel then
-      IO.FS.writeFile IO.CURLCFG (← mkGetConfigContent repo hashMap)
-      let args := #["--request", "GET", "--parallel",
-          -- commented as this creates a big slowdown on curl 8.13.0: "--fail",
-          "--silent",
-          "--retry", "5", -- there seem to be some intermittent failures
-          "--write-out", "%{json}\n", "--config", IO.CURLCFG.toString]
-      let {success, failed, done, ..} ←
-        monitorCurl args size "Downloaded" "speed_download" (removeOnError := true)
-      IO.FS.removeFile IO.CURLCFG
-      if warnOnMissing && success + failed < done then
-        IO.eprintln "Warning: some files were not found in the cache."
-        IO.eprintln "This usually means that your local checkout of mathlib4 has diverged from upstream."
-        IO.eprintln "If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later."
-        IO.eprintln "Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building."
-      pure failed
-    else
-      let r ← hashMap.foldM (init := []) fun acc _ hash => do
-        pure <| (← IO.asTask do downloadFile repo hash) :: acc
-      pure <| r.foldl (init := 0) fun f t => if let .ok true := t.get then f else f + 1
-    if failed > 0 then
-      IO.println s!"{failed} download(s) failed"
-      IO.Process.exit 1
-  else IO.println "No files to download"
+  IO.FS.createDirAll IO.CACHEDIR
+  IO.println s!"Attempting to download {size} file(s) from {repo} cache"
+  let failed ← if parallel then
+    IO.FS.writeFile IO.CURLCFG (← mkGetConfigContent repo hashMap)
+    let args := #["--request", "GET", "--parallel",
+        -- commented as this creates a big slowdown on curl 8.13.0: "--fail",
+        "--silent",
+        "--retry", "5", -- there seem to be some intermittent failures
+        "--write-out", "%{json}\n", "--config", IO.CURLCFG.toString]
+    let {success, failed, done, ..} ←
+      monitorCurl args size "Downloaded" "speed_download" (removeOnError := true)
+    IO.FS.removeFile IO.CURLCFG
+    if warnOnMissing && success + failed < done then
+      IO.eprintln "Warning: some files were not found in the cache."
+      IO.eprintln "This usually means that your local checkout of mathlib4 has diverged from upstream."
+      IO.eprintln "If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later."
+      IO.eprintln "Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building."
+    pure failed
+  else
+    let r ← hashMap.foldM (init := []) fun acc _ hash => do
+      pure <| (← IO.asTask do downloadFile repo hash) :: acc
+    pure <| r.foldl (init := 0) fun f t => if let .ok true := t.get then f else f + 1
+  if failed > 0 then
+    IO.println s!"{failed} download(s) failed"
+  return failed
 
 /-- Check if the project's `lean-toolchain` file matches mathlib's.
 Print and error and exit the process with error code 1 otherwise. -/
@@ -481,7 +480,8 @@ def getFiles
   getProofWidgets (← read).proofWidgetsBuildDir
 
   if let some repo := repo? then
-    downloadFiles repo hashMap forceDownload parallel (warnOnMissing := true)
+    let failed ← downloadFiles repo hashMap forceDownload parallel (warnOnMissing := true)
+    if failed > 0 then IO.Process.exit 1
   else
     let repoInfo ← getRemoteRepo (← read).mathlibDepPath
 
@@ -494,8 +494,15 @@ def getFiles
       else
         [MATHLIBREPO, repoInfo.repo]
 
+    let mut failed : Nat := 0
     for h : i in [0:repos.length] do
-      downloadFiles repos[i] hashMap forceDownload parallel (warnOnMissing := i = repos.length - 1)
+      failed := ← (downloadFiles repos[i] hashMap forceDownload parallel (warnOnMissing := i = repos.length - 1))
+      if failed > 10 then
+        IO.println s!"Too many downloads failed; stopping the downloading"
+        IO.Process.exit 1
+    if failed > 0 then
+      IO.println s!"Downloading {failed} files failed"
+      IO.Process.exit 1
 
   if decompress then
     IO.unpackCache hashMap forceUnpack

Mathlib.lean

@@ -1267,6 +1267,7 @@ public import Mathlib.Algebra.WithConv
 public import Mathlib.AlgebraicGeometry.AffineScheme
 public import Mathlib.AlgebraicGeometry.AffineSpace
 public import Mathlib.AlgebraicGeometry.AffineTransitionLimit
+public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
 public import Mathlib.AlgebraicGeometry.Artinian
 public import Mathlib.AlgebraicGeometry.ColimitsOver
 public import Mathlib.AlgebraicGeometry.Cover.Directed
@@ -1295,8 +1296,10 @@ public import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 public import Mathlib.AlgebraicGeometry.Fiber
 public import Mathlib.AlgebraicGeometry.FunctionField
 public import Mathlib.AlgebraicGeometry.GammaSpecAdjunction
+public import Mathlib.AlgebraicGeometry.Geometrically.Basic
 public import Mathlib.AlgebraicGeometry.Gluing
 public import Mathlib.AlgebraicGeometry.GluingOneHypercover
+public import Mathlib.AlgebraicGeometry.Group.Smooth
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Basic
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
 public import Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
@@ -2534,6 +2537,7 @@ public import Mathlib.CategoryTheory.Functor.KanExtension.Preserves
 public import Mathlib.CategoryTheory.Functor.OfSequence
 public import Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced
 public import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
+public import Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
 public import Mathlib.CategoryTheory.Functor.RegularEpi
 public import Mathlib.CategoryTheory.Functor.Trifunctor
 public import Mathlib.CategoryTheory.Functor.TwoSquare
@@ -2624,6 +2628,7 @@ public import Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
 public import Mathlib.CategoryTheory.Limits.Constructions.Over.Products
 public import Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
 public import Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial
+public import Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal
 public import Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
 public import Mathlib.CategoryTheory.Limits.Creates
 public import Mathlib.CategoryTheory.Limits.Elements
@@ -3142,6 +3147,7 @@ public import Mathlib.CategoryTheory.Sites.Over
 public import Mathlib.CategoryTheory.Sites.Plus
 public import Mathlib.CategoryTheory.Sites.Point.Basic
 public import Mathlib.CategoryTheory.Sites.Point.Category
+public import Mathlib.CategoryTheory.Sites.Point.Over
 public import Mathlib.CategoryTheory.Sites.Precoverage
 public import Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
 public import Mathlib.CategoryTheory.Sites.Preserves
@@ -3153,6 +3159,7 @@ public import Mathlib.CategoryTheory.Sites.Pullback
 public import Mathlib.CategoryTheory.Sites.RegularEpi
 public import Mathlib.CategoryTheory.Sites.Sheaf
 public import Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
+public import Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
 public import Mathlib.CategoryTheory.Sites.SheafHom
 public import Mathlib.CategoryTheory.Sites.SheafOfTypes
 public import Mathlib.CategoryTheory.Sites.Sheafification
@@ -5571,6 +5578,7 @@ public import Mathlib.Order.ConditionallyCompleteLattice.Defs
 public import Mathlib.Order.ConditionallyCompleteLattice.Finset
 public import Mathlib.Order.ConditionallyCompleteLattice.Group
 public import Mathlib.Order.ConditionallyCompleteLattice.Indexed
+public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs
 public import Mathlib.Order.Copy
 public import Mathlib.Order.CountableDenseLinearOrder
 public import Mathlib.Order.Cover
@@ -6073,6 +6081,7 @@ public import Mathlib.RingTheory.Finiteness.Bilinear
 public import Mathlib.RingTheory.Finiteness.Cardinality
 public import Mathlib.RingTheory.Finiteness.Cofinite
 public import Mathlib.RingTheory.Finiteness.Defs
+public import Mathlib.RingTheory.Finiteness.Descent
 public import Mathlib.RingTheory.Finiteness.Finsupp
 public import Mathlib.RingTheory.Finiteness.Ideal
 public import Mathlib.RingTheory.Finiteness.Lattice
@@ -6154,6 +6163,7 @@ public import Mathlib.RingTheory.Ideal.Lattice
 public import Mathlib.RingTheory.Ideal.Maps
 public import Mathlib.RingTheory.Ideal.Maximal
 public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic
+public import Mathlib.RingTheory.Ideal.MinimalPrime.Colon
 public import Mathlib.RingTheory.Ideal.MinimalPrime.Localization
 public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
 public import Mathlib.RingTheory.Ideal.NatInt
@@ -7481,6 +7491,7 @@ public import Mathlib.Topology.Order.ProjIcc
 public import Mathlib.Topology.Order.Real
 public import Mathlib.Topology.Order.Rolle
 public import Mathlib.Topology.Order.ScottTopology
+public import Mathlib.Topology.Order.SuccPred
 public import Mathlib.Topology.Order.T5
 public import Mathlib.Topology.Order.UpperLowerSetTopology
 public import Mathlib.Topology.Order.WithTop

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -10,7 +10,6 @@ public import Mathlib.Algebra.Group.Indicator
 public import Mathlib.Algebra.Group.Support
 public import Mathlib.Algebra.Module.Torsion.Free
 public import Mathlib.Algebra.Notation.FiniteSupport
-public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Algebra.Order.Ring.Defs
 public import Mathlib.Data.Set.Finite.Lattice
 

Mathlib/Algebra/BigOperators/Group/Finset/Gaps.lean

@@ -5,8 +5,8 @@ Authors: Yizheng Zhu
 -/
 module
 
-public import Mathlib.Algebra.BigOperators.Fin
 public import Mathlib.Order.Interval.Finset.Gaps
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 /-!
 # Sum of gaps