From 9914961590e72174fd603a1337265438f0bd8a04 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 27 Sep 2024 00:22:14 +0200 Subject: [PATCH 1/2] Add equations of 1 variable and their implications --- equational_theories/Basic.lean | 180 +++++++++++++++++++++++++++++++++ 1 file changed, 180 insertions(+) diff --git a/equational_theories/Basic.lean b/equational_theories/Basic.lean index af51dbff..2412a58e 100644 --- a/equational_theories/Basic.lean +++ b/equational_theories/Basic.lean @@ -36,6 +36,8 @@ def Equation7 (G: Type*) [Magma G] := ∀ x y z : G, x = y ∘ z def Equation8 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ x) +def Equation23 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ x + /-- value of multiplication is independent of right argument -/ def Equation38 (G: Type*) [Magma G] := ∀ x y : G, x ∘ x = x ∘ y @@ -57,11 +59,65 @@ def Equation43 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = y ∘ x /-- The constant law -/ def Equation46 (G: Type*) [Magma G] := ∀ x y z w : G, x ∘ y = z ∘ w +def Equation47 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ (x ∘ x)) + +def Equation99 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ x) ∘ x) + +def Equation151 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ (x ∘ x) + /-- The central groupoid law -/ def Equation168 (G: Type*) [Magma G] := ∀ x y z : G, x = (y ∘ x) ∘ (x ∘ z) +def Equation203 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ x)) ∘ x + +def Equation255 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ x) ∘ x + +def Equation307 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ (x ∘ x) + +def Equation359 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ x) ∘ x + def Equation387 (G: Type*) [Magma G] := ∀ x y : G, x ∘ y = (y ∘ y) ∘ x +def Equation411 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ (x ∘ (x ∘ x))) + +def Equation614 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (x ∘ ((x ∘ x) ∘ x)) + +def Equation817 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ x) ∘ (x ∘ x)) + +def Equation1020 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ ((x ∘ (x ∘ x)) ∘ x) + +def Equation1223 (G: Type*) [Magma G] := ∀ x : G, x = x ∘ (((x ∘ x) ∘ x) ∘ x) + +def Equation1426 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ (x ∘ (x ∘ x)) + +def Equation1629 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ x) ∘ ((x ∘ x) ∘ x) + +def Equation1832 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ x)) ∘ (x ∘ x) + +def Equation2035 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ x) ∘ (x ∘ x) + +def Equation2238 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ (x ∘ (x ∘ x))) ∘ x + +def Equation2441 (G: Type*) [Magma G] := ∀ x : G, x = (x ∘ ((x ∘ x) ∘ x)) ∘ x + +def Equation2644 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ x) ∘ (x ∘ x)) ∘ x + +def Equation2847 (G: Type*) [Magma G] := ∀ x : G, x = ((x ∘ (x ∘ x)) ∘ x) ∘ x + +def Equation3050 (G: Type*) [Magma G] := ∀ x : G, x = (((x ∘ x) ∘ x) ∘ x) ∘ x + +def Equation3253 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ (x ∘ (x ∘ x)) + +def Equation3456 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = x ∘ ((x ∘ x) ∘ x) + +def Equation3659 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ x) ∘ (x ∘ x) + +def Equation3862 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = (x ∘ (x ∘ x)) ∘ x + +def Equation4065 (G: Type*) [Magma G] := ∀ x : G, x ∘ x = ((x ∘ x) ∘ x) ∘ x + +def Equation4380 (G: Type*) [Magma G] := ∀ x : G, x ∘ (x ∘ x) = (x ∘ x) ∘ x + /-- The associative law -/ def Equation4512 (G: Type*) [Magma G] := ∀ x y z : G, x ∘ (y ∘ z) = (x ∘ y) ∘ z @@ -90,6 +146,82 @@ theorem Equation2_implies_Equation7 (G: Type*) [Magma G] (h: Equation2 G) : Equa theorem Equation2_implies_Equation46 (G: Type*) [Magma G] (h: Equation2 G) : Equation46 G := fun _ _ _ _ => h _ _ +theorem Equation3_implies_Equation8 (G: Type*) [Magma G] (h: Equation3 G) : Equation8 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation23 (G: Type*) [Magma G] (h: Equation3 G) : Equation23 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation47 (G: Type*) [Magma G] (h: Equation3 G) : Equation47 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation99 (G: Type*) [Magma G] (h: Equation3 G) : Equation99 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation151 (G: Type*) [Magma G] (h: Equation3 G) : Equation151 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation203 (G: Type*) [Magma G] (h: Equation3 G) : Equation203 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation255 (G: Type*) [Magma G] (h: Equation3 G) : Equation255 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation307 (G: Type*) [Magma G] (h: Equation3 G) : Equation307 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation359 (G: Type*) [Magma G] (h: Equation3 G) : Equation359 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation614 (G: Type*) [Magma G] (h: Equation3 G) : Equation614 G := by + intro x + rw [<-h, <-h, <-h, <-h] + +theorem Equation3_implies_Equation817 (G: Type*) [Magma G] (h: Equation3 G) : Equation817 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation1223 (G: Type*) [Magma G] (h: Equation3 G) : Equation1223 G := by + intro x + rw [<-h, <-h, <-h, <-h] + +theorem Equation3_implies_Equation1426 (G: Type*) [Magma G] (h: Equation3 G) : Equation1426 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation2035 (G: Type*) [Magma G] (h: Equation3 G) : Equation2035 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation2238 (G: Type*) [Magma G] (h: Equation3 G) : Equation2238 G := by + intro x + rw [<-h, <-h, <-h, <-h] + +theorem Equation3_implies_Equation2644 (G: Type*) [Magma G] (h: Equation3 G) : Equation2644 G := by + intro x + rw [<-h, <-h, <-h] + +theorem Equation3_implies_Equation2847 (G: Type*) [Magma G] (h: Equation3 G) : Equation2847 G := by + intro x + rw [<-h, <-h, <-h, <-h] + +theorem Equation3_implies_Equation3659 (G: Type*) [Magma G] (h: Equation3 G) : Equation3659 G := by + intro x + rw [<-h, <-h] + +theorem Equation3_implies_Equation4380 (G: Type*) [Magma G] (h: Equation3 G) : Equation4380 G := by + intro x + rw [<-h] + theorem Equation6_implies_Equation2 (G: Type*) [Magma G] (h: Equation6 G) : Equation2 G := by intro a b rw [h a a, ← h b] @@ -110,6 +242,46 @@ theorem Equation4_implies_Equation4522 (G: Type*) [Magma G] (h: Equation4 G) : E intro x y z w u rw [<-h, <-h, <-h] +theorem Equation8_implies_Equation411 (G: Type*) [Magma G] (h: Equation8 G) : Equation411 G := by + intro x + rw [<-h, <-h] + +theorem Equation8_implies_Equation1020 (G: Type*) [Magma G] (h: Equation8 G) : Equation1020 G := by + intro x + rw [<-h, <-h] + +theorem Equation8_implies_Equation1832 (G: Type*) [Magma G] (h: Equation8 G) : Equation1832 G := by + intro x + rw [<-h, <-h] + +theorem Equation8_implies_Equation3253 (G: Type*) [Magma G] (h: Equation8 G) : Equation3253 G := by + intro x + rw [<-h] + +theorem Equation8_implies_Equation3862 (G: Type*) [Magma G] (h: Equation8 G) : Equation3862 G := by + intro x + rw [<-h] + +theorem Equation23_implies_Equation1629 (G: Type*) [Magma G] (h: Equation23 G) : Equation1629 G := by + intro x + rw [<-h, <-h] + +theorem Equation23_implies_Equation2441 (G: Type*) [Magma G] (h: Equation23 G) : Equation2441 G := by + intro x + rw [<-h, <-h] + +theorem Equation23_implies_Equation3050 (G: Type*) [Magma G] (h: Equation23 G) : Equation3050 G := by + intro x + rw [<-h, <-h] + +theorem Equation23_implies_Equation3456 (G: Type*) [Magma G] (h: Equation23 G) : Equation3456 G := by + intro x + rw [<-h] + +theorem Equation23_implies_Equation4065 (G: Type*) [Magma G] (h: Equation23 G) : Equation4065 G := by + intro x + rw [<-h] + theorem Equation46_implies_Equation42 (G: Type*) [Magma G] (h: Equation46 G) : Equation42 G := fun _ _ _ => h _ _ _ _ @@ -119,6 +291,14 @@ theorem Equation46_implies_Equation387 (G: Type*) [Magma G] (h: Equation46 G) : theorem Equation46_implies_Equation4582 (G: Type*) [Magma G] (h: Equation46 G) : Equation4582 G := fun _ _ _ _ _ _ => h _ _ _ _ +theorem Equation307_implies_Equation3253 (G: Type*) [Magma G] (h: Equation307 G) : Equation3253 G := by + intro x + rw [<-h, <-h] + +theorem Equation359_implies_Equation4065 (G: Type*) [Magma G] (h: Equation359 G) : Equation4065 G := by + intro x + rw [<-h, <-h] + /-- This proof is from https://mathoverflow.net/a/450905/766 -/ theorem Equation387_implies_Equation43 (G: Type*) [Magma G] (h: Equation387 G) : Equation43 G := by have idem (x : G) : (x ∘ x) ∘ (x ∘ x) = (x ∘ x) := by From 79c372eb6b000e7673503b3cddd8f644d6f3e296 Mon Sep 17 00:00:00 2001 From: Vlad Tsyrklevich Date: Fri, 27 Sep 2024 00:49:29 +0200 Subject: [PATCH 2/2] Add equations to blueprint --- blueprint/src/chapter/equations.tex | 84 +++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/blueprint/src/chapter/equations.tex b/blueprint/src/chapter/equations.tex index b453dd23..25a489ce 100644 --- a/blueprint/src/chapter/equations.tex +++ b/blueprint/src/chapter/equations.tex @@ -24,6 +24,9 @@ \chapter{Equations} \begin{definition}[Equation 8]\label{eq8}\lean{Equation8}\leanok\uses{magma-def} Equation 8 is the law $x=x \circ (x \circ x)$. \end{definition} +\begin{definition}[Equation 23]\label{eq23}\lean{Equation23}\leanok\uses{magma-def} Equation 23 is the law $x = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 38]\label{eq38}\lean{Equation38}\leanok\uses{magma-def} Equation 38 is the law $x \circ x = x \circ y$. \end{definition} @@ -45,12 +48,93 @@ \chapter{Equations} \begin{definition}[Equation 46]\label{eq46}\lean{Equation46}\leanok\uses{magma-def} Equation 46 is the law $x \circ y = z \circ w$. \end{definition} +\begin{definition}[Equation 47]\label{eq47}\lean{Equation47}\leanok\uses{magma-def} Equation 47 is the law $x = x \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 99]\label{eq99}\lean{Equation99}\leanok\uses{magma-def} Equation 99 is the law $x = x \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 151]\label{eq151}\lean{Equation151}\leanok\uses{magma-def} Equation 151 is the law $x = (x \circ x) \circ (x \circ x)$. +\end{definition} + \begin{definition}[Equation 168]\label{eq168}\lean{Equation168}\leanok\uses{magma-def} Equation 168 is the law $x = (y \circ x) \circ (x \circ z)$. \end{definition} +\begin{definition}[Equation 203]\label{eq203}\lean{Equation203}\leanok\uses{magma-def} Equation 203 is the law $x = (x \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 255]\label{eq255}\lean{Equation255}\leanok\uses{magma-def} Equation 255 is the law $x = ((x \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 307]\label{eq307}\lean{Equation307}\leanok\uses{magma-def} Equation 307 is the law $x \circ x = x \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 359]\label{eq359}\lean{Equation359}\leanok\uses{magma-def} Equation 359 is the law $x \circ x = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 387]\label{eq387}\lean{Equation387}\leanok\uses{magma-def} Equation 387 is the law $x \circ y = (y \circ y) \circ x$. \end{definition} +\begin{definition}[Equation 411]\label{eq411}\lean{Equation411}\leanok\uses{magma-def} Equation 411 is the law $x = x \circ (x \circ (x \circ (x \circ x)))$. +\end{definition} + +\begin{definition}[Equation 614]\label{eq614}\lean{Equation614}\leanok\uses{magma-def} Equation 614 is the law $x = x \circ (x \circ ((x \circ x) \circ x))$. +\end{definition} + +\begin{definition}[Equation 817]\label{eq817}\lean{Equation817}\leanok\uses{magma-def} Equation 817 is the law $x = x \circ ((x \circ x) \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 1020]\label{eq1020}\lean{Equation1020}\leanok\uses{magma-def} Equation 1020 is the law $x = x \circ ((x \circ (x \circ x)) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1223]\label{eq1223}\lean{Equation1223}\leanok\uses{magma-def} Equation 1223 is the law $x = x \circ (((x \circ x) \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1426]\label{eq1426}\lean{Equation1426}\leanok\uses{magma-def} Equation 1426 is the law $x = (x \circ x) \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 1629]\label{eq1629}\lean{Equation1629}\leanok\uses{magma-def} Equation 1629 is the law $x = (x \circ x) \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 1832]\label{eq1832}\lean{Equation1832}\leanok\uses{magma-def} Equation 1832 is the law $x = (x \circ (x \circ x)) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 2035]\label{eq2035}\lean{Equation2035}\leanok\uses{magma-def} Equation 2035 is the law $x = ((x \circ x) \circ x) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 2238]\label{eq2238}\lean{Equation2238}\leanok\uses{magma-def} Equation 2238 is the law $x = (x \circ (x \circ (x \circ x))) \circ x$. +\end{definition} + +\begin{definition}[Equation 2441]\label{eq2441}\lean{Equation2441}\leanok\uses{magma-def} Equation 2441 is the law $x = (x \circ ((x \circ x) \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 2644]\label{eq2644}\lean{Equation2644}\leanok\uses{magma-def} Equation 2644 is the law $x = ((x \circ x) \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 2847]\label{eq2847}\lean{Equation2847}\leanok\uses{magma-def} Equation 2847 is the law $x = ((x \circ (x \circ x)) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 3050]\label{eq3050}\lean{Equation3050}\leanok\uses{magma-def} Equation 3050 is the law $x = (((x \circ x) \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 3253]\label{eq3253}\lean{Equation3253}\leanok\uses{magma-def} Equation 3253 is the law $x \circ x = x \circ (x \circ (x \circ x))$. +\end{definition} + +\begin{definition}[Equation 3456]\label{eq3456}\lean{Equation3456}\leanok\uses{magma-def} Equation 3456 is the law $x \circ x = x \circ ((x \circ x) \circ x)$. +\end{definition} + +\begin{definition}[Equation 3659]\label{eq3659}\lean{Equation3659}\leanok\uses{magma-def} Equation 3659 is the law $x \circ x = (x \circ x) \circ (x \circ x)$. +\end{definition} + +\begin{definition}[Equation 3862]\label{eq3862}\lean{Equation3862}\leanok\uses{magma-def} Equation 3862 is the law $x \circ x = (x \circ (x \circ x)) \circ x$. +\end{definition} + +\begin{definition}[Equation 4065]\label{eq4065}\lean{Equation4065}\leanok\uses{magma-def} Equation 4065 is the law $x \circ x = ((x \circ x) \circ x) \circ x$. +\end{definition} + +\begin{definition}[Equation 4380]\label{eq4380}\lean{Equation4380}\leanok\uses{magma-def} Equation 4380 is the law $x \circ (x \circ x) = (x \circ x) \circ x$. +\end{definition} + \begin{definition}[Equation 4512]\label{eq4512}\lean{Equation4512}\leanok\uses{magma-def} Equation 4512 is the law $x \circ (y \circ z) = (x \circ y) \circ z$. \end{definition}