-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'master' of https://github.com/Paul-Lez/PH_formalisation
- Loading branch information
Showing
23 changed files
with
755 additions
and
52 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,122 @@ | ||
| on: | ||
| push: | ||
| branches: | ||
| - master | ||
|
|
||
| # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages | ||
| permissions: | ||
| contents: read | ||
| pages: write | ||
| id-token: write | ||
|
|
||
| jobs: | ||
| style_lint: | ||
| name: Lint style | ||
| runs-on: ubuntu-latest | ||
| steps: | ||
| - name: Check for long lines | ||
| if: always() | ||
| run: | | ||
| ! (find PersistentDecomp -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://') | ||
| - name: Don't 'import Mathlib', use precise imports | ||
| if: always() | ||
| run: | | ||
| ! (find PersistentDecomp -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$') | ||
| build_project: | ||
| runs-on: ubuntu-latest | ||
| name: Build project | ||
| steps: | ||
| - name: Checkout project | ||
| uses: actions/checkout@v2 | ||
| with: | ||
| fetch-depth: 0 | ||
|
|
||
| - name: Print files to upstream | ||
| run: | | ||
| grep -r --files-without-match 'import PersistentDecomp' PersistentDecomp | sort > 1.txt | ||
| grep -r --files-with-match 'sorry' PersistentDecomp | sort > 2.txt | ||
| mkdir -p docs/_includes | ||
| comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/Paul-Lez\/PH_formalisation\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md | ||
| rm 1.txt 2.txt | ||
| - name: Count sorries | ||
| run: python scripts/count_sorry.py | ||
|
|
||
| - name: Install elan | ||
| run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.5.0 | ||
|
|
||
| - name: Get cache | ||
| run: ~/.elan/bin/lake exe cache get || true | ||
|
|
||
| - name: Build project | ||
| run: ~/.elan/bin/lake build PersistentDecomp | ||
|
|
||
| - name: Cache mathlib docs | ||
| uses: actions/cache@v3 | ||
| with: | ||
| path: | | ||
| .lake/build/doc/Init | ||
| .lake/build/doc/Lake | ||
| .lake/build/doc/Lean | ||
| .lake/build/doc/Std | ||
| .lake/build/doc/Mathlib | ||
| .lake/build/doc/declarations | ||
| key: MathlibDoc-${{ hashFiles('lake-manifest.json') }} | ||
| restore-keys: | | ||
| MathlibDoc- | ||
| - name: Build documentation | ||
| run: ~/.elan/bin/lake -R -Kenv=dev build PersistentDecomp:docs | ||
|
|
||
| - name: Build blueprint and copy to `docs/blueprint` | ||
| uses: xu-cheng/texlive-action@v2 | ||
| with: | ||
| docker_image: ghcr.io/xu-cheng/texlive-full:20231201 | ||
| run: | | ||
| apk update | ||
| apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev | ||
| git config --global --add safe.directory $GITHUB_WORKSPACE | ||
| git config --global --add safe.directory `pwd` | ||
| python3 -m venv env | ||
| source env/bin/activate | ||
| pip install --upgrade pip requests wheel | ||
| pip install pygraphviz --global-option=build_ext --global-option="-L/usr/lib/graphviz/" --global-option="-R/usr/lib/graphviz/" | ||
| pip install leanblueprint | ||
| leanblueprint pdf | ||
| cp blueprint/print/print.pdf docs/blueprint.pdf | ||
| leanblueprint web | ||
| cp -r blueprint/web docs/blueprint | ||
| - name: Move documentation to `docs/docs` | ||
| run: | | ||
| mv .lake/build/doc docs/docs | ||
| - name: Bundle dependencies | ||
| uses: ruby/setup-ruby@v1 | ||
| with: | ||
| working-directory: docs | ||
| ruby-version: "3.0" # Specify Ruby version | ||
| bundler-cache: true # Enable caching for bundler | ||
|
|
||
| - name: Build website using Jekyll | ||
| working-directory: docs | ||
| run: JEKYLL_ENV=production bundle exec jekyll build # Note this will also copy the blueprint and API doc into docs/_site | ||
|
|
||
| - name: Upload docs & blueprint artifact | ||
| uses: actions/upload-pages-artifact@v1 | ||
| with: | ||
| path: docs/_site | ||
|
|
||
| - name: Deploy to GitHub Pages | ||
| id: deployment | ||
| uses: actions/deploy-pages@v1 | ||
|
|
||
| # - name: Check declarations | ||
| # run: | | ||
| # ~/.elan/bin/lake exe checkdecls blueprint/lean_decls | ||
|
|
||
| - name: Make sure the cache works | ||
| run: | | ||
| mv docs/docs .lake/build/doc |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
2 changes: 1 addition & 1 deletion
2
...ntDecomp/Mathlib/Data/DFinsupp/Basic.lean → ...p/Mathlib/Data/DFinsupp/BigOperators.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,30 @@ | ||
| # Structure theory of persistence modules | ||
| # Decomposition of Persistence Modules | ||
|
|
||
| Temporary repo so we can use Lean project infratructure (setting it up seems to require creating a new repository) | ||
| The objective of this repository is to formalise the statement of the barcode decomposition theorem of persistence modules into the Lean proof assistant. | ||
|
|
||
| ## Source | ||
|
|
||
| The main source for our work is the paper "Decomposition of Persistence Modules" authored by Magnus Bakke Botnan and William Crawley-Boevey. This paper is available [here](https://arxiv.org/pdf/1811.08946). | ||
|
|
||
| The main result we currently aim to prove is Theorem 1.1: *Any pointwise finite-dimensional persistence module is a direct sum of indecomposable modules with local endomorphism ring*. | ||
|
|
||
| ## Contents | ||
|
|
||
| The code is contained in the directory `PH_formalisation`. It contains the following subdirectories: | ||
| * `Mathlib`: contains material missing from current files in Mathlib. | ||
| * `Prereqs`: contains basic definitions and properties of persistence modules. | ||
|
|
||
| In addition, we also have the following files: | ||
| * `DirectSumDecomposition`: defines direct sum decompositions of persistence modules and proves basic facts about them. | ||
| * `thm1_1`: proves that indecomposable modules have local endomorphism rings. | ||
| * `step_2`: proves that pointwise finite-dimensional persistence modules decompose as a direct sum of indecomposable modules. | ||
|
|
||
| ## Future Considerations | ||
|
|
||
| Once Theorem 1.1 is proven, we hope to be able to prove Theorem 1.2: *Pointwise finite-dimensional persistence modules over a totally ordered set decompose into interval modules*. This result is frequently used in topological data analysis, and hence it should be upstreamed to mathlib. | ||
|
|
||
| The current implementation views persistence modules and persistence submodules as purely separate objects. It should be a future goal to unify them. | ||
|
|
||
| ## Acknowledgements | ||
|
|
||
| Our project relies on mathlib and we thank all who have contributed on it in some manner for their help. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
| --- | ||
| BUNDLE_PATH: "vendor/bundle" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| _site | ||
| .sass-cache | ||
| .jekyll-cache | ||
| .jekyll-metadata | ||
| vendor | ||
| blueprint/ | ||
| blueprint.pdf | ||
| docs/ |
Oops, something went wrong.