Prove that Eq1323 does not imply Eq2744

blueprint/src/chapter/1323.tex

@@ -5,14 +5,12 @@ \chapter{Equation 1323}\label{1323-chapter}
   x = y \op (((y \op y) \op x) \op y)
 \end{equation}
 for all $x,y$.  Using the squaring operator $Sy := y \op y$ and the left and right multiplication operators $L_y x := y \op x$ and $R_y x = x \op y$, this law can be written as
-$$ L_y R_y L_{Sy} x = x$$
-and
-$$ R_{Sy} L_y R_y x = x$$
-respectively.  In particular, this gives a way to construct these magmas:
+$$ L_y R_y L_{Sy} x = x.$$
+In particular, this gives a way to construct these magmas:
 
-\begin{lemma}[Construction of 1323 magmas]\label{1323-construct}  Suppose that $M$ is a magma such that
+\begin{lemma}[Construction of 1323 magmas]\label{1323-construct}\leanok\lean{Eq1323.eq1323_if_conditions}  Suppose that $M$ is a magma such that
   \begin{equation}\label{lr}
-    L_{Sy} R_{Sy} = 1
+    R_{Sy} L_{Sy} = 1
    \end{equation}
 and
 \begin{equation}\label{lr-simp}
@@ -26,8 +24,8 @@ \chapter{Equation 1323}\label{1323-chapter}
 
  So now we would like to construct magmas satisfying \Cref{lr} and \Cref{lr-simp}.  We need some bijections:
 
- \begin{lemma}[Bijections]\label{bij}
-  Let $G$ be a countably infinite abelian group of order $2$.  Then there exists a bijection $\phi_a: G \to \Q^\times$ for each $a \in G \backslash \{0\}$ such that
+ \begin{lemma}[Bijections]\label{bij}\leanok\lean{Eq1323.Ingredients.ϕ}
+  Let $G$ be a countably infinite abelian torsion group of exponent $2$.  Then there exists a bijection $\phi_a: G \to \Q^\times$ for each $a \in G \backslash \{0\}$ such that
  $\phi_a(0) = 1$ and $\phi_a(a+b) = -\phi_a(b)$ for all $b \in G$, so in particular $\phi_a(a)=-1$.
  \end{lemma}
 
@@ -36,7 +34,7 @@ \chapter{Equation 1323}\label{1323-chapter}
  \end{proof}
 
 
- \begin{lemma}[Building a magma]\label{build-magma}  Let $G$ be a countably infinite abelian group of order $2$, and let $\phi_a$ be as in the previous lemma.  Let $N$ be the set of pairs $(x,a)$ with $x \in \Q^\times$ and $a \in G \backslash \{0\}$, and let $M = G \uplus N$ be the disjoint union of $G$ and $N$.  Suppose that we have an operation $\op : M \times M \to M$ obeying the following axioms:
+ \begin{lemma}[Building a magma]\label{build-magma}\leanok\lean{Eq1323.op}\lean{Eq1323.op_RSy_LSy_eq_Id}\lean{Eq1323.op_Ly_Ry_eq_LSy}  Let $G$ be a countably infinite abelian torsion group of exponent $2$, and let $\phi_a$ be as in the previous lemma.  Let $N$ be the set of pairs $(x,a)$ with $x \in \Q^\times$ and $a \in G \backslash \{0\}$, and let $M = G \uplus N$ be the disjoint union of $G$ and $N$.  Suppose that we have an operation $\op : M \times M \to M$ obeying the following axioms:
 \begin{itemize}
 \item (i) We have
 \begin{equation}\label{op-0}

blueprint/src/chapter/infinite_magma_constructions.tex

@@ -781,6 +781,7 @@ \subsection{Second construction}
 $$ f(-7)=-4, f(-3) = 4, f(-2)=-3, f(-1)=-1, f(0) = 1, f(1) = 3, f(3)=0, f(4) = -2, f(6) = 2.$$
 
 In this construction, we define a partial solution to be a function $f: E \to \Z$ defined on a finite subset of $E$ obeying the following axioms:
+\lean{Eq63.Greedy.PartialSolution}
 \begin{itemize}
 \item[(i)] $E$ contains $E_0$, and $f$ agrees with $f_0$ on $E_0$.
 \item[(ii)] If $h \in E$ and $f(h) \in E$, then $f^2(h)-h$ is also in $E$, and $f(f^2(h)-h) = -h$.
@@ -796,7 +797,7 @@ \subsection{Second construction}
 \begin{proof} Finite check.
 \end{proof}
 
-\begin{lemma}[Extension]\label{extension-lemma} If $f: E \to \Z$ is a partial solution and $h_0 \in \Z$, then there exists an extension $f': E' \to \Z$ for which axiom (ii) applies, i.e., $h_0 \in E'$, $f'(h_0) \in E'$, $(f')^2(h_0)-h_0 \in E'$, and $f'((f')^2(h_0)-h_0) = -h_0$.
+\begin{lemma}[Extension]\label{extension-lemma}\leanok\lean{Eq63.Greedy.Extension.Next}\lean{Eq63.Greedy.Extension.next} If $f: E \to \Z$ is a partial solution and $h_0 \in \Z$, then there exists an extension $f': E' \to \Z$ for which axiom (ii) applies, i.e., $h_0 \in E'$, $f'(h_0) \in E'$, $(f')^2(h_0)-h_0 \in E'$, and $f'((f')^2(h_0)-h_0) = -h_0$.
 \end{lemma}
 
 \begin{proof}  We divide into cases.
@@ -842,10 +843,10 @@ \subsection{Second construction}
 
 Iterating this lemma, we conclude
 
-\begin{corollary}[Greedy completion of Dupont]\label{dupont-iter} Every partial solution $f: E \to \Z$ can be extended to a global solution $f': \Z \to\Z$ of \Cref{dupont-eq}.
+\begin{corollary}[Greedy completion of Dupont]\label{dupont-iter}\leanok\lean{Eq63.Greedy.exists_extension} Every partial solution $f: E \to \Z$ can be extended to a global solution $f': \Z \to\Z$ of \Cref{dupont-eq}.
 \end{corollary}
 
-\begin{corollary}[Non-injective Dupont solution]\label{non-inject} The Dupont equation admits non-injective solutions, and hence can violate Equation 1692.
+\begin{corollary}[Non-injective Dupont solution]\label{non-inject}\leanok\lean{Eq63.Equation63_not_implies_Equation1692} The Dupont equation admits non-injective solutions, and hence can violate Equation 1692.
 \end{corollary}
 
 \begin{proof} It suffices to find a partial solution that violates injectivity.  This can be done for instance by adjoining $\{-13, 10\}$ to $E_0$ and defining $f(10)= 2 = f(6)$, $f(-13)=-10$, and performing a finite check to verify that this is still a partial solution.

equational_theories/ForMathlib/GroupTheory/FreeGroup/ReducedWords.lean

@@ -269,4 +269,13 @@ theorem ne_inv_of_ne_one {x : FreeGroup α} (x_ne_one : x ≠ 1) : x ≠ x⁻¹
   rw [← eq]
   exact pow_two x
 
+theorem pow_injective {x y : FreeGroup α} {n : ℕ} (hn : n ≠ 0) : x = y ↔ x ^ n = y ^ n := by
+  sorry
+
+theorem zpow_injective {x y : FreeGroup α} {n : ℤ} (hn : n ≠ 0) : x = y ↔ x ^ n = y ^ n := by
+  rw [pow_injective (Int.natAbs_ne_zero.mpr hn)]
+  rcases Int.natAbs_eq n with h | h
+  · rw [h, Int.natAbs_ofNat, zpow_natCast, zpow_natCast]
+  · rw [h, Int.natAbs_neg, Int.natAbs_ofNat, zpow_neg, zpow_neg, inv_inj, zpow_natCast, zpow_natCast]
+
 end FreeGroup

equational_theories/FreshGenerator.lean

@@ -26,6 +26,12 @@ instance [Nonempty α] : Infinite (FreeGroup α) :=
   Infinite.of_injective (FreeGroup.of a ^ ·) <| by
     simp [FreeGroup.norm_of_pow, infinite_order]
 
+instance [DecidableEq α] : DecidableEq (FreeGroup α) :=
+  fun a b =>
+    if h : a.toWord = b.toWord
+      then isTrue (FreeGroup.toWord_inj.mp h)
+      else isFalse (mt FreeGroup.toWord_inj.mpr h)
+
 
 def generatorNames' : List (α × Bool) → Finset α
   | [] => ∅
@@ -247,4 +253,42 @@ theorem forgetOld_old {S : Finset (FreeGroup α)} {x : FreeGroup α} (hxS : x 
   apply dropGenerators_generatorNames
   exact Finset.subset_biUnion_of_mem _ hxS
 
+noncomputable section
+
+/- This is a simpler version of the above, that only projects into a single dimension - of the
+freshGenerator. Calculation with numbers works a bit better with `simp` so this is easier to use
+if it's suitable. -/
+
+def projectFresh' (S : Finset (FreeGroup α)) (a : α) : Multiplicative ℤ :=
+  if a = freshGeneratorName S then (1 : ℤ) else (0 : ℤ)
+
+def projectFresh (S : Finset (FreeGroup α)) : FreeGroup α →* Multiplicative ℤ where
+  toFun x := FreeGroup.lift (projectFresh' S) x
+  map_one' := rfl
+  map_mul' := by intros; simp
+
+@[simp] theorem projectFresh_fresh {S : Finset (FreeGroup α)} : projectFresh S (freshGenerator S) = (1 : ℤ) := by
+  simp [projectFresh, projectFresh', freshGenerator]
+
+theorem projectFresh_old' {S : Finset (FreeGroup α)} (L : List (α × Bool)) :
+    generatorNames' L ⊆ S.biUnion generatorNames → projectFresh S (mk L) = 1 := by
+  induction L
+  case nil => simp [generatorNames', ← one_eq_mk]
+  case cons head _ ih =>
+    rw [← List.singleton_append]
+    intro hn
+    simp only [generatorNames', List.singleton_append] at hn
+    rw [← mul_mk, projectFresh, MonoidHom.map_mul, ← projectFresh, ih]
+    · have : head.1 ∈ S.biUnion generatorNames :=
+        Finset.singleton_subset_iff.mp $ Finset.union_subset_left hn
+      have : freshGeneratorName S ∉ S.biUnion generatorNames := (existsFreshGeneratorName S).choose_spec
+      simp [projectFresh, projectFresh']
+      by_cases head.2 <;> aesop
+    · exact Finset.union_subset_right hn
+
+theorem projectFresh_old {S : Finset (FreeGroup α)} {x} (h : x ∈ S) : projectFresh S x = 1 :=
+  mk_toWord (x := x) ▸ projectFresh_old' _ fun _ h' ↦ Finset.mem_biUnion.mpr ⟨x, h, h'⟩
+
+end
+
 end FreshGenerator