Grace/Cumulus/Algebra/Group/FreeGroup.g17

Open in Workbench Download source

Imports

Words · Coset

Declarations

Source

1-- The free group on two generators as a structure value: the reduced2-- words under the reduction of their concatenation, the generators freeA3-- and freeB, the reduced words starting with a given letter, and the4-- paradoxical decomposition of the free group into those sets5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Group.FreeGroup11import Words12import Coset1314-- The product of two reduced words reduces their concatenation, and the15-- inverse of a reduced word reduces its inverse word; both are graphs on16-- the reduced words.17defgraph freeMul (p ∈ reducedWords × reducedWords) : reducedWords :=18  reduce(concat(fst(p), snd(p)))19proof20  obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with member21  have listU := reducedWords.list with hu22  have listV := reducedWords.list with hv23  rw [shape, fst.pair, snd.pair]24  exact reduce.mem with *2526defgraph freeInv (w ∈ reducedWords) : reducedWords := reduce(inverseWord(w))27proof28  have list := reducedWords.list with member29  have inverse := inverseWord.closed with list30  exact reduce.mem with inverse3132-- The free group on the two generators freeA = [0] and freeB = [2].33def freeGroup : Set := Group.mk(reducedWords, freeMul, [], freeInv)34def freeA : Set := 0 :: []35def freeB : Set := 2 :: []3637-- The reduced words whose first letter is ℓ.38def startsWith (ℓ : Set) : Set := { w ∈ reducedWords | ∃ u, w = ℓ :: u }3940theorem freeGroup.carrierOf41  shows Group.carrier(freeGroup) = reducedWords42proof43  simp [freeGroup, Group.mk.carrier]4445theorem freeGroup.operation46  shows Group.mul(freeGroup) = freeMul47proof48  simp [freeGroup, Group.mk.mul]4950theorem freeGroup.unit51  shows Group.one(freeGroup) = []52proof53  simp [freeGroup, Group.mk.one]5455theorem freeGroup.inverse56  shows Group.inv(freeGroup) = freeInv57proof58  simp [freeGroup, Group.mk.inv]5960-- The product and the inverse on reduced words.61theorem freeMul.apply (u v : Set)62  requires hu : u ∈ reducedWords63  requires hv : v ∈ reducedWords64  shows freeMul(u, v) = reduce(concat(u, v))65proof66  have pair := product.pair at u, v, reducedWords, reducedWords with *67  have value := freeMul.value at (u, v) with pair68  simp [call2]69  rw [fst.pair, snd.pair]70  rfl7172theorem freeMul.mem (u v : Set)73  requires hu : u ∈ reducedWords74  requires hv : v ∈ reducedWords75  shows freeMul(u, v) ∈ reducedWords76proof77  have listU := reducedWords.list with hu78  have listV := reducedWords.list with hv79  rw freeMul.apply80  exact reduce.mem with *8182theorem freeInv.apply (w : Set)83  requires hw : w ∈ reducedWords84  shows freeInv(w) = reduce(inverseWord(w))85proof86  exact freeInv.value at w with hw8788theorem freeInv.mem (w : Set)89  requires hw : w ∈ reducedWords90  shows freeInv(w) ∈ reducedWords91proof92  have list := reducedWords.list with hw93  have inverse := inverseWord.closed with list94  rw freeInv.apply95  exact reduce.mem with inverse9697-- The free group is a group.98theorem freeGroup.group99  shows Group(freeGroup)100proof101  have mulFunction := freeMul.function102  have invFunction := freeInv.function103  have unitIn := reducedWords.nil_mem104  unfold freeGroup105  apply Group.intro with mulFunction, unitIn, invFunction106  . intros a ha b hb c hc107    have listA := reducedWords.list with ha108    have listB := reducedWords.list with hb109    have listC := reducedWords.list with hc110    have abIn := freeMul.mem with ha, hb111    have bcIn := freeMul.mem with hb, hc112    have ab := freeMul.apply with ha, hb113    have bc := freeMul.apply with hb, hc114    have left := freeMul.apply with abIn, hc115    have right := freeMul.apply with ha, bcIn116    have leftLaw := reduce.concat_left at concat(a, b), c with *117    have rightLaw := reduce.concat_right at a, concat(b, c) with *118    have assoc := concat.associative at a, b, c with *119    rw [left, right, ab, bc, ← leftLaw, ← rightLaw, assoc]120    rfl121  . intros a ha122    have listA := reducedWords.list with ha123    have value := freeMul.apply with unitIn, ha124    rw [value, concat.nil_left]125    exact reducedWords.fixed with ha126  . intros a ha127    have listA := reducedWords.list with ha128    have value := freeMul.apply with ha, unitIn129    rw [value, concat.nil_right]130    exact reducedWords.fixed with ha131  . intros a ha132    have listA := reducedWords.list with ha133    have invIn := freeInv.mem with ha134    have value := freeMul.apply with invIn, ha135    have invValue := freeInv.apply with ha136    have law := reduce.concat_left at inverseWord(a), a with *137    rw [value, invValue, ← law]138    exact reduce.inverse_left with listA139  . intros a ha140    have listA := reducedWords.list with ha141    have invIn := freeInv.mem with ha142    have value := freeMul.apply with ha, invIn143    have invValue := freeInv.apply with ha144    have law := reduce.concat_right at a, inverseWord(a) with *145    rw [value, invValue, ← law]146    exact reduce.inverse_right with listA147148theorem freeA.mem149  shows freeA ∈ reducedWords150proof151  have letter := letter.zero_mem152  have reduced := Reduced.singleton with letter153  have list : List(4, 0 :: []) by typecheck154  unfold freeA155  exact reducedWords.of_reduced with list, reduced156157theorem freeB.mem158  shows freeB ∈ reducedWords159proof160  have letter := letter.two_mem161  have reduced := Reduced.singleton with letter162  have list : List(4, 2 :: []) by typecheck163  unfold freeB164  exact reducedWords.of_reduced with list, reduced165166-- Multiplying by a single letter pushes it onto the word.167theorem freeMul.letter (ℓ w : Set)168  requires hℓ : ℓ ∈ 4169  requires hw : w ∈ reducedWords170  shows freeMul(ℓ :: [], w) = pushLetter(ℓ, w)171proof172  have list := reducedWords.list with hw173  have single : List(4, ℓ :: []) by typecheck174  have singleIn := reducedWords.of_reduced with single, (Reduced.singleton with hℓ)175  have value := freeMul.apply with singleIn, hw176  have fixed := reducedWords.fixed with hw177  rw [value, concat.singleton, reduce.cons, fixed]178  rfl179180-- The words starting with a letter.181theorem startsWith.subset (ℓ : Set)182  shows startsWith(ℓ) ⊆ reducedWords183proof184  intros w hw185  have parts := startsWith.membership.forward with hw186  exact parts.left187188theorem startsWith.of_reduced (ℓ : Set) (u : List(4))189  requires hℓ : ℓ ∈ 4190  requires reduced : Reduced(ℓ :: u)191  shows ℓ :: u ∈ startsWith(ℓ)192proof193  have list : List(4, ℓ :: u) by typecheck194  have member := reducedWords.of_reduced with list, reduced195  exact startsWith.membership.backward with ⟨member, u, rfl⟩196197theorem startsWith.nil_not_mem (ℓ : Set)198  shows ¬([] ∈ startsWith(ℓ))199proof200  intro member201  obtain ⟨bound, u, equal⟩ := startsWith.membership.forward with member202  have distinct := List.inductive.disjoint.nil.cons at ℓ, u203  exact distinct with equal204205theorem startsWith.head (ℓ m : Set) (u : List(4))206  requires hℓ : ℓ ∈ 4207  requires hm : m ∈ 4208  requires member : m :: u ∈ startsWith(ℓ)209  shows m = ℓ210proof211  obtain ⟨bound, v, equal⟩ := startsWith.membership.forward with member212  have both := List.inductive.injective.cons with equal213  exact both.left214215theorem startsWith.disjoint (ℓ m : Set)216  requires hℓ : ℓ ∈ 4217  requires hm : m ∈ 4218  requires different : ℓ ≠ m219  shows Disjoint(startsWith(ℓ), startsWith(m))220proof221  apply Disjoint.iff.backward222  intros w hwℓ hwm223  obtain ⟨boundℓ, u, equalℓ⟩ := startsWith.membership.forward with hwℓ224  obtain ⟨boundm, v, equalm⟩ := startsWith.membership.forward with hwm225  have same : ℓ :: u = m :: v by cc226  have both := List.inductive.injective.cons with same227  exact different with both.left228229-- Every reduced word is empty or starts with one of the four letters.230theorem reducedWords.cases (w : Set)231  requires hw : w ∈ reducedWords232  shows w = [] ∨ ∃ ℓ ∈ 4, w ∈ startsWith(ℓ)233proof234  have list := reducedWords.list with hw235  have shape := List.cases with list236  cases shape with nil | cons237  . left238    exact nil239  . right240    obtain ⟨ℓ, hℓ, u, tailList, equal⟩ := cons241    rw equal at hw242    refine ⟨ℓ, hℓ, ?_⟩243    rw equal244    exact startsWith.membership.backward with ⟨hw, u, rfl⟩245246-- The five pieces: the empty word and the words starting with each letter.247theorem reducedWords.decomposition248  shows reducedWords =249    {[]} ∪ startsWith(0) ∪ startsWith(1) ∪ startsWith(2) ∪ startsWith(3)250proof251  ext w252  constructor253  . intro hw254    have split := reducedWords.cases with hw255    cases split with nil | cons256    . rw nil257      simp [union2.membership, singleton.membership]258    . obtain ⟨ℓ, hℓ, member⟩ := cons259      have letters := letter.cases with hℓ260      rcases letters with zero | one | two | three261      . rw zero at member262        simp [union2.membership, member]263      . rw one at member264        simp [union2.membership, member]265      . rw two at member266        simp [union2.membership, member]267      . rw three at member268        simp [union2.membership, member]269  . intro hw270    have nilSubset : {[]} ⊆ reducedWords271      intros z hz272      have equal := singleton.membership.forward with hz273      rw equal274      exact reducedWords.nil_mem275    have first := union2.subset with nilSubset, (startsWith.subset at 0)276    have second := union2.subset with first, (startsWith.subset at 1)277    have third := union2.subset with second, (startsWith.subset at 2)278    have fourth := union2.subset with third, (startsWith.subset at 3)279    exact fourth with w, hw280281-- Translating the words starting with the inverse of ℓ by the letter ℓ282-- gives exactly the reduced words not starting with ℓ.283theorem leftCoset.letter (ℓ m : Set)284  requires hℓ : ℓ ∈ 4285  requires hm : m ∈ 4286  requires inverse : m = inverseLetter(ℓ)287  shows leftCoset(freeGroup, ℓ :: [], startsWith(m)) = reducedWords ∖ startsWith(ℓ)288proof289  have cancel : cancels(ℓ, m) = Bool.true290    rw inverse291    exact cancels.self_inverse with hℓ292  have cancelBack : cancels(m, ℓ) = Bool.true293    rw inverse294    exact cancels.inverse_self with hℓ295  ext w296  constructor297  . intro hw298    obtain ⟨bound, h, hh, equal⟩ := leftCoset.membership.forward with hw299    rw freeGroup.operation at equal300    have hIn := startsWith.subset at m with h, hh301    obtain ⟨boundH, u, hShape⟩ := startsWith.membership.forward with hh302    have listH := reducedWords.list with hIn303    rw hShape at listH304    have tailList := List.tail_list with listH305    have reducedH := reducedWords.reduced with hIn306    rw hShape at reducedH307    have reducedU := Reduced.tail with hm, reducedH308    have pushed := freeMul.letter with hℓ, hIn309    rw [hShape, pushLetter.cancel] at pushed310    rw [equal, hShape, pushed]311    apply difference.membership.backward312    constructor313    . exact reducedWords.of_reduced with tailList, reducedU314    . intro inLetter315      obtain ⟨boundU, v, uShape⟩ := startsWith.membership.forward with inLetter316      rw uShape at reducedH317      rw uShape at tailList318      have listV := List.tail_list with tailList319      have parts := Reduced.cons_cons.forward with hm, hℓ, reducedH320      have distinct := Bool.inductive.disjoint.false.true321      have mixed : Bool.false = Bool.true by cc322      exact distinct with mixed323  . intro hw324    obtain ⟨hwIn, notℓ⟩ := difference.membership.forward with hw325    have listW := reducedWords.list with hwIn326    have reducedW := reducedWords.reduced with hwIn327    have fits : fitsTest(m, w) = Bool.true328      have shape := List.cases with listW329      cases shape with nil | cons330      . rw nil331        exact fitsTest.nil with hm332      . obtain ⟨y, hy, ys, ysList, consShape⟩ := cons333        have headDifferent : y ≠ ℓ334          intro same335          apply notℓ336          rw [consShape, same]337          rw [consShape, same] at reducedW338          exact startsWith.of_reduced with hℓ, reducedW339        have keep : cancels(m, y) = Bool.false340          apply cancels.false_iff.backward with hm, hy341          rw inverse342          rw inverseLetter.involutive343          exact headDifferent344        have boolean := cancels.boolean at m, y345        rw [consShape, fitsTest.cons]346        exact not.true_iff.backward with boolean, keep347    have reducedH := Reduced.cons_iff.backward with hm, ⟨fits, reducedW⟩348    have hIn := startsWith.of_reduced with hm, reducedH349    have listH : List(4, m :: w) by typecheck350    have hCarrier := reducedWords.of_reduced with listH, reducedH351    have pushed := freeMul.letter with hℓ, hCarrier352    rw pushLetter.cancel at pushed353    apply leftCoset.membership.backward354    rw freeGroup.carrierOf355    refine ⟨hwIn, m :: w, hIn, ?_⟩356    rw freeGroup.operation357    symm358    exact pushed359360-- The paradoxical decomposition of the free group: the words starting361-- with a together with the translate by a of the words starting with a⁻¹362-- exhaust the group, and likewise for b.363theorem freeGroup.decomposition_a364  shows startsWith(0) ∪ leftCoset(freeGroup, freeA, startsWith(1)) = reducedWords ∧365    Disjoint(startsWith(0), leftCoset(freeGroup, freeA, startsWith(1)))366proof367  have zero := letter.zero_mem368  have one := letter.one_mem369  have inverse : 1 = inverseLetter(0)370    symm371    exact inverseLetter.zero372  have translate := leftCoset.letter with zero, one, inverse373  have value : freeA = 0 :: [] by simp [freeA]374  rw [value, translate]375  constructor376  . exact difference.union2_of_subset with (startsWith.subset at 0)377  . have disjoint := difference.disjoint at reducedWords, startsWith(0)378    exact Disjoint.symmetric with disjoint379380theorem freeGroup.decomposition_b381  shows startsWith(2) ∪ leftCoset(freeGroup, freeB, startsWith(3)) = reducedWords ∧382    Disjoint(startsWith(2), leftCoset(freeGroup, freeB, startsWith(3)))383proof384  have two := letter.two_mem385  have three := letter.three_mem386  have inverse : 3 = inverseLetter(2)387    symm388    exact inverseLetter.two389  have translate := leftCoset.letter with two, three, inverse390  have value : freeB = 2 :: [] by simp [freeB]391  rw [value, translate]392  constructor393  . exact difference.union2_of_subset with (startsWith.subset at 2)394  . have disjoint := difference.disjoint at reducedWords, startsWith(2)395    exact Disjoint.symmetric with disjoint396