From 203dfb64efb5fad4fa32c9a85a3bfd801bae75da Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 18 May 2026 17:09:48 +0900 Subject: [PATCH 1/6] Vendor Polylean unit conjecture infrastructure --- LeanPool.lean | 12 + LeanPool/Polylean.lean | 18 + LeanPool/Polylean/UnitConjecture.lean | 61 + .../Polylean/UnitConjecture/AddFreeGroup.lean | 132 ++ LeanPool/Polylean/UnitConjecture/Cocycle.lean | 150 ++ .../Polylean/UnitConjecture/EnumDecide.lean | 267 ++++ .../Polylean/UnitConjecture/FreeModule.lean | 1392 +++++++++++++++++ .../Polylean/UnitConjecture/GardamGroup.lean | 204 +++ .../Polylean/UnitConjecture/GroupRing.lean | 627 ++++++++ .../UnitConjecture/MetabelianGroup.lean | 104 ++ LeanPool/Polylean/UnitConjecture/Tactics.lean | 13 + .../UnitConjecture/Tactics/AesopRuleSets.lean | 16 + .../Polylean/UnitConjecture/TorsionFree.lean | 189 +++ LeanPool/projects.yml | 25 + 14 files changed, 3210 insertions(+) create mode 100644 LeanPool/Polylean.lean create mode 100644 LeanPool/Polylean/UnitConjecture.lean create mode 100644 LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean create mode 100644 LeanPool/Polylean/UnitConjecture/Cocycle.lean create mode 100644 LeanPool/Polylean/UnitConjecture/EnumDecide.lean create mode 100644 LeanPool/Polylean/UnitConjecture/FreeModule.lean create mode 100644 LeanPool/Polylean/UnitConjecture/GardamGroup.lean create mode 100644 LeanPool/Polylean/UnitConjecture/GroupRing.lean create mode 100644 LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean create mode 100644 LeanPool/Polylean/UnitConjecture/Tactics.lean create mode 100644 LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean create mode 100644 LeanPool/Polylean/UnitConjecture/TorsionFree.lean diff --git a/LeanPool.lean b/LeanPool.lean index 39c8ce5387..83fddf9176 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -173,6 +173,18 @@ import LeanPool.LatticeTriangle import LeanPool.LatticeTriangle.Solution import LeanPool.PartialRegularity import LeanPool.PartialRegularity.Extension +import LeanPool.Polylean +import LeanPool.Polylean.UnitConjecture +import LeanPool.Polylean.UnitConjecture.AddFreeGroup +import LeanPool.Polylean.UnitConjecture.Cocycle +import LeanPool.Polylean.UnitConjecture.EnumDecide +import LeanPool.Polylean.UnitConjecture.FreeModule +import LeanPool.Polylean.UnitConjecture.GardamGroup +import LeanPool.Polylean.UnitConjecture.GroupRing +import LeanPool.Polylean.UnitConjecture.MetabelianGroup +import LeanPool.Polylean.UnitConjecture.Tactics +import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets +import LeanPool.Polylean.UnitConjecture.TorsionFree import LeanPool.RamanujanTauMissesPrimes import LeanPool.RamanujanTauMissesPrimes.Solution import LeanPool.RiemannMappingTheorem diff --git a/LeanPool/Polylean.lean b/LeanPool/Polylean.lean new file mode 100644 index 0000000000..8228c431e4 --- /dev/null +++ b/LeanPool/Polylean.lean @@ -0,0 +1,18 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.UnitConjecture + +/-! +# Polylean Unit Conjecture Infrastructure + +Source: url:https://github.com/siddhartha-gadgil/Polylean +Authors: Siddhartha Gadgil, Anand Rao +Status: verified +Main declarations: `LeanPool.Polylean.P.torsionFree` +Tags: algebra, group-theory, ring-theory, unit-conjecture +MSC: 16S34, 20F65 +-/ diff --git a/LeanPool/Polylean/UnitConjecture.lean b/LeanPool/Polylean/UnitConjecture.lean new file mode 100644 index 0000000000..a712357fc4 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.UnitConjecture.TorsionFree +import LeanPool.Polylean.UnitConjecture.GroupRing + +/-! +# Polylean Unit Conjecture infrastructure + +This library contains the verified infrastructure from the Polylean formalization around +Gardam's [disproof](https://arxiv.org/abs/2102.11818) of the Kaplansky Unit Conjecture. + + +## Imported Results + +Gardam proved that for a group `P` (the *Promislow* or *Hantzsche-Wendt* group), we have the +following: + +* `P` is torsion free; this is proved in [`TorsionFree.lean`](UnitConjecture/TorsionFree.html) + +The imported code constructs `P`, constructs group rings, and proves the required algebraic +properties. + +## Constructing the group `P` + +The group `P` is a so called _Metabelian Group_, an extension of an abelian group by an abelian +group. + +* In the file [`GardamGroup.lean`](UnitConjecture/GardamGroup.html), the specific construction of + `P` is given using the general construction of metabelian groups. +* In the file [`MetabelianGroup.lean`](UnitConjecture/MetabelianGroup.html), metabelian groups are + constructed based on appropriate data, and proved to be groups. +* The data for a metabelian group includes a _group action_ and a _cocycle_. These are defined and + their basic properties proved in [`Cocycle.lean`](UnitConjecture/Cocycle.html). + +## Constructing group rings + +A group ring $K[G]$ is the free module on $K$ with basis elements of a group $G$ with a natural +ring structure. + +* Free modules are constructed in [`FreeModule.lean`](UnitConjecture/FreeModule.html) with + properties proved. This crucially includes decidable equality of elements, assuming decidable + equality for $G$ and $R$. +* The Group Ring structure is defined in [`GroupRing.lean`](UnitConjecture/GroupRing.html) and + shown to give a ring. + +## Proofs and Definitions by Computation and Enumeration + +We set things up to use typeclasses to deduce decidable equality, both by finite enumeration and by +checking equality on a basis for finitely generated abelian groups. + +* In [`EnumDecide.lean`](UnitConjecture/EnumDecide.html) we set up the typeclasses for deducing + decidable equality, and prove the basic cases. +* In [`AddFreeGroup.lean`](UnitConjecture/AddFreeGroup.html) we define bases of free abelian groups + via a universal property, show that products of $\mathbb{Z}$ have bases, show that homomorphisms + can be defined by giving functions on a basis, and show that we have decidable equality for + homomorphisms on finitely generated free abelian groups. +-/ diff --git a/LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean b/LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean new file mode 100644 index 0000000000..263cb7adb9 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/AddFreeGroup.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Algebra.Group.Prod +import Mathlib.Data.Int.Cast.Lemmas +import Mathlib.Algebra.Ring.Basic +import LeanPool.Polylean.UnitConjecture.EnumDecide + +namespace LeanPool.Polylean + +/-! + +## Free groups + +The definition of a free group on a basis, along with a few properties. + +Free groups are defined constructively to allow automatic equality checking of +homomorphisms on finitely generated free groups. + +## Overview +- `AddFreeGroup` - the main definition. +- `decideHomsEqual` - the crucial result that allows the + automatic comparison of homomorphisms by checking their values on the basis. +- `ℤFree` - a proof that the additive group of integers is a free group on the one-element type. +- `prodFree` - a proof that the product of free groups is free. +-/ + +/-- Free (Additive) Groups, implemented as a typeclass. + A free additive group with a basis `X` is an additive group `F` with an + inclusion map `ι : X → F`, + such that any map `f : X → A` from the basis to any Abelian group `A` + extends *uniquely* to an *additive group homomorphism* `φ : F →+ A`. -/ +class AddFreeGroup (F : Type _) [AddCommGroup F] (X : Type _) where + /-- The inclusion map from the basis to the free group. -/ + ι : X → F + /-- The homomorphism from the free group induced by a map from the basis. -/ + inducedHom : (A : Type) → [AddCommGroup A] → (X → A) → (F →+ A) + /-- A proof that the induced homomorphism extends the map from the basis. -/ + induced_extends {A : Type} [AddCommGroup A] : ∀ f : X → A, (inducedHom A f) ∘ ι = f + /-- A proof that any homomorphism extending a map from the basis must be unique. -/ + unique_extension {A : Type} [AddCommGroup A] (f g : F →+ A) : f ∘ ι = g ∘ ι → f = g + + +/-- The additive group of integers `ℤ` is the free group on a singleton basis. -/ +instance ℤFree : AddFreeGroup ℤ Unit where + ι := fun _ => 1 + inducedHom := fun A _ f => (zmultiplesHom A).toFun (f ()) + induced_extends := by + intro A _ f + funext u; cases u + simp [one_zsmul] + unique_extension := by + intro A abg f g hyp + let hyp' := congrFun hyp () + dsimp at hyp' + rwa [← zmultiplesHom_symm_apply, ← zmultiplesHom_symm_apply, Equiv.apply_eq_iff_eq] at hyp' + + +open EnumDecide in +/-- Equality of homomorphisms from a free group on an exhaustively searchable basis is decidable. -/ +def decideHomsEqual {F : Type _} [AddCommGroup F] {X : Type _} [DecideForall X] + [fgp : AddFreeGroup F X] + {A : Type _} [AddCommGroup A] [DecidableEq A] : DecidableEq (F →+ A) := fun f g => + if c : ∀ x : X, f (fgp.ι x) = g (fgp.ι x) then by + apply Decidable.isTrue + apply fgp.unique_extension + funext x + exact c x + else by + apply Decidable.isFalse + intro contra + let c' : ∀ (x : X), f (fgp.ι x) = g (fgp.ι x) := by + intro; apply congrFun (congrArg _ contra) + contradiction + +namespace AddFreeGroup.Product + +variable {A B : Type _} [AddCommGroup A] [AddCommGroup B] +variable {X_A X_B : Type _} +variable [FAb_A : AddFreeGroup A X_A] [FAb_B : AddFreeGroup B X_B] + +/-- The inclusion map from the direct sum of the bases of two free groups into their product. -/ +def ι : (X_A ⊕ X_B) → A × B + | Sum.inl x_a => (FAb_A.ι x_a, 0) + | Sum.inr x_b => (0, FAb_B.ι x_b) + +/-- The group homomorphism from the product of two free groups induced by a map from the basis. -/ +def inducedProdHom (G : Type _) [AddCommGroup G] (f : X_A ⊕ X_B → G) : A × B →+ G := + let f_A : X_A → G := f ∘ Sum.inl + let f_B : X_B → G := f ∘ Sum.inr + AddMonoidHom.coprod + (FAb_A.inducedHom G f_A) + (FAb_B.inducedHom G f_B) + +/-- The product of free groups is free. -/ +instance prodFree : AddFreeGroup (A × B) (X_A ⊕ X_B) := + { + ι := ι + inducedHom := inducedProdHom + induced_extends := by + intro _ _ f + funext x + cases x with + | inl x => + unfold inducedProdHom ι + dsimp + rw [map_zero, add_zero] + exact congrFun (FAb_A.induced_extends (f ∘ Sum.inl)) x + | inr x => + unfold inducedProdHom ι + dsimp + rw [map_zero, zero_add] + exact congrFun (FAb_B.induced_extends (f ∘ Sum.inr)) x + unique_extension := by + intro _ _ f g hyp + ext ⟨a, b⟩ + rw [show (a, b) = (a, 0) + (0, b) by simp, map_add, map_add] + have A_unique : f.comp (.inl A B) = g.comp (.inl A B) := by + apply FAb_A.unique_extension; funext x_A; apply congrFun hyp (Sum.inl x_A) + have B_unique : f.comp (.inr A B) = g.comp (.inr A B) := by + apply FAb_B.unique_extension; funext x_B; apply congrFun hyp (Sum.inr x_B) + change f.comp (.inl _ _) a + f.comp (.inr _ _) b = + g.comp (.inl _ _) a + g.comp (.inr _ _) b + rw [A_unique, B_unique] + } + +end AddFreeGroup.Product + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/Cocycle.lean b/LeanPool/Polylean/UnitConjecture/Cocycle.lean new file mode 100644 index 0000000000..4efcc75313 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/Cocycle.lean @@ -0,0 +1,150 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Tactic +import Mathlib.Algebra.Group.Action.Defs +import Mathlib.Algebra.Group.Hom.Defs +import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets + +namespace LeanPool.Polylean + +/-! +## Cocycles and Group actions by automorphisms +The definitions of cocycles and group actions by automorphisms, which are required for the +Metabelian construction. + +## Overview +- `AutAction` - the definition of an action of one group on another by automorphisms. + This is done as a typeclass representing the property of being an action by automorphisms. +- `Cocycle` - the definition of a *cocycle* associated with a certain action by + automorphisms. This is also done as a typeclass with the function as an explicit + argument and the action as a field of the structure. +-/ + +/-! +### Actions by automorphisms +-/ + +/-- An action of an additive group on another additive group by automorphisms. + There is a closely related typeclass `DistribMulAction` in `Mathlib` that uses + multiplicative notation. -/ +class AutAction {A B : Type _} [AddGroup A] [AddGroup B] (α : A → (B →+ B)) where + /-- The automorphism corresponding to the zero element is the identity. -/ + id_action : α 0 = .id _ + /-- The compatibility of group addition with the action by automorphisms. -/ + compatibility : ∀ a a' : A, α (a + a') = (α a).comp (α a') + + +namespace AutAction + +attribute [aesop norm (rule_sets := [AutAction])] id_action compatibility + +variable {A B : Type _} [AddGroup A] [AddGroup B] (α : A → (B →+ B)) [AutAction α] + +/-! +Some easy consequences of the definition of an action by automorphisms. +-/ + +omit [AddGroup A] [AutAction α] in +@[aesop norm (rule_sets := [AutAction])] +lemma apply_zero : ∀ {a : A}, α a (0 : B) = (0 : B) := by + intro a + exact map_zero (α a) + +@[aesop norm (rule_sets := [AutAction])] +lemma zero_apply : ∀ {b : B}, α (0 : A) b = b := by + intro b + have h := congrArg (fun f : B →+ B => f b) (AutAction.id_action (α := α)) + simpa using h + +omit [AddGroup A] [AutAction α] in +@[aesop norm (rule_sets := [AutAction])] +lemma apply_add : ∀ {a : A} {b b' : B}, α a (b + b') = α a b + α a b' := by + intro a b b' + exact map_add (α a) b b' + +@[aesop safe (rule_sets := [AutAction])] +lemma compatibility' : ∀ {a a' : A} {b : B}, α a (α a' b) = α (a + a') b := by + intro a a' b + have h := congrArg (fun f : B →+ B => f b) (AutAction.compatibility (α := α) a a') + simpa [AddMonoidHom.comp_apply] using h.symm + +@[aesop norm (rule_sets := [AutAction])] +lemma act_neg_act {a : A} {b : B} : α a (α (-a) b) = b := by + rw [compatibility'] + aesop (erase compatibility) (rule_sets := [AutAction]) + +omit [AddGroup A] [AutAction α] in +@[aesop safe (rule_sets := [AutAction])] +lemma apply_neg : ∀ {a : A} {b : B}, α a (-b) = -α a b := by + intro a b + exact map_neg (α a) b + +end AutAction + + +/-! +### Cocycles +-/ + +/-- +A cocycle associated with a certain action of `Q` on `K` via automorphisms is a +function from `Q × Q` to `K` satisfying a certain requirement known as the "cocycle condition". -/ +class Cocycle {Q K : Type _} [AddGroup Q] [AddGroup K] (c : Q → Q → K) where + /-- An action of the quotient on the kernel by automorphisms. -/ + α : Q → (K →+ K) + /-- A typeclass instance for the action by automorphisms. -/ + autAct : AutAction α + /-- The value of the cocycle is zero when its inputs are zero, as a convention. -/ + cocycle_zero : c 0 0 = (0 : K) + /-- The *cocycle condition*. -/ + cocycle_condition : + ∀ q q' q'' : Q, c q q' + c (q + q') q'' = α q (c q' q'') + c q (q' + q'') + + +namespace Cocycle + +/-! +A few deductions from the cocycle condition. +-/ + +variable {Q K : Type _} [AddGroup Q] [AddGroup K] +variable (c : Q → Q → K) [ccl : Cocycle c] + +attribute [aesop norm (rule_sets := [Cocycle])] Cocycle.cocycle_zero +attribute [aesop norm (rule_sets := [Cocycle])] Cocycle.cocycle_condition + +instance : AutAction ccl.α := ccl.autAct + +@[aesop norm (rule_sets := [Cocycle])] +lemma left_id {q : Q} : c 0 q = (0 : K) := by + have := ccl.cocycle_condition 0 0 q + simp only [ccl.cocycle_zero, AutAction.id_action, zero_add, add_zero, + AddMonoidHom.id_apply] at this + exact (add_left_cancel (a := c 0 q) + (show c 0 q + 0 = c 0 q + c 0 q by simpa only [add_zero] using this)).symm + + +@[aesop norm (rule_sets := [Cocycle])] +lemma right_id {q : Q} : c q 0 = (0 : K) := by + have := ccl.cocycle_condition q 0 0 + simp only [ccl.cocycle_zero, AutAction.apply_zero, zero_add, add_zero] at this + exact add_left_cancel (a := c q 0) + (show c q 0 + c q 0 = c q 0 + 0 by simpa only [add_zero] using this) + +@[aesop safe (rule_sets := [Cocycle])] +lemma inv_rel (q : Q) : c q (-q) = ccl.α q (c (-q) q) := by + have := ccl.cocycle_condition q (-q) q + simpa [left_id, right_id] using this + +@[aesop safe (rule_sets := [Cocycle])] +lemma inv_rel' (q : Q) : c (-q) q = ccl.α (-q) (c q (-q)) := by + have := inv_rel c (-q) + simp_all only [neg_neg] + +end Cocycle + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/EnumDecide.lean b/LeanPool/Polylean/UnitConjecture/EnumDecide.lean new file mode 100644 index 0000000000..b48f4fbafd --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/EnumDecide.lean @@ -0,0 +1,267 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +namespace LeanPool.Polylean + +/-! +## Decision by enumeration + +For a type `X` that is finite (or more generally, *compact*), it is possible to +automatically decide any statement of the form `∀ x : X, P x` by enumeration +when `P` is a decidable predicate on `X` +(i.e., a predicate for the individual propositions `P x` are decidable for any given `x : X`). + +## Overview + +The `EnumDecide.decideForall` typeclass defines the property of a type being exhaustively checkable. + +Results in this file include +- `EnumDecide.decideFin` - the type `Fin n` (the canonical finite set with + `n` elements) is checkable for any `n : ℕ`. +- `EnumDecide.decideUnit` - the single-element type is exhaustively checkable. +- `EnumDecide.decideProd`, `EnumDecide.decideSum` - the product and direct sum + of two exhaustively checkable types. +- `EnumDecide.funEnum` - the type of functions from an exhaustively checkable + type to a type with decidable equality is exhaustively checkable. +-/ + +namespace EnumDecide + +/-- +It is possible to check whether a given decidable predicate holds for all natural +numbers below a given bound. +-/ +def decideBelow (p : Nat → Prop) [DecidablePred p] (bound : Nat) : + Decidable (∀ n : Nat, n < bound → p n) := + match bound with + | 0 => by + apply Decidable.isTrue + intro n bd + contradiction + | k + 1 => + let prev := decideBelow p k + match prev with + | Decidable.isTrue hyp => + if c: p k then + by + apply Decidable.isTrue + intro n bd + cases Nat.eq_or_lt_of_le bd with + | inl eql => + have eql' : n = k := by + injection eql + simp [eql'] + assumption + | inr lt => + have lt' : n < k := by + apply Nat.le_of_succ_le_succ + assumption + exact hyp n lt' + else + by + apply Decidable.isFalse + intro contra + have lem : p k := by + apply contra k + apply Nat.le_refl + contradiction + | Decidable.isFalse hyp => by + apply Decidable.isFalse + intro contra + have lem : ∀ (n : Nat), n < k → p n := by + intro n bd + have bd' : n < k + 1 := by + apply Nat.le_succ_of_le + exact bd + exact contra n bd' + contradiction + +/-- +It is possible to check whether a decidable predicate on `Fin m` holds below a +given natural-number bound. +-/ +def decideBelowFin {m : Nat} (p : Fin m → Prop) [DecidablePred p] (bound : Nat) : + Decidable (∀ n : Fin m, n < bound → p n) := + match bound with + | 0 => by + apply Decidable.isTrue + intro n bd + contradiction + | k + 1 => + let prev := decideBelowFin p k + match prev with + | Decidable.isTrue hyp => + if ineq : k < m then + if c: p ⟨k, ineq⟩ then + by + apply Decidable.isTrue + intro n bd + cases Nat.eq_or_lt_of_le bd with + | inl eql => + have eql' : n = ⟨k, ineq⟩ := by + apply Fin.eq_of_val_eq + injection eql + simp [eql'] + assumption + | inr lt => + have lt' : n < k := by + apply Nat.le_of_succ_le_succ + assumption + exact hyp n lt' + else + by + apply Decidable.isFalse + intro contra + have lem : p ⟨k, ineq⟩ := by + apply contra ⟨k, ineq⟩ + apply Nat.le_refl + contradiction + else + by + apply Decidable.isTrue + intro ⟨n, nbd⟩ _ + have ineq' : m ≤ k := by + apply Nat.le_of_succ_le_succ + apply Nat.gt_of_not_le ineq + have ineq'' := Nat.le_trans nbd ineq' + exact hyp ⟨n, nbd⟩ ineq'' + | Decidable.isFalse hyp => by + apply Decidable.isFalse + intro contra + have lem : ∀ (n : Fin m), n < k → p n := by + intro n bd + have bd' : n < k + 1 := by + apply Nat.le_succ_of_le + exact bd + exact contra n bd' + contradiction + +/-- It is possible to decide whether a predicate holds for all elements of `Fin n`. -/ +def decideFin {m : Nat} (p : Fin m → Prop) [DecidablePred p] : + Decidable (∀ n : Fin m, p n) := + match decideBelowFin p m with + | Decidable.isTrue hyp => + by + apply Decidable.isTrue + intro ⟨n, ineq⟩ + exact hyp ⟨n, ineq⟩ ineq + | Decidable.isFalse hyp => by + apply Decidable.isFalse + intro contra + apply hyp + intro ⟨n, ineq⟩ _ + exact contra ⟨n, ineq⟩ + +/-- +A typeclass for "exhaustively verifiable types", i.e., types for which it is +possible to decide whether a given (decidable) predicate holds for all its +elements. +-/ +class DecideForall (α : Type _) where + /-- Decide whether a decidable predicate holds for all elements. -/ + decideForall (p : α → Prop) [DecidablePred p]: + Decidable (∀ x : α, p x) + +instance {k : Nat} : DecideForall (Fin k) := + ⟨by apply decideFin⟩ + +instance {α : Type _} [dfa : DecideForall α] {p : α → Prop} [DecidablePred p] : + Decidable (∀ x : α, p x) := + dfa.decideForall p + +example : ∀ x : Fin 3, x + 0 = x := by decide + +example : ∀ x y : Fin 3, x + y = y + x := by decide + +example : ∀ x y z : Fin 3, (x + y) + z = x + (y + z) := by decide + +@[reducible, instance] +def decideProd {α β : Type _} [dfa : DecideForall α] [dfb : DecideForall β] + (p : α × β → Prop) [DecidablePred p] : Decidable (∀ xy : α × β, p xy) := + if c: (∀ x: α, ∀ y : β, p (x, y)) + then + by + apply Decidable.isTrue + intro (x, y) + exact c x y + else + by + apply Decidable.isFalse + intro contra + apply c + intro x y + exact contra (x, y) + +instance {α β : Type _} [dfa : DecideForall α] [dfb : DecideForall β] : + DecideForall (α × β) := + ⟨by apply decideProd⟩ + +@[reducible, instance] +def decideUnit (p : Unit → Prop) [DecidablePred p] : Decidable (∀ x : Unit, p x) := + if c : p (()) then by + apply Decidable.isTrue + intro x + have l : x = () := by rfl + rw [l] + exact c + else by + apply Decidable.isFalse + intro contra + apply c + exact contra () + +instance : DecideForall Unit := + ⟨by apply decideUnit⟩ + +@[reducible, instance] +def decideSum {α β : Type _} [dfa : DecideForall α] [dfb : DecideForall β] + (p : α ⊕ β → Prop) [DecidablePred p] : Decidable (∀ x : α ⊕ β, p x) := + if c: ∀x: α, p (Sum.inl x) then + if c': ∀y: β , p (Sum.inr y) then + by + apply Decidable.isTrue + intro x + cases x with + | inl a => exact c a + | inr a => exact c' a + else by + apply Decidable.isFalse + intro contra + apply c' + intro x + exact contra (Sum.inr x) + else by + apply Decidable.isFalse + intro contra + apply c + intro x + exact contra (Sum.inl x) + +instance {α β : Type _} [dfa : DecideForall α] [dfb : DecideForall β] : + DecideForall (α ⊕ β) := + ⟨by apply decideSum⟩ + +instance funEnum {α β : Type _} [dfa : DecideForall α] [dfb : DecidableEq β] : + DecidableEq (α → β) := fun f g => + if c: ∀ x: α, f x = g x then + by + apply Decidable.isTrue + apply funext + intro x + exact c x + else + by + apply Decidable.isFalse + intro contra + apply c + intro x + exact congrFun contra x + + +example : ∀ xy : (Fin 3) × (Fin 2), + xy.1.val + xy.2.val = xy.2.val + xy.1.val := by decide +end EnumDecide +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/FreeModule.lean b/LeanPool/Polylean/UnitConjecture/FreeModule.lean new file mode 100644 index 0000000000..889a9766ae --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/FreeModule.lean @@ -0,0 +1,1392 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Algebra.Ring.Basic +import Mathlib.Algebra.Group.Defs + +namespace LeanPool.Polylean + +/-! +# Free modules + +We construct the free module over a ring `R` generated by a set `X`. It is assumed that both +`R` and `X` have decidable equality. This is to obtain decidable equality for the elements of +the module, which we do (`FreeModule.decEq`). +We choose our definition to allow both such computations and to prove results. + +The definition is as a quotient of *Formal Sums* (`FormalSum`), +which are simply lists of pairs `(a, x)` where `a` is a coefficient in `R` and `x` is a term in `X`. +We associate to such a formal sum a coordinate function `X → R` (`FormalSum.coords`). +We see that having the same coordinate functions gives an equivalence relation on the formal sums. +The free module (`FreeModule`) is then defined as the corresponding quotient of such formal sums. + +We also give an alternative description via moves, which is more convenient for universal +properties. +-/ + +variable {R : Type _} [Ring R] [DecidableEq R] + +variable {X : Type _} [DecidableEq X] + +/-! + +## Formal sums +-/ + + + +/-- A *formal sum* represents an `R`-linear combination of finitely many elements of `X`. + This is implemented as a list `R × X`, which associates to each element `X` of the list a + coefficient from `R`. -/ +abbrev FormalSum (R X : Type _) [Ring R] := + let _ringR : Ring R := inferInstance + List (R × X) + +/-! +## Coordinate functions and Supports + +* We define coordinate functions X → R for formal sums. +* We define (weak) support, relate non-zero coordinates. +* We prove decidable equality on a list (easy fact). + +-/ + +/-! +### Coordinate functions + +The definition of coordinate functions is in two steps. We first define the coordinate for a pair +`(a, x)`, and then define the coordinate function for a formal sum by summing over such terms. + +-/ + +/-- Coordinates for a formal sum with one term. -/ +def monomCoeff (R X : Type _) [Ring R] [DecidableEq X] (x₀ : X) (nx : R × X) : R := + match (nx.2 == x₀) with + | true => nx.1 + | false => 0 + +omit [DecidableEq R] in +/-- Homomorphism property for coordinates for a formal sum with one term. -/ +theorem monom_coords_hom (x₀ x : X) (a b : R) : + monomCoeff R X x₀ (a + b, x) = + monomCoeff R X x₀ (a, x) + monomCoeff R X x₀ (b, x) := by + repeat + ( + rw [monomCoeff]) + cases x == x₀ <;> simp + +omit [DecidableEq R] in +/-- Associativity of scalar multiplication coordinates for a formal sum with one term. -/ +theorem monom_coords_mul (x₀ : X) (a b : R) : + monomCoeff R X x₀ (a * b, x) = a * monomCoeff R X x₀ (b, x) := by + repeat + ( + rw [monomCoeff]) + cases x == x₀ <;> simp + +omit [DecidableEq R] in +/-- Coordinates for a formal sum with one term with scalar `0`. +-/ +theorem monom_coords_at_zero (x₀ x : X) : monomCoeff R X x₀ (0, x) = 0 := by + rw [monomCoeff] + cases x == x₀ <;> rfl + +/-- The coordinates for a formal sum. -/ +def _root_.LeanPool.Polylean.FormalSum.coords : FormalSum R X → X → R + | [], _ => 0 + | h :: t, x₀ => monomCoeff R X x₀ h + coords t x₀ + +/-! + +### Support of a formal sum + +We next define the support of a formal sum and prove the property that coordinates vanish outside +the support. +-/ + +/-- Support for a formal sum in a weak sense (coordinates may vanish on this). -/ +def _root_.LeanPool.Polylean.FormalSum.support (s : FormalSum R X) : List X := + s.map <| fun (_, x) => x + +open FormalSum + +omit [DecidableEq R] in +/-- Support contains elements `x : X` where the coordinate is not `0`. -/ +theorem nonzero_coord_in_support (s : FormalSum R X) : + ∀ x : X, 0 ≠ s.coords x → x ∈ s.support := + match s with + | [] => fun x hyp => by + have d : coords [] x = (0 : R) := by + rfl + rw [d] at hyp + contradiction + | h :: t => by + intro x hyp + let (a₀, x₀) := h + have d : support ((a₀, x₀) :: t) = x₀ :: (support t) := by + rfl + rw [d] + match p : x₀ == x with + | true => + have eqn : x₀ = x := of_decide_eq_true p + rw [eqn] + apply List.mem_of_elem_eq_true + simp only [List.elem, BEq.rfl] + | false => + rw [coords, monomCoeff, p, zero_add] at hyp + let step := nonzero_coord_in_support t x hyp + apply List.mem_of_elem_eq_true + simp only [List.elem, List.elem_eq_contains, List.contains_eq_mem] + have p' : (x == x₀) = false := by + have eqn := of_decide_eq_false p + have eqn' : ¬(x = x₀) := by + intro contra + let contra' := Eq.symm contra + contradiction + exact decide_eq_false eqn' + rw [p'] + simp only [decide_eq_true_eq] + exact step + +/-! +### Equality of coordinates on a list + +We define equality of coordinates on a list and prove that it is decidable and implied by equality +of formal sums. +-/ + +/-- The condition of being equal on all elements is a given list -/ +def equalOnList (l : List X) (f g : X → R) : Prop := + match l with + | [] => true + | h :: t => (f h = g h) ∧ (equalOnList t f g) + +omit [Ring R] [DecidableEq R] [DecidableEq X] in +/-- Equal functions are equal on arbitrary supports. -/ +theorem equalOnList_of_equal (l : List X) (f g : X → R) : + f = g → equalOnList l f g := by + intro hyp + induction l with + | nil => + rw [equalOnList] + | cons h t step => + rw [equalOnList] + constructor + · rw [hyp] + · exact step + +omit [Ring R] [DecidableEq R] [DecidableEq X] in +/-- Functions equal on support `l` are equal on each `x ∈ l`. -/ +theorem eq_mem_of_equalOnList (l : List X) (f g : X → R) (x : X) (mhyp : x ∈ l) : + equalOnList l f g → f x = g x := + match l with + | [] => by + contradiction + | h :: t => by + intro hyp + simp only [equalOnList] at hyp + cases mhyp + · exact hyp.left + · have inTail : x ∈ t := by + assumption + have step := eq_mem_of_equalOnList t f g x inTail hyp.right + exact step + +/-- Decidability of equality on list. -/ +@[reducible, instance] def decidableEqualOnList (l : List X) (f g : X → R) : + Decidable (equalOnList l f g) := + match l with + | [] => + Decidable.isTrue + (by + simp only [equalOnList]) + | h :: t => by + simp only [equalOnList] + cases (decidableEqualOnList t f g) with + | isTrue hs => + exact + (if c : f h = g h then (Decidable.isTrue ⟨c, hs⟩) + else by + apply Decidable.isFalse + intro contra + have contra' := contra.left + contradiction) + | isFalse hs => + apply Decidable.isFalse + intro contra + have contra' := contra.right + contradiction + + +/-! +## Quotient Free Module + + +* We define relation by having equal coordinates +* We show this is an equivalence relation and define the quotient +-/ +/-- Relation by equal coordinates. -/ +def eqlCoords (R X : Type) [Ring R] [DecidableEq X] (s₁ s₂ : FormalSum R X) : Prop := + s₁.coords = s₂.coords + +namespace eqlCoords + +omit [DecidableEq R] in +/-- Relation by equal coordinates is reflexive. -/ +theorem refl (s : FormalSum R X) : eqlCoords R X s s := + by + rfl + +omit [DecidableEq R] in +/-- Relation by equal coordinates is symmetric. -/ +theorem symm {s₁ s₂ : FormalSum R X} : eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₁ := by + intro hyp + apply funext + intro x + apply Eq.symm + exact congrFun hyp x + +omit [DecidableEq R] in +/-- Relation by equal coordinates is transitive. -/ +theorem trans {s₁ s₂ s₃ : FormalSum R X} : + eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₃ → eqlCoords R X s₁ s₃ := by + intro hyp₁ hyp₂ + apply funext + intro x + have l₁ := congrFun hyp₁ x + have l₂ := congrFun hyp₂ x + exact Eq.trans l₁ l₂ + +omit [DecidableEq R] in +/-- Relation by equal coordinates is an equivalence relation. -/ +theorem is_equivalence : Equivalence (eqlCoords R X) := + { refl := refl, symm := symm, trans := trans } + +end eqlCoords + +/-- Setoid based on equal coordinates. -/ +instance formalSumSetoid (R X : Type) [Ring R] [DecidableEq X] [DecidableEq R] : + Setoid (FormalSum R X) := + let _decidableEqR : DecidableEq R := inferInstance + ⟨eqlCoords R X, eqlCoords.is_equivalence⟩ + +/-- Quotient free module. -/ +abbrev FreeModule (R X : Type) [Ring R] [DecidableEq X] [DecidableEq R] := + Quotient (formalSumSetoid R X) + +/-- Notation for the quotient free module over `R` generated by `G`. -/ +notation R"["G"]" => FreeModule R G + +/-! +## Decidable equality on quotient free modules + +We show that the free module `F[X]` has decidable equality. This has two steps: + +* show decidable equality for images of formal sums. +* lift to quotient (by relating to formal sums). + +We also show that the coordinate functions are defined on the quotient. -/ + + + +namespace FreeModule + +/-- Decidable equality for quotient elements in the free module -/ +@[reducible, instance] +def decideEqualQuotient (s₁ s₂ : FormalSum R X) : + Decidable (@Eq (R[X]) ⟦s₁⟧ ⟦s₂⟧) := + if ch₁ : equalOnList s₁.support s₁.coords s₂.coords then + if ch₂ : equalOnList s₂.support s₁.coords s₂.coords then + Decidable.isTrue + (by + apply Quotient.sound + apply funext + intro x + exact + if h₁ : (0 = s₁.coords x) then + if h₂ : (0 = s₂.coords x) then by + rw [← h₁, h₂] + else by + have lem : x ∈ s₂.support := by + apply nonzero_coord_in_support + assumption + let lem' := eq_mem_of_equalOnList s₂.support s₁.coords s₂.coords x lem ch₂ + exact lem' + else by + have lem : x ∈ s₁.support := by + apply nonzero_coord_in_support + assumption + let lem' := eq_mem_of_equalOnList s₁.support s₁.coords s₂.coords x lem ch₁ + exact lem') + else + Decidable.isFalse + (by + intro contra + let lem := + equalOnList_of_equal s₂.support s₁.coords s₂.coords (Quotient.exact contra) + contradiction) + else + Decidable.isFalse + (by + intro contra + let lem := + equalOnList_of_equal s₁.support s₁.coords s₂.coords (Quotient.exact contra) + contradiction) + +/-! +### Lift to quotient +-/ + +/-- Boolean equality on support. -/ +def beqOnSupport (l : List X) (f g : X → R) : Bool := + l.all <| fun x => decide (f x = g x) + +omit [Ring R] [DecidableEq X] in +/-- Equality on support from boolean equality. -/ +theorem eql_on_support_of_true {l : List X} {f g : X → R} : + beqOnSupport l f g = true → equalOnList l f g := by + intro hyp + induction l with + | nil => + simp only [equalOnList] + | cons h t step => + simp only [equalOnList] + simp only [beqOnSupport, List.all, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true] at hyp + simp only [beqOnSupport, List.all_eq_true, decide_eq_true_eq] at step + let p₂ := step hyp.right + exact And.intro hyp.left p₂ + +/-- Boolean equality on support gives equal quotients. -/ +theorem eqlquot_of_beq_support (s₁ s₂ : FormalSum R X) + (c₁ : beqOnSupport s₁.support s₁.coords s₂.coords) + (c₂ : beqOnSupport s₂.support s₁.coords s₂.coords) : @Eq (R[X]) ⟦s₁⟧ ⟦s₂⟧ := + by + let ch₁ := eql_on_support_of_true c₁ + let ch₂ := eql_on_support_of_true c₂ + apply Quotient.sound + apply funext + intro x + exact + if h₁ : (0 = s₁.coords x) then + if h₂ : (0 = s₂.coords x) then by + rw [← h₁, h₂] + else by + have lem : x ∈ s₂.support := by + apply nonzero_coord_in_support + assumption + let lem' := eq_mem_of_equalOnList s₂.support s₁.coords s₂.coords x lem ch₂ + exact lem' + else by + have lem : x ∈ s₁.support := by + apply nonzero_coord_in_support + assumption + let lem' := eq_mem_of_equalOnList s₁.support s₁.coords s₂.coords x lem ch₁ + exact lem' + + +/-- +Boolean equality for the quotient via lifting +-/ +def beq_quot : (x₁ x₂ : R[X]) → Bool := by + apply Quotient.lift₂ + (fun (s₁ s₂ : FormalSum R X) => decide (@Eq (R[X]) ⟦s₁⟧ ⟦s₂⟧)) + intro a₁ b₁ a₂ b₂ eqv₁ eqv₂ + let eq₁ : Eq (α := R[X]) ⟦a₁⟧ ⟦a₂⟧ := Quot.sound eqv₁ + let eq₂ : Eq (α := R[X]) ⟦b₁⟧ ⟦b₂⟧ := Quot.sound eqv₂ + conv => lhs; congr; rw [eq₁, eq₂] + +/-- +Boolean equality for the quotient is equality. +-/ +lemma eq_of_beq_true : ∀ x₁ x₂ : R[X], x₁.beq_quot x₂ = true → x₁ = x₂ := by + apply Quotient.ind₂ + (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = true → x₁ = x₂) + intro s₁ s₂ eqv + let eql := of_decide_eq_true eqv + assumption + +/-- +Boolean inequality for the quotient is inequality. +-/ +lemma neq_of_beq_false : + ∀ x₁ x₂ : R[X], x₁.beq_quot x₂ = false → Not (x₁ = x₂) := by + apply Quotient.ind₂ + (motive := fun (x₁ x₂ : R[X]) => x₁.beq_quot x₂ = false → Not (x₁ = x₂)) + intro s₁ s₂ neqv + let neql := of_decide_eq_false neqv + assumption + +/-- +Decidable equality for the free module. +-/ +@[reducible, instance] def decEq (x₁ x₂ : R[X]) : Decidable (x₁ = x₂) := by + match p : x₁.beq_quot x₂ with + | true => + apply Decidable.isTrue + apply FreeModule.eq_of_beq_true + assumption + | false => + apply Decidable.isFalse + apply FreeModule.neq_of_beq_false + assumption + +/-! +### Induced coordinates on the quotient. +-/ + +/-- Coordinates are well defined on the quotient. -/ +theorem equal_coords_of_approx (s₁ s₂ : FormalSum R X) : + s₁ ≈ s₂ → s₁.coords = s₂.coords := by + intro hyp + apply funext; intro x₀ + exact congrFun hyp x₀ + +/-- coordinates for the quotient -/ +def coordinates (x₀ : X) : R[X] → R := by + apply Quotient.lift (fun s : FormalSum R X => s.coords x₀) + intro a b hyp + let l := equal_coords_of_approx _ _ hyp + exact congrFun l x₀ + +end FreeModule + +/-! +## Module structure + +We define the module structure on the quotient of the free module by the equivalence relation. + +* We define scalar multiplication and addition on formal sums. +* We show that we have induced operations on the quotient. +* We show that the induced operations give a module structure on the quotient. +-/ +open FormalSum +namespace FormalSum +/-! +### Scalar multiplication: on formal sums and on the quotient. +-/ + +/-- Scalar multiplication on formal sums. -/ +def scmul : R → FormalSum R X → FormalSum R X + | _, [] => [] + | r, (h :: t) => + let (a₀, x₀) := h + (r * a₀, x₀) :: (scmul r t) + +omit [DecidableEq R] in +/-- Coordinates after scalar multiplication. -/ +theorem scmul_coords (r : R) (s : FormalSum R X) (x₀ : X) : + (r * s.coords x₀) = (s.scmul r).coords x₀ := by + induction s with + | nil => + simp only [coords, mul_zero, scmul] + | cons h t ih => + simp only [coords, left_distrib, ih, scmul, monom_coords_mul] + +/-- Scalar multiplication on the Free Module. -/ +def _root_.LeanPool.Polylean.FreeModule.scmul : R → R[X] → R[X] := by + intro r + let f : FormalSum R X → R[X] := fun s => ⟦s.scmul r⟧ + apply Quotient.lift f + intro s₁ s₂ + simp only [f] + intro hypeq + apply Quotient.sound + apply funext + intro x₀ + have l₁ := scmul_coords r s₁ x₀ + have l₂ := scmul_coords r s₂ x₀ + rw [← l₁, ← l₂] + rw [hypeq] + +/-! +### Addition: on formal sums and on the quotient. +-/ + +omit [DecidableEq R] in +/-- Coordinates add when appending. -/ +theorem append_coords (s₁ s₂ : FormalSum R X) (x₀ : X) : + (s₁.coords x₀) + (s₂.coords x₀) = (s₁ ++ s₂).coords x₀ := by + induction s₁ with + | nil => + simp only [coords, zero_add, List.nil_append] + | cons h t ih => + simp only [coords, add_assoc, List.cons_append, ← ih] + +/-- Coordinates well-defined up to equivalence. -/ +theorem append_equiv (s₁ s₂ t₁ t₂ : FormalSum R X) : + (s₁ ≈ s₂) → (t₁ ≈ t₂) → s₁ ++ t₁ ≈ s₂ ++ t₂ := by + intro eqv₁ eqv₂ + apply funext + intro x₀ + rw [← append_coords] + rw [← append_coords] + have ls : coords s₁ x₀ = coords s₂ x₀ := by + apply congrFun eqv₁ + have lt : coords t₁ x₀ = coords t₂ x₀ := by + apply congrFun eqv₂ + rw [← ls, ← lt] + +end FormalSum + +/-- Addition of elements in the free module. -/ +def _root_.LeanPool.Polylean.FreeModule.add : R[X] → R[X] → R[X] := by + let f : FormalSum R X → FormalSum R X → R[X] := fun s₁ s₂ => ⟦s₁ ++ s₂⟧ + apply Quotient.lift₂ f + intro a₁ b₁ a₂ b₂ + simp only [f] + intro eq₁ eq₂ + apply Quotient.sound + apply funext + intro x₀ + have l₁ := append_coords a₁ b₁ x₀ + have l₂ := append_coords a₂ b₂ x₀ + rw [← l₁, ← l₂] + rw [eq₁, eq₂] + +instance : Add (R[X]) := + ⟨FreeModule.add⟩ + +instance : HSMul R (R[X]) (R[X]) := + ⟨FreeModule.scmul⟩ +namespace FormalSum + +/-! +### Properties of operations on formal sums. +-/ + +omit [DecidableEq R] [DecidableEq X] in +/-- Associativity for scalar multiplication for formal sums. -/ +theorem action (a b : R) (s : FormalSum R X) : (s.scmul b).scmul a = s.scmul (a * b) := by + induction s with + | nil => + simp only [scmul] + | cons h t ih => + simp only [scmul, ih, mul_assoc] + +/-- Distributivity for the module operations. -/ +theorem act_sum (a b : R) (s : FormalSum R X) : (s.scmul a) ++ (s.scmul b) ≈ s.scmul (a + b) := by + induction s with + | nil => + simp only [scmul, List.append_nil] + apply eqlCoords.refl + | cons h t ih => + apply funext; intro x₀ + let il₁ := congrFun ih x₀ + rw [← append_coords] + simp only [scmul, coords, right_distrib, monom_coords_hom] + rw [← append_coords] at il₁ + rw [← il₁] + conv => + lhs + rw [add_assoc] + arg 2 + rw [← add_assoc] + arg 1 + rw [add_comm] + conv => + lhs + rw [add_assoc] + rw [← add_assoc] + + +end FormalSum + +namespace FreeModule + +/-! +### Module properties for the free module. +-/ + +/-- Associativity for scalar and ring products. -/ +theorem module_action (a b : R) (x : R[X]) : a • (b • x) = (a * b) • x := by + apply @Quotient.ind (motive := fun x : R[X] => a • (b • x) = (a * b) • x) + intro s + apply Quotient.sound + rw [FormalSum.action] + apply eqlCoords.refl + +/-- Commutativity of addition. -/ +theorem addn_comm (x₁ x₂ : R[X]) : x₁ + x₂ = x₂ + x₁ := by + apply @Quotient.ind₂ (motive := fun x₁ x₂ : R[X] => x₁ + x₂ = x₂ + x₁) + intro s₁ s₂ + apply Quotient.sound + apply funext + intro x₀ + let lm₁ := append_coords s₁ s₂ x₀ + let lm₂ := append_coords s₂ s₁ x₀ + rw [← lm₁, ← lm₂] + simp only [add_comm] + +theorem add_assoc_aux (s₁ : FormalSum R X) (x₂ x₃ : R[X]) : + (⟦s₁⟧ + x₂) + x₃ = ⟦s₁⟧ + (x₂ + x₃) := by + apply @Quotient.ind₂ + (motive := fun x₂ x₃ : R[X] => (⟦s₁⟧ + x₂) + x₃ = ⟦s₁⟧ + (x₂ + x₃)) + intro x₂ x₃ + apply Quotient.sound + apply funext + intro x₀ + rw [← append_coords] + rw [← append_coords] + rw [← append_coords] + rw [← append_coords] + simp only [add_assoc] + +/-- Associativity of addition. -/ +theorem addn_assoc (x₁ x₂ x₃ : R[X]) : (x₁ + x₂) + x₃ = x₁ + (x₂ + x₃) := by + apply @Quotient.ind (motive := fun x₁ : R[X] => (x₁ + x₂) + x₃ = x₁ + (x₂ + x₃)) + intro x₁ + apply add_assoc_aux + +/-- The zero element of the free module. -/ +def zero : R[X] := ⟦[]⟧ + +/-- adding zero -/ +theorem addn_zero (x : R[X]) : x + zero = x := by + apply @Quotient.ind (motive := fun x : R[X] => x + zero = x) + intro x + apply Quotient.sound + apply funext + intro x₀ + rw [← append_coords] + simp only [coords, add_zero] + +/-- adding zero -/ +theorem zero_addn (x : R[X]) : zero + x = x := by + apply @Quotient.ind (motive := fun x : R[X] => zero + x = x) + intro x + apply Quotient.sound + apply funext + intro x₀ + rw [← append_coords] + simp only [coords, zero_add] + +/-- Distributivity for addition of module elements. -/ +theorem elem_distrib (a : R) (x₁ x₂ : R[X]) : + a • (x₁ + x₂) = a • x₁ + a • x₂ := by + apply @Quotient.ind₂ + (motive := fun x₁ x₂ : R[X] => a • (x₁ + x₂) = a • x₁ + a • x₂) + intro s₁ s₂ + apply Quotient.sound + apply funext + intro x₀ + rw [← scmul_coords] + rw [← append_coords] + rw [← append_coords] + rw [← scmul_coords] + rw [← scmul_coords] + simp only [left_distrib] + +/-- Distributivity with respect to scalars. -/ +theorem coeffs_distrib (a b : R) (x : R[X]) : a • x + b • x = (a + b) • x := by + apply @Quotient.ind (motive := fun x : R[X] => + a • x + b • x = (a + b) • x) + intro s + apply Quotient.sound + apply funext + intro x₀ + let l := act_sum a b s + let l'' := congrFun l x₀ + exact l'' + +/-- Multiplication by `1 : R`. -/ +theorem unit_coeffs (x : R[X]) : (1 : R) • x = x := by + apply @Quotient.ind (motive := fun x : R[X] => + (1 : R) • x = x) + intro s + apply Quotient.sound + apply funext + intro x₀ + let l := scmul_coords 1 s x₀ + rw [← l] + simp only [one_mul] + +/-- Multiplication by `0 : R`. -/ +theorem zero_coeffs (x : R[X]) : (0 : R) • x = ⟦ [] ⟧ := by + apply @Quotient.ind (motive := fun x : R[X] => + (0 : R) • x = ⟦ [] ⟧) + intro s + apply Quotient.sound + apply funext + intro x₀ + let l := scmul_coords 0 s x₀ + rw [← l] + simp only [zero_mul, coords] + +instance : Zero (R[X]) := + ⟨FreeModule.zero⟩ + +instance : Neg (R[X]) := + ⟨fun x => (-1 : R) • x⟩ + +/-- The module is an additive commutative group, mainly proved as a check -/ +instance : AddCommGroup (R[X]) := + { + zero := _ + add := FreeModule.add + add_assoc := FreeModule.addn_assoc + add_zero := FreeModule.addn_zero + zero_add := FreeModule.zero_addn + neg := fun x => (-1 : R) • x + nsmul := nsmulRec + zsmul := zsmulRec + + sub_eq_add_neg := by intros; rfl + + neg_add_cancel := by + intro x + let l := FreeModule.coeffs_distrib (-1 : R) (1 : R) x + simp only [neg_add_cancel] at l + rw [FreeModule.unit_coeffs] at l + rw [FreeModule.zero_coeffs] at l + exact l + + add_comm := FreeModule.addn_comm + } + +end FreeModule + +/-! +## Equivalent definition of the relation via moves + +For conceptual results such as the universal property (needed for the group ring structure) it is +useful to define the relation on the free module in terms of moves. We do this, and show that +this is the same as the relation defined by equality of coordinates. + +* We define elementary moves on formal sums +* We show coordinates equal if and only if related by elementary moves +* Hence can define map on Free Module when invariant under elementary moves + -/ + +open FormalSum +/-- Elementary moves for formal sums. -/ +inductive ElementaryMove (R X : Type) [Ring R] [DecidableEq R] [DecidableEq X] : + FormalSum R X → FormalSum R X → Prop where + | zeroCoeff (tail : FormalSum R X) (x : X) (a : R) (h : a = 0) : + ElementaryMove R X ((a, x) :: tail) tail + | addCoeffs (a b : R) (x : X) (tail : FormalSum R X) : + ElementaryMove R X ((a, x) :: (b, x) :: tail) ((a + b, x) :: tail) + | cons (a : R) (x : X) (s₁ s₂ : FormalSum R X) : + ElementaryMove R X s₁ s₂ → ElementaryMove R X ((a, x) :: s₁) ((a, x) :: s₂) + | swap (a₁ a₂ : R) (x₁ x₂ : X) (tail : FormalSum R X) : + ElementaryMove R X ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail) + +/-- Free module quotient using elementary moves on formal sums. -/ +def FreeModuleAux (R X : Type) [Ring R] [DecidableEq R] [DecidableEq X] := + Quot (ElementaryMove R X) + +namespace FormalSum + +/-- Image in the quotient (i.e., actual, not formal, sum). -/ +def sum (s : FormalSum R X) : FreeModuleAux R X := + Quot.mk (ElementaryMove R X) s + +/-- Equivalence by having the same image. -/ +def equiv (s₁ s₂ : FormalSum R X) : Prop := + s₁.sum = s₂.sum + +/-- Infix notation for equivalence by elementary moves. -/ +infix: 65 " ≃ " => FormalSum.equiv + +/-! +### Invariance of coordinates under elementary moves +-/ + +/-- Coordinates are invariant under moves. -/ +theorem coords_move_invariant (x₀ : X) (s₁ s₂ : FormalSum R X) + (h : ElementaryMove R X s₁ s₂) : coords s₁ x₀ = coords s₂ x₀ := by + induction h with + | zeroCoeff tail x a hyp => + simp only [coords, hyp, monom_coords_at_zero, zero_add] + | addCoeffs a b x tail => + simp only [coords, ← add_assoc, monom_coords_hom] + | cons a x s₁ s₂ _ step => + simp only [coords, step] + | swap a₁ a₂ x₁ x₂ tail => + simp only [coords, ← add_assoc, add_comm] + +end FormalSum + +/-- Coordinates on the quotients. -/ +def _root_.LeanPool.Polylean.FreeModuleAux.coeff (x₀ : X) : FreeModuleAux R X → R := + Quot.lift (fun s => s.coords x₀) (coords_move_invariant x₀) + +namespace FormalSum + +/-- Commutative diagram for coordinates. -/ +theorem coeff_factors (x : X) (s : FormalSum R X) : FreeModuleAux.coeff x (sum s) = s.coords x := by + simp only [FreeModuleAux.coeff] + apply @Quot.liftBeta (r := ElementaryMove R X) (f := fun s => s.coords x) + apply coords_move_invariant + +/-- Coordinates well-defined under the equivalence generated by moves. -/ +theorem coords_well_defined (x : X) (s₁ s₂ : FormalSum R X) : + s₁ ≃ s₂ → s₁.coords x = s₂.coords x := by + intro hyp + have l : FreeModuleAux.coeff x (sum s₂) = s₂.coords x := by + simp only [coeff_factors] + rw [← l] + rw [← coeff_factors] + rw [hyp] + +/-! +### Equal coordinates implies related by elementary moves. +-/ + +/-- Cons respects equivalence. -/ +theorem cons_equiv_of_equiv (s₁ s₂ : FormalSum R X) (a : R) (x : X) : + s₁ ≃ s₂ → (a, x) :: s₁ ≃ (a, x) :: s₂ := by + intro h + let f : FormalSum R X → FreeModuleAux R X := fun s => sum <| (a, x) :: s + let wit : (s₁ s₂ : FormalSum R X) → (ElementaryMove R X s₁ s₂) → f s₁ = f s₂ := by + intro s₁ s₂ hyp + apply Quot.sound + apply ElementaryMove.cons + assumption + let g := Quot.lift f wit + let factorizes : (s : FormalSum R X) → g (s.sum) = sum ((a, x) :: s) := Quot.liftBeta f wit + rw [equiv] + rw [← factorizes] + rw [← factorizes] + rw [h] + +/-- If a coordinate `x` for a formal sum `s` is non-zero, `s` is related by moves to a formal sum +with first term `x` with coefficient its coordinates, and the rest shorter than `s`. -/ +theorem nonzero_coeff_has_complement (x₀ : X) (s : FormalSum R X) : + 0 ≠ s.coords x₀ → + (∃ ys : FormalSum R X, (((s.coords x₀, x₀) :: ys) ≃ s) ∧ + (List.length ys < s.length)) := + by + induction s with + | nil => + intro contra + contradiction + | cons head tail hyp => + let (a, x) := head + intro pos + cases c : x == x₀ with + | true => + let k := FormalSum.coords tail x₀ + have lem : a + k = coords ((a, x) :: tail) x₀ := by + rw [coords, monomCoeff, c] + have c'' : x = x₀ := of_decide_eq_true c + rw [c''] + rw [c''] at lem + exact + if c' : (0 = k) then by + have lIneq : tail.length < List.length ((a, x) :: tail) := by + simp only [List.length_cons, Nat.lt_add_one] + rw [← c', add_zero] at lem + rw [← lem] + exact ⟨tail, rfl, lIneq⟩ + else by + let ⟨ys, eqnStep, lIneqStep⟩ := hyp c' + have eqn₁ : (a, x₀) :: (k, x₀) :: ys ≃ (a + k, x₀) :: ys := by + apply Quot.sound + apply ElementaryMove.addCoeffs + have eqn₂ : (a, x₀) :: (k, x₀) :: ys ≃ (a, x₀) :: tail := by + apply cons_equiv_of_equiv + assumption + have eqn : (a + k, x₀) :: ys ≃ (a, x₀) :: tail := Eq.trans (Eq.symm eqn₁) eqn₂ + rw [← lem] + have lIneq : ys.length < List.length ((a, x₀) :: tail) := by + apply Nat.le_trans lIneqStep + simp only [List.length_cons, Nat.le_succ] + exact ⟨ys, eqn, lIneq⟩ + | false => + let k := coords tail x₀ + have lem : k = coords ((a, x) :: tail) x₀ := by + simp only [coords, monomCoeff, c, zero_add, k] + rw [← lem] at pos + let ⟨ys', eqnStep, lIneqStep⟩ := hyp pos + rw [← lem] + let ys := (a, x) :: ys' + have lIneq : ys.length < ((a, x) :: tail).length := by + simp only [List.length_cons] + apply Nat.succ_lt_succ + exact lIneqStep + have eqn₁ : (k, x₀) :: ys ≃ (a, x) :: (k, x₀) :: ys' := by + apply Quot.sound + apply ElementaryMove.swap + have eqn₂ : (a, x) :: (k, x₀) :: ys' ≃ (a, x) :: tail := by + apply cons_equiv_of_equiv + assumption + have eqn : (k, x₀) :: ys ≃ (a, x) :: tail := by + exact Eq.trans eqn₁ eqn₂ + exact ⟨ys, eqn, lIneq⟩ + +/-- If all coordinates are zero, then moves relate to the empty sum. -/ +theorem equiv_e_of_zero_coeffs (s : FormalSum R X) (hyp : ∀ x : X, s.coords x = 0) : s ≃ [] := + -- let canc : IsAddLeftCancel R := + -- ⟨fun a b c h => by + -- rw [← neg_add_cancel_left a b, h, neg_add_cancel_left]⟩ + match mt : s with + | [] => rfl + | h :: t => by + let (a₀, x₀) := h + let hyp₀ := hyp x₀ + rw [coords] at hyp₀ + have c₀ : monomCoeff R X x₀ (a₀, x₀) = a₀ := by + simp only [monomCoeff, BEq.rfl] + rw [c₀] at hyp₀ + exact + if hz : a₀ = 0 then by + rw [hz] at hyp₀ + rw [zero_add] at hyp₀ + have tail_coeffs : ∀ x : X, coords t x = 0 := by + intro x + exact + if c : (x₀ = x) then by + rw [← c] + assumption + else by + let hx := hyp x + simp only [coords, monomCoeff] at hx + have lf : (x₀ == x) = false := decide_eq_false c + rw [lf] at hx + simp only [zero_add] at hx + assumption + have _ : t.length < (h :: t).length := by + simp only [List.length_cons, Nat.lt_add_one] + let step : t ≃ [] := by + apply equiv_e_of_zero_coeffs + exact tail_coeffs + rw [hz] + have ls : (0, x₀) :: t ≃ t := by + apply Quot.sound + apply ElementaryMove.zeroCoeff + rfl + exact Eq.trans ls step + else by + have non_zero : 0 ≠ coords t x₀ := by + intro contra' + let contra := Eq.symm contra' + rw [contra, add_zero] at hyp₀ + contradiction + let ⟨ys, eqnStep, lIneqStep⟩ := nonzero_coeff_has_complement x₀ t non_zero + have tail_coeffs : ∀ x : X, coords ys x = 0 := by + intro x + exact + if c : (x₀ = x) then by + rw [← c] + let ceq := coords_well_defined x₀ _ _ eqnStep + simp only [coords, monomCoeff, BEq.rfl, add_eq_left] at ceq + assumption + else by + let hx := hyp x + simp only [coords, monomCoeff] at hx + have lf : (x₀ == x) = false := decide_eq_false c + rw [lf] at hx + simp only [zero_add] at hx + let ceq := coords_well_defined x _ _ eqnStep + simp only [coords, monomCoeff, lf, zero_add] at ceq + rw [hx] at ceq + exact ceq + have _ : ys.length < (h :: t).length := by + simp only [List.length_cons] + apply Nat.le_trans lIneqStep + apply Nat.le_succ + let step : ys ≃ [] := by + apply equiv_e_of_zero_coeffs + exact tail_coeffs + let eqn₁ := cons_equiv_of_equiv _ _ (coords t x₀) x₀ step + let eqn₂ : t ≃ (coords t x₀, x₀) :: [] := Eq.trans (Eq.symm eqnStep) eqn₁ + let eqn₃ := cons_equiv_of_equiv _ _ a₀ x₀ eqn₂ + apply Eq.trans eqn₃ + have eqn₄ : + sum [(a₀, x₀), (coords t x₀, x₀)] = sum [(a₀ + coords t x₀, x₀)] := by + apply Quot.sound + apply ElementaryMove.addCoeffs + apply Eq.trans eqn₄ + rw [hyp₀] + apply Quot.sound + apply ElementaryMove.zeroCoeff + rfl + termination_by s.length + +/-- If coordinates are equal, the sums are related by moves. -/ +theorem equiv_of_equal_coeffs (s₁ s₂ : FormalSum R X) + (hyp : ∀ x : X, s₁.coords x = s₂.coords x) : s₁ ≃ s₂ := + match s₁ with + | [] => + have coeffs : ∀ x : X, s₂.coords x = 0 := by + intro x + let h := hyp x + rw [← h] + rfl + let zl := equiv_e_of_zero_coeffs s₂ coeffs + Eq.symm zl + | (a₀, x₀) :: t => + by + exact + if p : 0 = a₀ then by + have eq₁ : (a₀, x₀) :: t ≃ t := by + apply Quot.sound + apply ElementaryMove.zeroCoeff + apply Eq.symm + assumption + have _ : t.length < ((a₀, x₀) :: t).length := by + simp only [List.length_cons, Nat.lt_add_one] + have eq₂ : t ≃ s₂ := by + apply equiv_of_equal_coeffs t s₂ + intro x + let ceq := coords_well_defined x ((a₀, x₀) :: t) t eq₁ + simp only [← ceq, hyp] + exact Eq.trans eq₁ eq₂ + else by + let a₁ := coords t x₀ + exact + if p₁ : 0 = a₁ then by + have cf₂ : s₂.coords x₀ = a₀ := by + rw [← hyp] + simp only [coords, monomCoeff, BEq.rfl, add_eq_left] + exact Eq.symm p₁ + let ⟨ys, eqn, _⟩ := + nonzero_coeff_has_complement x₀ s₂ + (by + rw [cf₂] + assumption) + let cfs := fun x => coords_well_defined x _ _ eqn + rw [cf₂] at cfs + let cfs' := fun (x : X) => Eq.trans (hyp x) (Eq.symm (cfs x)) + simp only [coords, add_right_inj] at cfs' + have _ : t.length < ((a₀, x₀) :: t).length := by + simp only [List.length_cons, Nat.lt_add_one] + let step := equiv_of_equal_coeffs t ys cfs' + let _step' := cons_equiv_of_equiv t ys a₀ x₀ step + rw [cf₂] at eqn + exact Eq.trans _step' eqn + else by + let ⟨ys, eqn, ineqn⟩ := nonzero_coeff_has_complement x₀ t p₁ + let s₃ := (a₀ + a₁, x₀) :: ys + have eq₁ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ s₃ := by + apply Quot.sound + let lem := ElementaryMove.addCoeffs a₀ a₁ x₀ ys + exact lem + have eq₂ : (a₀, x₀) :: (a₁, x₀) :: ys ≃ (a₀, x₀) :: t := by + apply cons_equiv_of_equiv + assumption + have eq₃ : s₃ ≃ s₂ := by + have _ : ys.length + 1 < t.length + 1 := by + apply Nat.succ_lt_succ + exact ineqn + apply equiv_of_equal_coeffs + intro x + rw [← hyp x] + simp only [coords, s₃] + let d := coords_well_defined x _ _ eqn + rw [coords] at d + rw [← d] + simp only [monom_coords_hom] + rw [add_assoc] + apply Eq.trans (Eq.trans (Eq.symm eq₂) eq₁) eq₃ + termination_by s₁.length +/-! +## Functions invariant under moves pass to the quotient. +-/ +/-- Lifting functions to the move induced quotient. -/ +theorem func_eql_of_move_equiv {β : Sort u} (f : FormalSum R X → β) : + (∀ s₁ s₂ : FormalSum R X, ElementaryMove R X s₁ s₂ → f s₁ = f s₂) → + (∀ s₁ s₂ : FormalSum R X, s₁ ≈ s₂ → f s₁ = f s₂) := + by + intro hyp + let fbar : FreeModuleAux R X → β := Quot.lift f hyp + let fct : ∀ s : FormalSum R X, f s = fbar (sum s) := by + apply Quot.liftBeta + apply hyp + intro s₁ s₂ sim + have ec : eqlCoords R X s₁ s₂ := sim + rw [eqlCoords] at ec + have pullback : sum s₁ = sum s₂ := by + apply equiv_of_equal_coeffs + intro x + exact congrFun ec x + simp only [fct, pullback] + +end FormalSum + +/-! +## Injectivity of inclusions + +We show that, under appropriate hypotheses, two inclusions into Free Modules are injective. + +* If `a : R` is nonzero, then `x : X ↦ ⟦[(a, x)]⟧` is injective. +* If `x: X`, then `a : R ↦ ⟦[(a, x)]⟧` is injective. + +These are used in proving injectivity results for related functions on group rings, which act as a +check on the correctness of the definitions. +-/ +open FormalSum + +omit [DecidableEq R] in +/-- For `a : R` and `a ≠ 0`, injectivity of the function `x : X ↦ [(a, x)]` up to +equivalence. -/ +theorem monom_elem_eq_of_coord_eq_nonzero (a : R) (non_zero : a ≠ 0) (x₀ x₁ : X) : + coords [(a, x₀)] = coords [(a, x₁)] → x₀ = x₁ := by + intro hyp + have sup₀ : support [(a, x₀)] = [x₀] := by + rfl + have c₁ : coords [(a, x₁)] x₁ = a := by + simp only [coords, monomCoeff, BEq.rfl, add_zero] + rw [← c₁] at non_zero + symm at non_zero + rw [← hyp] at non_zero + let lem := nonzero_coord_in_support [(a, x₀)] x₁ non_zero + have lem' : x₁ = x₀ := by + simpa only [support, List.map_cons, List.map_nil, List.mem_cons, List.not_mem_nil, + or_false] using lem + exact Eq.symm lem' + +omit [DecidableEq R] in +/-- For `x : X`, injectivity of the function `a : R ↦ [(a, x)]` up to equivalence. -/ +theorem monom_coeff_eq_of_coord_eq (x : X) (a₀ a₁ : R) : + coords [(a₀, x)] = coords [(a₁, x)] → a₀ = a₁ := by + intro hyp + let h₁ := congrFun hyp x + simp only [coords, monomCoeff, BEq.rfl, add_zero] at h₁ + assumption + + +/-- For `x: X`, the functions `a : R ↦ ⟦[(a, x)]⟧` -/ +def coeffInclusion (x₀ : X) : R → R[X] := + fun a₀ => ⟦[(a₀, x₀)]⟧ + +/-- Injectivity of `coeffInclusion` -/ +theorem coeffInclusion_injective (x₀ : X) + (a₀ a₁ : R) : coeffInclusion x₀ a₀ = + coeffInclusion x₀ a₁ → a₀ = a₁ := by + intro hyp + simp only [coeffInclusion] at hyp + rw [Quotient.eq] at hyp + exact monom_coeff_eq_of_coord_eq x₀ a₀ a₁ hyp + +/-- For `a: A`, the function `x: X ↦ ⟦[(a, x)]⟧` -/ +def baseInclusion (a₀ : R) : X → R[X] := + fun x₀ => ⟦[(a₀, x₀)]⟧ + +/-- Injectivity of `baseInclusion a` give `a ≠0` -/ +theorem baseInclusion_injective (a₀ : R) (non_zero : a₀ ≠ 0) + (x₀ x₁ : X) : baseInclusion a₀ x₀ = + baseInclusion a₀ x₁ → x₀ = x₁ := by + intro hyp + simp only [baseInclusion] at hyp + rw [Quotient.eq] at hyp + exact monom_elem_eq_of_coord_eq_nonzero a₀ non_zero x₀ x₁ hyp +/-! +## Basic `Repr` + +An instance of `Repr` on Free Modules, mainly for debugging (fairly crude). This is implemented +by constructing a norm ball containing all the non-zero coordinates, and then making a list of +non-zero coordinates. +-/ + +theorem fst_le_max (a b : Nat) : a ≤ max a b := by + exact if c : a ≤ b + then by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_pos c] + assumption + else by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_neg c, Std.le_refl] + + +theorem snd_le_max (a b : Nat) : b ≤ max a b := by + exact if c : a ≤ b + then by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_pos c, Std.le_refl] + else by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_neg c] + apply Nat.le_of_lt + let c' := Nat.gt_of_not_le c + assumption + + +theorem eq_fst_or_snd_of_max (a b : Nat) : (max a b = a) ∨ (max a b = b) := by + exact if c : a ≤ b + then by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_pos c, or_true] + else by + unfold max + unfold Nat.instMax + unfold maxOfLe + simp only [if_neg c, true_or] + +/-- The successor of the largest norm with nonzero coordinate on a support list. -/ +def maxNormSuccOnSupp (norm : X → Nat) (crds : X → R) (s : List X) : Nat := + match s with + | [] => 0 + | head :: tail => + if crds head ≠ 0 then + max (norm head + 1) (maxNormSuccOnSupp norm crds tail) + else + maxNormSuccOnSupp norm crds tail + +omit [DecidableEq X] in +theorem max_in_support (norm : X → Nat) (crds : X → R) (s : List X) : + maxNormSuccOnSupp norm crds s > 0 → + ∃ x : X, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1 := by + intro h + induction s with + | nil => + simp only [maxNormSuccOnSupp, gt_iff_lt, Nat.lt_irrefl] at h + | cons head tail ih => + exact if c : crds head = 0 then + by + simp only [ne_eq, maxNormSuccOnSupp, c, not_true_eq_false, ↓reduceIte] + simp only [maxNormSuccOnSupp, c, ne_eq, not_true_eq_false, ↓reduceIte, gt_iff_lt] at h + exact ih h + else by + simp only [ne_eq, maxNormSuccOnSupp, c, not_false_eq_true, ↓reduceIte] + simp only [maxNormSuccOnSupp, ne_eq, c, not_false_eq_true, ↓reduceIte, gt_iff_lt] at h + let sl := eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail) + cases sl + case inr p => + rw [p] + rw [p] at h + exact ih h + case inl p => + rw [p] + rw [p] at h + exact ⟨head, And.intro c rfl⟩ + +omit [DecidableEq X] in +theorem supp_below_max (norm : X → Nat) (crds : X → R) (s : List X) : + (x : X) → x ∈ s → crds x ≠ 0 → norm x + 1 ≤ maxNormSuccOnSupp norm crds s := by + intro x h₁ h₂ + cases h₁ + case head as => + rw [maxNormSuccOnSupp] + simp only [ne_eq, h₂, not_false_eq_true, ↓reduceIte] + apply fst_le_max + case tail a as th => + rw [maxNormSuccOnSupp] + let l := supp_below_max norm crds as x th h₂ + exact if c : crds a ≠ 0 then + by + simp only [ne_eq, c, not_false_eq_true, ↓reduceIte, ge_iff_le] + apply Nat.le_trans l + apply snd_le_max + else + by + simp only [c, ↓reduceIte, ge_iff_le] + exact l + +omit [DecidableEq X] in +theorem supp_zero_of_max_zero (norm : X → Nat) (crds : X → R) (s : List X) : + maxNormSuccOnSupp norm crds s = 0 → + (x : X) → x ∈ s → crds x = 0 := fun hyp x hm => + if c : crds x = 0 then c + else by + let l := supp_below_max norm crds s x hm c + rw [hyp] at l + contradiction + +/-- The successor of the largest norm with nonzero coefficient in a formal sum. -/ +def _root_.LeanPool.Polylean.FormalSum.normSucc (norm : X → Nat) (s : FormalSum R X) : Nat := + maxNormSuccOnSupp norm s.coords (s.support) + +open FormalSum +theorem normsucc_le (norm : X → Nat) (s₁ s₂ : FormalSum R X) (eql : s₁ ≈ s₂) : + s₁.normSucc norm ≤ s₂.normSucc norm := + if c : s₁.normSucc norm = 0 then + by + rw [c] + apply Nat.zero_le + else by + simp only [normSucc] + simp only [normSucc] at c + let c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 := + by + cases Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) + · contradiction + · assumption + let l := max_in_support norm s₁.coords s₁.support c' + let ⟨x₀, p⟩ := l + let nonzr' := p.left + let l := congrFun eql x₀ + rw [l] at nonzr' + let nonzr : 0 ≠ s₂.coords x₀ := by + intro hyp + let l' := Eq.symm hyp + contradiction + let in_supp := nonzero_coord_in_support s₂ x₀ nonzr + rw [p.right] + apply supp_below_max norm s₂.coords s₂.support x₀ in_supp nonzr' + +theorem norm_succ_eq (norm : X → Nat) (s₁ s₂ : FormalSum R X) (eql : s₁ ≈ s₂) : + s₁.normSucc norm = s₂.normSucc norm := by + apply Nat.le_antisymm + · apply normsucc_le + assumption + · apply normsucc_le + apply eqlCoords.symm + assumption + +/-- Finite exhaustive approximations to a type, organized by a norm. -/ +class NormCube (α : Type) where + /-- A size function on elements. -/ + norm : α → Nat + /-- Elements whose norm is bounded by a given natural number. -/ + cube : Nat → List α + +/-- The finite cube at radius `k`. -/ +def normCube (α : Type) [nc : NormCube α] (k : Nat) := nc.cube k + +instance natCube : NormCube Nat := ⟨id, fun n => (List.range n).reverse⟩ + +instance finCube {k : Nat} : NormCube (Fin (Nat.succ k)) := + let i : Nat → Fin (Nat.succ k) := fun n => ⟨n % (Nat.succ k), by + apply Nat.mod_lt + apply Nat.zero_lt_succ + ⟩ + ⟨fun j => j.val, fun n => (List.range (min (k + 1) n)).reverse.map i⟩ + + +instance intCube : NormCube ℤ where + norm := Int.natAbs + cube : Nat → List ℤ := fun n => + (List.range (n)).reverse.map (Int.ofNat) ++ + (List.range (n - 1)).map (Int.negSucc) + +instance prodCube {α β : Type} [na : NormCube α] [nb : NormCube β] : NormCube (α × β) where + norm : (α × β) → Nat := + fun ⟨a, b⟩ => max (na.norm a) (nb.norm b) + cube : Nat → List (α × β) := + fun n => + (na.cube n).flatMap (fun a => + (nb.cube n).map (fun b => + (a, b))) + +/-- A norm bound for the support of a quotient free-module element. -/ +def _root_.LeanPool.Polylean.FreeModule.normBound (x : R[X]) [nx : NormCube X] : Nat := + Quotient.lift (fun s : FormalSum R X => s.normSucc nx.norm) + (fun s₁ s₂ eql => norm_succ_eq nx.norm s₁ s₂ eql) x + +/-- The nonzero coefficients of a quotient free-module element in a bounded cube. -/ +def _root_.LeanPool.Polylean.FreeModule.coeffList (x : R[X]) [nx : NormCube X] : + List (R × X) := + (nx.cube (x.normBound)).filterMap fun x₀ => + let a := x.coordinates x₀ + if a = 0 then none else some (a, x₀) + +-- basic repr +instance basicRepr [NormCube X] [Repr X] [Repr R] : Repr (R[X]) := + ⟨fun x _ => reprStr (x.coeffList)⟩ + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/GardamGroup.lean b/LeanPool/Polylean/UnitConjecture/GardamGroup.lean new file mode 100644 index 0000000000..d115139c01 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/GardamGroup.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Tactic +import Mathlib.Algebra.Group.Prod +import Mathlib.Algebra.Group.Hom.Basic +import Mathlib.Data.Int.Basic +import Mathlib.Data.Fin.Basic +import LeanPool.Polylean.UnitConjecture.MetabelianGroup +import LeanPool.Polylean.UnitConjecture.AddFreeGroup + +namespace LeanPool.Polylean + +/-! +## The construction of the group `P` + +We construct the group `P` (the *Promislow* or *Hantzsche–Wendt* group) as a Metabelian group. + +This is done via the cocycle construction, using the explicit action and cocycle described in +Section 3.1 of Giles Gardam's paper (https: //arxiv.org/abs/2102.11818). +-/ + +/-! +### The components of the group `P` +The group `P` is constructed as a Metabelian group with kernel `K := ℤ³` and +quotient `Q := ℤ/2 × ℤ/2`. +-/ + +/-! The *kernel* group -/ + +/-- The *kernel* group - `ℤ³`, the free Abelian group on three generators. -/ +@[aesop safe (rule_sets := [P])] +abbrev K := ℤ × ℤ × ℤ + +instance KGrp : AddCommGroup K := inferInstance + +/-- Equality of endomorphisms of `K` is decidable, as `K` is a free group with +basis `Unit ⊕ Unit ⊕ Unit`. -/ +instance : DecidableEq (K →+ K) := decideHomsEqual (X := Unit ⊕ Unit ⊕ Unit) + + +/-! The *quotient* group -/ + +/-- The *quotient* group - `ℤ/2 × ℤ/2`, the Klein Four group. -/ +abbrev Q := Fin 2 × Fin 2 + +instance QGrp : AddCommGroup Q := inferInstance + +/-! +### The group elements +-/ + +namespace K + +/-! The generators of the free Abelian group `K`. -/ + +/-- The first generator of `K`. -/ +@[aesop norm unfold (rule_sets := [P])] +abbrev x : K := (1, 0, 0) +/-- The second generator of `K`. -/ +@[aesop norm unfold (rule_sets := [P])] +abbrev y : K := (0, 1, 0) +/-- The third generator of `K`. -/ +@[aesop norm unfold (rule_sets := [P])] +abbrev z : K := (0, 0, 1) + +end K + + +namespace Q + +/-! The elements of the Klein Four group `Q`. -/ + +/-- The identity element of `Q`. -/ +@[match_pattern] +def e : Q := (⟨0, by decide⟩, ⟨0, by decide⟩) +/-- The first generator of `Q`. -/ +@[match_pattern] +def a : Q := (⟨1, by decide⟩, ⟨0, by decide⟩) +/-- The second generator of `Q`. -/ +@[match_pattern] +def b : Q := (⟨0, by decide⟩, ⟨1, by decide⟩) +/-- The product of the first two generators of `Q`. -/ +@[match_pattern] +def c : Q := (⟨1, by decide⟩, ⟨1, by decide⟩) + +end Q + + +/-! +### The action of `Q` on `K` by automorphisms +The action of the group `Q` on the kernel `K` by automorphisms required for constructing `P`. +-/ + +/-- An abbreviation for the negation homomorphism on commutative groups. -/ +@[aesop norm unfold (rule_sets := [P])] +abbrev neg (α : Type _) [SubtractionCommMonoid α] := negAddMonoidHom (α := α) + +attribute [aesop norm unfold (rule_sets := [P])] negAddMonoidHom + +/-- A temporary notation for easily describing products of additive monoid homomorphisms. -/ +local infixr: 100 " × " => AddMonoidHom.prodMap + +/-- The action of `Q` on `K` by automorphisms. +The action can be given a component-wise description in terms of `id` and `neg`, the +identity and negation homomorphisms. -/ +@[aesop norm unfold (rule_sets := [P]), reducible] +def action : Q → (K →+ K) + | .e => .id ℤ × .id ℤ × .id ℤ + | .a => .id ℤ × neg ℤ × neg ℤ + | .b => neg ℤ × .id ℤ × neg ℤ + | .c => neg ℤ × neg ℤ × .id ℤ + +/-- A verification that the above action is indeed an action by automorphisms. + This is done automatically with the machinery of decidable equality of homomorphisms + on free groups. -/ +instance : AutAction action := + { id_action := rfl + compatibility := by decide } + +/-! ### The cocycle -/ + +open K Q in +/-- The cocycle in the construction of `P`. -/ +@[aesop norm unfold (rule_sets := [P]), reducible] +def cocycle : Q → Q → K + | a , a => x + | a , c => x + | b , b => y + | c , b => -y + | c , c => z + | b , c => -x + -z + | c , a => -y + z + | b , a => -x + y + -z + | _ , _ => 0 + +/-- A verification that the `cocycle` function indeed satisfies the cocycle condition. + This check is performed fully automatically using previously defined decision procedures. -/ +instance P_cocycle : Cocycle cocycle := + { α := action + autAct := inferInstance + cocycle_zero := rfl + cocycle_condition := by decide } + +/-! +### The construction of `P` +The construction of the group `P` as a Metabelian group from the given action and cocycle. +-/ + +/-- the group `P` constructed via the cocycle construction -/ +@[aesop norm unfold (rule_sets := [P])] +def P := K × Q + +namespace P + +instance (priority := high) PGrp : Group P := MetabelianGroup.metabelianGroup cocycle + +/-- Multiplication for `P` coming from its metabelian group structure. -/ +scoped instance (priority := high) : HMul (K × Q) (K × Q) (K × Q) := ⟨PGrp.mul⟩ +/-- Multiplication for `P` coming from its metabelian group structure. -/ +scoped instance (priority := high) : Mul (K × Q) := ⟨PGrp.mul⟩ +@[reducible] +instance instPow : Pow (K × Q) ℕ := + ⟨fun p n => PGrp.toMonoid.npow n p⟩ + + +instance : DecidableEq P := inferInstanceAs <| DecidableEq (K × Q) + +/-- A confirmation that multiplication in `P` is as expected from the Metabelian +group structure. -/ +@[aesop norm (rule_sets := [P]), simp] +theorem mul (k k' : K) (q q' : Q) : + (k, q) * (k', q') = (k + action q k' + cocycle q q', q + q') := rfl + +@[aesop norm (rule_sets := [P])] +theorem one : (1 : P) = ((0, 0, 0), Q.e) := rfl + +/-- Powers of kernel elements remain in the kernel. -/ +theorem kernel_pow (k : K) (n : ℕ) : ((k, Q.e) : P) ^ n = (n • k, Q.e) := by + induction n with + | zero => + unfold HPow.hPow instHPow Pow.pow instPow + simp + rfl + | succ n ih => + unfold HPow.hPow instHPow Pow.pow instPow + change PGrp.toMonoid.npow (n + 1) ((k, Q.e) : P) = ((n + 1) • k, Q.e) + rw [PGrp.toMonoid.npow_succ] + change ((k, Q.e) : P) ^ n * (k, Q.e) = ((n + 1) • k, Q.e) + rw [ih] + rw [P.mul] + simp only [nsmul_eq_mul, AddMonoidHom.coe_prodMap, AddMonoidHom.coe_id, + Prod.map_id, id_eq, add_zero, Nat.cast_add, Nat.cast_one, Prod.mk.injEq, + add_eq_left] + constructor + · ext <;> ring_nf + · rfl + +end P + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/GroupRing.lean b/LeanPool/Polylean/UnitConjecture/GroupRing.lean new file mode 100644 index 0000000000..d261788de2 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/GroupRing.lean @@ -0,0 +1,627 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.UnitConjecture.FreeModule +import Mathlib.Algebra.Field.Basic + +namespace LeanPool.Polylean + +/-! +# Group Rings + +We construct the Group ring `R[G]` given a group `G` and a ring `R`, both having +decidable equality. The ring structures is constructed using the (implicit) universal +property of `R`-modules. As a check on our definitions, `R[G]` is proved to be a Ring. + +We first define multiplication on formal sums. We prove many properties that are used both +to show invariance under elementary moves and to prove that `R[G]` is a ring. + +-/ + +variable {R : Type} [Ring R] [DecidableEq R] + +variable {G : Type} [Group G] [DecidableEq G] + +/-! +## Multiplication on formal sums +-/ +/-- multiplication by a monomial -/ +def _root_.LeanPool.Polylean.FormalSum.mulMonom + (b : R) (h : G) : FormalSum R G → FormalSum R G +| [] => [] +| (a, g) :: tail => (a * b, g * h) :: (mulMonom b h tail) + +/-- multiplication for formal sums -/ +def _root_.LeanPool.Polylean.FormalSum.mul + (fst : FormalSum R G) : FormalSum R G → FormalSum R G +| [] => [] +| (b, h) :: ys => + (FormalSum.mulMonom b h fst) ++ (mul fst ys) + +/-! + +## Properties of multiplication on formal sums +-/ +namespace GroupRing + +open FormalSum +-- multiplication by the zero monomial +omit [DecidableEq R] in +theorem mul_monom_zero (g x₀ : G) (s : FormalSum R G) : + coords (mulMonom 0 g s) x₀ = 0 := by + induction s with + | nil => + simp only [mulMonom, coords] + | cons h t ih => + simp only [mulMonom, mul_zero, coords, monom_coords_at_zero, zero_add] + assumption + +-- distributivity of multiplication by a monomial +omit [DecidableEq R] in +theorem mul_monom_dist (b : R) (h x₀ : G) + (s₁ s₂ : FormalSum R G) : + coords (mulMonom b h (s₁ ++ s₂)) x₀ = + coords (mulMonom b h s₁) x₀ + coords (mulMonom b h s₂) x₀ := by + induction s₁ with + | nil => + simp only [List.nil_append, mulMonom, coords, zero_add] + | cons head tail ih => + simp only [List.cons_append, mulMonom, coords] + rw [ih] + simp only [add_assoc] + +-- right distributivity +omit [DecidableEq R] in +theorem mul_dist (x₀ : G) (s₁ s₂ s₃ : FormalSum R G) : + coords (mul s₁ (s₂ ++ s₃)) x₀ = + coords (mul s₁ s₂) x₀ + coords (mul s₁ s₃) x₀ := by + induction s₂ with + | nil => + simp only [List.nil_append, mul, coords, zero_add] + | cons head tail ih => + simp only [List.cons_append, mul] + rw [← append_coords] + rw [← append_coords] + rw [ih] + simp only [add_assoc] + + +-- associativity with two terms monomials +omit [DecidableEq R] in +theorem mul_monom_monom_assoc (a b : R) (h x₀ : G) + (s : FormalSum R G) : + coords (mulMonom b h (mulMonom a x s)) x₀ = + coords (mulMonom (a * b) (x * h) s) x₀ := by + induction s with + | nil => + simp only [mulMonom, coords] + | cons head tail ih => + let (a₁, x₁) := head + simp only [mulMonom, mul_assoc, coords, add_right_inj] + rw [ih] + +-- associativity with one term a monomial +omit [DecidableEq R] in +theorem mul_monom_assoc (b : R) (h x₀ : G) + (s₁ s₂ : FormalSum R G) : + coords (mulMonom b h (mul s₁ s₂)) x₀ = + coords (mul s₁ (mulMonom b h s₂)) x₀ := by + induction s₂ with + | nil => + simp only [mul, mulMonom, coords] + | cons head tail ih => + let (a, x) := head + simp only [mul, mulMonom] + rw [← append_coords] + rw [mul_monom_dist] + rw [ih] + simp only [add_left_inj] + rw [mul_monom_monom_assoc] + +-- left distributivity for multiplication by a monomial +omit [DecidableEq R] in +theorem mul_monom_add (b₁ b₂ : R) (h x₀ : G) + (s : FormalSum R G) : + coords (mulMonom (b₁ + b₂) h s) x₀ = + coords (mulMonom b₁ h s) x₀ + coords (mulMonom b₂ h s) x₀ := by + induction s with + | nil => + simp only [mulMonom, coords, add_zero] + | cons head tail ih => + let (a, g) := head + simp only [mulMonom, coords] + rw [left_distrib] + rw [monom_coords_hom] + rw [ih] + conv => + lhs + rw [add_assoc] + arg 2 + rw [← add_assoc] + congr + rw [add_comm] + conv => + rhs + rw [add_assoc] + conv => + rhs + arg 2 + skip + rw [← add_assoc] + +/-- multiplication equivalent when adding term with `0` coefficient -/ +theorem mul_zero_cons (s t : FormalSum R G) : mul s ((0, h) :: t) ≈ mul s t := by + induction s + case nil => + simp only [mul, mulMonom, List.nil_append] + apply eqlCoords.refl + case cons head tail _ => + simp only [mul, mulMonom, mul_zero, List.cons_append] + apply funext; intro x₀ + simp only [coords] + rw [monom_coords_at_zero] + rw [zero_add] + rw [← append_coords] + simp only [add_eq_right] + let l := mul_monom_zero h x₀ tail + rw [l] + +/-! +## Induced product on the quotient +-/ + +/-- Quotient in second argument for group ring multiplication +-/ +def mulAux : FormalSum R G → R[G] → R[G] := by + intro s + apply Quotient.lift (⟦FormalSum.mul s ·⟧) + apply func_eql_of_move_equiv + intro t t' rel + induction rel with + | zeroCoeff tail g a hyp => + rw [hyp] + dsimp [mul] + apply Quotient.sound + apply funext + intro x₀ + rw [← append_coords] + let l := mul_monom_zero g x₀ s + rw [l] + simp only [zero_add] + | addCoeffs a b x tail => + apply Quotient.sound + apply funext; intro x₀ + simp only [mul] + repeat (rw [← append_coords]) + simp only [mul_monom_add, add_assoc] + | cons a x s₁ s₂ _ step => + apply Quotient.sound + apply funext; intro x₀ + simp only [mul] + rw [← append_coords] + rw [← append_coords] + simp only [add_right_inj] + let l := congrFun (Quotient.exact step) x₀ + rw [l] + | swap a₁ a₂ x₁ x₂ tail => + apply Quotient.sound + apply funext; intro x₀ + simp only [mul, ← append_coords] + rw [← add_assoc] + rw [← add_assoc] + simp only [add_left_inj] + let lc := + add_comm + (coords (mulMonom a₁ x₁ s) x₀) + (coords (mulMonom a₂ x₂ s) x₀) + rw [lc] + +open ElementaryMove +/-- invariance under moves of multiplication by monomials -/ +theorem mul_monom_invariant (b : R) (h x₀ : G) (s₁ s₂ : FormalSum R G) + (rel : ElementaryMove R G s₁ s₂) : + coords (mulMonom b h s₁) x₀ = coords (mulMonom b h s₂) x₀ := by + induction rel with + | zeroCoeff tail g a hyp => + rw [hyp] + simp only [mulMonom, zero_mul, coords, monom_coords_at_zero, zero_add] + | addCoeffs a₁ a₂ x tail => + simp only [mulMonom, coords, right_distrib, monom_coords_hom, add_assoc] + | cons a x t₁ t₂ _ step => + simp only [mulMonom, coords, step] + | swap a₁ a₂ x₁ x₂ tail => + simp only [mulMonom, coords] + conv => + lhs + rw [← add_assoc] + arg 1 + rw [add_comm] + rw [← add_assoc] + + +/-- invariance under moves for the first argument for multipilication -/ +theorem first_arg_invariant (s₁ s₂ t : FormalSum R G) + (rel : ElementaryMove R G s₁ s₂) : + FormalSum.mul s₁ t ≈ FormalSum.mul s₂ t := by + cases t + case nil => + simp only [mul] + rfl + case cons head' tail' => + let (b, h) := head' + induction rel with + | zeroCoeff tail g a hyp => + rw [hyp] + simp only [mul, mulMonom, zero_mul, List.cons_append] + apply funext; intro x₀ + rw [← append_coords] + simp only [coords, monom_coords_at_zero, zero_add] + rw [← append_coords] + simp only [add_right_inj] + let rel' : ElementaryMove R G ((0, g) :: tail) tail := by + apply ElementaryMove.zeroCoeff + rfl + let prev := first_arg_invariant _ _ tail' rel' + let pl := congrFun prev x₀ + rw [pl] + | addCoeffs a₁ a₂ x tail => + simp only [mul] + apply funext; intro x₀ + rw [← append_coords] + rw [← append_coords] + simp only [mulMonom, coords] + rw [right_distrib] + simp only [monom_coords_hom] + let rel' : ElementaryMove R G + ((a₁, x) :: (a₂, x) :: tail) + ((a₁ + a₂, x) :: tail) := by + apply ElementaryMove.addCoeffs + let prev := first_arg_invariant _ _ tail' rel' + let pl := congrFun prev x₀ + rw [pl] + simp only [add_assoc] + | cons a x s₁ s₂ r _ => + simp only [mul] + apply funext; intro x₀ + rw [← append_coords] + rw [← append_coords] + simp only [mulMonom, coords] + let rel' : ElementaryMove R G + ((a, x) :: s₁) + ((a, x) :: s₂) := by + apply ElementaryMove.cons + assumption + let prev := first_arg_invariant _ _ tail' rel' + let pl := congrFun prev x₀ + rw [pl] + let ps := mul_monom_invariant b h x₀ s₁ s₂ r + rw [ps] + | swap a₁ a₂ x₁ x₂ tail => + simp only [mul] + apply funext; intro x₀ + rw [← append_coords] + rw [← append_coords] + rw [mulMonom] + rw [mulMonom] + rw [coords] + rw [coords] + rw [mulMonom] + rw [mulMonom] + rw [coords] + rw [coords] + let rel' : ElementaryMove R G + ((a₁, x₁) :: (a₂, x₂) :: tail) + ((a₂, x₂) :: (a₁, x₁) :: tail) := by + apply ElementaryMove.swap + let prev := first_arg_invariant _ _ tail' rel' + let pl := congrFun prev x₀ + rw [pl] + simp only [add_left_inj] + rw [← add_assoc] + rw [← add_assoc] + simp only [add_left_inj] + conv => + lhs + rw [add_comm] + +/-- The empty right factor is preserved by elementary moves in the first factor. -/ +theorem first_arg_invariant_nil (s₁ s₂ : FormalSum R G) + (rel : ElementaryMove R G s₁ s₂) : + FormalSum.mul s₁ [] ≈ FormalSum.mul s₂ [] := + first_arg_invariant s₁ s₂ [] rel + +/-- multiplication for free modules -/ +def mul : R[G] → R[G] → R[G] := by + let f := fun (s : FormalSum R G) => + fun (t : R[G]) => mulAux s t + apply Quotient.lift f + apply func_eql_of_move_equiv + intro s₁ s₂ rel + simp only [f] + apply funext + apply Quotient.ind + intro t + let lhs : mulAux s₁ (Quotient.mk (formalSumSetoid R G) t) = + ⟦FormalSum.mul s₁ t⟧ := by + simp only [mulAux, Quotient.lift_mk] + let rhs : mulAux s₂ (Quotient.mk (formalSumSetoid R G) t) = + ⟦FormalSum.mul s₂ t⟧ := by + simp only [mulAux, Quotient.lift_mk] + rw [lhs, rhs] + apply Quotient.sound + apply first_arg_invariant + exact rel + +/-! +## The Ring Structure +-/ + +instance groupRingMul : Mul (R[G]) := + ⟨mul⟩ + +instance : One (R[G]) := + ⟨⟦[(1, 1)]⟧⟩ + +instance : AddCommGroup (R[G]) := + { + zero := ⟦ [] ⟧ + add := FreeModule.add + + nsmul := nsmulRec + zsmul := zsmulRec + + add_assoc := FreeModule.addn_assoc + add_zero := FreeModule.addn_zero + zero_add := FreeModule.zero_addn + add_comm := FreeModule.addn_comm + neg_add_cancel := by + intro x + let l := FreeModule.coeffs_distrib (-1 : R) (1 : R) x + rw [neg_add_cancel, FreeModule.unit_coeffs, FreeModule.zero_coeffs] at l + exact l + } + +/-- The group ring is a ring -/ +instance : Ring (R[G]) := + { + mul := mul + neg := fun x => (-1 : R) • x + zsmul := zsmulRec + + sub_eq_add_neg := by + intro x y + rfl + + neg_add_cancel := by + intro x + let l := FreeModule.coeffs_distrib (-1 : R) (1 : R) x + simp only [neg_add_cancel] at l + have lc : (-1 : R) + 1 = 0 := by + apply neg_add_cancel + -- rw [lc] at l + rw [FreeModule.unit_coeffs] at l + rw [FreeModule.zero_coeffs] at l + exact l + + left_distrib := by + apply @Quotient.ind (motive := fun a => + ∀ b c, a * (b + c) = a * b + a * c) + intro x + apply @Quotient.ind₂ (motive := fun b c => + ⟦ x ⟧ * (b + c) = ⟦ x ⟧ * b + ⟦ x ⟧ * c) + intro y z + apply Quotient.sound + induction y with + | nil => + simp only [List.nil_append] + simp only [FormalSum.mul, List.nil_append] + apply eqlCoords.refl + | cons h t ih => + simp only [List.cons_append, FormalSum.mul, List.append_assoc] + apply funext; intro x₀ + repeat (rw [← append_coords]) + simp only [add_right_inj] + let lih := congrFun ih x₀ + rw [← append_coords] at lih + rw [lih] + right_distrib := by + apply @Quotient.ind (motive := fun a => + ∀ b c, (a + b) * c = a * c + b * c) + intro x + apply @Quotient.ind₂ (motive := fun b c => + (⟦ x ⟧ + b) * c = ⟦ x ⟧ * c + b * c) + intro y z + apply Quotient.sound + induction z with + | nil => + simp only [FormalSum.mul, List.append_nil] + apply eqlCoords.refl + | cons h t ih => + let (a, h) := h + simp only [FormalSum.mul, List.append_assoc] + funext x₀ + repeat (rw [← append_coords]) + let lih := congrFun ih x₀ + rw [← append_coords] at lih + rw [lih] + rw [mul_monom_dist] + simp only [add_left_comm, add_assoc] + zero_mul := by + apply Quotient.ind + intro x + apply Quotient.sound + induction x with + | nil => + rfl + | cons h t ih => + rw [FormalSum.mul] + simp only [mulMonom, List.nil_append] + apply funext; intro x₀ + let lih := congrFun ih x₀ + rw [coords] at lih + -- rw [← append_coords] + rw [lih] + simp only [coords] + + mul_zero := by + apply Quotient.ind + intro x + rfl + + one := ⟦[(1, 1)]⟧ + natCast := fun n => ⟦ [(n, 1)] ⟧ + natCast_zero := + by + apply Quotient.sound + apply funext; intro x₀ + simp only [coords, monomCoeff, Nat.cast_zero, add_zero] + cases 1 == x₀ <;> rfl + natCast_succ := by + intro n + apply Quotient.sound + apply funext; intro x₀ + rw [← append_coords] + simp only [Nat.cast_add, Nat.cast_one] + cases m: 1 == x₀ with + | true => simp only [coords, monomCoeff, m, add_zero] + | false => simp only [coords, monomCoeff, m, add_zero] + mul_assoc := by + apply @Quotient.ind (motive := fun a => + ∀ b c, a * b * c = a * (b * c)) + intro x + apply @Quotient.ind₂ (motive := fun b c => + ⟦ x ⟧ * b * c = ⟦ x ⟧ * (b * c)) + intro y z + apply Quotient.sound + apply funext; intro x₀ + induction z with + | nil => + simp only [FormalSum.mul] + | cons h t ih => + let (a, h) := h + simp only [FormalSum.mul] + repeat (rw [← append_coords]) + rw [mul_dist] + rw [ih] + rw [mul_monom_assoc] + mul_one := by + apply Quotient.ind + intro x + apply Quotient.sound + apply funext; intro x₀ + repeat (rw[FormalSum.mul]) + simp only [List.append_nil] + induction x with + | nil => rfl + | cons h t ih => + let (a, x) := h + rw [mulMonom, coords, monomCoeff] + simp only [mul_one] + rw [coords, monomCoeff] + simp only [ih] + + one_mul := by + apply Quotient.ind + intro x + apply Quotient.sound + apply funext; intro x₀ + induction x with + | nil => rfl + | cons h t ih => + let (a, x) := h + repeat (rw [coords]) + rw [FormalSum.mul] + rw [← append_coords] + simp only [mulMonom, one_mul, coords, add_zero, ih] + } + +end GroupRing + +/-! +## Inclusions of the group and ring into the group ring +-/ +/-- Product `R → G → R[G]`, `r ↦ g ↦ r ⬝ g`; used only in verification results. -/ +instance groupRingMul {R G : Type _} [Ring R] [DecidableEq G] [DecidableEq R] : + HMul R G (FreeModule R G) := ⟨fun r g ↦ ⟦[(r, g)]⟧⟩ + +/-- Scalar multiplication by a group element is represented by the singleton formal sum. -/ +theorem groupRingMul_apply {R G : Type _} [Ring R] [DecidableEq G] [DecidableEq R] + (r : R) (g : G) : r * g = (⟦[(r, g)]⟧ : FreeModule R G) := rfl + +/-- Monoid homomorphism from `G` to `R[G]` given by `g ↦ 1 ⬝ g` -/ +def groupInclusionHom (G : Type) [Group G] [DecidableEq G] : G →* R[G] := + { toFun := baseInclusion 1, + map_one' := rfl, + map_mul' := + by + intro _ _ + apply Quotient.sound + funext x + simp only [FormalSum.coords, monomCoeff, add_zero, FormalSum.mul, FormalSum.mulMonom, mul_one, + List.append_nil] + + } + +/-- As a function `groupInclusionHom` is `g ↦ 1 ⬝ g` -/ +theorem groupInclusionHom_formula (G : Type) [Group G] [DecidableEq G] : + (groupInclusionHom (R := R) G).toFun = + fun g : G ↦ (1 : R) * g := rfl + +/-- The monoid homomorphism `G → R[G]`, `g ↦ 1 ⬝ g` is injective if `1 ≠ 0` in `R`. -/ +theorem groupInclusionHom_injective' (hR : (1 : R) ≠ (0 : R)) : + Function.Injective (groupInclusionHom (R := R) G) := by + intro _ _ + apply baseInclusion_injective (1 : R) hR (X := G) + +/-- For a field `F` the monoid homomorphism `G → F[G]`, `g ↦ 1 ⬝ g` is injective. -/ +theorem groupInclusionHom_injective {F : Type} [Field F] [DecidableEq F] + (G : Type) [Group G] [DecidableEq G] : + Function.Injective (groupInclusionHom (R := F) G) := by + intro _ _ + apply groupInclusionHom_injective' + have : (0 : F) ≠ (1 : F) := zero_ne_one + simp_all only [ne_eq, zero_ne_one, not_false_iff, one_ne_zero] + +/-- The ring homomorphism `R → R[G]` given by `a ↦ a ⬝ 1` -/ +def ringInclusionHom (G : Type) [Group G] [DecidableEq G] : R →+* R[G] := + { toFun := coeffInclusion 1, + map_one' := rfl, + map_mul' := + by + intro _ _ + apply Quotient.sound + funext x + simp only [FormalSum.coords, monomCoeff, add_zero, FormalSum.mul, FormalSum.mulMonom, mul_one, + List.append_nil] + map_zero' := by + apply Quotient.sound + funext x + simp only [FormalSum.coords, monomCoeff, add_zero] + split <;> rfl, + map_add' := by + intro _ _ + apply Quotient.sound + funext x + rw [← FormalSum.append_coords] + simp only [FormalSum.coords, monomCoeff] + by_cases h : (1 : G) == x + · simp only [h, add_zero] + · simp only [h, add_zero] + } + + +/-- As a function, `ringInclusionHom` is `r ↦ r ⬝ 1` -/ +theorem ringInclusionHom_formula (G : Type) [Group G] [DecidableEq G] : + (ringInclusionHom (R := R) G).toFun = + fun r : R ↦ r * (1 : G) := rfl + +/-- The ring homomorphism `R → R[G]` given by `a ↦ a ⬝ 1` is injective -/ +theorem ringInclusionHom_injective' + (G : Type) [Group G] [DecidableEq G] : Function.Injective (ringInclusionHom (R := R) G) := by + intro _ _ + apply coeffInclusion_injective + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean b/LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean new file mode 100644 index 0000000000..90bc2dff6a --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/MetabelianGroup.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Tactic +import Mathlib.Algebra.Group.Hom.Basic +import Mathlib.Algebra.Group.Submonoid.Operations +import LeanPool.Polylean.UnitConjecture.Cocycle +import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets + +namespace LeanPool.Polylean + +/-! + +## Metabelian groups + +Metabelian groups are group extensions `1 → K → G → Q → 1` with both the kernel +and the quotient Abelian. +Such an extension is determined by data: + +* a group action of `Q` on `K` by automorphisms +* a cocyle `c: Q → Q → K` + +We define the cocycle condition and construct a group structure on a structure extending `K × Q`. +The main step is to show that the cocyle condition implies associativity. +-/ + +namespace MetabelianGroup + +variable {Q K : Type _} [AddGroup Q] [AddCommGroup K] +variable (c : Q → Q → K) [ccl : Cocycle c] + +/-- The multiplication operation defined using the cocycle. +The cocycle condition is crucially used in showing associativity and other properties. -/ +@[reducible, aesop norm unfold (rule_sets := [Metabelian])] +def mul : (K × Q) → (K × Q) → (K × Q) + | (k, q), (k', q') => (k + ccl.α q k' + c q q', q + q') + +/-- The identity element of the Metabelian group, + which is the ordered pair of the identities of the individual groups. -/ +@[reducible, aesop norm unfold (rule_sets := [Metabelian])] +def e : K × Q := (0, 0) + +/-- The inverse operation of the Metabelian group. -/ +@[reducible, aesop norm unfold (rule_sets := [Metabelian])] +def inv : K × Q → K × Q + | (k, q) => (- (ccl.α (-q) (k + c q (-q))), -q) + +/-! +Some of the standard lemmas to show that `K × Q` has the structure of a group with the +above operations. +-/ + +@[aesop norm (rule_sets := [Metabelian])] +lemma left_id : ∀ (g : K × Q), mul c e g = g + | (k, q) => by + haveI : AutAction ccl.α := ccl.autAct + simp [mul, Cocycle.left_id (c := c), AutAction.zero_apply] + +@[aesop norm (rule_sets := [Metabelian])] +lemma right_id : ∀ (g : K × Q), mul c g e = g + | (k, q) => by + haveI : AutAction ccl.α := ccl.autAct + simp [mul, Cocycle.right_id (c := c), AutAction.apply_zero] + +@[aesop norm (rule_sets := [Metabelian])] +lemma left_inv : ∀ (g : K × Q), mul c (inv c g) g = e + | (k , q) => by + have := Cocycle.inv_rel' c q + aesop (rule_sets := [Metabelian, Cocycle, AutAction]) + +@[aesop norm (rule_sets := [Metabelian])] +lemma right_inv : ∀ (g : K × Q), mul c g (inv c g) = e + | (k, q) => by aesop (rule_sets := [Metabelian, Cocycle, AutAction]) + +@[aesop safe (rule_sets := [Metabelian])] +theorem mul_assoc : ∀ (g g' g'' : K × Q), mul c (mul c g g') g'' = mul c g (mul c g' g'') + | (k, q), (k', q'), (k'', q'') => by + simp only [mul, Prod.mk.injEq, map_add, AutAction.compatibility'] + constructor + · simp only [add_assoc, add_left_cancel_iff] + rw [add_left_comm, add_left_cancel_iff] + exact ccl.cocycle_condition q q' q'' + · apply add_assoc + +/-- A group structure on `K × Q` using the above multiplication operation. -/ +@[reducible] +def metabelianGroup : Group (K × Q) := + { + mul := mul c, + one := e, + inv := inv c, + mul_one := right_id c, + one_mul := left_id c, + mul_assoc := mul_assoc c, + inv_mul_cancel := left_inv c, + div_eq_mul_inv := by intros; rfl + } + +end MetabelianGroup + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/Tactics.lean b/LeanPool/Polylean/UnitConjecture/Tactics.lean new file mode 100644 index 0000000000..c8f19fc7ad --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/Tactics.lean @@ -0,0 +1,13 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.UnitConjecture.Tactics.AesopRuleSets + +/-! +# Unit Conjecture tactics + +Import-only index for the local Aesop rule sets used by the Unit Conjecture formalization. +-/ diff --git a/LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean b/LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean new file mode 100644 index 0000000000..0da61087c6 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/Tactics/AesopRuleSets.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Aesop + +namespace LeanPool.Polylean + +declare_aesop_rule_sets [AutAction] +declare_aesop_rule_sets [Cocycle] +declare_aesop_rule_sets [Metabelian] +declare_aesop_rule_sets [P] + +end LeanPool.Polylean diff --git a/LeanPool/Polylean/UnitConjecture/TorsionFree.lean b/LeanPool/Polylean/UnitConjecture/TorsionFree.lean new file mode 100644 index 0000000000..1a33977421 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/TorsionFree.lean @@ -0,0 +1,189 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.UnitConjecture.GardamGroup +namespace LeanPool.Polylean + +open scoped P + +-- import Mathlib.Algebra.GroupPower.Basic + +/-! +## Torsion-freeness of `P` + +This file contains a proof that the group `P` defined is in fact torsion-free. + +Roughly, the steps are as follows (further details can be found in the corresponding +`.md` file): +1. Define a function `sq : P -> K` taking a group element `(q, k)` to its square. This + element lies in the kernel as the group `ℤ/2 × ℤ/2` has exponent `2`. +2. Show that elements in `K`, which are integer triples of the form `(a, b, c)`, do not + have torsion. This requires the fact that the group `ℤ`, and hence `ℤ³`, is + torsion-free. +3. Show that no element of `P` has order precisely `2`. This is an argument by cases on + the `Q` part of a general element of `P`. +4. Finally, show that if an element `g : G` of a group `G` satisfies `g ^ n = (1 : G)`, + then it also satisfies `(g ^ 2) ^ n = (1 : G)`. +5. Together, these statements show that `P` is torsion-free. +-/ + +/-! +### Torsion-free groups +-/ + +/-- The definition of a torsion-free group. -/ +class TorsionFree (G : Type _) [Group G] where + /-- A group is *torsion-free* if the only element with non-trivial torsion is the + identity element. -/ + torsionFree : ∀ g : G, ∀ n : ℕ, g ^ n.succ = 1 → g = 1 + +/-- The definition of torsion-free additive groups. -/ +class AddTorsionFree (A : Type _) [AddGroup A] where + /-- An additive group is *torsion-free* if the only element with non-trivial torsion is + the identity element. -/ + torsionFree : ∀ a : A, ∀ n : ℕ, n.succ • a = 0 → a = 0 + +/-- ℤ is torsion-free, since it is an integral domain. -/ +instance : AddTorsionFree ℤ where + torsionFree := by + intro a n (h : n.succ * a = 0) + cases Int.mul_eq_zero.mp h with + | inl hyp => injection hyp; contradiction + | inr _ => assumption + +/-- The product of torsion-free additive groups is torsion-free. -/ +instance {A B : Type _} [AddGroup A] [AddGroup B] [AddTorsionFree A] + [AddTorsionFree B] : AddTorsionFree (A × B) where + torsionFree := by + intro (a, b) n + rw [show n.succ • (a, b) = (n.succ • a, n.succ • b) from rfl, + Prod.ext_iff, Prod.ext_iff] + intro ⟨_, _⟩; refine ⟨?_, ?_⟩ <;> + (apply AddTorsionFree.torsionFree; assumption) +/-! ### **Step 1:** Defining the square of an element of `P`. -/ + +/-- The function taking an element of `P` to its square, which lies in the kernel `K`. -/ +@[aesop norm unfold (rule_sets := [P]), reducible] +def _root_.LeanPool.Polylean.P.sq : P → K + | ((p, q, r), .e) => (p + p, q + q, r + r) + | ((_, q, _), .b) => (0, q + q + 1, 0) + | ((p, _, _), .a) => (p + p + 1, 0, 0) + | ((_, _, r), .c) => (0, 0, r + r + 1) + +open P + +/-- A proof that the function `sq` indeed takes an element of `P` to its square in `K`. -/ +@[aesop norm apply (rule_sets := [P]), simp] +theorem sq_square : ∀ g : P, g * g = (P.sq g, .e) + | ((p, q, r), .e) => by + refine (P.mul (p, q, r) (p, q, r) Q.e Q.e).trans ?_ + simp [P.sq, Q.e, action, cocycle] + | ((p, q, r), .a) => by + refine (P.mul (p, q, r) (p, q, r) Q.a Q.a).trans ?_ + simp [P.sq, Q.e, Q.a, action, cocycle] + | ((p, q, r), .b) => by + refine (P.mul (p, q, r) (p, q, r) Q.b Q.b).trans ?_ + simp [P.sq, Q.e, Q.b, action, cocycle] + | ((p, q, r), .c) => by + refine (P.mul (p, q, r) (p, q, r) Q.c Q.c).trans ?_ + simp [P.sq, Q.e, Q.c, action, cocycle] + +/-! ### **Step 2:** Proving that `K` (= `ℤ³`) is torsion-free. -/ + +/-- The kernel `ℤ³` is torsion-free. -/ +instance _root_.LeanPool.Polylean.K.torsionFree : AddTorsionFree K := inferInstance + +/-! ### **Step 3:** Showing that no element of `P` has order precisely two. -/ + +namespace Int + +/-! Some basic lemmas about integers needed to prove facts about `P`. -/ + +lemma add_twice_eq_mul_two {a : ℤ} : a + a = a * 2 := by + rw [show (2 : ℤ) = 1 + 1 by rfl, mul_add, mul_one] + +attribute [local simp] add_twice_eq_mul_two + +/-- No odd integer is zero. -/ +lemma odd_ne_zero : ∀ a : ℤ, ¬(a + a + 1 = 0) := by + omega + +/-- If the sum of an integer with itself is zero, then the integer is itself zero. -/ +lemma zero_of_twice_zero : ∀ a : ℤ, a + a = 0 → a = 0 := by + omega + +end Int + +/-- The only element of `P` with order dividing `2` is the identity. -/ +theorem square_free : ∀ {g : P}, g * g = (1 : P) → g = (1 : P) + | ((p, q, r), .e) => by + intro h + rw [sq_square] at h + change ((p + p, q + q, r + r), Q.e) = (((0, 0, 0) : K), Q.e) at h + injection h with hk _ + injection hk with hp hqr + injection hqr with hq hr + have hp0 := Int.zero_of_twice_zero p hp + have hq0 := Int.zero_of_twice_zero q hq + have hr0 := Int.zero_of_twice_zero r hr + rw [P.one] + simp [hp0, hq0, hr0] + | ((p, q, r), .a) => by + intro h + rw [sq_square] at h + change ((p + p + 1, 0, 0), Q.e) = (((0, 0, 0) : K), Q.e) at h + injection h with hk _ + injection hk with hp _ + exact False.elim (Int.odd_ne_zero p hp) + | ((p, q, r), .b) => by + intro h + rw [sq_square] at h + change ((0, q + q + 1, 0), Q.e) = (((0, 0, 0) : K), Q.e) at h + injection h with hk _ + injection hk with _ hqr + injection hqr with hq _ + exact False.elim (Int.odd_ne_zero q hq) + | ((p, q, r), .c) => by + intro h + rw [sq_square] at h + change ((0, 0, r + r + 1), Q.e) = (((0, 0, 0) : K), Q.e) at h + injection h with hk _ + injection hk with _ hqr + injection hqr with _ hr + exact False.elim (Int.odd_ne_zero r hr) + + +/-! ### **Step 4:** Showing square powers of torsion elements are trivial. -/ + +/-- If `g` is a torsion element of a group, then so is `g ^ 2`. -/ +lemma torsion_implies_square_torsion {G : Type _} [Group G] (g : G) (n : ℕ) + (g_tor : g ^ n = 1) : (g ^ 2) ^ n = 1 := + calc (g ^ 2) ^ n = g ^ (2 * n) := by rw [← pow_mul] + _ = g ^ (n * 2) := by rw [mul_comm] + _ = (g ^ n) ^ 2 := by rw [pow_mul] + _ = (1 : G) ^ 2 := by rw [← g_tor] + _ = (1 : G) := by rw [one_pow] + +/-! ### **Step 5:** Putting the facts together. -/ + +/-- `P` is torsion-free. -/ +instance _root_.LeanPool.Polylean.P.torsionFree : TorsionFree P where + torsionFree := by + intros g n g_tor -- assume `g` is a torsion element + -- then `g ^ 2` is also a torsion element + have square_tor : (g ^ 2) ^ n.succ = ((0, 0, 0), Q.e) := + torsion_implies_square_torsion g n.succ g_tor + erw [pow_two, sq_square, P.kernel_pow, Prod.mk.injEq] at square_tor + -- since `g ^ 2 = s g`, we have that `s g` is a torsion element + have s_tor : n.succ • (P.sq g) = 0 := square_tor.left + -- since `s g` lies in the kernel and the kernel is torsion-free, `s g = 0` + have square_zero : (P.sq g, Q.e) = (0, Q.e) := + congrArg (·, Q.e) (K.torsionFree.torsionFree (P.sq g) n s_tor) + rw [← sq_square] at square_zero + -- this means `g ^ 2 = e`, and also `g = e` because `P` has no order 2 elements + exact square_free square_zero + +end LeanPool.Polylean diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 8d2bc9c42b..7d230b0c59 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -444,3 +444,28 @@ projects: msc: - "11E25" - "11H06" + - slug: polylean + title: Polylean Unit Conjecture Infrastructure + summary: Vendors the verified Polylean infrastructure for Gardam's Unit Conjecture counterexample, including the Promislow group, group rings, and torsion-freeness of the group. + branch: algebra + entry_module: LeanPool.Polylean + authors: + - Siddhartha Gadgil + - Anand Rao + source: + url: https://github.com/siddhartha-gadgil/Polylean + github_repo: siddhartha-gadgil/Polylean + status: verified + main_declarations: + - LeanPool.Polylean.P.torsionFree + main_results: + - declaration: LeanPool.Polylean.P.torsionFree + informal: Proves that the Promislow group used in Gardam's construction is torsion-free. + tags: + - algebra + - group-theory + - ring-theory + - unit-conjecture + msc: + - "16S34" + - "20F65" From c7304a8c18445108e89036917af897c1266aa841 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 11:48:42 +0900 Subject: [PATCH 2/6] Restore polylean Gardam theorem --- LeanPool.lean | 1 + LeanPool/Polylean.lean | 4 +- LeanPool/Polylean/UnitConjecture.lean | 3 + .../UnitConjecture/GardamTheorem.lean | 232 ++++++++++++++++++ LeanPool/projects.yml | 7 +- 5 files changed, 243 insertions(+), 4 deletions(-) create mode 100644 LeanPool/Polylean/UnitConjecture/GardamTheorem.lean diff --git a/LeanPool.lean b/LeanPool.lean index 83fddf9176..b71fe8cb9b 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -180,6 +180,7 @@ import LeanPool.Polylean.UnitConjecture.Cocycle import LeanPool.Polylean.UnitConjecture.EnumDecide import LeanPool.Polylean.UnitConjecture.FreeModule import LeanPool.Polylean.UnitConjecture.GardamGroup +import LeanPool.Polylean.UnitConjecture.GardamTheorem import LeanPool.Polylean.UnitConjecture.GroupRing import LeanPool.Polylean.UnitConjecture.MetabelianGroup import LeanPool.Polylean.UnitConjecture.Tactics diff --git a/LeanPool/Polylean.lean b/LeanPool/Polylean.lean index 8228c431e4..c5ab0e5ba9 100644 --- a/LeanPool/Polylean.lean +++ b/LeanPool/Polylean.lean @@ -7,12 +7,12 @@ Authors: Siddhartha Gadgil, Anand Rao import LeanPool.Polylean.UnitConjecture /-! -# Polylean Unit Conjecture Infrastructure +# Polylean Unit Conjecture Counterexample Source: url:https://github.com/siddhartha-gadgil/Polylean Authors: Siddhartha Gadgil, Anand Rao Status: verified -Main declarations: `LeanPool.Polylean.P.torsionFree` +Main declarations: `LeanPool.Polylean.P.torsionFree`, `LeanPool.Polylean.Gardam.GardamTheorem` Tags: algebra, group-theory, ring-theory, unit-conjecture MSC: 16S34, 20F65 -/ diff --git a/LeanPool/Polylean/UnitConjecture.lean b/LeanPool/Polylean/UnitConjecture.lean index a712357fc4..23db25562c 100644 --- a/LeanPool/Polylean/UnitConjecture.lean +++ b/LeanPool/Polylean/UnitConjecture.lean @@ -6,6 +6,7 @@ Authors: Siddhartha Gadgil, Anand Rao import LeanPool.Polylean.UnitConjecture.TorsionFree import LeanPool.Polylean.UnitConjecture.GroupRing +import LeanPool.Polylean.UnitConjecture.GardamTheorem /-! # Polylean Unit Conjecture infrastructure @@ -20,6 +21,8 @@ Gardam proved that for a group `P` (the *Promislow* or *Hantzsche-Wendt* group), following: * `P` is torsion free; this is proved in [`TorsionFree.lean`](UnitConjecture/TorsionFree.html) +* `𝔽₂[P]` has a non-trivial unit, so Kaplansky's Unit Conjecture is false; + this is proved in [`GardamTheorem.lean`](UnitConjecture/GardamTheorem.html). The imported code constructs `P`, constructs group rings, and proves the required algebraic properties. diff --git a/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean b/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean new file mode 100644 index 0000000000..477a697de7 --- /dev/null +++ b/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean @@ -0,0 +1,232 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Algebra.Field.Basic +import Mathlib.Data.ZMod.Defs +import LeanPool.Polylean.UnitConjecture.TorsionFree +import LeanPool.Polylean.UnitConjecture.GroupRing + +namespace LeanPool.Polylean + + +/-! + +## Giles Gardam's result + +The proof of the theorem `𝔽₂[P]` has non-trivial units. Together with the main +result of `TorsionFree` -- that `P` is torsion-free, this completes the formal +proof of Gardam's theorem that Kaplansky's Unit Conjecture is false. +-/ + + +/-! ### Preliminaries -/ + +/-- An element of a free module is trivial but not zero if it is supported on one basis vector. -/ +def trivialNonZeroElem {R X : Type _} [Ring R] [DecidableEq X] [DecidableEq R] + (a : FreeModule R X) : Prop := + ∃! x : X, FreeModule.coordinates x a ≠ 0 + +/-- The statement of Kaplansky's Unit Conjecture: +The only units in a group ring, when the group is torsion-free and the ring is a field, +are the trivial units. -/ +def UnitConjecture : Prop := + ∀ {F : Type _} [Field F] [DecidableEq F] + {G : Type _} [Group G] [DecidableEq G] [TorsionFree G], + ∀ u : (F[G])ˣ, trivialNonZeroElem (u : F[G]) + +/-- The finite field on two elements. -/ +abbrev 𝔽₂ := Fin 2 + +instance : Field 𝔽₂ where + inv := id + exists_pair_ne := ⟨0, 1, by decide⟩ + mul_inv_cancel := fun + | 0 => by intro; contradiction + | 1 => by intro; rfl + inv_zero := rfl + div_eq_mul_inv := by decide + qsmul := _ + nnqsmul := _ + +instance ringElem : Coe P (𝔽₂[P]) where + coe g := ⟦[(1, g)]⟧ + +namespace P + +/-! +The main constants of the group `P`. +-/ + +/-- The first kernel generator of the Promislow group. -/ +abbrev x : P := (K.x, Q.e) +/-- The second kernel generator of the Promislow group. -/ +abbrev y : P := (K.y, Q.e) +/-- The third kernel generator of the Promislow group. -/ +abbrev z : P := (K.z, Q.e) +/-- The first nontrivial quotient generator of the Promislow group. -/ +abbrev a : P := ((0, 0, 0), Q.a) +/-- The second nontrivial quotient generator of the Promislow group. -/ +abbrev b : P := ((0, 0, 0), Q.b) + +end P + +namespace Gardam + +open P + +/-- Embed a group element as the corresponding basis element of `𝔽₂[P]`. -/ +private abbrev groupRingOf (g : P) : 𝔽₂[P] := + ⟦[(1, g)]⟧ + +/-- The group-ring multiplication, made explicit to avoid the monomial `HMul R G` notation. -/ +private abbrev ringMul (u v : 𝔽₂[P]) : 𝔽₂[P] := + GroupRing.mul u v + +/-- The `p` component of Gardam's non-trivial unit `α`. -/ +def p : 𝔽₂[P] := + (1 : 𝔽₂[P]) + groupRingOf x + groupRingOf y + groupRingOf (x * y) + + groupRingOf (z⁻¹) + groupRingOf (x * z⁻¹) + groupRingOf (y * z⁻¹) + + groupRingOf (x * y * z⁻¹) +/-- The `q` component of Gardam's non-trivial unit `α`. -/ +def q : 𝔽₂[P] := groupRingOf (x⁻¹ * y⁻¹) + groupRingOf x + groupRingOf (y⁻¹ * z) + + groupRingOf z +/-- The `r` component of Gardam's non-trivial unit `α`. -/ +def r : 𝔽₂[P] := (1 : 𝔽₂[P]) + groupRingOf x + groupRingOf (y⁻¹ * z) + + groupRingOf (x * y * z) +/-- The `s` component of Gardam's non-trivial unit `α`. -/ +def s : 𝔽₂[P] := (1 : 𝔽₂[P]) + groupRingOf (x * z⁻¹) + groupRingOf (x⁻¹ * z⁻¹) + + groupRingOf (y * z⁻¹) + groupRingOf (y⁻¹ * z⁻¹) + +/-- The non-trivial unit `α`. -/ +def α : 𝔽₂[P] := + p + ringMul q (groupRingOf a) + ringMul r (groupRingOf b) + + ringMul (ringMul s (groupRingOf a)) (groupRingOf b) + +/-- The `p'` component of the inverse `α'`. -/ +def p' : 𝔽₂[P] := + ringMul (groupRingOf (x⁻¹)) + (ringMul (ringMul (groupRingOf (a⁻¹)) p) (groupRingOf a)) +/-- The `q'` component of the inverse `α'`. -/ +def q' : 𝔽₂[P] := -ringMul (groupRingOf (x⁻¹)) q +/-- The `r'` component of the inverse `α'`. -/ +def r' : 𝔽₂[P] := -ringMul (groupRingOf (y⁻¹)) r +/-- The `s'` component of the inverse `α'`. -/ +def s' : 𝔽₂[P] := + ringMul (groupRingOf (z⁻¹)) + (ringMul (ringMul (groupRingOf (a⁻¹)) s) (groupRingOf a)) + +/-- The inverse `α'` of the non-trivial unit `α`. -/ +def α' : 𝔽₂[P] := + p' + ringMul q' (groupRingOf a) + ringMul r' (groupRingOf b) + + ringMul (ringMul s' (groupRingOf a)) (groupRingOf b) + +end Gardam + +/-! +### Verification + +The main verification of Giles Gardam's result. +-/ + +namespace Gardam + +open P + +/-- A proof that the unit is non-trivial. -/ +theorem α_nonTrivial : ¬ (trivialNonZeroElem α) := by + intro ⟨g, _, (eqg : ∀ y, α.coordinates y ≠ 0 → y = g)⟩ + have l₁ : z⁻¹ = g := by + apply eqg; decide + have l₂ : x * y = g := by + apply eqg; decide + have l₃ : z⁻¹ = x * y := by + exact Eq.trans l₁ l₂.symm + exact (by decide : z⁻¹ ≠ x * y) l₃ + +/-! The fact that the counter-example `α` is in fact a unit of the group ring `𝔽₂[P]` + is verified by computing the product of `α` with its inverse `α'` and checking that the + result is `(1 : 𝔽₂[P])`. + + The computational aspects of the group ring implementation and the Metabelian construction + are used here. -/ + +/-- A proof of the existence of a non-trivial unit in `𝔽₂[P]`. -/ +def Counterexample : {u : (𝔽₂[P])ˣ // ¬(trivialNonZeroElem u.val)} := + ⟨⟨α, α', by native_decide, by native_decide⟩, α_nonTrivial⟩ + +/-- Giles Gardam's result - Kaplansky's Unit Conjecture is false. -/ +theorem GardamTheorem : ¬ UnitConjecture := + fun conjecture => Counterexample.prop <| + conjecture (F := 𝔽₂) (G := P) Counterexample.val + +end Gardam + +/-! +We check that our definition of "trivial but not zero" is correct by showing it equivalent +to a more direct definition. +-/ + +theorem trivialNonZeroElem_trivial_nonzeroAux {R G : Type _} [Ring R] [Group G] + [DecidableEq G] [DecidableEq R] (p : FormalSum R G) : + trivialNonZeroElem ⟦p⟧ ↔ ∃ a: R, ∃ g : G, p ≈ [(a, g)] ∧ (a ≠ 0) := by + apply Iff.intro + · rw [trivialNonZeroElem] + intro ⟨x, hyp⟩ + let ⟨hyp₁, hyp₂⟩ := hyp + use FreeModule.coordinates x ⟦p⟧ + use x + apply And.intro + · funext x₁ + simp only [FormalSum.coords, monomCoeff, FreeModule.coordinates, Quotient.lift_mk, add_zero] + by_cases h:x = x₁ + · simp [h] + · let hyp₃ := hyp₂ x₁ + simp only [FreeModule.coordinates, ne_eq] at hyp₃ + let neqLem : ((x == x₁) = false) := + by apply beq_false_of_ne; assumption + simp only [neqLem] + by_cases h:FormalSum.coords p x₁ = 0 + · assumption + · simp only [Quotient.lift_mk, h, not_false_iff, forall_true_left] at hyp₃ + have := Eq.symm hyp₃ + contradiction + · assumption + · intro ⟨a, g, hyp⟩ + simp only [trivialNonZeroElem, ne_eq] + use g + apply And.intro + · intro h + simp only [FreeModule.coordinates, Quotient.lift_mk] at h + have : p.coords = FormalSum.coords [(a, g)] := hyp.left + rw [this] at h + simp only [FormalSum.coords, monomCoeff, beq_self_eq_true, add_zero] at h + have := hyp.right + contradiction + · intro x h + simp only [FreeModule.coordinates, Quotient.lift_mk] at h + have : p.coords = FormalSum.coords [(a, g)] := hyp.left + rw [this] at h + simp only [FormalSum.coords, monomCoeff, add_zero] at h + by_cases c:x = g + · assumption + · have neq : (g == x) = false := by aesop + simp only [neq, not_true] at h + +/-- Triviality of `p : R[G]` coincides with the direct definition `p = a ⬝ g`, `a ≠ 0`. -/ +theorem trivialNonZeroElem_trivial_nonzero {R G : Type _} [Ring R] [Group G] + [DecidableEq G] [DecidableEq R] : + ∀ (p : FreeModule R G), + trivialNonZeroElem p ↔ ∃ a: R, ∃ g : G, p = (a * g) ∧ (a ≠ 0) := by + rw [groupRingMul] + apply Quotient.ind + simp only [trivialNonZeroElem_trivial_nonzeroAux] + conv => + enter [a, 2, 1, a, 1, g, 1] + rw [Quotient.eq] + intro a + rfl + +end LeanPool.Polylean diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 7d230b0c59..9e71bd5568 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -445,8 +445,8 @@ projects: - "11E25" - "11H06" - slug: polylean - title: Polylean Unit Conjecture Infrastructure - summary: Vendors the verified Polylean infrastructure for Gardam's Unit Conjecture counterexample, including the Promislow group, group rings, and torsion-freeness of the group. + title: Polylean Unit Conjecture Counterexample + summary: Formalizes Gardam's counterexample to Kaplansky's Unit Conjecture, including the Promislow group, group rings, torsion-freeness of the group, and the non-trivial unit in 𝔽₂[P]. branch: algebra entry_module: LeanPool.Polylean authors: @@ -458,9 +458,12 @@ projects: status: verified main_declarations: - LeanPool.Polylean.P.torsionFree + - LeanPool.Polylean.Gardam.GardamTheorem main_results: - declaration: LeanPool.Polylean.P.torsionFree informal: Proves that the Promislow group used in Gardam's construction is torsion-free. + - declaration: LeanPool.Polylean.Gardam.GardamTheorem + informal: Proves Gardam's counterexample to Kaplansky's Unit Conjecture by constructing a non-trivial unit in the group ring 𝔽₂[P]. tags: - algebra - group-theory From 05759bbfb78da7498be2ffc9de548393bbac9b0b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 12:54:42 +0900 Subject: [PATCH 3/6] Replace Gardam native decide proofs --- LeanPool/Polylean/UnitConjecture/GardamTheorem.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean b/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean index 477a697de7..ad93d6e9ca 100644 --- a/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean +++ b/LeanPool/Polylean/UnitConjecture/GardamTheorem.lean @@ -153,9 +153,17 @@ theorem α_nonTrivial : ¬ (trivialNonZeroElem α) := by The computational aspects of the group ring implementation and the Metabelian construction are used here. -/ +/-- The product of Gardam's unit and its inverse is one. -/ +theorem α_mul_α' : ringMul α α' = (1 : 𝔽₂[P]) := by + decide +kernel + +/-- The product of Gardam's inverse and its unit is one. -/ +theorem α'_mul_α : ringMul α' α = (1 : 𝔽₂[P]) := by + decide +kernel + /-- A proof of the existence of a non-trivial unit in `𝔽₂[P]`. -/ def Counterexample : {u : (𝔽₂[P])ˣ // ¬(trivialNonZeroElem u.val)} := - ⟨⟨α, α', by native_decide, by native_decide⟩, α_nonTrivial⟩ + ⟨⟨α, α', α_mul_α', α'_mul_α⟩, α_nonTrivial⟩ /-- Giles Gardam's result - Kaplansky's Unit Conjecture is false. -/ theorem GardamTheorem : ¬ UnitConjecture := From f65b963c8de08299ef16d58c2dfbf2618404af98 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 17:35:18 +0900 Subject: [PATCH 4/6] Add Polylean graph paths --- LeanPool.lean | 1 + LeanPool/Polylean.lean | 1 + LeanPool/Polylean/Complexes/GraphPaths.lean | 479 ++++++++++++++++++++ 3 files changed, 481 insertions(+) create mode 100644 LeanPool/Polylean/Complexes/GraphPaths.lean diff --git a/LeanPool.lean b/LeanPool.lean index b71fe8cb9b..1f978f9dd8 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -174,6 +174,7 @@ import LeanPool.LatticeTriangle.Solution import LeanPool.PartialRegularity import LeanPool.PartialRegularity.Extension import LeanPool.Polylean +import LeanPool.Polylean.Complexes.GraphPaths import LeanPool.Polylean.UnitConjecture import LeanPool.Polylean.UnitConjecture.AddFreeGroup import LeanPool.Polylean.UnitConjecture.Cocycle diff --git a/LeanPool/Polylean.lean b/LeanPool/Polylean.lean index c5ab0e5ba9..64d6fec091 100644 --- a/LeanPool/Polylean.lean +++ b/LeanPool/Polylean.lean @@ -5,6 +5,7 @@ Authors: Siddhartha Gadgil, Anand Rao -/ import LeanPool.Polylean.UnitConjecture +import LeanPool.Polylean.Complexes.GraphPaths /-! # Polylean Unit Conjecture Counterexample diff --git a/LeanPool/Polylean/Complexes/GraphPaths.lean b/LeanPool/Polylean/Complexes/GraphPaths.lean new file mode 100644 index 0000000000..6ebb0338d0 --- /dev/null +++ b/LeanPool/Polylean/Complexes/GraphPaths.lean @@ -0,0 +1,479 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Algebra.Group.Basic +import Mathlib.Algebra.Group.Defs + +namespace LeanPool.Polylean + +/-- A graph with directed edges, distinguished null edge, and edge reversal. -/ +structure Graph(V: Type) (E: Type) where + /-- The distinguished null edge. -/ + null : E + /-- The initial vertex of an edge. -/ + init : E → V + /-- The reverse of an edge. -/ + bar : E → E + barInv : bar ∘ bar = id + barNoFP : ∀ e: E, bar e ≠ e + +variable {V : Type} {E : Type} {x₁ x₂ : V} + + +/-- The terminal vertex of an edge, defined as the initial vertex of its reverse. -/ +@[inline] def term (graph: Graph V E): E → V := + fun e => graph.init (graph.bar e) + +/-- Edge paths in a graph, indexed by their initial and terminal vertices. -/ +inductive EdgePath (graph: Graph V E): V → V → Type where + | single : (x: V) → EdgePath graph x x + | cons : {x y z : V} → (e : E) → graph.init e = x → term graph e = y → + EdgePath graph y z → EdgePath graph x z + +namespace EdgePath + +/-- The number of edges in an edge path. -/ +def length {graph: Graph V E}{x y: V}: EdgePath graph x y → Nat + | EdgePath.single x => 0 + | EdgePath.cons _ _ _ path => length path + 1 + +end EdgePath + +/--proves that bar is an involution-/ +theorem bar_involution {G : Graph V E} : (ex : E) → G.bar (G.bar ex) = ex := by + intro ex + apply congr G.barInv (Eq.refl ex) + + +open EdgePath + +/-- concatenates two edgepaths -/ +def multiply {G : Graph V E} {x y z : V}: (EdgePath G x y) → (EdgePath G y z) → (EdgePath G x z) := by +intro p q +match p with +| single x => exact q +| cons ex h1 h2 exy => exact (cons ex h1 h2 (multiply exy q)) + + +/--proves that the endpoint of the reverse of an edge is the start point of the edge-/ +theorem term_bar_equals_init {G : Graph V E} {x : V}{e : E}: G.init e = x → (term G (G.bar e) = x) := +by +intro h +have h₁ : G.bar (G.bar e) = e := congr G.barInv (Eq.refl e) +have h₂ : G.init (G.bar (G.bar e)) = G.init e := congrArg G.init h₁ +apply Eq.trans h₂ h + +/--proves that initial vertex of reversed edge is the terminal vertex of the original edge-/ +theorem init_bar_equals_term {G : Graph V E} {x :V} {e : E}: (term G e = x) → G.init (G.bar e) = x:= by +intro hyp +have : G.init (G.bar e) = term G e := by rfl +exact Eq.trans this hyp + +/-- proves associativity of path multiplication-/ +theorem mult_assoc {G : Graph V E} (p : EdgePath G w x) (q : EdgePath G x y) (r : EdgePath G y z): + (multiply (multiply p q) r) = (multiply p (multiply q r)) := by + induction p with + | single w => simp[multiply] + | cons ex h1 h2 exy ih => simp[multiply, ih] + +/--proves that "single x" is an identity element for multiplication-/ +theorem mult_const {G : Graph V E} (p : EdgePath G x y) : + (multiply p (single y)) = p := by + induction p with + | single x => simp [multiply] + | cons ex h1 h2 exy ih => simp[multiply, ih] + +/-- reverses an edgepath-/ +def inverse {G : Graph V E} {x y : V}: (EdgePath G x y) → (EdgePath G y x) +| single x => single x +| cons ex h₁ h₂ exy => multiply (inverse exy) (cons (G.bar (ex)) h₂ (term_bar_equals_init h₁) (single x)) + + +/--defines an edgepath with a single edge-/ +def basicpath {G : Graph V E} (x : V) (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y): EdgePath G x y := cons ex h₁ h₂ (single y) + +/--proves that multiplication with a basicpath gives inductive definition of edgepath-/ +theorem basicpath_mult {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : multiply (basicpath x ex h₁ h₂) exy = cons ex h₁ h₂ exy := by + simp[basicpath, multiply] + +/--defines inverse in terms of basicpath-/ +theorem inverse_lemma {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : inverse (cons ex h₁ h₂ exy) = multiply (inverse exy) (basicpath y (G.bar ex) h₂ (term_bar_equals_init h₁) ) := by rfl + + +/--proves the basic relation between inverse and multiply-/ +theorem inverse_mult {G : Graph V E} (x y z : V) (p : EdgePath G x y) (q : EdgePath G y z) : + inverse (multiply p q) = multiply (inverse q) (inverse p) := by + induction p with + | single x => + have p₁ : multiply (single x) q = q := by rfl + rw[p₁] + have p₂ : @inverse V E G x x (single x) = single x := by simp[inverse] + rw[p₂] + rw[mult_const (inverse q)] + | cons ex t₁ t₂ exy ih => + have p₃ : multiply (cons ex t₁ t₂ exy) q = cons ex t₁ t₂ (multiply exy q) := by simp[mult_assoc, basicpath_mult, multiply] + rw[p₃] + have p₄ : inverse (cons ex t₁ t₂ exy) = multiply (inverse exy) (basicpath _ (G.bar ex) t₂ (term_bar_equals_init t₁)) := by simp[inverse_lemma] + rw[p₄] + have p₅ : multiply (inverse q) (inverse exy) = inverse ( multiply exy q) := by simp[ih q] + let p₆ := inverse_lemma ex t₁ t₂ (multiply exy q) + rw[p₆] + simp[Eq.symm (p₅), mult_assoc] + + +/--proves that inverse is an involution on paths-/ +theorem inverse_involution {G : Graph V E} {x y : V} (p : EdgePath G x y) : inverse (inverse p) = p := by + induction p with + | single x => rfl + | cons ex h₁ h₂ exy ih => + have p₁ : inverse (cons ex h₁ h₂ exy) = multiply (inverse exy) (inverse (basicpath _ ex h₁ h₂)) := by rfl + rw[p₁] + let k := inverse_mult _ _ _ (inverse exy) (inverse (basicpath _ ex h₁ h₂)) + rw[k] + have p₂ : inverse (inverse (basicpath _ ex h₁ h₂)) = basicpath _ ex h₁ h₂ := by + simp[basicpath, inverse] + have p₃ : G.bar (G.bar ex) = ex := by apply congr G.barInv (Eq.refl ex) + simp only [p₃, inverse, multiply] + rw[p₂] + simp[basicpath_mult ex h₁ h₂ exy, ih] + + + +/--helper function for reducePath, that reduces the first two edges of the path-/ +def reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : { rp : EdgePath G x z // rp.length ≤ (cons ex h₁ h₂ exy).length} := by +cases exy with + | single x => exact ⟨cons ex h₁ h₂ (single y), by simp⟩ + | cons ey h₃ h₄ eyz => + apply + if c : (x = term G ey) ∧ (ey = G.bar (ex)) then + ⟨ Eq.symm (Eq.trans (And.left c) h₄) ▸ eyz, by + have h₅ : (Eq.symm (Eq.trans (And.left c) h₄) ▸ eyz).length = eyz.length := by + let ih := Eq.symm (Eq.trans (And.left c) h₄) + cases ih with + | refl => rfl + simp[EdgePath.length, h₅, Nat.le_trans (Nat.le_succ (length eyz)) (Nat.le_succ (length eyz +1))] + ⟩ + else + ⟨ cons ex h₁ h₂ (cons ey h₃ h₄ (eyz)), by apply Nat.le_refl⟩ + + +/-- reduces given path such that no two consecutive edges are inverses of each other-/ +def reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} : (p : EdgePath G x y ) → + {rp : EdgePath G x y // rp.length ≤ p.length} +| single x => ⟨single x, by simp⟩ +| cons ex h₁ h₂ ey'y => + let ⟨ey'z, ih1⟩ := reducePath ey'y + let ⟨ ez, ih⟩ := reducePathAux ex h₁ h₂ ey'z + ⟨ ez , by + have : length (cons ex h₁ h₂ ey'z) = length ey'z + 1 := by simp[length] + let k := this ▸ ih + have pr : length ey'z +1 ≤ length ey'y +1 := by apply Nat.succ_le_succ ih1 + simp[length, Nat.le_trans k pr] ⟩ + + termination_by p => p.length + decreasing_by + simp_wf + simp[EdgePath.length, Nat.lt_succ_self] + + +/--defines moves allowing homotopy of edgepaths-/ +inductive basicht {G : Graph V E} : EdgePath G x y → EdgePath G x y → Prop where + | consht : (x : V) → (basicht (single x) (single x)) -- constant homotopy + | cancel : (ex ex' : E) → { x w y : V} → (p : EdgePath G x y) → -- cancelling consecutive opposite edges from a path + (h : G.init ex = x) → (h' : term G ex = w) → (t : G.bar ex = ex') → + basicht p (cons ex h h' (cons ex' (t ▸ init_bar_equals_term h') (t ▸ term_bar_equals_init h) p)) + | mult : {x y z : V} → {p q : EdgePath G y z} → -- adding an edge to homotopic paths + basicht p q → (ex : E) →(h' : G.init ex = x) → ( h : term G ex = y)→ + basicht (cons ex h' h p) (cons ex h' h q) + + +/-- The set of homotopy classes of edge paths from `x` to `y`. -/ +def ht (G : Graph V E) (x y : V) := Quot (@basicht V E G x y ) + +/-- The homotopy class of an edge path. -/ +def htclass {G : Graph V E} {x y : V} ( p : EdgePath G x y) : ht G x y := + Quot.mk (@basicht V E G x y ) p + +/-- Homotopy of edge paths as equality of their quotient classes. -/ +def homotopy {G : Graph V E} {x y : V} ( p' q' : EdgePath G x y) : Prop := + htclass p' = htclass q' + + +/--proves that homotopy is a transitive relation-/ +theorem homotopy_trans {G : Graph V E} {x y : V} (p q r : EdgePath G x y) : homotopy p q → homotopy q r → homotopy p r := by + intro h₁ h₂ + simp[homotopy, htclass] + have p₁ : Quot.mk basicht p = Quot.mk basicht q := by apply h₁ + have p₂ : Quot.mk basicht q = Quot.mk basicht r := by apply h₂ + apply Eq.trans p₁ p₂ + + +/--proves that homotopy is preserved by multiplying an edge to the left-/ +theorem homotopy_left_mult_edge {G : Graph V E} {x y z : V}: (p q : EdgePath G y z) → homotopy p q → (ex : E) →(h1 : G.init ex = x) → ( h : term G ex = y)→ homotopy (cons ex h1 h p) (cons ex h1 h q) := by + intro p q h ex h1 h2 + let func (r : EdgePath G y z) : ht G x z := htclass (cons ex h1 h2 r) + have g : (r₁ r₂ : EdgePath G y z) → basicht r₁ r₂ → func r₁ = func r₂ := by + intro r₁ r₂ h₁ + let t := basicht.mult h₁ ex h1 h2 + have : htclass (cons ex h1 h2 r₁) = htclass (cons ex h1 h2 r₂) := by simp[htclass]; apply Quot.sound t + exact this + simp[homotopy] + let k := Quot.lift func g + apply congrArg k h + + +/--proves that homotopy is left multiplicative-/ +theorem homotopy_left_mult {G : Graph V E} {x y z : V} (p1 p2 : EdgePath G y z) (q : EdgePath G x y) (h :homotopy p1 p2): + (homotopy (multiply q p1) (multiply q p2)) := by + induction q with + | single w => + simp [multiply, h] + | cons ex h1 h2 exy ih => + let c := ih p1 p2 h + have t₁ : multiply (cons ex h1 h2 exy) p1 = cons ex h1 h2 (multiply exy p1) := by simp[multiply, mult_assoc] + have t₂ : multiply (cons ex h1 h2 exy) p2 = cons ex h1 h2 (multiply exy p2) := by simp[multiply, mult_assoc] + rw[t₁, t₂] + simp[homotopy_left_mult_edge, c] + + +/--proves that homotopy is reflexive-/ +theorem homotopy_rfl {G :Graph V E} {x y : V} (p : EdgePath G x y) : homotopy p p := by rfl + + +/--proves that path is homotopic to itself after appending cancelling pair of edges at its end-/ +theorem induct_homotopy_inverse_cancel {G : Graph V E} (ey ey' : E) { x w y : V} (p : EdgePath G x y) (h₁ : G.init ey = y) (h₂ : term G ey = w) (t : G.bar ey = ey') (h₃ : G.init ey' = w) (h₄ : term G ey' = y) : + homotopy p (multiply p (cons ey h₁ h₂ (cons ey' h₃ h₄ (single y)) )) := by + induction p with + | single x => simp[multiply, basicpath, homotopy, htclass, Quot.sound (basicht.cancel ey ey' (single x) h₁ h₂ t)] + | cons ex t₁ t₂ exy ih => + let x := ih h₁ h₄ + have p₁ : homotopy (cons ex t₁ t₂ exy) (cons ex t₁ t₂ (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))))) := by simp[homotopy_left_mult_edge _ _ x ex t₁ t₂] + have : cons ex t₁ t₂ (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _)))) = multiply (cons ex t₁ t₂ exy) (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))) := by simp[multiply] + exact this ▸ p₁ + + +/--proves that a pair of paths remains homotopic after appending a single edge at their ends-/ +theorem induct_homotopy_inverse_mult {G : Graph V E} {x y z : V} (p q : EdgePath G x y) (ey : E) (h₁ : G.init ey = y) (h₂ : term G ey = z) : homotopy p q → homotopy (multiply p (basicpath y ey h₁ h₂)) (multiply q (basicpath y ey h₁ h₂)) := by + intro h + let func : EdgePath G x y → ht G x z := by intro p; exact htclass (multiply p (basicpath y ey h₁ h₂)) + have g : (s₁ s₂ : EdgePath G x y) → (basicht s₁ s₂) → func s₁ = func s₂ := by + intro s₁ s₂ ht + induction ht with + | consht x => simp[homotopy_rfl] + | cancel ex ex' r t₁ t₂ t₃ => + let x := basicht.cancel ex ex' (multiply r (basicpath _ ey h₁ h₂)) t₁ t₂ t₃ + exact Quot.sound x + | @mult _ _ _ p₁ p₂ b ex t₁ t₂ ih => + let x := homotopy_left_mult_edge _ _ (ih p₁ p₂ h₁ (Quot.sound b)) ex t₁ t₂ + exact x + simp[homotopy] + let k := Quot.lift func g + apply congrArg k h + + +/--proves that homotopy of paths implies homotopy of their inverses-/ +theorem homotopy_inverse {G : Graph V E} {x y : V} (p₁ p₂: EdgePath G x y) (q₁ q₂ : EdgePath G y x) (h₁ : q₁ = inverse p₁) (h₂ : q₂ = inverse p₂) : homotopy p₁ p₂ → homotopy q₁ q₂ := by + intro h₀ + let func : EdgePath G x y → ht G y x := by intro p; exact htclass (inverse p) + have g : (s₁ s₂ : EdgePath G x y) → (h : basicht s₁ s₂) → homotopy (inverse s₁) (inverse s₂) := by + intro s₁ s₂ h + induction h with + | consht x => simp[inverse, homotopy_rfl] + + | cancel ex ex' p t₁ t₂ t₃ => + simp[htclass, inverse, mult_assoc] + apply induct_homotopy_inverse_cancel (G.bar ex') (G.bar ex) (inverse p) (by rw[← t₃]; rw[bar_involution ex]; apply t₁) (by rw[← t₃]; rw[(bar_involution ex)]; apply t₂) (by rw[bar_involution ex']; apply (Eq.symm t₃)) (init_bar_equals_term t₂) (term_bar_equals_init t₁) + + | @mult _ _ _ s₁ s₂ b ex t₁ t₂ ih => + simp[homotopy, inverse] + let c := ih s₁ s₂ (inverse s₁) (inverse s₂) rfl rfl (Quot.sound b) + let k := induct_homotopy_inverse_mult (inverse s₁) (inverse s₂) (G.bar ex) t₂ (term_bar_equals_init t₁) c + apply k + let k₂ := Quot.lift func g + rw [h₁, h₂] + exact congrArg k₂ h₀ + + +/--homotopy_inverse with lesser arguments-/ +theorem homotopy_inverse_quick {G : Graph V E} {x y : V} {p₁ p₂: EdgePath G x y} : homotopy p₁ p₂ → homotopy (inverse p₁) (inverse p₂) := by + apply homotopy_inverse p₁ p₂ (inverse p₁) (inverse p₂) rfl rfl + + +/-- proves that homotopy is right multiplicative-/ +theorem homotopy_right_mult {G : Graph V E} {x y z : V} (p₁ p₂ : EdgePath G x y) (q : EdgePath G y z) (h :homotopy p₁ p₂): + (homotopy (multiply p₁ q) (multiply p₂ q)) := by + have r₁ : homotopy (inverse p₁) (inverse p₂) := by apply homotopy_inverse_quick h + have r₂ : homotopy (multiply (inverse q) (inverse p₁)) (multiply (inverse q) (inverse p₂)) := by apply homotopy_left_mult; apply r₁ + have r₃ : homotopy (inverse (multiply (inverse q) (inverse p₁))) (inverse (multiply (inverse q) (inverse p₂))) := by apply homotopy_inverse_quick r₂ + let s₁ := inverse_mult x y z p₁ q + let s₂ := inverse_involution (multiply p₁ q) + let s₃ := Eq.trans (Eq.symm s₂) (congrArg inverse s₁) + let t₁ := inverse_mult x y z p₂ q + let t₂ := inverse_involution (multiply p₂ q) + let t₃ := Eq.trans (Eq.symm t₂) (congrArg inverse t₁) + apply s₃ ▸ t₃ ▸ r₃ + + +/--defines multiplication of homotopy class with a path to its left-/ +def homotopy_left_multiplication {G :Graph V E} {x y z : V} (p₁ : EdgePath G x y) : ht G y z → ht G x z := by + let func: EdgePath G y z → ht G x z := by intro p; exact htclass (multiply p₁ p) + have g : (q₁ q₂ : EdgePath G y z) → basicht q₁ q₂ → func q₁ = func q₂ := by + intro q₁ q₂ h + have h' : homotopy q₁ q₂ := by simp[homotopy, htclass, Quot.sound h ] + apply homotopy_left_mult q₁ q₂ p₁ h' + apply Quot.lift func g + + +/--proves that the multiplication defined above equals homotopy class of multiplied paths -/ +theorem homotopy_left_multiplication_class {G :Graph V E} {x y z : V} (p₁ : EdgePath G x y) (p₂ : EdgePath G y z): homotopy_left_multiplication p₁ (htclass p₂) = htclass (multiply p₁ p₂) := by + simp[htclass, homotopy_left_multiplication] + + +/--defines multiplication of homotopy-/ +def homotopy_multiplication : ht G x y → ht G y z → ht G x z := by + intro p₁ p₂ + let func (p : EdgePath G x y) : ht G x z := homotopy_left_multiplication p p₂ + have g : (q₁ q₂ : EdgePath G x y) → basicht q₁ q₂ → func q₁ = func q₂ := by + intro q₁ q₂ h + let crop (p : ht G y z) : Prop := homotopy_left_multiplication q₁ p = homotopy_left_multiplication q₂ p + have g' : (p : ht G y z) → crop p := by + intro p + have g'' : (p' : EdgePath G y z) → crop (htclass p') := by + intro p' + have h' : homotopy q₁ q₂ := by simp[homotopy, htclass, Quot.sound h] + have : htclass (multiply q₁ p') = htclass (multiply q₂ p') := by + exact homotopy_right_mult q₁ q₂ p' h' + exact this + apply Quot.ind g'' + let hh := g' p₂ + exact hh + let k := (Quot.lift (fun x => func x) g) + apply k p₁ + + +/-- Multiplication of homotopy classes of composable edge paths. -/ +infixl: 65 " # " => homotopy_multiplication + + +/--proves that # is associative up to multiplication by a pair of paths and one homotopy class-/ +theorem homotopy_mult_path_path_assoc {G :Graph V E} {w x y z : V} (p : EdgePath G w x) (q : EdgePath G x y): (r : ht G y z) → (htclass (multiply p q)) # r = (htclass p) # ((htclass q) # r) := by + apply Quot.ind + intro b + simp[htclass, homotopy_multiplication] + have p₁ : homotopy_left_multiplication (multiply p q) (Quot.mk basicht b) = htclass ( multiply (multiply p q) b) := by rfl + have p₂ : (homotopy_left_multiplication q (Quot.mk basicht b)) = htclass (multiply q b) := by rfl + have p₃ : (homotopy_left_multiplication p (homotopy_left_multiplication q (Quot.mk basicht b))) = htclass (multiply p (multiply q b)) := by rw[p₂]; rfl + rw[p₁,p₃] + simp[mult_assoc] + + +/--proves that # is associative up to multiplication by one path and a pair of homotopy classes -/ +theorem homotopy_mult_path_assoc {G :Graph V E} {w x y z : V} (p : EdgePath G w x) (r : ht G y z): (q : ht G x y) → (htclass p # q) # r = (htclass p) # (q # r) := by + apply Quot.ind + intro a + simp[htclass] + have p₁ : Quot.mk basicht p # Quot.mk basicht a = htclass (multiply p a) := by rfl + rw[p₁] + apply homotopy_mult_path_path_assoc p a r + +/--proves that # is associative on homotopy classes-/ +theorem homotopy_mult_assoc {G :Graph V E} {w x y z : V} (b : ht G x y) (c : ht G y z) : (a : ht G w x) → ((a # b) # c ) = (a # (b # c) ) := by + apply Quot.ind + intro a + apply homotopy_mult_path_assoc a c b + + + +/--proves that reducePathAux preserves the homotopy class-/ +theorem homotopy_reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : homotopy (cons ex h₁ h₂ exy) (reducePathAux ex h₁ h₂ exy) := by + simp[homotopy, htclass] + cases exy with + | single y => + have : reducePathAux ex h₁ h₂ (single y) = cons ex h₁ h₂ (single y) := by rfl + rfl + | cons ey h₃ h₄ eyz => + by_cases c : (x = term G ey) ∧ (ey = G.bar (ex)) + · + let ih := Eq.symm (Eq.trans (And.left c) h₄) + cases ih with + |refl => + have : basicht (ih ▸ eyz) (cons ex h₁ h₂ (cons ey h₃ h₄ eyz)) := by + let j := @basicht.cancel V E G ex ey x y _ (ih ▸ eyz) h₁ h₂ (Eq.symm c.2) + apply j + have pr : (reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz)).1 = (ih ▸ eyz) := by simp[reducePathAux, c] + let k := Quot.sound (Eq.symm pr ▸ this) + exact (Eq.symm k) + · + have : reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz) = cons ex h₁ h₂ (cons ey h₃ h₄ (eyz)) := by simp[reducePathAux, c] + simp [this] + +/--proves that reducePath preserves the homotopy class-/ +theorem homotopy_reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y : V} (p₁ : EdgePath G x y): homotopy p₁ (reducePath p₁) := by + induction p₁ with + | single x => + simp [homotopy, htclass, reducePath] + + | cons ex h₁ h₂ exy ih' => + let p₃ := reducePath exy + let q := p₃.1 + let p₄ := reducePathAux ex h₁ h₂ q + have : p₄.1 = (reducePath (cons ex h₁ h₂ exy)).1 := by + simp [reducePath, p₃, q, p₄] + have t₁ : homotopy (cons ex h₁ h₂ q) (p₄.1) := by apply homotopy_reducePathAux ex h₁ h₂ q + have t₂ : homotopy exy q := by apply ih' + have t₃ : homotopy (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) := by apply homotopy_left_mult_edge exy q t₂ ex h₁ h₂ + apply homotopy_trans (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) (reducePath (cons ex h₁ h₂ exy)) t₃ (this ▸ t₁) + + + + + +instance ht_mul {G : Graph V E} {x : V} : Mul (ht G x x) where +mul : ht G x x → ht G x x → ht G x x := fun a b => homotopy_multiplication a b + +--defines the identity homotopy class +instance ht_one {G : Graph V E} {x : V} : One (ht G x x) where +one : ht G x x := htclass (single x) + +/--proves that multiplication of homotopy classes is associative-/ +theorem ht_mult_assoc {G : Graph V E} {x : V} (a b c : ht G x x) : ((a # b) # c) = (a # ( b # c)) := by +let k := @homotopy_mult_assoc V E G x x x x +let l (a b c : ht G x x) := k b c a +apply (l a b c) + +/--proves that the identity homotopy class is the right multiplicative identity-/ +theorem ht_right_identity {G : Graph V E} {x : V} : (a₀ : ht G x x) → ht_mul.mul a₀ (@ht_one V E G x).one = a₀ := by +have k (b : EdgePath G x x) : homotopy_multiplication (htclass b) (htclass (single x)) = (htclass b) := by + let l :=mult_const b ▸ homotopy_left_multiplication_class b (single x) + have : (htclass b) # (htclass (single x)) = homotopy_left_multiplication b (htclass (single x)) := by rfl + apply Eq.trans this l +have k₂ (b : EdgePath G x x) : ht_mul.mul (htclass b) (@ht_one V E G x).one = htclass b := by + apply k +apply Quot.ind +apply k₂ + +/--proves that the identity homotopy class is the left multiplicative identity-/ +theorem ht_left_identity {G : Graph V E} {x : V} : (a₀ : ht G x x) → ht_mul.mul (@ht_one V E G x).one a₀ = a₀ := by +have k (b : EdgePath G x x) : homotopy_multiplication (htclass (single x)) (htclass b) = (htclass b) := by + exact homotopy_left_multiplication_class (single x) b +have k₂ (b : EdgePath G x x) : ht_mul.mul (@ht_one V E G x).one (htclass b) = htclass b := by + apply k +apply Quot.ind +apply k₂ + +instance ht_semigroup {G : Graph V E} {x : V} : Semigroup (ht G x x) where +mul := (@ht_mul V E G x).mul +mul_assoc := by apply ht_mult_assoc + +/-- The monoid structure on loops at a vertex modulo homotopy. -/ +@[reducible] def ht_monoid (G : Graph V E) (x : V) : Monoid (ht G x x) where + mul := (· # ·) + mul_assoc := ht_mult_assoc + one := htclass (single x) + one_mul := ht_left_identity + mul_one := ht_right_identity + +end LeanPool.Polylean From 7ce8ee52861976b4077bfbf5a4b5ca819d3fe121 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 18:06:18 +0900 Subject: [PATCH 5/6] Add remaining Polylean importable modules --- LeanPool.lean | 8 + LeanPool/Polylean.lean | 8 + .../Complexes/Structures/Category.lean | 120 +++++++++++ .../Complexes/Structures/Groupoid.lean | 110 ++++++++++ .../Polylean/Complexes/Structures/Quiver.lean | 185 +++++++++++++++++ LeanPool/Polylean/ConjInvLength/Length.lean | 140 +++++++++++++ .../Polylean/ConjInvLength/LengthBound.lean | 99 +++++++++ .../Polylean/ConjInvLength/MemoLength.lean | 38 ++++ .../Polylean/ConjInvLength/ProvedBound.lean | 194 ++++++++++++++++++ LeanPool/Polylean/ConjInvLength/WordTree.lean | 133 ++++++++++++ 10 files changed, 1035 insertions(+) create mode 100644 LeanPool/Polylean/Complexes/Structures/Category.lean create mode 100644 LeanPool/Polylean/Complexes/Structures/Groupoid.lean create mode 100644 LeanPool/Polylean/Complexes/Structures/Quiver.lean create mode 100644 LeanPool/Polylean/ConjInvLength/Length.lean create mode 100644 LeanPool/Polylean/ConjInvLength/LengthBound.lean create mode 100644 LeanPool/Polylean/ConjInvLength/MemoLength.lean create mode 100644 LeanPool/Polylean/ConjInvLength/ProvedBound.lean create mode 100644 LeanPool/Polylean/ConjInvLength/WordTree.lean diff --git a/LeanPool.lean b/LeanPool.lean index 1f978f9dd8..e1c36a394c 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -175,6 +175,14 @@ import LeanPool.PartialRegularity import LeanPool.PartialRegularity.Extension import LeanPool.Polylean import LeanPool.Polylean.Complexes.GraphPaths +import LeanPool.Polylean.Complexes.Structures.Category +import LeanPool.Polylean.Complexes.Structures.Groupoid +import LeanPool.Polylean.Complexes.Structures.Quiver +import LeanPool.Polylean.ConjInvLength.Length +import LeanPool.Polylean.ConjInvLength.LengthBound +import LeanPool.Polylean.ConjInvLength.MemoLength +import LeanPool.Polylean.ConjInvLength.ProvedBound +import LeanPool.Polylean.ConjInvLength.WordTree import LeanPool.Polylean.UnitConjecture import LeanPool.Polylean.UnitConjecture.AddFreeGroup import LeanPool.Polylean.UnitConjecture.Cocycle diff --git a/LeanPool/Polylean.lean b/LeanPool/Polylean.lean index 64d6fec091..349649961c 100644 --- a/LeanPool/Polylean.lean +++ b/LeanPool/Polylean.lean @@ -6,6 +6,14 @@ Authors: Siddhartha Gadgil, Anand Rao import LeanPool.Polylean.UnitConjecture import LeanPool.Polylean.Complexes.GraphPaths +import LeanPool.Polylean.Complexes.Structures.Category +import LeanPool.Polylean.Complexes.Structures.Groupoid +import LeanPool.Polylean.Complexes.Structures.Quiver +import LeanPool.Polylean.ConjInvLength.Length +import LeanPool.Polylean.ConjInvLength.LengthBound +import LeanPool.Polylean.ConjInvLength.MemoLength +import LeanPool.Polylean.ConjInvLength.ProvedBound +import LeanPool.Polylean.ConjInvLength.WordTree /-! # Polylean Unit Conjecture Counterexample diff --git a/LeanPool/Polylean/Complexes/Structures/Category.lean b/LeanPool/Polylean/Complexes/Structures/Category.lean new file mode 100644 index 0000000000..599147578e --- /dev/null +++ b/LeanPool/Polylean/Complexes/Structures/Category.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.Complexes.Structures.Quiver + +namespace LeanPool.Polylean + +/-- The definition of a `CategoryStruct`, a barebones structure for a category containing none of the axioms (following `mathlib`). -/ +class CategoryStruct (Obj : Sort _) extends Quiver Obj where + /-- The identity morphism at an object. -/ + id : (X : Obj) → (X ⟶ X) + /-- Composition of composable morphisms. -/ + comp : {X Y Z : Obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z) + +attribute [reducible] CategoryStruct.id +attribute [reducible] CategoryStruct.comp + +/-- Identity morphism notation. -/ +notation "𝟙" => CategoryStruct.id -- type as `\b1` +/-- Morphism composition notation. -/ +infixr:80 " ≫ " => CategoryStruct.comp -- type as `\gg` +/-- Reverse-order morphism composition notation. -/ +infixl:80 " ⊚ " => λ f g => CategoryStruct.comp g f + +/-- The definition of a Category. -/ +class Category (Obj : Sort _) extends CategoryStruct Obj where + id_comp : {X Y : Obj} → (f : X ⟶ Y) → 𝟙 X ≫ f = f + comp_id : {X Y : Obj} → (f : X ⟶ Y) → f ≫ 𝟙 Y = f + comp_assoc : {W X Y Z : Obj} → (f : W ⟶ X) → (g : X ⟶ Y) → (h : Y ⟶ Z) → + (f ≫ g) ≫ h = f ≫ (g ≫ h) + +attribute [simp] Category.id_comp +attribute [simp] Category.comp_id +attribute [simp] Category.comp_assoc + +namespace Category + +/-- A functor is a morphism of categories. -/ +structure Functor {C D : Sort _} (𝓒 : Category C) (𝓓 : Category D) + extends Quiver.PreFunctor 𝓒.toQuiver 𝓓.toQuiver where + map_id : (X : C) → map (𝟙 X) = 𝟙 (obj X) + map_comp : {X Y Z : C} → (f : X ⟶ Y) → (g : Y ⟶ Z) → + map (f ≫ g) = map f ≫ map g + +namespace Functor + +/-- Functor notation between categories. -/ +infixr:26 " ⥤ " => Functor -- type as `\func` + +attribute [simp] map_id +attribute [simp] map_comp + +/-- The identity functor. -/ +@[simp] protected def id (C : Sort _) [𝓒 : Category C] : 𝓒 ⥤ 𝓒 := +-- TODO Use `..` notation : { .. , mapId := λ _ => rfl, mapComp := λ _ _ => rfl } + { obj := id, map := id, map_id := λ _ => rfl, map_comp := λ _ _ => rfl } + +/-- Composition of functors. -/ +def comp {C D E : Sort _} {𝓒 : Category C} {𝓓 : Category D} {𝓔 : Category E} + (F : 𝓒 ⥤ 𝓓) (G : 𝓓 ⥤ 𝓔) : 𝓒 ⥤ 𝓔 := +-- TODO Use `..` notation + { obj := G.obj ∘ F.obj, map := G.map ∘ F.map, map_id := by intro; simp, map_comp := by intros; simp } + +/-- Functor composition notation. -/ +infix:80 " ⋙ " => comp + + +/-- The object map of a composed functor is the composite object map. -/ +@[simp] theorem comp_obj : (Φ.obj ∘ Ψ.obj) = (Ψ ⋙ Φ).obj := rfl + +/-- Pointwise form of `Category.Functor.comp_obj`. -/ +@[simp] theorem comp_obj' : ∀ x, (Φ.obj (Ψ.obj x)) = (Ψ ⋙ Φ).obj x := λ _ => rfl + +end Functor + +end Category + + +namespace Path + +variable {C : Sort _} [𝓒 : Category C] + +/-- Compose the arrows appearing in a category path. -/ +def compose {X Y : C} : @Path C 𝓒.toQuiver X Y → (X ⟶ Y) + | .nil => 𝟙 _ + | .cons e p => e ≫ p.compose + +@[simp] theorem compose_nil {X : C} : (Path.nil' X).compose = 𝟙 X := rfl + +/-- Composing an appended path equals composing the two pieces. -/ +theorem compose_append {X Y Z : C} : {p : Path X Y} → {q : Path Y Z} → (append p q).compose = p.compose ≫ q.compose + | .nil, _ => by simp + | .cons _ _, _ => by + dsimp [append, compose] + rw [compose_append, Category.comp_assoc] + +end Path + +/-- Paths in a quiver form a category under concatenation. -/ +instance (priority := low) Quiver.PathCategory {V : Sort _} [Quiver V] : Category V where + hom := Path + id := Path.nil' + comp := Path.append + + id_comp := Path.nil_append + comp_id := Path.append_nil + comp_assoc := Path.append_assoc + +namespace Quiver + +/-- Embedding of a `Quiver` into its category of paths. -/ +def toPathCategory {V : Sort _} [Q : Quiver V] : Quiver.PreFunctor Q Q.PathCategory.toQuiver where + obj := id + map := Quiver.toPath + +end Quiver +end LeanPool.Polylean diff --git a/LeanPool/Polylean/Complexes/Structures/Groupoid.lean b/LeanPool/Polylean/Complexes/Structures/Groupoid.lean new file mode 100644 index 0000000000..038f9e18b2 --- /dev/null +++ b/LeanPool/Polylean/Complexes/Structures/Groupoid.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.Complexes.Structures.Category + +namespace LeanPool.Polylean + +/-- A `Groupoid` is defined as a `Category` in which every morphism has an inverse satisfying certain conditions. -/ +class Groupoid (S : Sort _) extends Category S where + /-- The inverse of a morphism. -/ + inv : {X Y : S} → (X ⟶ Y) → (Y ⟶ X) + inv_comp_id : {X Y : S} → (g : X ⟶ Y) → (inv g) ≫ g = 𝟙 Y + comp_inv_id : {X Y : S} → (g : X ⟶ Y) → g ≫ (inv g) = 𝟙 X + +namespace Groupoid + +open Category + +attribute [simp] inv_comp_id +attribute [simp] comp_inv_id + +variable {S : Sort _} [G : Groupoid S] {X Y Z : S} (g g' : X ⟶ Y) (h h' : Y ⟶ Z) + +/-- Groupoid inverse notation. -/ +postfix:max " ⁻¹ " => Groupoid.inv -- type as `\inv` + +@[simp] theorem left_inv_cancel : g⁻¹ ≫ (g ≫ h) = h := by + rw [← comp_assoc]; simp + +@[simp] theorem id_inv : (𝟙 X)⁻¹ = 𝟙 X := by + have := left_inv_cancel (𝟙 X) (𝟙 X) + rw [comp_id, comp_id] at this; assumption + +@[simp] theorem inv_inv : (g⁻¹)⁻¹ = g := by + have := left_inv_cancel (g⁻¹) g + rw [inv_comp_id, comp_id] at this; assumption + +@[simp] theorem left_cancel_inv (h : X ⟶ Z) : g ≫ (g⁻¹ ≫ h) = h := by + have := left_inv_cancel g⁻¹ h + rw [inv_inv] at this; assumption + +@[simp] theorem inv_comp : (g ≫ h)⁻¹ = h⁻¹ ≫ g⁻¹ := by + have := left_cancel_inv (g ≫ h)⁻¹ (h⁻¹ ≫ g⁻¹) + simp at this; assumption + +@[simp] theorem left_cancel : g ≫ h = g ≫ h' ↔ h = h' := + ⟨by + intro hyp + have := congrArg (g⁻¹ ≫ ·) hyp + simp at this + assumption + , + congrArg _⟩ + +@[simp] theorem right_cancel : g ≫ h = g' ≫ h ↔ g = g' := + ⟨by + intro hyp + have := congrArg (· ≫ h⁻¹) hyp + simp at this + assumption + , + congrArg (· ≫ h)⟩ + +@[simp] theorem left_cancel_id : (g = g ≫ e) ↔ 𝟙 Y = e := by + have := left_cancel g (𝟙 _) e + simp at this; assumption + +@[simp] theorem left_cancel_id' : (g ≫ e = g) ↔ e = 𝟙 Y := by + have := left_cancel g e (𝟙 Y) + simp at this; assumption + +@[simp] theorem right_cancel_id : (g = e ≫ g) ↔ 𝟙 X = e := by + have := right_cancel (𝟙 X) e g + simp at this; assumption + +@[simp] theorem right_cancel_id' : (e ≫ g = g) ↔ e = 𝟙 X := by + have := right_cancel e (𝟙 X) g + simp at this; assumption + +end Groupoid + + +namespace Groupoid + +/-- A `Functor` is a morphism of `Groupoid`s. -/ +structure Functor {S S' : Sort _} (G : Groupoid S) (G' : Groupoid S') + extends Category.Functor G.toCategory G'.toCategory + +namespace Functor + +variable {R S T : Sort _} [F : Groupoid R] [G : Groupoid S] [H : Groupoid T] +variable (Ψ : Groupoid.Functor F G) (Φ : Groupoid.Functor G H) + +theorem map_id' {X : S} : Φ.map (𝟙 X) = 𝟙 (Φ.obj X) := by + have := Φ.map_comp (𝟙 X) (𝟙 X) + rw [Category.comp_id, right_cancel_id] at this + exact this.symm + +@[simp] theorem map_inv {X Y : S} (g : X ⟶ Y) : Φ.map g⁻¹ = (Φ.map g)⁻¹ := by + apply (Groupoid.left_cancel (Φ.map g) _ _).mp + rw [← Φ.map_comp] + simp + +end Functor + +end Groupoid +end LeanPool.Polylean diff --git a/LeanPool/Polylean/Complexes/Structures/Quiver.lean b/LeanPool/Polylean/Complexes/Structures/Quiver.lean new file mode 100644 index 0000000000..111083539c --- /dev/null +++ b/LeanPool/Polylean/Complexes/Structures/Quiver.lean @@ -0,0 +1,185 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +namespace LeanPool.Polylean + +universe u v w + +/-- A `Quiver` `G` on a type `V` of vertices assigns to every pair `a b : V` of vertices + a type `a ⟶ b` of arrows from `a` to `b`. + + It is a common generalisation of multigraphs and categories. + This definition is taken from `mathlib`: + https://leanprover-community.github.io/mathlib_docs/combinatorics/quiver/basic.html#quiver. -/ +class Quiver (V : Sort u) where + /-- The type of arrows from one vertex to another. -/ + hom : V → V → Sort v + +/-- Arrow notation for the hom type of a quiver. -/ +infixr:10 " ⟶ " => Quiver.hom -- type using `\-->` or `\hom` + +namespace Quiver + +/-- A pre-functor is a morphism of quivers. -/ +structure PreFunctor {V V' : Sort _} (Q : Quiver V) (Q' : Quiver V') where + /-- The map on vertices. -/ + obj : V → V' + /-- The map on arrows. -/ + map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y) + +namespace PreFunctor + +/-- The identity morphism between quivers. -/ +@[simp] protected def id (V : Sort _) [Q : Quiver V] : PreFunctor Q Q := +{ obj := id, map := id } + +instance (V : Sort _) [Q : Quiver V] : Inhabited (PreFunctor Q Q) := ⟨PreFunctor.id V⟩ + +/-- Composition of morphisms between quivers. -/ +@[simp] def comp {U V W : Sort _} {QU : Quiver U} {QV : Quiver V} {QW : Quiver W} + (F : PreFunctor QU QV) (G : PreFunctor QV QW) : PreFunctor QU QW := + { obj := G.obj ∘ F.obj, map := G.map ∘ F.map } + +end PreFunctor + +end Quiver + + +/-- Paths in a quiver. -/ +inductive Path {V : Sort _} [Quiver V] : V → V → Sort _ + | nil : {A : V} → Path A A + | cons : {A B C : V} → (A ⟶ B) → Path B C → Path A C + +namespace Quiver + +/-- Convert a single quiver arrow to a path. -/ +def toPath {V : Sort _} [Quiver V] {A B : V} (e : A ⟶ B) : Path A B := + .cons e .nil + +end Quiver + +namespace Path + +variable {V : Sort _} [Quiver V] {A B C D : V} + +/-- The empty path at a vertex, with its vertex explicit for pattern matching. -/ +@[match_pattern] abbrev nil' (A : V) : Path A A := Path.nil +/-- A path formed by adding an edge to the front, with endpoints explicit for matching. -/ +@[match_pattern] abbrev cons' (A B C : V) : + (A ⟶ B) → Path B C → Path A C := Path.cons + +/-- Concatenate an edge to the end of a path. -/ +@[match_pattern] +abbrev snoc : {A B C : V} → Path A B → (B ⟶ C) → Path A C + | _, _, _, .nil, e => .cons e .nil + | _, _, _, .cons e p', e' => .cons e (snoc p' e') + +/-- Append an edge to the end of a path, with endpoints explicit for matching. -/ +@[match_pattern] +abbrev snoc' (A B C : V) : Path A B → (B ⟶ C) → Path A C := Path.snoc + +/-- Concatenation of paths. -/ +def append : {A B C : V} → Path A B → Path B C → Path A C + | _, _, _, .nil, p => p + | _, _, _, .cons e p', p => cons e (append p' p) + +/-- The length of a path. -/ +def length : {A B : V} → Path A B → Nat + | _, _, .nil => .zero + | _, _, .cons _ p => .succ (length p) + +@[simp] theorem nil_append (p : Path A B) : .append .nil p = p := rfl + +@[simp] theorem append_nil (p : Path A B) : .append p .nil = p := by + induction p + · case nil => rfl + · case cons => + simp only [append] + apply congrArg + assumption + +theorem snoc_cons (e : A ⟶ B) (p : Path B C) (e' : C ⟶ D) : + snoc (cons e p) e' = cons e (snoc p e') := by cases p <;> simp + +theorem append_snoc (p : Path A B) (p' : Path B C) (e : C ⟶ D) : + append p (snoc p' e) = snoc (append p p') e := by + induction p + · case nil => rfl + · case cons ih => simp [append, ih p'] + +theorem append_cons (p : Path A B) (e : B ⟶ C) (p' : Path C D) : + append p (cons e p') = append (snoc p e) p' := by + induction p + · case nil => rfl + · case cons ih => dsimp [append]; rw [ih] + +theorem append_assoc (p : Path A B) (q : Path B C) (r : Path C D) : + append (append p q) r = append p (append q r) := by + induction p + · case nil => rfl + · case cons ih => simp [append]; apply ih + +-- TODO Rephrase this to work for general paths, not just loops +theorem nil_length {A : V} : (p : Path A A) → p.length = .zero ↔ p = .nil' A + | .nil => ⟨λ _ => rfl, λ _ => rfl⟩ + | .cons _ p => by apply Iff.intro <;> (intro; simp [length] at *) + +theorem snoc_length {A B C : V} : (p : Path A B) → (e : B ⟶ C) → length (.snoc p e) = .succ (length p) + | .nil, e => rfl + | .cons _ p', e => by + rw [snoc_cons] + dsimp only [length] + apply congrArg + apply snoc_length + +theorem length_append {A B C : V} : (p : Path A B) → (q : Path B C) → (append p q).length = p.length + q.length + | .nil, q => by rw [Nat.add_comm]; rfl + | .cons _ p', q => by + dsimp [append, length] + simpa [Nat.succ_add] using congrArg Nat.succ (length_append p' q) + +/-- The end-point of the first edge in the path. -/ +def first : Path A B → V + | .nil' v => v + | .cons' _ v _ _ _ => v + +/-- The source of the last end in the path. -/ +def last : {A B : V} → Path A B → V + | _, _, .nil' v => v + | .(v), _, .cons' v _ _ _ .nil => v + | _, _, .cons' _ _ _ _ (.cons e p) => last (.cons e p) + +theorem first_cons (A B C : V) (e : A ⟶ B) (p : Path B C) : first (cons e p) = B := rfl + +theorem last_snoc : (A B C : V) → (p : Path A B) → (e : B ⟶ C) → last (snoc p e) = B + | _, _, _, .nil, _ => rfl + | _, _, _, .cons' _ _ _ _ .nil, _ => by rw [snoc_cons]; rfl + | _, _, _, .cons' _ _ _ _ (.cons _ _), _ => by rw [snoc_cons, snoc, last, ← snoc_cons]; apply last_snoc + +end Path + + +/-- A loop is a path whose source and target are the same vertex. -/ +abbrev Loop {V : Sort _} [Quiver V] (A : V) := Path A A + +namespace Loop + +variable {V : Sort _} [Quiver V] (A : V) + +/-- Regard a loop as a path. -/ +def toPath : Loop A → Path A A := id + +/-- The empty loop. -/ +abbrev nil : Loop A := Path.nil + +/-- The next vertex reached by the first edge of a loop. -/ +abbrev next : Loop A → V := Path.first + +/-- Concatenate two loops. -/ +abbrev concat : Loop A → Loop A → Loop A := Path.append + +end Loop +end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/Length.lean b/LeanPool/Polylean/ConjInvLength/Length.lean new file mode 100644 index 0000000000..739514cb2f --- /dev/null +++ b/LeanPool/Polylean/ConjInvLength/Length.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Batteries +import LeanPool.Polylean.ConjInvLength.LengthBound + +namespace LeanPool.Polylean +open Batteries +open Letter + +namespace Letter + +/-- Integer code for each letter. -/ +def int : Letter → Int + | α => 1 + | β => 2 + | α! => -1 + | β! => -2 + +end Letter + +open Letter + +instance : Pow Word Nat where + pow w n := w.pow n + +/-- Array-backed words used by the memoized length computation. -/ +abbrev Wrd := Array Letter + +namespace Word + +/-- Convert a list-backed word to an array-backed word. -/ +def wrd (w: Word) : Wrd := w.toArray -- .map <| fun l => l.int + +end Word + +namespace Wrd + +/-- Render an array-backed word by concatenating rendered letters. -/ +def toString(w: Wrd) := w.foldl (fun x y => s!"{x}{y}") "" + +instance : ToString Wrd := ⟨Wrd.toString⟩ + +/-- Repeated concatenation of an array-backed word. -/ +def pow : Wrd → Nat → Wrd + | _, 0 => #[] + | w, Nat.succ m => w ++ (pow w m) + +instance : Pow Wrd Nat where + pow w n := w.pow n + +/-- Hash function for array-backed words. -/ +def hashfn (w: Wrd) : UInt64 := + w.foldl (fun h i => mixHash h (hash i)) 7 + +instance : Hashable Wrd := ⟨hashfn⟩ + +/-- Cache for normalized word lengths. -/ +initialize normCache : IO.Ref (HashMap Wrd Nat) ← IO.mkRef (HashMap.empty) + +/-- All splits of an array-backed word around occurrences of a letter. -/ +def splits(l : Letter) : (w : Wrd) → Array {p : Wrd × Wrd // p.1.size + p.2.size < w.size} := fun w => + match h:w.size with + | 0 => #[] + | m + 1 => + let x := w.back + have _ : w.size -1 < w.size := by + rw [h] + apply Nat.le_refl + let ys := w.pop + have ysize : ys.size = m := by + rw [Array.size_pop, h] + rfl + let tailSplits := (splits l ys).map fun ⟨(fst, snd), h⟩ => + ⟨(fst, snd.push x), by + rw [Array.size_push] + rw [ysize] at h + simp + simp at h + rw [← Nat.add_assoc] + simp [Nat.succ_lt_succ h]⟩ + if x = l then tailSplits.push ⟨(ys, #[]), + by + rw [ysize] + apply Nat.le_refl⟩ else tailSplits +termination_by w => w.size + +/-- Memoized conjugation-invariant length candidate for array-backed words. -/ +def length(w : Wrd) : IO Nat := +do + let cache ← normCache.get + match cache.find? w with + | some n => + pure n + | none => + let res ← + match h:w.size with + | 0 => pure 0 + | m + 1 => do + let ys := w.pop + let x := w.back + have lll : w.size -1 < w.size := by + rw [h] + apply Nat.le_refl + let base := 1 + (← length <| ys) + let derived ← (splits x⁻¹ ys).mapM fun ⟨(fst, snd), h0⟩ => + have ysize : ys.size = m := by + rw [Array.size_pop, h] + rfl + have h0 : fst.size + snd.size < w.size := by + rw [h] + rw [← ysize] + apply Nat.lt_trans h0 (Nat.lt_succ_self _) + have _ : snd.size < w.size := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) h0 + have _ : fst.size < w.size := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) h0 + return (← length fst) + (← length snd) + derived.foldl (fun x y => do return min (← x) y) (pure base) + normCache.set <| (← normCache.get).insert w res + return res +termination_by w.size + +end Wrd + +/-- Memoized length for list-backed words. -/ +def wordLength(w: Word):IO Nat := + Wrd.length <| Word.wrd w + +namespace Wrd + +/-- Conjugate an array-backed word by a letter. -/ +def conj: Wrd → Letter → Wrd := fun w l => #[l] ++ w ++ #[l⁻¹] + +end Wrd + +instance: Pow Wrd Letter where + pow w l := w.conj l +end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/LengthBound.lean b/LeanPool/Polylean/ConjInvLength/LengthBound.lean new file mode 100644 index 0000000000..2f856c948f --- /dev/null +++ b/LeanPool/Polylean/ConjInvLength/LengthBound.lean @@ -0,0 +1,99 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Mathlib.Algebra.Group.Defs + +namespace LeanPool.Polylean +/-- The four generators used for words in the conjugation-invariant length example. -/ +inductive Letter where + | α : Letter + | β : Letter + | α! : Letter + | β! : Letter + deriving DecidableEq, Repr, Hashable, Inhabited + +namespace Letter + +/-- Render a letter as a string. -/ +def toString : Letter → String +| α => "α" +| β => "β" +| α! => "alpha!" +| β! => "beta!" + +instance : ToString Letter := ⟨Letter.toString⟩ + +/-- The formal inverse of a letter. -/ +def inv : Letter → Letter + | α => α! + | β => β! + | α! => α + | β! => β + +end Letter + +@[inline] instance letInv : Inv Letter := ⟨Letter.inv⟩ + + +open Letter + +/-- A word is a list of letters. -/ +abbrev Word := List Letter + +namespace Word + +/-- Render a word by concatenating its rendered letters. -/ +def toString(w: Word) := w.foldl (fun x y => s!"{x}{y}") "" + +instance : ToString Word := ⟨Word.toString⟩ + +/-- Repeated concatenation of a word. -/ +def pow : Word → Nat → Word + | w, 0 => [] + | w, Nat.succ m => w ++ (pow w m) + +instance : Pow Word Nat where + pow w n := w.pow n + +end Word + +-- The code below (with better termination) is due to Mario Carneiro +-- split a word into parts before and after each occurrence of a letter `l` +/-- All splits of a word around occurrences of a letter, with length witnesses. -/ +def splits (l : Letter) : (w : Word) → List {p : Word × Word // p.1.length + p.2.length < w.length} + | [] => [] + | x :: ys => + let tailSplits := (splits l ys).map fun ⟨(fst, snd), h⟩ => + ⟨(x :: fst, snd), by simp [Nat.succ_add, Nat.succ_lt_succ h]⟩ + if x = l then ⟨([], ys), by simp [Nat.lt_succ_self]⟩ :: tailSplits else tailSplits + +/-- A recursively computed conjugation-invariant length candidate. -/ +def length : Word → Nat + | [] => 0 + | x :: ys => + have lb : (List.length ys) < List.length (x :: ys) := by + simp [List.length_cons, Nat.le_refl] + let base := 1 + (length ys) + let derived := (splits x⁻¹ ys).map fun ⟨(fst, snd), h⟩ => + have h : fst.length + snd.length < ys.length + 1 := Nat.lt_trans h (Nat.lt_succ_self _) + have _ : snd.length < ys.length + 1 := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) h + have _ : fst.length < ys.length + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) h + length fst + length snd + derived.foldl min base -- minimum of base and elements of derived +termination_by l => l.length + +-- For proofs + +namespace Word + +/-- Conjugate a word by a letter. -/ +def conj: Word → Letter → Word := fun w l => [l] ++ w ++ [l⁻¹] + +end Word + +instance: Pow Word Letter where + pow w l := w.conj l +end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/MemoLength.lean b/LeanPool/Polylean/ConjInvLength/MemoLength.lean new file mode 100644 index 0000000000..626143433e --- /dev/null +++ b/LeanPool/Polylean/ConjInvLength/MemoLength.lean @@ -0,0 +1,38 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import Batteries +import LeanPool.Polylean.ConjInvLength.LengthBound + +namespace LeanPool.Polylean +open Batteries + +/-- Cache for memoized word lengths. -/ +initialize normCache : IO.Ref (HashMap Word Nat) ← IO.mkRef (HashMap.empty) + +/-- Memoized list-backed conjugation-invariant length candidate. -/ +def memoLength : Word → IO Nat := fun w => do + let cache ← normCache.get + match cache.find? w with + | some n => + pure n + | none => + match w with + | [] => return 0 + | x :: ys => do + have lb : (List.length ys) < List.length (x :: ys) := by + simp [List.length_cons, Nat.le_refl] + let base := 1 + (← memoLength ys) + let derived ← (splits x⁻¹ ys).mapM fun ⟨(fst, snd), h⟩ => do + have h : fst.length + snd.length < ys.length + 1 := Nat.lt_trans h (Nat.lt_succ_self _) + have h1 : snd.length < ys.length + 1 := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) h + have h2 : fst.length < ys.length + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right _ _) h + return (← memoLength fst) + (← memoLength snd) + let res := derived.foldl min base -- minimum of base and elements of derived + normCache.set <| (← normCache.get).insert w res + return res +termination_by l => l.length +end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/ProvedBound.lean b/LeanPool/Polylean/ConjInvLength/ProvedBound.lean new file mode 100644 index 0000000000..d8773abe16 --- /dev/null +++ b/LeanPool/Polylean/ConjInvLength/ProvedBound.lean @@ -0,0 +1,194 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.ConjInvLength.LengthBound + +namespace LeanPool.Polylean +open Letter + +/-- A split of a word around a distinguished letter, with a proof of reconstruction. -/ +structure ProvedSplit (l: Letter)(w : Word) where + /-- The part before the distinguished letter. -/ + fst : Word + /-- The part after the distinguished letter. -/ + snd: Word + /-- Reconstruction proof for the split. -/ + proof : w = fst ++ [l] ++ snd + + +-- Split with first piece empty when head matches the splitting letter. +namespace ProvedSplit + +/-- Split with the first piece empty when the head matches the splitting letter. -/ +def head (x: Letter) (ys: Word) : ProvedSplit x (x :: ys) := + ⟨[], ys, rfl⟩ + +-- Prepend to a proved split of the tail (`l` and `ys` implicit). +/-- Prepend a letter to the first component of a proved split. -/ +def prepend{l: Letter}{ys : Word} (x: Letter) + (ps: ProvedSplit l ys) : ProvedSplit l (x :: ys) := + let newFst := x :: ps.fst + let newSnd := ps.snd + have newProof : x :: ys = newFst ++ [l] ++ newSnd := + by + rw [ps.proof] + simp [newFst, newSnd] + ⟨newFst, newSnd, newProof⟩ + +end ProvedSplit + +-- all proved splits of a word +/-- All proved splits of a word around a letter. -/ +def provedSplits(z: Letter) : (w : Word) → List (ProvedSplit z w) + | [] => [] + | x :: ys => + let tailSplits := (provedSplits z ys).map (ProvedSplit.prepend x) + if c:x = z then + let headSplit : ProvedSplit z (x :: ys) := by rw [c]; exact ProvedSplit.head z ys + headSplit :: tailSplits + else tailSplits + +/-- A length function on words. -/ +abbrev Length := Word → Nat + +/-- A length function invariant under conjugation by letters. -/ +def conjInv(l: Length) : Prop := (x : Letter) → (g : Word) → l (g^x) = l (g) + +/-- The triangle inequality for a length function. -/ +def triangIneq(l: Length) : Prop := (g h : Word) → l (g ++ h) ≤ l g + l h + +/-- A length function normalized on single letters. -/ +def normalized(l: Length) : Prop := (x : Letter) → l [x] = 1 + +/-- A length function that sends the empty word to zero. -/ +def emptyWord(l: Length) : Prop := l [] = 0 + +/-- A certified upper bound for the length of a word. -/ +structure ProvedBound(g: Word): Type where + /-- The numeric upper bound. -/ + bound: Nat + /-- The proof that every normalized conjugation-invariant length is bounded by `bound`. -/ + pf : (l: Length) → emptyWord l → + normalized l → conjInv l → triangIneq l → l g ≤ bound + +theorem conj_split (x: Letter) (ys fst snd: Word) : + ys = fst ++ [x⁻¹] ++ snd → x :: ys = fst^x ++ snd := + by + intro hyp + have expand : fst^x = [x] ++ fst ++ [x⁻¹] := rfl + rw [expand] + rw [hyp] + simp + +-- deducing bound using `l (xh₁x⁻¹h₂) ≤ b₁ + b₂` given `l (hᵢ) ≤ bᵢ`, `i = 1, 2` +namespace ProvedBound + +/-- Combine certified bounds across a split around a conjugating letter. -/ +def headMatches(x: Letter)(ys fst snd: Word) + (eqn : ys = fst ++ [x⁻¹] ++ snd) : + ProvedBound fst → ProvedBound snd → ProvedBound (x :: ys) := + fun pb1 pb2 => + let bound := pb1.bound + pb2.bound + let pf : + (l: Length) → emptyWord l → normalized l → conjInv l → triangIneq l → + l (x :: ys) ≤ bound := by + intros l emp norm conj triang + rw [conj_split x ys fst snd eqn] + have lem : l (fst ^ x ++ snd) ≤ l (fst^x) + l snd := by apply triang + have clem : l (fst^x) = l fst := by apply conj + rw [clem] at lem + apply Nat.le_trans lem + have l1 : l fst ≤ pb1.bound := pb1.pf l emp norm conj triang + have l2 : l snd ≤ pb2.bound := pb2.pf l emp norm conj triang + apply Nat.add_le_add l1 l2 + ⟨bound, pf⟩ + +-- deducing `l(xh) ≤ b + 1` given `l(h) ≤ b` +/-- Prepend a letter to a certified bound. -/ +def prepend{w : Word} (x: Letter) + (ps: ProvedBound w) : ProvedBound (x :: w) := + let newBound := ps.bound + 1 + ⟨newBound, fun l emp norm conj triang => by + let prev := ps.pf l emp norm conj triang + have lemTri : l (x :: w) ≤ l ([x]) + l w := by apply triang [x] + apply Nat.le_trans lemTri + rw [norm x] + rw [Nat.add_comm] + apply Nat.add_le_add_right prev⟩ + +-- `l(e) ≤ 0` +/-- The zero bound for the empty word. -/ +def emptyWord: ProvedBound [] := + ⟨0, fun l emp _ _ _ => by + rw [emp] + apply Nat.zero_le + ⟩ + +-- the best proved bound for a word +/-- Choose the better bound from a nonempty list of alternatives. -/ +def min {w: Word}: ProvedBound w → List (ProvedBound w) → + ProvedBound w := + fun head tail => + tail.foldl (fun pb1 pb2 => + if pb1.bound ≤ pb2.bound then pb1 else pb2) head + +end ProvedBound + +theorem splitFirst{l: Letter}{w: Word}(ps: ProvedSplit l w): + ps.fst.length + 1 ≤ w.length := + by + let lem : (ps.fst ++ [l] ++ ps.snd).length = + (ps.fst ++ [l]).length + ps.snd.length := by apply List.length_append + rw [← ps.proof] at lem + rw [lem] + have lem2 : List.length (ps.fst ++ [l]) = ps.fst.length + 1 := by + apply List.length_append + rw [lem2] + apply Nat.le_add_right + +theorem splitSecond{l: Letter}{w: Word}(ps: ProvedSplit l w): + ps.snd.length + 1 ≤ w.length := + by + let lem : (ps.fst ++ [l] ++ ps.snd).length = + (ps.fst ++ [l]).length + ps.snd.length := by apply List.length_append + rw [← ps.proof] at lem + rw [lem] + have lem2 : List.length (ps.fst ++ [l]) = ps.fst.length + 1 := by + apply List.length_append + rw [lem2] + rw [Nat.add_assoc] + rw [Nat.add_comm] + apply Nat.le_add_left + +-- bound with proof for words +/-- Compute a certified length bound for a word. -/ +def provedBound : (w: Word) → ProvedBound w := fun w => + match h:w with + | [] => ProvedBound.emptyWord + | x :: ys => + have lb : (List.length ys) < List.length (x :: ys) := by + simp [List.length_cons, Nat.le_refl] + let head := ProvedBound.prepend x (provedBound ys) + let splits := provedSplits x⁻¹ ys + have wl: w.length = ys.length + 1 := by + rw[h] + rfl + let tail := splits.map (fun ps : ProvedSplit x⁻¹ ys => + have l1 : ps.fst.length + 1 ≤ ys.length + 1 := + by + have lm := splitFirst ps + apply Nat.le_trans lm + apply Nat.le_succ + have l2 : ps.snd.length + 1 ≤ ys.length + 1 := + by + have lm := splitSecond ps + apply Nat.le_trans lm + apply Nat.le_succ + ProvedBound.headMatches x ys ps.fst ps.snd ps.proof + (provedBound ps.fst) (provedBound ps.snd)) + ProvedBound.min head tail +termination_by w => w.length +end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/WordTree.lean b/LeanPool/Polylean/ConjInvLength/WordTree.lean new file mode 100644 index 0000000000..0e2510c06c --- /dev/null +++ b/LeanPool/Polylean/ConjInvLength/WordTree.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 Siddhartha Gadgil, Anand Rao. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddhartha Gadgil, Anand Rao +-/ + +import LeanPool.Polylean.ConjInvLength.ProvedBound + +namespace LeanPool.Polylean + +/-- A proof tree witnessing an upper bound for a word length. -/ +inductive ProofTree : Word → Type where + | emptyWord : ProofTree [] + | normalized : (l : Letter) → ProofTree [l] + | conjugate : (l : Letter) → (w: Word) → ProofTree w → ProofTree (w^l) + | triangleIneq : (w₁ : Word) → (w₂ : Word) → + ProofTree w₁ → ProofTree w₂ → ProofTree (w₁ ++ w₂) + deriving Repr + +namespace ProofTree + +/-- The numeric bound represented by a proof tree. -/ +def bound: (w: Word) → ProofTree w → Nat := + fun w t => + match t with + | ProofTree.emptyWord => 0 + | ProofTree.normalized l => 1 + | ProofTree.conjugate l w t => bound w t + | ProofTree.triangleIneq w₁ w₂ t₁ t₂ => bound w₁ t₁ + bound w₂ t₂ + +/-- Convert a proof tree into a certified bound. -/ +def provedBound: (w: Word) → ProofTree w → ProvedBound w := + fun w t => + match t with + | ProofTree.emptyWord => ProvedBound.emptyWord + | ProofTree.normalized x => + ⟨1, by + intros l emp norm conj triang + rw [norm x] + exact Nat.le_refl 1⟩ + | ProofTree.conjugate x w t => + let pb := provedBound w t + ⟨pb.bound, by + intros l emp norm conj triang + rw [conj x w] + apply pb.pf l emp norm conj triang⟩ + | ProofTree.triangleIneq w₁ w₂ t₁ t₂ => + let pb1 := provedBound w₁ t₁ + let pb2 := provedBound w₂ t₂ + ⟨pb1.bound + pb2.bound, by + intros l emp norm conj triang + apply Nat.le_trans (triang w₁ w₂) + apply Nat.add_le_add + exact pb1.pf l emp norm conj triang + exact pb2.pf l emp norm conj triang + ⟩ + +/-- Combine proof trees across a split around a conjugating letter. -/ +def headMatches(x: Letter)(ys fst snd: Word) + (eqn : ys = fst ++ [x⁻¹] ++ snd) : + ProofTree fst → ProofTree snd → ProofTree (x :: ys) := by + intros pt1 pt2 + rw [conj_split x ys fst snd eqn] + apply ProofTree.triangleIneq + exact ProofTree.conjugate x fst pt1 + exact pt2 + +/-- Prepend a normalized letter to a proof tree. -/ +def prepend{w : Word} (x: Letter) + (pt: ProofTree w) : ProofTree (x :: w) := by + have exp : x :: w = [x] ++ w := by rfl + rw [exp] + apply ProofTree.triangleIneq + exact ProofTree.normalized x + exact pt + +/-- Choose the proof tree with the smallest bound from a nonempty list. -/ +def min {w: Word}: ProofTree w → List (ProofTree w) → + ProofTree w := + fun head tail => + tail.foldl (fun pt1 pt2 => + if pt1.bound ≤ pt2.bound then pt1 else pt2) head + +end ProofTree + +/-- A simple proof tree obtained by splitting a word into letters. -/ +def simpleTree(w: Word) : ProofTree w := + match w with + | [] => ProofTree.emptyWord + | x :: ys => by + have exp : x :: ys = [x] ++ ys := by rfl + rw [exp] + apply ProofTree.triangleIneq + exact ProofTree.normalized x + exact simpleTree ys + + +instance {w: Word} : Inhabited (ProofTree w) :=⟨simpleTree w⟩ + +/-- Compute a proof tree for a word. -/ +def proofTree : (w: Word) → ProofTree w := fun w => + match h:w with + | [] => ProofTree.emptyWord + | x :: ys => + have : ys.length < (x :: ys).length := by + simp + let head := ProofTree.prepend x (proofTree ys) + let splits := provedSplits x⁻¹ ys + have wl: w.length = ys.length + 1 := by + rw[h] + rfl + let tail := splits.map (fun ps : ProvedSplit x⁻¹ ys => + have l1 : ps.fst.length + 1 ≤ ys.length + 1 := + by + have lm := splitFirst ps + apply Nat.le_trans lm + apply Nat.le_succ + have l2 : ps.snd.length + 1 ≤ ys.length + 1 := + by + have lm := splitSecond ps + apply Nat.le_trans lm + apply Nat.le_succ + ProofTree.headMatches x ys ps.fst ps.snd ps.proof + (proofTree ps.fst) (proofTree ps.snd)) + ProofTree.min head tail +termination_by w => w.length +decreasing_by + · exact this + · exact Nat.lt_of_succ_le (by simpa using l1) + · exact Nat.lt_of_succ_le (by simpa using l2) + +open Letter +end LeanPool.Polylean From b1185ec6c943ba7147824e3314a192dafb05c664 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 22:13:20 +0900 Subject: [PATCH 6/6] Clean Polylean build warnings --- LeanPool/Polylean/Complexes/GraphPaths.lean | 473 +++++++++++------- LeanPool/Polylean/ConjInvLength/Length.lean | 25 +- .../Polylean/ConjInvLength/LengthBound.lean | 12 +- .../Polylean/ConjInvLength/MemoLength.lean | 9 +- .../Polylean/ConjInvLength/ProvedBound.lean | 48 +- LeanPool/Polylean/ConjInvLength/WordTree.lean | 36 +- 6 files changed, 358 insertions(+), 245 deletions(-) diff --git a/LeanPool/Polylean/Complexes/GraphPaths.lean b/LeanPool/Polylean/Complexes/GraphPaths.lean index 6ebb0338d0..8fc9f61262 100644 --- a/LeanPool/Polylean/Complexes/GraphPaths.lean +++ b/LeanPool/Polylean/Complexes/GraphPaths.lean @@ -10,7 +10,7 @@ import Mathlib.Algebra.Group.Defs namespace LeanPool.Polylean /-- A graph with directed edges, distinguished null edge, and edge reversal. -/ -structure Graph(V: Type) (E: Type) where +structure Graph (V : Type) (E : Type) where /-- The distinguished null edge. -/ null : E /-- The initial vertex of an edge. -/ @@ -18,31 +18,31 @@ structure Graph(V: Type) (E: Type) where /-- The reverse of an edge. -/ bar : E → E barInv : bar ∘ bar = id - barNoFP : ∀ e: E, bar e ≠ e + barNoFP : ∀ e : E, bar e ≠ e variable {V : Type} {E : Type} {x₁ x₂ : V} /-- The terminal vertex of an edge, defined as the initial vertex of its reverse. -/ -@[inline] def term (graph: Graph V E): E → V := +@[inline] def term (graph : Graph V E) : E → V := fun e => graph.init (graph.bar e) /-- Edge paths in a graph, indexed by their initial and terminal vertices. -/ -inductive EdgePath (graph: Graph V E): V → V → Type where - | single : (x: V) → EdgePath graph x x +inductive EdgePath (graph : Graph V E) : V → V → Type where + | single : (x : V) → EdgePath graph x x | cons : {x y z : V} → (e : E) → graph.init e = x → term graph e = y → EdgePath graph y z → EdgePath graph x z namespace EdgePath /-- The number of edges in an edge path. -/ -def length {graph: Graph V E}{x y: V}: EdgePath graph x y → Nat +def length {graph : Graph V E} {x y : V} : EdgePath graph x y → Nat | EdgePath.single x => 0 | EdgePath.cons _ _ _ path => length path + 1 end EdgePath -/--proves that bar is an involution-/ +/-- proves that bar is an involution -/ theorem bar_involution {G : Graph V E} : (ex : E) → G.bar (G.bar ex) = ex := by intro ex apply congr G.barInv (Eq.refl ex) @@ -51,59 +51,71 @@ theorem bar_involution {G : Graph V E} : (ex : E) → G.bar (G.bar ex) = ex := b open EdgePath /-- concatenates two edgepaths -/ -def multiply {G : Graph V E} {x y z : V}: (EdgePath G x y) → (EdgePath G y z) → (EdgePath G x z) := by -intro p q -match p with -| single x => exact q -| cons ex h1 h2 exy => exact (cons ex h1 h2 (multiply exy q)) - - -/--proves that the endpoint of the reverse of an edge is the start point of the edge-/ -theorem term_bar_equals_init {G : Graph V E} {x : V}{e : E}: G.init e = x → (term G (G.bar e) = x) := -by -intro h -have h₁ : G.bar (G.bar e) = e := congr G.barInv (Eq.refl e) -have h₂ : G.init (G.bar (G.bar e)) = G.init e := congrArg G.init h₁ -apply Eq.trans h₂ h - -/--proves that initial vertex of reversed edge is the terminal vertex of the original edge-/ -theorem init_bar_equals_term {G : Graph V E} {x :V} {e : E}: (term G e = x) → G.init (G.bar e) = x:= by -intro hyp -have : G.init (G.bar e) = term G e := by rfl -exact Eq.trans this hyp - -/-- proves associativity of path multiplication-/ -theorem mult_assoc {G : Graph V E} (p : EdgePath G w x) (q : EdgePath G x y) (r : EdgePath G y z): +def multiply {G : Graph V E} {x y z : V} : + (EdgePath G x y) → (EdgePath G y z) → (EdgePath G x z) := by + intro p q + match p with + | single x => exact q + | cons ex h1 h2 exy => exact (cons ex h1 h2 (multiply exy q)) + + +/-- proves that the endpoint of the reverse of an edge is the start point of the edge -/ +theorem term_bar_equals_init {G : Graph V E} {x : V} {e : E} : + G.init e = x → (term G (G.bar e) = x) := by + intro h + have h₁ : G.bar (G.bar e) = e := congr G.barInv (Eq.refl e) + have h₂ : G.init (G.bar (G.bar e)) = G.init e := congrArg G.init h₁ + apply Eq.trans h₂ h + +/-- proves that initial vertex of reversed edge is the terminal vertex of the original edge -/ +theorem init_bar_equals_term {G : Graph V E} {x : V} {e : E} : + (term G e = x) → G.init (G.bar e) = x := by + intro hyp + have : G.init (G.bar e) = term G e := by rfl + exact Eq.trans this hyp + +/-- proves associativity of path multiplication -/ +theorem mult_assoc {G : Graph V E} + (p : EdgePath G w x) (q : EdgePath G x y) (r : EdgePath G y z) : (multiply (multiply p q) r) = (multiply p (multiply q r)) := by - induction p with - | single w => simp[multiply] - | cons ex h1 h2 exy ih => simp[multiply, ih] + induction p with + | single w => simp[multiply] + | cons ex h1 h2 exy ih => simp[multiply, ih] -/--proves that "single x" is an identity element for multiplication-/ +/-- proves that "single x" is an identity element for multiplication -/ theorem mult_const {G : Graph V E} (p : EdgePath G x y) : (multiply p (single y)) = p := by induction p with | single x => simp [multiply] | cons ex h1 h2 exy ih => simp[multiply, ih] -/-- reverses an edgepath-/ -def inverse {G : Graph V E} {x y : V}: (EdgePath G x y) → (EdgePath G y x) +/-- reverses an edgepath -/ +def inverse {G : Graph V E} {x y : V} : (EdgePath G x y) → (EdgePath G y x) | single x => single x -| cons ex h₁ h₂ exy => multiply (inverse exy) (cons (G.bar (ex)) h₂ (term_bar_equals_init h₁) (single x)) +| cons ex h₁ h₂ exy => + multiply (inverse exy) (cons (G.bar ex) h₂ (term_bar_equals_init h₁) (single x)) -/--defines an edgepath with a single edge-/ -def basicpath {G : Graph V E} (x : V) (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y): EdgePath G x y := cons ex h₁ h₂ (single y) +/-- defines an edgepath with a single edge -/ +def basicpath {G : Graph V E} (x : V) (ex : E) + (h₁ : G.init ex = x) (h₂ : term G ex = y) : EdgePath G x y := + cons ex h₁ h₂ (single y) -/--proves that multiplication with a basicpath gives inductive definition of edgepath-/ -theorem basicpath_mult {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : multiply (basicpath x ex h₁ h₂) exy = cons ex h₁ h₂ exy := by - simp[basicpath, multiply] +/-- proves that multiplication with a basicpath gives inductive definition of edgepath -/ +theorem basicpath_mult {G : Graph V E} {x y z : V} (ex : E) + (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : + multiply (basicpath x ex h₁ h₂) exy = cons ex h₁ h₂ exy := by + simp[basicpath, multiply] -/--defines inverse in terms of basicpath-/ -theorem inverse_lemma {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : inverse (cons ex h₁ h₂ exy) = multiply (inverse exy) (basicpath y (G.bar ex) h₂ (term_bar_equals_init h₁) ) := by rfl +/-- defines inverse in terms of basicpath -/ +theorem inverse_lemma {G : Graph V E} {x y z : V} (ex : E) + (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : + inverse (cons ex h₁ h₂ exy) = + multiply (inverse exy) (basicpath y (G.bar ex) h₂ (term_bar_equals_init h₁)) := by + rfl -/--proves the basic relation between inverse and multiply-/ +/-- proves the basic relation between inverse and multiply -/ theorem inverse_mult {G : Graph V E} (x y z : V) (p : EdgePath G x y) (q : EdgePath G y z) : inverse (multiply p q) = multiply (inverse q) (inverse p) := by induction p with @@ -114,22 +126,33 @@ theorem inverse_mult {G : Graph V E} (x y z : V) (p : EdgePath G x y) (q : EdgeP rw[p₂] rw[mult_const (inverse q)] | cons ex t₁ t₂ exy ih => - have p₃ : multiply (cons ex t₁ t₂ exy) q = cons ex t₁ t₂ (multiply exy q) := by simp[mult_assoc, basicpath_mult, multiply] + have p₃ : + multiply (cons ex t₁ t₂ exy) q = cons ex t₁ t₂ (multiply exy q) := by + simp [multiply] rw[p₃] - have p₄ : inverse (cons ex t₁ t₂ exy) = multiply (inverse exy) (basicpath _ (G.bar ex) t₂ (term_bar_equals_init t₁)) := by simp[inverse_lemma] + have p₄ : + inverse (cons ex t₁ t₂ exy) = + multiply (inverse exy) + (basicpath _ (G.bar ex) t₂ (term_bar_equals_init t₁)) := by + simp[inverse_lemma] rw[p₄] - have p₅ : multiply (inverse q) (inverse exy) = inverse ( multiply exy q) := by simp[ih q] + have p₅ : multiply (inverse q) (inverse exy) = inverse (multiply exy q) := by + simp[ih q] let p₆ := inverse_lemma ex t₁ t₂ (multiply exy q) rw[p₆] simp[Eq.symm (p₅), mult_assoc] -/--proves that inverse is an involution on paths-/ -theorem inverse_involution {G : Graph V E} {x y : V} (p : EdgePath G x y) : inverse (inverse p) = p := by +/-- proves that inverse is an involution on paths -/ +theorem inverse_involution {G : Graph V E} {x y : V} (p : EdgePath G x y) : + inverse (inverse p) = p := by induction p with | single x => rfl | cons ex h₁ h₂ exy ih => - have p₁ : inverse (cons ex h₁ h₂ exy) = multiply (inverse exy) (inverse (basicpath _ ex h₁ h₂)) := by rfl + have p₁ : + inverse (cons ex h₁ h₂ exy) = + multiply (inverse exy) (inverse (basicpath _ ex h₁ h₂)) := by + rfl rw[p₁] let k := inverse_mult _ _ _ (inverse exy) (inverse (basicpath _ ex h₁ h₂)) rw[k] @@ -142,25 +165,28 @@ theorem inverse_involution {G : Graph V E} {x y : V} (p : EdgePath G x y) : inv -/--helper function for reducePath, that reduces the first two edges of the path-/ -def reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : { rp : EdgePath G x z // rp.length ≤ (cons ex h₁ h₂ exy).length} := by -cases exy with - | single x => exact ⟨cons ex h₁ h₂ (single y), by simp⟩ - | cons ey h₃ h₄ eyz => - apply - if c : (x = term G ey) ∧ (ey = G.bar (ex)) then - ⟨ Eq.symm (Eq.trans (And.left c) h₄) ▸ eyz, by +/-- helper function for reducePath, that reduces the first two edges of the path -/ +def reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} + (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : + { rp : EdgePath G x z // rp.length ≤ (cons ex h₁ h₂ exy).length} := by + cases exy with + | single x => exact ⟨cons ex h₁ h₂ (single y), by simp⟩ + | cons ey h₃ h₄ eyz => + apply + if c : (x = term G ey) ∧ (ey = G.bar ex) then + ⟨ Eq.symm (Eq.trans (And.left c) h₄) ▸ eyz, by have h₅ : (Eq.symm (Eq.trans (And.left c) h₄) ▸ eyz).length = eyz.length := by let ih := Eq.symm (Eq.trans (And.left c) h₄) cases ih with | refl => rfl - simp[EdgePath.length, h₅, Nat.le_trans (Nat.le_succ (length eyz)) (Nat.le_succ (length eyz +1))] - ⟩ - else - ⟨ cons ex h₁ h₂ (cons ey h₃ h₄ (eyz)), by apply Nat.le_refl⟩ + simp [EdgePath.length, h₅, + Nat.le_trans (Nat.le_succ (length eyz)) (Nat.le_succ (length eyz + 1))] + ⟩ + else + ⟨ cons ex h₁ h₂ (cons ey h₃ h₄ eyz), by apply Nat.le_refl⟩ -/-- reduces given path such that no two consecutive edges are inverses of each other-/ +/-- reduces given path such that no two consecutive edges are inverses of each other -/ def reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} : (p : EdgePath G x y ) → {rp : EdgePath G x y // rp.length ≤ p.length} | single x => ⟨single x, by simp⟩ @@ -170,144 +196,191 @@ def reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} : (p : EdgePath G ⟨ ez , by have : length (cons ex h₁ h₂ ey'z) = length ey'z + 1 := by simp[length] let k := this ▸ ih - have pr : length ey'z +1 ≤ length ey'y +1 := by apply Nat.succ_le_succ ih1 + have pr : length ey'z + 1 ≤ length ey'y + 1 := by apply Nat.succ_le_succ ih1 simp[length, Nat.le_trans k pr] ⟩ - termination_by p => p.length decreasing_by - simp_wf - simp[EdgePath.length, Nat.lt_succ_self] + simp[EdgePath.length] -/--defines moves allowing homotopy of edgepaths-/ +/-- defines moves allowing homotopy of edgepaths -/ inductive basicht {G : Graph V E} : EdgePath G x y → EdgePath G x y → Prop where | consht : (x : V) → (basicht (single x) (single x)) -- constant homotopy - | cancel : (ex ex' : E) → { x w y : V} → (p : EdgePath G x y) → -- cancelling consecutive opposite edges from a path - (h : G.init ex = x) → (h' : term G ex = w) → (t : G.bar ex = ex') → - basicht p (cons ex h h' (cons ex' (t ▸ init_bar_equals_term h') (t ▸ term_bar_equals_init h) p)) + | cancel : + (ex ex' : E) → {x w y : V} → (p : EdgePath G x y) → + (h : G.init ex = x) → (h' : term G ex = w) → (t : G.bar ex = ex') → + basicht p + (cons ex h h' (cons ex' (t ▸ init_bar_equals_term h') + (t ▸ term_bar_equals_init h) p)) | mult : {x y z : V} → {p q : EdgePath G y z} → -- adding an edge to homotopic paths - basicht p q → (ex : E) →(h' : G.init ex = x) → ( h : term G ex = y)→ + basicht p q → (ex : E) → (h' : G.init ex = x) → (h : term G ex = y) → basicht (cons ex h' h p) (cons ex h' h q) /-- The set of homotopy classes of edge paths from `x` to `y`. -/ -def ht (G : Graph V E) (x y : V) := Quot (@basicht V E G x y ) +def ht (G : Graph V E) (x y : V) := Quot (@basicht V E G x y) /-- The homotopy class of an edge path. -/ -def htclass {G : Graph V E} {x y : V} ( p : EdgePath G x y) : ht G x y := - Quot.mk (@basicht V E G x y ) p +def htclass {G : Graph V E} {x y : V} (p : EdgePath G x y) : ht G x y := + Quot.mk (@basicht V E G x y) p /-- Homotopy of edge paths as equality of their quotient classes. -/ -def homotopy {G : Graph V E} {x y : V} ( p' q' : EdgePath G x y) : Prop := +def homotopy {G : Graph V E} {x y : V} (p' q' : EdgePath G x y) : Prop := htclass p' = htclass q' -/--proves that homotopy is a transitive relation-/ -theorem homotopy_trans {G : Graph V E} {x y : V} (p q r : EdgePath G x y) : homotopy p q → homotopy q r → homotopy p r := by +/-- proves that homotopy is a transitive relation -/ +theorem homotopy_trans {G : Graph V E} {x y : V} (p q r : EdgePath G x y) : + homotopy p q → homotopy q r → homotopy p r := by intro h₁ h₂ - simp[homotopy, htclass] + change Quot.mk basicht p = Quot.mk basicht r have p₁ : Quot.mk basicht p = Quot.mk basicht q := by apply h₁ have p₂ : Quot.mk basicht q = Quot.mk basicht r := by apply h₂ apply Eq.trans p₁ p₂ -/--proves that homotopy is preserved by multiplying an edge to the left-/ -theorem homotopy_left_mult_edge {G : Graph V E} {x y z : V}: (p q : EdgePath G y z) → homotopy p q → (ex : E) →(h1 : G.init ex = x) → ( h : term G ex = y)→ homotopy (cons ex h1 h p) (cons ex h1 h q) := by +/-- proves that homotopy is preserved by multiplying an edge to the left -/ +theorem homotopy_left_mult_edge {G : Graph V E} {x y z : V} : + (p q : EdgePath G y z) → homotopy p q → (ex : E) → (h1 : G.init ex = x) → + (h : term G ex = y) → homotopy (cons ex h1 h p) (cons ex h1 h q) := by intro p q h ex h1 h2 let func (r : EdgePath G y z) : ht G x z := htclass (cons ex h1 h2 r) have g : (r₁ r₂ : EdgePath G y z) → basicht r₁ r₂ → func r₁ = func r₂ := by intro r₁ r₂ h₁ let t := basicht.mult h₁ ex h1 h2 - have : htclass (cons ex h1 h2 r₁) = htclass (cons ex h1 h2 r₂) := by simp[htclass]; apply Quot.sound t + have : htclass (cons ex h1 h2 r₁) = htclass (cons ex h1 h2 r₂) := by + exact Quot.sound t exact this - simp[homotopy] + change Quot.lift func g (htclass p) = Quot.lift func g (htclass q) let k := Quot.lift func g apply congrArg k h -/--proves that homotopy is left multiplicative-/ -theorem homotopy_left_mult {G : Graph V E} {x y z : V} (p1 p2 : EdgePath G y z) (q : EdgePath G x y) (h :homotopy p1 p2): +/-- proves that homotopy is left multiplicative -/ +theorem homotopy_left_mult {G : Graph V E} {x y z : V} + (p1 p2 : EdgePath G y z) (q : EdgePath G x y) (h : homotopy p1 p2) : (homotopy (multiply q p1) (multiply q p2)) := by induction q with | single w => simp [multiply, h] | cons ex h1 h2 exy ih => let c := ih p1 p2 h - have t₁ : multiply (cons ex h1 h2 exy) p1 = cons ex h1 h2 (multiply exy p1) := by simp[multiply, mult_assoc] - have t₂ : multiply (cons ex h1 h2 exy) p2 = cons ex h1 h2 (multiply exy p2) := by simp[multiply, mult_assoc] + have t₁ : + multiply (cons ex h1 h2 exy) p1 = cons ex h1 h2 (multiply exy p1) := by + simp [multiply] + have t₂ : + multiply (cons ex h1 h2 exy) p2 = cons ex h1 h2 (multiply exy p2) := by + simp [multiply] rw[t₁, t₂] simp[homotopy_left_mult_edge, c] -/--proves that homotopy is reflexive-/ -theorem homotopy_rfl {G :Graph V E} {x y : V} (p : EdgePath G x y) : homotopy p p := by rfl +/-- proves that homotopy is reflexive -/ +theorem homotopy_rfl {G : Graph V E} {x y : V} (p : EdgePath G x y) : homotopy p p := by rfl -/--proves that path is homotopic to itself after appending cancelling pair of edges at its end-/ -theorem induct_homotopy_inverse_cancel {G : Graph V E} (ey ey' : E) { x w y : V} (p : EdgePath G x y) (h₁ : G.init ey = y) (h₂ : term G ey = w) (t : G.bar ey = ey') (h₃ : G.init ey' = w) (h₄ : term G ey' = y) : +/-- proves that path is homotopic to itself after appending cancelling pair of edges at its end -/ +theorem induct_homotopy_inverse_cancel {G : Graph V E} (ey ey' : E) {x w y : V} + (p : EdgePath G x y) (h₁ : G.init ey = y) (h₂ : term G ey = w) + (t : G.bar ey = ey') (h₃ : G.init ey' = w) (h₄ : term G ey' = y) : homotopy p (multiply p (cons ey h₁ h₂ (cons ey' h₃ h₄ (single y)) )) := by induction p with - | single x => simp[multiply, basicpath, homotopy, htclass, Quot.sound (basicht.cancel ey ey' (single x) h₁ h₂ t)] + | single x => + simp [multiply, homotopy, htclass, + Quot.sound (basicht.cancel ey ey' (single x) h₁ h₂ t)] | cons ex t₁ t₂ exy ih => let x := ih h₁ h₄ - have p₁ : homotopy (cons ex t₁ t₂ exy) (cons ex t₁ t₂ (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))))) := by simp[homotopy_left_mult_edge _ _ x ex t₁ t₂] - have : cons ex t₁ t₂ (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _)))) = multiply (cons ex t₁ t₂ exy) (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))) := by simp[multiply] + have p₁ : + homotopy (cons ex t₁ t₂ exy) + (cons ex t₁ t₂ + (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))))) := by + simp[homotopy_left_mult_edge _ _ x ex t₁ t₂] + have : + cons ex t₁ t₂ + (multiply exy (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _)))) = + multiply (cons ex t₁ t₂ exy) + (cons ey h₁ h₂ (cons ey' h₃ h₄ (single _))) := by + simp[multiply] exact this ▸ p₁ -/--proves that a pair of paths remains homotopic after appending a single edge at their ends-/ -theorem induct_homotopy_inverse_mult {G : Graph V E} {x y z : V} (p q : EdgePath G x y) (ey : E) (h₁ : G.init ey = y) (h₂ : term G ey = z) : homotopy p q → homotopy (multiply p (basicpath y ey h₁ h₂)) (multiply q (basicpath y ey h₁ h₂)) := by +/-- proves that a pair of paths remains homotopic after appending a single edge at their ends -/ +theorem induct_homotopy_inverse_mult {G : Graph V E} {x y z : V} + (p q : EdgePath G x y) (ey : E) (h₁ : G.init ey = y) (h₂ : term G ey = z) : + homotopy p q → + homotopy (multiply p (basicpath y ey h₁ h₂)) + (multiply q (basicpath y ey h₁ h₂)) := by intro h - let func : EdgePath G x y → ht G x z := by intro p; exact htclass (multiply p (basicpath y ey h₁ h₂)) + let func : EdgePath G x y → ht G x z := by + intro p + exact htclass (multiply p (basicpath y ey h₁ h₂)) have g : (s₁ s₂ : EdgePath G x y) → (basicht s₁ s₂) → func s₁ = func s₂ := by intro s₁ s₂ ht induction ht with - | consht x => simp[homotopy_rfl] + | consht x => simp | cancel ex ex' r t₁ t₂ t₃ => let x := basicht.cancel ex ex' (multiply r (basicpath _ ey h₁ h₂)) t₁ t₂ t₃ exact Quot.sound x | @mult _ _ _ p₁ p₂ b ex t₁ t₂ ih => let x := homotopy_left_mult_edge _ _ (ih p₁ p₂ h₁ (Quot.sound b)) ex t₁ t₂ exact x - simp[homotopy] + change Quot.lift func g (htclass p) = Quot.lift func g (htclass q) let k := Quot.lift func g apply congrArg k h -/--proves that homotopy of paths implies homotopy of their inverses-/ -theorem homotopy_inverse {G : Graph V E} {x y : V} (p₁ p₂: EdgePath G x y) (q₁ q₂ : EdgePath G y x) (h₁ : q₁ = inverse p₁) (h₂ : q₂ = inverse p₂) : homotopy p₁ p₂ → homotopy q₁ q₂ := by +/-- proves that homotopy of paths implies homotopy of their inverses -/ +theorem homotopy_inverse {G : Graph V E} {x y : V} + (p₁ p₂ : EdgePath G x y) (q₁ q₂ : EdgePath G y x) + (h₁ : q₁ = inverse p₁) (h₂ : q₂ = inverse p₂) : + homotopy p₁ p₂ → homotopy q₁ q₂ := by intro h₀ - let func : EdgePath G x y → ht G y x := by intro p; exact htclass (inverse p) - have g : (s₁ s₂ : EdgePath G x y) → (h : basicht s₁ s₂) → homotopy (inverse s₁) (inverse s₂) := by + let func : EdgePath G x y → ht G y x := by + intro p + exact htclass (inverse p) + have g : (s₁ s₂ : EdgePath G x y) → (h : basicht s₁ s₂) → + homotopy (inverse s₁) (inverse s₂) := by intro s₁ s₂ h induction h with | consht x => simp[inverse, homotopy_rfl] - | cancel ex ex' p t₁ t₂ t₃ => - simp[htclass, inverse, mult_assoc] - apply induct_homotopy_inverse_cancel (G.bar ex') (G.bar ex) (inverse p) (by rw[← t₃]; rw[bar_involution ex]; apply t₁) (by rw[← t₃]; rw[(bar_involution ex)]; apply t₂) (by rw[bar_involution ex']; apply (Eq.symm t₃)) (init_bar_equals_term t₂) (term_bar_equals_init t₁) - + simpa [inverse, mult_assoc] using + induct_homotopy_inverse_cancel (G.bar ex') (G.bar ex) (inverse p) + (by rw[← t₃]; rw[bar_involution ex]; apply t₁) + (by rw[← t₃]; rw[(bar_involution ex)]; apply t₂) + (by rw[bar_involution ex']; apply (Eq.symm t₃)) + (init_bar_equals_term t₂) (term_bar_equals_init t₁) | @mult _ _ _ s₁ s₂ b ex t₁ t₂ ih => - simp[homotopy, inverse] let c := ih s₁ s₂ (inverse s₁) (inverse s₂) rfl rfl (Quot.sound b) - let k := induct_homotopy_inverse_mult (inverse s₁) (inverse s₂) (G.bar ex) t₂ (term_bar_equals_init t₁) c - apply k + let k := + induct_homotopy_inverse_mult (inverse s₁) (inverse s₂) (G.bar ex) t₂ + (term_bar_equals_init t₁) c + simpa [homotopy, inverse] using k let k₂ := Quot.lift func g rw [h₁, h₂] exact congrArg k₂ h₀ -/--homotopy_inverse with lesser arguments-/ -theorem homotopy_inverse_quick {G : Graph V E} {x y : V} {p₁ p₂: EdgePath G x y} : homotopy p₁ p₂ → homotopy (inverse p₁) (inverse p₂) := by - apply homotopy_inverse p₁ p₂ (inverse p₁) (inverse p₂) rfl rfl +/-- homotopy_inverse with lesser arguments -/ +theorem homotopy_inverse_quick {G : Graph V E} {x y : V} {p₁ p₂ : EdgePath G x y} : + homotopy p₁ p₂ → homotopy (inverse p₁) (inverse p₂) := by + apply homotopy_inverse p₁ p₂ (inverse p₁) (inverse p₂) rfl rfl -/-- proves that homotopy is right multiplicative-/ -theorem homotopy_right_mult {G : Graph V E} {x y z : V} (p₁ p₂ : EdgePath G x y) (q : EdgePath G y z) (h :homotopy p₁ p₂): +/-- proves that homotopy is right multiplicative -/ +theorem homotopy_right_mult {G : Graph V E} {x y z : V} + (p₁ p₂ : EdgePath G x y) (q : EdgePath G y z) (h : homotopy p₁ p₂) : (homotopy (multiply p₁ q) (multiply p₂ q)) := by have r₁ : homotopy (inverse p₁) (inverse p₂) := by apply homotopy_inverse_quick h - have r₂ : homotopy (multiply (inverse q) (inverse p₁)) (multiply (inverse q) (inverse p₂)) := by apply homotopy_left_mult; apply r₁ - have r₃ : homotopy (inverse (multiply (inverse q) (inverse p₁))) (inverse (multiply (inverse q) (inverse p₂))) := by apply homotopy_inverse_quick r₂ + have r₂ : + homotopy (multiply (inverse q) (inverse p₁)) + (multiply (inverse q) (inverse p₂)) := by + apply homotopy_left_mult + apply r₁ + have r₃ : + homotopy (inverse (multiply (inverse q) (inverse p₁))) + (inverse (multiply (inverse q) (inverse p₂))) := by + apply homotopy_inverse_quick r₂ let s₁ := inverse_mult x y z p₁ q let s₂ := inverse_involution (multiply p₁ q) let s₃ := Eq.trans (Eq.symm s₂) (congrArg inverse s₁) @@ -317,9 +390,12 @@ theorem homotopy_right_mult {G : Graph V E} {x y z : V} (p₁ p₂ : EdgePath G apply s₃ ▸ t₃ ▸ r₃ -/--defines multiplication of homotopy class with a path to its left-/ -def homotopy_left_multiplication {G :Graph V E} {x y z : V} (p₁ : EdgePath G x y) : ht G y z → ht G x z := by - let func: EdgePath G y z → ht G x z := by intro p; exact htclass (multiply p₁ p) +/-- defines multiplication of homotopy class with a path to its left -/ +def homotopy_left_multiplication {G : Graph V E} {x y z : V} + (p₁ : EdgePath G x y) : ht G y z → ht G x z := by + let func : EdgePath G y z → ht G x z := by + intro p + exact htclass (multiply p₁ p) have g : (q₁ q₂ : EdgePath G y z) → basicht q₁ q₂ → func q₁ = func q₂ := by intro q₁ q₂ h have h' : homotopy q₁ q₂ := by simp[homotopy, htclass, Quot.sound h ] @@ -327,18 +403,21 @@ def homotopy_left_multiplication {G :Graph V E} {x y z : V} (p₁ : EdgePath G x apply Quot.lift func g -/--proves that the multiplication defined above equals homotopy class of multiplied paths -/ -theorem homotopy_left_multiplication_class {G :Graph V E} {x y z : V} (p₁ : EdgePath G x y) (p₂ : EdgePath G y z): homotopy_left_multiplication p₁ (htclass p₂) = htclass (multiply p₁ p₂) := by +/-- proves that the multiplication defined above equals homotopy class of multiplied paths -/ +theorem homotopy_left_multiplication_class {G : Graph V E} {x y z : V} + (p₁ : EdgePath G x y) (p₂ : EdgePath G y z) : + homotopy_left_multiplication p₁ (htclass p₂) = htclass (multiply p₁ p₂) := by simp[htclass, homotopy_left_multiplication] -/--defines multiplication of homotopy-/ +/-- defines multiplication of homotopy -/ def homotopy_multiplication : ht G x y → ht G y z → ht G x z := by intro p₁ p₂ let func (p : EdgePath G x y) : ht G x z := homotopy_left_multiplication p p₂ have g : (q₁ q₂ : EdgePath G x y) → basicht q₁ q₂ → func q₁ = func q₂ := by intro q₁ q₂ h - let crop (p : ht G y z) : Prop := homotopy_left_multiplication q₁ p = homotopy_left_multiplication q₂ p + let crop (p : ht G y z) : Prop := + homotopy_left_multiplication q₁ p = homotopy_left_multiplication q₂ p have g' : (p : ht G y z) → crop p := by intro p have g'' : (p' : EdgePath G y z) → crop (htclass p') := by @@ -358,115 +437,151 @@ def homotopy_multiplication : ht G x y → ht G y z → ht G x z := by infixl: 65 " # " => homotopy_multiplication -/--proves that # is associative up to multiplication by a pair of paths and one homotopy class-/ -theorem homotopy_mult_path_path_assoc {G :Graph V E} {w x y z : V} (p : EdgePath G w x) (q : EdgePath G x y): (r : ht G y z) → (htclass (multiply p q)) # r = (htclass p) # ((htclass q) # r) := by +/-- proves that # is associative up to multiplication by a pair of paths and one homotopy class -/ +theorem homotopy_mult_path_path_assoc {G : Graph V E} {w x y z : V} + (p : EdgePath G w x) (q : EdgePath G x y) : + (r : ht G y z) → (htclass (multiply p q)) # r = (htclass p) # ((htclass q) # r) := by apply Quot.ind intro b - simp[htclass, homotopy_multiplication] - have p₁ : homotopy_left_multiplication (multiply p q) (Quot.mk basicht b) = htclass ( multiply (multiply p q) b) := by rfl - have p₂ : (homotopy_left_multiplication q (Quot.mk basicht b)) = htclass (multiply q b) := by rfl - have p₃ : (homotopy_left_multiplication p (homotopy_left_multiplication q (Quot.mk basicht b))) = htclass (multiply p (multiply q b)) := by rw[p₂]; rfl + change + homotopy_left_multiplication (multiply p q) (Quot.mk basicht b) = + homotopy_left_multiplication p (homotopy_left_multiplication q (Quot.mk basicht b)) + have p₁ : + homotopy_left_multiplication (multiply p q) (Quot.mk basicht b) = + htclass (multiply (multiply p q) b) := by + rfl + have p₂ : + homotopy_left_multiplication q (Quot.mk basicht b) = htclass (multiply q b) := by + rfl + have p₃ : + homotopy_left_multiplication p (homotopy_left_multiplication q (Quot.mk basicht b)) = + htclass (multiply p (multiply q b)) := by + rw[p₂] + rfl rw[p₁,p₃] simp[mult_assoc] -/--proves that # is associative up to multiplication by one path and a pair of homotopy classes -/ -theorem homotopy_mult_path_assoc {G :Graph V E} {w x y z : V} (p : EdgePath G w x) (r : ht G y z): (q : ht G x y) → (htclass p # q) # r = (htclass p) # (q # r) := by +/-- proves that # is associative up to multiplication by one path and a pair of homotopy classes -/ +theorem homotopy_mult_path_assoc {G : Graph V E} {w x y z : V} + (p : EdgePath G w x) (r : ht G y z) : + (q : ht G x y) → (htclass p # q) # r = (htclass p) # (q # r) := by apply Quot.ind intro a - simp[htclass] + change Quot.mk basicht p # Quot.mk basicht a # r = Quot.mk basicht p # (Quot.mk basicht a # r) have p₁ : Quot.mk basicht p # Quot.mk basicht a = htclass (multiply p a) := by rfl rw[p₁] apply homotopy_mult_path_path_assoc p a r -/--proves that # is associative on homotopy classes-/ -theorem homotopy_mult_assoc {G :Graph V E} {w x y z : V} (b : ht G x y) (c : ht G y z) : (a : ht G w x) → ((a # b) # c ) = (a # (b # c) ) := by +/-- proves that # is associative on homotopy classes -/ +theorem homotopy_mult_assoc {G : Graph V E} {w x y z : V} + (b : ht G x y) (c : ht G y z) : + (a : ht G w x) → ((a # b) # c) = (a # (b # c)) := by apply Quot.ind intro a apply homotopy_mult_path_assoc a c b -/--proves that reducePathAux preserves the homotopy class-/ -theorem homotopy_reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) (exy : EdgePath G y z) : homotopy (cons ex h₁ h₂ exy) (reducePathAux ex h₁ h₂ exy) := by - simp[homotopy, htclass] +/-- proves that reducePathAux preserves the homotopy class -/ +theorem homotopy_reducePathAux [DecidableEq V] [DecidableEq E] {G : Graph V E} + {x y z : V} (ex : E) (h₁ : G.init ex = x) (h₂ : term G ex = y) + (exy : EdgePath G y z) : homotopy (cons ex h₁ h₂ exy) (reducePathAux ex h₁ h₂ exy) := by + change + Quot.mk basicht (cons ex h₁ h₂ exy) = + Quot.mk basicht (reducePathAux ex h₁ h₂ exy).val cases exy with | single y => have : reducePathAux ex h₁ h₂ (single y) = cons ex h₁ h₂ (single y) := by rfl rfl | cons ey h₃ h₄ eyz => by_cases c : (x = term G ey) ∧ (ey = G.bar (ex)) - · - let ih := Eq.symm (Eq.trans (And.left c) h₄) + · let ih := Eq.symm (Eq.trans (And.left c) h₄) cases ih with |refl => have : basicht (ih ▸ eyz) (cons ex h₁ h₂ (cons ey h₃ h₄ eyz)) := by let j := @basicht.cancel V E G ex ey x y _ (ih ▸ eyz) h₁ h₂ (Eq.symm c.2) apply j - have pr : (reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz)).1 = (ih ▸ eyz) := by simp[reducePathAux, c] + have pr : (reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz)).1 = (ih ▸ eyz) := by + simp[reducePathAux, c] let k := Quot.sound (Eq.symm pr ▸ this) exact (Eq.symm k) - · - have : reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz) = cons ex h₁ h₂ (cons ey h₃ h₄ (eyz)) := by simp[reducePathAux, c] + · have : + reducePathAux ex h₁ h₂ (cons ey h₃ h₄ eyz) = + cons ex h₁ h₂ (cons ey h₃ h₄ eyz) := by + simp[reducePathAux, c] simp [this] -/--proves that reducePath preserves the homotopy class-/ -theorem homotopy_reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y : V} (p₁ : EdgePath G x y): homotopy p₁ (reducePath p₁) := by +/-- proves that reducePath preserves the homotopy class -/ +theorem homotopy_reducePath [DecidableEq V] [DecidableEq E] {G : Graph V E} {x y : V} + (p₁ : EdgePath G x y) : homotopy p₁ (reducePath p₁) := by induction p₁ with | single x => simp [homotopy, htclass, reducePath] - | cons ex h₁ h₂ exy ih' => let p₃ := reducePath exy let q := p₃.1 let p₄ := reducePathAux ex h₁ h₂ q have : p₄.1 = (reducePath (cons ex h₁ h₂ exy)).1 := by simp [reducePath, p₃, q, p₄] - have t₁ : homotopy (cons ex h₁ h₂ q) (p₄.1) := by apply homotopy_reducePathAux ex h₁ h₂ q + have t₁ : homotopy (cons ex h₁ h₂ q) (p₄.1) := by + apply homotopy_reducePathAux ex h₁ h₂ q have t₂ : homotopy exy q := by apply ih' - have t₃ : homotopy (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) := by apply homotopy_left_mult_edge exy q t₂ ex h₁ h₂ - apply homotopy_trans (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) (reducePath (cons ex h₁ h₂ exy)) t₃ (this ▸ t₁) + have t₃ : homotopy (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) := by + apply homotopy_left_mult_edge exy q t₂ ex h₁ h₂ + apply homotopy_trans (cons ex h₁ h₂ exy) (cons ex h₁ h₂ q) + (reducePath (cons ex h₁ h₂ exy)) t₃ (this ▸ t₁) -instance ht_mul {G : Graph V E} {x : V} : Mul (ht G x x) where -mul : ht G x x → ht G x x → ht G x x := fun a b => homotopy_multiplication a b +instance ht_mul {G : Graph V E} {x : V} : Mul (ht G x x) where + mul : ht G x x → ht G x x → ht G x x := fun a b => homotopy_multiplication a b --defines the identity homotopy class instance ht_one {G : Graph V E} {x : V} : One (ht G x x) where -one : ht G x x := htclass (single x) - -/--proves that multiplication of homotopy classes is associative-/ -theorem ht_mult_assoc {G : Graph V E} {x : V} (a b c : ht G x x) : ((a # b) # c) = (a # ( b # c)) := by -let k := @homotopy_mult_assoc V E G x x x x -let l (a b c : ht G x x) := k b c a -apply (l a b c) - -/--proves that the identity homotopy class is the right multiplicative identity-/ -theorem ht_right_identity {G : Graph V E} {x : V} : (a₀ : ht G x x) → ht_mul.mul a₀ (@ht_one V E G x).one = a₀ := by -have k (b : EdgePath G x x) : homotopy_multiplication (htclass b) (htclass (single x)) = (htclass b) := by - let l :=mult_const b ▸ homotopy_left_multiplication_class b (single x) - have : (htclass b) # (htclass (single x)) = homotopy_left_multiplication b (htclass (single x)) := by rfl + one : ht G x x := htclass (single x) + +/-- proves that multiplication of homotopy classes is associative -/ +theorem ht_mult_assoc {G : Graph V E} {x : V} (a b c : ht G x x) : + ((a # b) # c) = (a # (b # c)) := by + let k := @homotopy_mult_assoc V E G x x x x + let l (a b c : ht G x x) := k b c a + apply (l a b c) + +/-- proves that the identity homotopy class is the right multiplicative identity -/ +theorem ht_right_identity {G : Graph V E} {x : V} : + (a₀ : ht G x x) → ht_mul.mul a₀ (@ht_one V E G x).one = a₀ := by + have k (b : EdgePath G x x) : + homotopy_multiplication (htclass b) (htclass (single x)) = htclass b := by + let l := mult_const b ▸ homotopy_left_multiplication_class b (single x) + have : + (htclass b) # (htclass (single x)) = + homotopy_left_multiplication b (htclass (single x)) := by + rfl apply Eq.trans this l -have k₂ (b : EdgePath G x x) : ht_mul.mul (htclass b) (@ht_one V E G x).one = htclass b := by - apply k -apply Quot.ind -apply k₂ - -/--proves that the identity homotopy class is the left multiplicative identity-/ -theorem ht_left_identity {G : Graph V E} {x : V} : (a₀ : ht G x x) → ht_mul.mul (@ht_one V E G x).one a₀ = a₀ := by -have k (b : EdgePath G x x) : homotopy_multiplication (htclass (single x)) (htclass b) = (htclass b) := by + have k₂ (b : EdgePath G x x) : + ht_mul.mul (htclass b) (@ht_one V E G x).one = htclass b := by + apply k + apply Quot.ind + apply k₂ + +/-- proves that the identity homotopy class is the left multiplicative identity -/ +theorem ht_left_identity {G : Graph V E} {x : V} : + (a₀ : ht G x x) → ht_mul.mul (@ht_one V E G x).one a₀ = a₀ := by + have k (b : EdgePath G x x) : + homotopy_multiplication (htclass (single x)) (htclass b) = htclass b := by exact homotopy_left_multiplication_class (single x) b -have k₂ (b : EdgePath G x x) : ht_mul.mul (@ht_one V E G x).one (htclass b) = htclass b := by - apply k -apply Quot.ind -apply k₂ + have k₂ (b : EdgePath G x x) : + ht_mul.mul (@ht_one V E G x).one (htclass b) = htclass b := by + apply k + apply Quot.ind + apply k₂ instance ht_semigroup {G : Graph V E} {x : V} : Semigroup (ht G x x) where -mul := (@ht_mul V E G x).mul -mul_assoc := by apply ht_mult_assoc + mul := (@ht_mul V E G x).mul + mul_assoc := by apply ht_mult_assoc /-- The monoid structure on loops at a vertex modulo homotopy. -/ @[reducible] def ht_monoid (G : Graph V E) (x : V) : Monoid (ht G x x) where diff --git a/LeanPool/Polylean/ConjInvLength/Length.lean b/LeanPool/Polylean/ConjInvLength/Length.lean index 739514cb2f..863ff09049 100644 --- a/LeanPool/Polylean/ConjInvLength/Length.lean +++ b/LeanPool/Polylean/ConjInvLength/Length.lean @@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Siddhartha Gadgil, Anand Rao -/ -import Batteries +import Std.Data.HashMap import LeanPool.Polylean.ConjInvLength.LengthBound namespace LeanPool.Polylean -open Batteries open Letter namespace Letter @@ -33,14 +32,14 @@ abbrev Wrd := Array Letter namespace Word /-- Convert a list-backed word to an array-backed word. -/ -def wrd (w: Word) : Wrd := w.toArray -- .map <| fun l => l.int +def wrd (w : Word) : Wrd := w.toArray -- .map <| fun l => l.int end Word namespace Wrd /-- Render an array-backed word by concatenating rendered letters. -/ -def toString(w: Wrd) := w.foldl (fun x y => s!"{x}{y}") "" +def toString (w : Wrd) := w.foldl (fun x y => s!"{x}{y}") "" instance : ToString Wrd := ⟨Wrd.toString⟩ @@ -53,16 +52,17 @@ instance : Pow Wrd Nat where pow w n := w.pow n /-- Hash function for array-backed words. -/ -def hashfn (w: Wrd) : UInt64 := +def hashfn (w : Wrd) : UInt64 := w.foldl (fun h i => mixHash h (hash i)) 7 instance : Hashable Wrd := ⟨hashfn⟩ /-- Cache for normalized word lengths. -/ -initialize normCache : IO.Ref (HashMap Wrd Nat) ← IO.mkRef (HashMap.empty) +initialize normCache : IO.Ref (Std.HashMap Wrd Nat) ← IO.mkRef Std.HashMap.emptyWithCapacity /-- All splits of an array-backed word around occurrences of a letter. -/ -def splits(l : Letter) : (w : Wrd) → Array {p : Wrd × Wrd // p.1.size + p.2.size < w.size} := fun w => +def splits (l : Letter) : + (w : Wrd) → Array {p : Wrd × Wrd // p.1.size + p.2.size < w.size} := fun w => match h:w.size with | 0 => #[] | m + 1 => @@ -78,7 +78,6 @@ def splits(l : Letter) : (w : Wrd) → Array {p : Wrd × Wrd // p.1.size + p.2.s ⟨(fst, snd.push x), by rw [Array.size_push] rw [ysize] at h - simp simp at h rw [← Nat.add_assoc] simp [Nat.succ_lt_succ h]⟩ @@ -89,10 +88,10 @@ def splits(l : Letter) : (w : Wrd) → Array {p : Wrd × Wrd // p.1.size + p.2.s termination_by w => w.size /-- Memoized conjugation-invariant length candidate for array-backed words. -/ -def length(w : Wrd) : IO Nat := +def length (w : Wrd) : IO Nat := do let cache ← normCache.get - match cache.find? w with + match cache.get? w with | some n => pure n | none => @@ -125,16 +124,16 @@ termination_by w.size end Wrd /-- Memoized length for list-backed words. -/ -def wordLength(w: Word):IO Nat := +def wordLength (w : Word) : IO Nat := Wrd.length <| Word.wrd w namespace Wrd /-- Conjugate an array-backed word by a letter. -/ -def conj: Wrd → Letter → Wrd := fun w l => #[l] ++ w ++ #[l⁻¹] +def conj : Wrd → Letter → Wrd := fun w l => #[l] ++ w ++ #[l⁻¹] end Wrd -instance: Pow Wrd Letter where +instance : Pow Wrd Letter where pow w l := w.conj l end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/LengthBound.lean b/LeanPool/Polylean/ConjInvLength/LengthBound.lean index 2f856c948f..3b328dabad 100644 --- a/LeanPool/Polylean/ConjInvLength/LengthBound.lean +++ b/LeanPool/Polylean/ConjInvLength/LengthBound.lean @@ -46,13 +46,13 @@ abbrev Word := List Letter namespace Word /-- Render a word by concatenating its rendered letters. -/ -def toString(w: Word) := w.foldl (fun x y => s!"{x}{y}") "" +def toString (w : Word) := w.foldl (fun x y => s!"{x}{y}") "" instance : ToString Word := ⟨Word.toString⟩ /-- Repeated concatenation of a word. -/ def pow : Word → Nat → Word - | w, 0 => [] + | _, 0 => [] | w, Nat.succ m => w ++ (pow w m) instance : Pow Word Nat where @@ -68,14 +68,14 @@ def splits (l : Letter) : (w : Word) → List {p : Word × Word // p.1.length + | x :: ys => let tailSplits := (splits l ys).map fun ⟨(fst, snd), h⟩ => ⟨(x :: fst, snd), by simp [Nat.succ_add, Nat.succ_lt_succ h]⟩ - if x = l then ⟨([], ys), by simp [Nat.lt_succ_self]⟩ :: tailSplits else tailSplits + if x = l then ⟨([], ys), by simp⟩ :: tailSplits else tailSplits /-- A recursively computed conjugation-invariant length candidate. -/ def length : Word → Nat | [] => 0 | x :: ys => have lb : (List.length ys) < List.length (x :: ys) := by - simp [List.length_cons, Nat.le_refl] + simp [List.length_cons] let base := 1 + (length ys) let derived := (splits x⁻¹ ys).map fun ⟨(fst, snd), h⟩ => have h : fst.length + snd.length < ys.length + 1 := Nat.lt_trans h (Nat.lt_succ_self _) @@ -90,10 +90,10 @@ termination_by l => l.length namespace Word /-- Conjugate a word by a letter. -/ -def conj: Word → Letter → Word := fun w l => [l] ++ w ++ [l⁻¹] +def conj : Word → Letter → Word := fun w l => [l] ++ w ++ [l⁻¹] end Word -instance: Pow Word Letter where +instance : Pow Word Letter where pow w l := w.conj l end LeanPool.Polylean diff --git a/LeanPool/Polylean/ConjInvLength/MemoLength.lean b/LeanPool/Polylean/ConjInvLength/MemoLength.lean index 626143433e..086558813b 100644 --- a/LeanPool/Polylean/ConjInvLength/MemoLength.lean +++ b/LeanPool/Polylean/ConjInvLength/MemoLength.lean @@ -4,19 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Siddhartha Gadgil, Anand Rao -/ -import Batteries +import Std.Data.HashMap import LeanPool.Polylean.ConjInvLength.LengthBound namespace LeanPool.Polylean -open Batteries /-- Cache for memoized word lengths. -/ -initialize normCache : IO.Ref (HashMap Word Nat) ← IO.mkRef (HashMap.empty) +initialize normCache : IO.Ref (Std.HashMap Word Nat) ← IO.mkRef Std.HashMap.emptyWithCapacity /-- Memoized list-backed conjugation-invariant length candidate. -/ def memoLength : Word → IO Nat := fun w => do let cache ← normCache.get - match cache.find? w with + match cache.get? w with | some n => pure n | none => @@ -24,7 +23,7 @@ def memoLength : Word → IO Nat := fun w => do | [] => return 0 | x :: ys => do have lb : (List.length ys) < List.length (x :: ys) := by - simp [List.length_cons, Nat.le_refl] + simp [List.length_cons] let base := 1 + (← memoLength ys) let derived ← (splits x⁻¹ ys).mapM fun ⟨(fst, snd), h⟩ => do have h : fst.length + snd.length < ys.length + 1 := Nat.lt_trans h (Nat.lt_succ_self _) diff --git a/LeanPool/Polylean/ConjInvLength/ProvedBound.lean b/LeanPool/Polylean/ConjInvLength/ProvedBound.lean index d8773abe16..598d58dd88 100644 --- a/LeanPool/Polylean/ConjInvLength/ProvedBound.lean +++ b/LeanPool/Polylean/ConjInvLength/ProvedBound.lean @@ -10,11 +10,11 @@ namespace LeanPool.Polylean open Letter /-- A split of a word around a distinguished letter, with a proof of reconstruction. -/ -structure ProvedSplit (l: Letter)(w : Word) where +structure ProvedSplit (l : Letter) (w : Word) where /-- The part before the distinguished letter. -/ fst : Word /-- The part after the distinguished letter. -/ - snd: Word + snd : Word /-- Reconstruction proof for the split. -/ proof : w = fst ++ [l] ++ snd @@ -23,13 +23,13 @@ structure ProvedSplit (l: Letter)(w : Word) where namespace ProvedSplit /-- Split with the first piece empty when the head matches the splitting letter. -/ -def head (x: Letter) (ys: Word) : ProvedSplit x (x :: ys) := +def head (x : Letter) (ys : Word) : ProvedSplit x (x :: ys) := ⟨[], ys, rfl⟩ -- Prepend to a proved split of the tail (`l` and `ys` implicit). /-- Prepend a letter to the first component of a proved split. -/ -def prepend{l: Letter}{ys : Word} (x: Letter) - (ps: ProvedSplit l ys) : ProvedSplit l (x :: ys) := +def prepend {l : Letter} {ys : Word} (x : Letter) + (ps : ProvedSplit l ys) : ProvedSplit l (x :: ys) := let newFst := x :: ps.fst let newSnd := ps.snd have newProof : x :: ys = newFst ++ [l] ++ newSnd := @@ -42,7 +42,7 @@ end ProvedSplit -- all proved splits of a word /-- All proved splits of a word around a letter. -/ -def provedSplits(z: Letter) : (w : Word) → List (ProvedSplit z w) +def provedSplits (z : Letter) : (w : Word) → List (ProvedSplit z w) | [] => [] | x :: ys => let tailSplits := (provedSplits z ys).map (ProvedSplit.prepend x) @@ -55,26 +55,26 @@ def provedSplits(z: Letter) : (w : Word) → List (ProvedSplit z w) abbrev Length := Word → Nat /-- A length function invariant under conjugation by letters. -/ -def conjInv(l: Length) : Prop := (x : Letter) → (g : Word) → l (g^x) = l (g) +def conjInv (l : Length) : Prop := (x : Letter) → (g : Word) → l (g^x) = l (g) /-- The triangle inequality for a length function. -/ -def triangIneq(l: Length) : Prop := (g h : Word) → l (g ++ h) ≤ l g + l h +def triangIneq (l : Length) : Prop := (g h : Word) → l (g ++ h) ≤ l g + l h /-- A length function normalized on single letters. -/ -def normalized(l: Length) : Prop := (x : Letter) → l [x] = 1 +def normalized (l : Length) : Prop := (x : Letter) → l [x] = 1 /-- A length function that sends the empty word to zero. -/ -def emptyWord(l: Length) : Prop := l [] = 0 +def emptyWord (l : Length) : Prop := l [] = 0 /-- A certified upper bound for the length of a word. -/ -structure ProvedBound(g: Word): Type where +structure ProvedBound (g : Word) : Type where /-- The numeric upper bound. -/ - bound: Nat + bound : Nat /-- The proof that every normalized conjugation-invariant length is bounded by `bound`. -/ - pf : (l: Length) → emptyWord l → + pf : (l : Length) → emptyWord l → normalized l → conjInv l → triangIneq l → l g ≤ bound -theorem conj_split (x: Letter) (ys fst snd: Word) : +theorem conj_split (x : Letter) (ys fst snd : Word) : ys = fst ++ [x⁻¹] ++ snd → x :: ys = fst^x ++ snd := by intro hyp @@ -87,13 +87,13 @@ theorem conj_split (x: Letter) (ys fst snd: Word) : namespace ProvedBound /-- Combine certified bounds across a split around a conjugating letter. -/ -def headMatches(x: Letter)(ys fst snd: Word) +def headMatches (x : Letter) (ys fst snd : Word) (eqn : ys = fst ++ [x⁻¹] ++ snd) : ProvedBound fst → ProvedBound snd → ProvedBound (x :: ys) := fun pb1 pb2 => let bound := pb1.bound + pb2.bound let pf : - (l: Length) → emptyWord l → normalized l → conjInv l → triangIneq l → + (l : Length) → emptyWord l → normalized l → conjInv l → triangIneq l → l (x :: ys) ≤ bound := by intros l emp norm conj triang rw [conj_split x ys fst snd eqn] @@ -108,8 +108,8 @@ def headMatches(x: Letter)(ys fst snd: Word) -- deducing `l(xh) ≤ b + 1` given `l(h) ≤ b` /-- Prepend a letter to a certified bound. -/ -def prepend{w : Word} (x: Letter) - (ps: ProvedBound w) : ProvedBound (x :: w) := +def prepend {w : Word} (x : Letter) + (ps : ProvedBound w) : ProvedBound (x :: w) := let newBound := ps.bound + 1 ⟨newBound, fun l emp norm conj triang => by let prev := ps.pf l emp norm conj triang @@ -121,7 +121,7 @@ def prepend{w : Word} (x: Letter) -- `l(e) ≤ 0` /-- The zero bound for the empty word. -/ -def emptyWord: ProvedBound [] := +def emptyWord : ProvedBound [] := ⟨0, fun l emp _ _ _ => by rw [emp] apply Nat.zero_le @@ -129,7 +129,7 @@ def emptyWord: ProvedBound [] := -- the best proved bound for a word /-- Choose the better bound from a nonempty list of alternatives. -/ -def min {w: Word}: ProvedBound w → List (ProvedBound w) → +def min {w : Word} : ProvedBound w → List (ProvedBound w) → ProvedBound w := fun head tail => tail.foldl (fun pb1 pb2 => @@ -137,7 +137,7 @@ def min {w: Word}: ProvedBound w → List (ProvedBound w) → end ProvedBound -theorem splitFirst{l: Letter}{w: Word}(ps: ProvedSplit l w): +theorem splitFirst {l : Letter} {w : Word} (ps : ProvedSplit l w) : ps.fst.length + 1 ≤ w.length := by let lem : (ps.fst ++ [l] ++ ps.snd).length = @@ -149,7 +149,7 @@ theorem splitFirst{l: Letter}{w: Word}(ps: ProvedSplit l w): rw [lem2] apply Nat.le_add_right -theorem splitSecond{l: Letter}{w: Word}(ps: ProvedSplit l w): +theorem splitSecond {l : Letter} {w : Word} (ps : ProvedSplit l w) : ps.snd.length + 1 ≤ w.length := by let lem : (ps.fst ++ [l] ++ ps.snd).length = @@ -165,12 +165,12 @@ theorem splitSecond{l: Letter}{w: Word}(ps: ProvedSplit l w): -- bound with proof for words /-- Compute a certified length bound for a word. -/ -def provedBound : (w: Word) → ProvedBound w := fun w => +def provedBound : (w : Word) → ProvedBound w := fun w => match h:w with | [] => ProvedBound.emptyWord | x :: ys => have lb : (List.length ys) < List.length (x :: ys) := by - simp [List.length_cons, Nat.le_refl] + simp [List.length_cons] let head := ProvedBound.prepend x (provedBound ys) let splits := provedSplits x⁻¹ ys have wl: w.length = ys.length + 1 := by diff --git a/LeanPool/Polylean/ConjInvLength/WordTree.lean b/LeanPool/Polylean/ConjInvLength/WordTree.lean index 0e2510c06c..cb375f4e05 100644 --- a/LeanPool/Polylean/ConjInvLength/WordTree.lean +++ b/LeanPool/Polylean/ConjInvLength/WordTree.lean @@ -12,7 +12,7 @@ namespace LeanPool.Polylean inductive ProofTree : Word → Type where | emptyWord : ProofTree [] | normalized : (l : Letter) → ProofTree [l] - | conjugate : (l : Letter) → (w: Word) → ProofTree w → ProofTree (w^l) + | conjugate : (l : Letter) → (w : Word) → ProofTree w → ProofTree (w^l) | triangleIneq : (w₁ : Word) → (w₂ : Word) → ProofTree w₁ → ProofTree w₂ → ProofTree (w₁ ++ w₂) deriving Repr @@ -20,7 +20,7 @@ inductive ProofTree : Word → Type where namespace ProofTree /-- The numeric bound represented by a proof tree. -/ -def bound: (w: Word) → ProofTree w → Nat := +def bound : (w : Word) → ProofTree w → Nat := fun w t => match t with | ProofTree.emptyWord => 0 @@ -29,7 +29,7 @@ def bound: (w: Word) → ProofTree w → Nat := | ProofTree.triangleIneq w₁ w₂ t₁ t₂ => bound w₁ t₁ + bound w₂ t₂ /-- Convert a proof tree into a certified bound. -/ -def provedBound: (w: Word) → ProofTree w → ProvedBound w := +def provedBound : (w : Word) → ProofTree w → ProvedBound w := fun w t => match t with | ProofTree.emptyWord => ProvedBound.emptyWord @@ -51,31 +51,31 @@ def provedBound: (w: Word) → ProofTree w → ProvedBound w := intros l emp norm conj triang apply Nat.le_trans (triang w₁ w₂) apply Nat.add_le_add - exact pb1.pf l emp norm conj triang - exact pb2.pf l emp norm conj triang + · exact pb1.pf l emp norm conj triang + · exact pb2.pf l emp norm conj triang ⟩ /-- Combine proof trees across a split around a conjugating letter. -/ -def headMatches(x: Letter)(ys fst snd: Word) +def headMatches (x : Letter) (ys fst snd : Word) (eqn : ys = fst ++ [x⁻¹] ++ snd) : ProofTree fst → ProofTree snd → ProofTree (x :: ys) := by intros pt1 pt2 rw [conj_split x ys fst snd eqn] apply ProofTree.triangleIneq - exact ProofTree.conjugate x fst pt1 - exact pt2 + · exact ProofTree.conjugate x fst pt1 + · exact pt2 /-- Prepend a normalized letter to a proof tree. -/ -def prepend{w : Word} (x: Letter) - (pt: ProofTree w) : ProofTree (x :: w) := by +def prepend {w : Word} (x : Letter) + (pt : ProofTree w) : ProofTree (x :: w) := by have exp : x :: w = [x] ++ w := by rfl rw [exp] apply ProofTree.triangleIneq - exact ProofTree.normalized x - exact pt + · exact ProofTree.normalized x + · exact pt /-- Choose the proof tree with the smallest bound from a nonempty list. -/ -def min {w: Word}: ProofTree w → List (ProofTree w) → +def min {w : Word} : ProofTree w → List (ProofTree w) → ProofTree w := fun head tail => tail.foldl (fun pt1 pt2 => @@ -84,21 +84,21 @@ def min {w: Word}: ProofTree w → List (ProofTree w) → end ProofTree /-- A simple proof tree obtained by splitting a word into letters. -/ -def simpleTree(w: Word) : ProofTree w := +def simpleTree (w : Word) : ProofTree w := match w with | [] => ProofTree.emptyWord | x :: ys => by have exp : x :: ys = [x] ++ ys := by rfl rw [exp] apply ProofTree.triangleIneq - exact ProofTree.normalized x - exact simpleTree ys + · exact ProofTree.normalized x + · exact simpleTree ys -instance {w: Word} : Inhabited (ProofTree w) :=⟨simpleTree w⟩ +instance {w : Word} : Inhabited (ProofTree w) := ⟨simpleTree w⟩ /-- Compute a proof tree for a word. -/ -def proofTree : (w: Word) → ProofTree w := fun w => +def proofTree : (w : Word) → ProofTree w := fun w => match h:w with | [] => ProofTree.emptyWord | x :: ys =>