Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

Author: kbuzzard

.github/workflows/01-claim-issue.yml

@@ -84,7 +84,7 @@ jobs:
           COMMENT_RESPONSE=$(curl -s -o /dev/null -w "%{http_code}" -X POST \
             -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
             -H "Content-Type: application/json" \
-            -d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been added to the project board by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md)."}' \
+            -d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been added to the project board by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
             https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/comments)
 
           if [ "$COMMENT_RESPONSE" -eq 201 ]; then
@@ -113,7 +113,7 @@ jobs:
         if [ "$CURRENT_STATUS_ID" != "$UNCLAIMED_TASKS_ID" ]; then
           echo "Issue is not classified as 'Unclaimed'. Posting comment."
           curl -X POST -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
-          -d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed Outstanding Task\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md)."}' \
+          -d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed Outstanding Task\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
           https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/comments
           exit 1
         fi

.github/workflows/push.yml

@@ -103,6 +103,8 @@ jobs:
 
       - name: Bundle website
         working-directory: docs
+        env:
+          JEKYLL_GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: JEKYLL_ENV=production bundle exec jekyll build
 
       - name: Upload docs & blueprint artifact

FLT/FLT_files.lean

@@ -9,12 +9,7 @@ import FLT.GaloisRepresentation.HardlyRamified
 import FLT.GlobalLanglandsConjectures.GLnDefs
 import FLT.GlobalLanglandsConjectures.GLzero
 import FLT.GroupScheme.FiniteFlat
-import FLT.HIMExperiments.ContinuousSMul_topology
-import FLT.HIMExperiments.dual_topology
-import FLT.HIMExperiments.FGModuleTopology
 import FLT.HIMExperiments.flatness
-import FLT.HIMExperiments.module_topology
-import FLT.HIMExperiments.right_module_topology
 import FLT.Hard.Results
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler

FLT/ForMathlib/MiscLemmas.lean

@@ -83,13 +83,6 @@ theorem induced_continuous_add [AddCommMonoid A] [τA : TopologicalSpace A] [Con
     @ContinuousAdd B (TopologicalSpace.induced h τA) _ := by
   convert Inducing.continuousAdd h (inducing_induced h)
 
-theorem induced_sInf {α β : Type*} {g : β → α}
-    {s : Set (TopologicalSpace α)} :
-    TopologicalSpace.induced g (sInf s) =
-    sInf ((TopologicalSpace.induced g) '' s) := by
-  rw [sInf_eq_iInf' s, sInf_image']
-  exact induced_iInf
-
 end induced
 
 -- elsewhere