diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 51c22550..05efdd38 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,7 +1 @@ -# Contributing to [Project] - -Thank you for your interest in contributing to [Project]! We welcome contributions from the -community and appreciate your efforts to improve the project. Please follow the guidelines below -to ensure a smooth contribution process. - -... \ No newline at end of file +# Contributing to Equational Theories diff --git a/README.md b/README.md index 02f61e7e..5b00ae2d 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,8 @@ The purpose of this project is to explore the space of equational theories of magmas, ordered by implication. To begin with we shall focus only on theories of a single equation, which are listed [here](https://github.com/teorth/equational_theories/blob/main/scripts/equations.txt). +A (manually created) graph of the dependencies obtained so far can be found [here](images/implications.png), current as of Sep 26 2024. + Links: - [Main web page](https://teorth.github.io/equational_theories/) diff --git a/blueprint/src/chapter/intro.tex b/blueprint/src/chapter/intro.tex index 801b1617..ee6eb746 100644 --- a/blueprint/src/chapter/intro.tex +++ b/blueprint/src/chapter/intro.tex @@ -3,7 +3,7 @@ \chapter{Introduction} \begin{definition}\label{magma-def}\lean{Magma}\leanok A Magma is a set $G$ equipped with a binary operation $\circ: G \times G \to G$. \end{definition} -A \emph{law} is a equation involving a finite number of indeterminate variables and the operation $\circ$. A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$. For instance, the commutative law +A \emph{law} is an equation involving a finite number of indeterminate variables and the operation $\circ$. A magma $G$ then obeys that law if the equation holds for all possible choices of indeterminate variables in $G$. For instance, the commutative law $$ x \circ y = y \circ x$$ holds in a magma $G$ if and only if that magma is abelian. diff --git a/home_page/_layouts/default.html b/home_page/_layouts/default.html index 22a44e98..a66082d1 100644 --- a/home_page/_layouts/default.html +++ b/home_page/_layouts/default.html @@ -28,6 +28,7 @@

{{ page.title | default: site.title | default: site.git

{{ page.description | default: site.description | default: site.github.project_tagline }}

Blueprint (web) + Blueprint (pdf) Documentation {% if site.github.is_project_page %} GitHub @@ -46,4 +47,4 @@

{{ page.description | default: site.description | de - \ No newline at end of file + diff --git a/home_page/index.md b/home_page/index.md index 6ffef044..e4ffb643 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -8,8 +8,8 @@ usemathjax: true Useful links: -* [Zulip chat for Lean](https://leanprover.zulipchat.com/) for coordination -* [Blueprint](blueprint/) -* [Blueprint as pdf](blueprint.pdf) -* [Dependency graph](blueprint/dep_graph_document.html) -* [Doc pages for this repository](docs/) \ No newline at end of file +* [Zulip chat for Lean](https://leanprover.zulipchat.com/#narrow/stream/458659-Equational) for coordination +* [Blueprint]({{ site.url }}/blueprint/) +* [Blueprint as pdf]({{ site.url }}/blueprint.pdf) +* [Dependency graph]({{ site.url }}/blueprint/dep_graph_document.html) +* [Doc pages for this repository]({{ site.url }}/docs/) diff --git a/images/implications.png b/images/implications.png new file mode 100644 index 00000000..11ebf37d Binary files /dev/null and b/images/implications.png differ diff --git a/images/implications.svg b/images/implications.svg new file mode 100644 index 00000000..5c1451a0 --- /dev/null +++ b/images/implications.svg @@ -0,0 +1,3854 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + To be placed: + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/lakefile.toml b/lakefile.toml index 9b525148..c1a2ab13 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,7 +10,6 @@ relaxedAutoImplicit = false name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" - [[require]] name = "checkdecls" git = "https://github.com/PatrickMassot/checkdecls.git" @@ -19,6 +18,7 @@ git = "https://github.com/PatrickMassot/checkdecls.git" name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" rev = "main" + [[lean_lib]] name = "equational_theories" diff --git a/scripts/update_mathlib.bat b/scripts/update_mathlib.bat index 48cd7350..83c2f97f 100644 --- a/scripts/update_mathlib.bat +++ b/scripts/update_mathlib.bat @@ -5,8 +5,8 @@ rem Download the latest lean-toolchain file from the Mathlib4 repository curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain rem Update the Mathlib dependencies and ensure doc-gen is also updated -rem The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen -lake -Kenv=dev update +rem The `-R -Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -R -Kenv=dev update rem Retrieve and cache the latest Mathlib dependencies -lake exe cache get \ No newline at end of file +lake exe cache get diff --git a/scripts/update_mathlib.sh b/scripts/update_mathlib.sh index f24c177c..ee844740 100644 --- a/scripts/update_mathlib.sh +++ b/scripts/update_mathlib.sh @@ -4,8 +4,8 @@ curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain # Update the Mathlib dependencies and ensure doc-gen is also updated -# The `-Kenv=dev` flag ensures that the development environment is updated, including doc-gen -lake -Kenv=dev update +# The `-R -Kenv=dev` flag ensures that the development environment is updated, including doc-gen +lake -R -Kenv=dev update # Retrieve and cache the latest Mathlib dependencies -lake exe cache get \ No newline at end of file +lake exe cache get