sequence w/ many variables

Stream: new members

[Holly Liu]

i'm wondering how one could create a sequence like so: σ₁^{a₁} * σ₂^{b₁} * σ₁^{a₂} * σ₂^{b₂} ... σ₁^{aₙ} * σ₂^{bₙ} where all a₁, b₁, ..., aₙ, bₙ are nonzero integers and only a₁, bₙ may be zero and σ₁, σ₂ : braid_group 2.
i was thinking of inductively doing it but run into the problem of using a separate variable for each a₁, b₁, ..., aₙ, bₙ.
specifically i'm trying to prove that every 3-braid, for some integer n ≥ 0, can be written in this form, though i'm not sure if braid groups affect this problem with variables specifically.

[Scott Morrison]

It sounds like you want to create a function from lists of pairs of integers to the 3-strand braid group

[Scott Morrison]

(which can just be defined by induction on the list)

[Scott Morrison]

and then proving that this function is surjective

[Scott Morrison]

(and even surjective when restricted to the subtype with the zero-ness conditions you specified)

[Scott Morrison]

(also --- yay braid groups :-)

[Yakov Pechersky]

import data.zmod.basic
import group_theory.presented_group
import group_theory.free_group
import data.equiv.mul_add
import algebra.group_power


def alt {S : Type*} : ℕ → S → S → free_group S
| 0 _ _ := 1
| (n+1) s t := free_group.of s * alt n t s

def artin_tits_rels (S : Type*) (m : S → S → ℕ) :
  set (free_group S) :=
{g | ∃ s t, g = (alt (m s t) s t)⁻¹ * (alt (m t s) t s)}

/-- Artin-Tits groups.  Traditionally we require that
`∀ s t, m s t = m t s` but the hypothesis isn't used in the definition. -/
abbreviation artin_tits (S : Type*) (m : S → S → ℕ) :=
presented_group (artin_tits_rels S m)

abbreviation braid_group (n : ℕ) :=
artin_tits (fin (n - 1))
  (λ i j, if abs ((i : ℤ) - j) = 1 then 3 else 2)

example (σ₁ σ₂ x : braid_group 2) :
  ∃ (la lb : list ℕ) (a0 b0 : ℕ), (list.zip_with (*)
    ((a0 :: (la.map nat.succ)).map (λ k, σ₁ ^ k))
    ((b0 :: (lb.map nat.succ)).map (λ k, σ₂ ^ k)).reverse).prod = x :=
sorry

[Yakov Pechersky]

Is that the statement you're trying to prove?

[Yakov Pechersky]

Whoops, sorry, this is missing an quantifier. Fixed

[Scott Morrison]

You presumably don't want σ₁ σ₂ as variables here, but rather the fixed generators.

[Yakov Pechersky]

of 0 and of 1, I take it?

[Holly Liu]

thanks for the help!

Yakov Pechersky said:

example (σ₁ σ₂ x : braid_group 2) :
  ∃ (la lb : list ℕ) (a0 b0 : ℕ), (list.zip_with (*)
    ((a0 :: (la.map nat.succ)).map (λ k, σ₁ ^ k))
    ((b0 :: (lb.map nat.succ)).map (λ k, σ₂ ^ k)).reverse).prod = x :=
sorry

sorry for the late reply. i was wondering if list.zip_with (*) is just saying a list multiplied by a list is also a list?

[Eric Wieser]

docs#list.zip_with

[Holly Liu]

yes but what does putting the (*) next to it mean?

[Kyle Miller]

hint:

#check (*)

(though this shows some metavariables, but it gives a hint of what it is)

[Kyle Miller]

I can't find where it's described in the Lean documentation, but putting an operator in parentheses gives you the operator as a function. You can also do some limited partial application of operators (called sections in Haskell), like (*2) for the multiplication-by-two function. Lean only has "right sections," no "left sections."

[Yakov Pechersky]

((*) 2) is the left section

[Kyle Miller]

"left section" is a name for the notation itself, so I'm not sure I'd call it a left section, but it's definitely semantically equivalent (and why it's OK that lean doesn't have left sections).

[Yakov Pechersky]

Fair point

[Yakov Pechersky]

list.zip_with (*) is basically the element-wide product of the elements of two lists.

[Yakov Pechersky]

Up to the length of the shortest of the two

[Yakov Pechersky]

list.zip_with f xs ys is provably equal to (list.zip xs ys).map (uncurry f)

[Yakov Pechersky]

docs#function.uncurry, docs#list.map_uncurry_zip_eq_zip_with

[Kyle Miller]

You can tell someone is a Haskeller (or functional programmer) if they reach for zips and maps and such so readily :smile:

[Eric Wieser]

(*) is notation for has_mul.mul and is defeq to (λ x y, x * y)

[Holly Liu]

Yakov Pechersky said:

Up to the length of the shortest of the two

so you just truncate the rest of it?

[Kyle Miller]

I just want to throw out another way of stating what you're wanting to prove.

import data.zmod.basic
import group_theory.presented_group
import group_theory.free_group
import data.equiv.mul_add
import algebra.group_power

def alt {S : Type*} : ℕ → S → S → free_group S
| 0 _ _ := 1
| (n+1) s t := free_group.of s * alt n t s

def artin_tits_rels (S : Type*) (m : S → S → ℕ) :
  set (free_group S) :=
{g | ∃ s t, g = (alt (m s t) s t)⁻¹ * (alt (m t s) t s)}

/-- Artin-Tits groups.  Traditionally we require that
`∀ s t, m s t = m t s` but the hypothesis isn't used in the definition. -/
abbreviation artin_tits (S : Type*) (m : S → S → ℕ) :=
presented_group (artin_tits_rels S m)

abbreviation braid_group (n : ℕ) :=
artin_tits (fin (n - 1))
  (λ i j, if abs ((i : ℤ) - j) = 1 then 3 else 2)

section three_braids

def σ₁ : braid_group 3 := presented_group.of 0

def σ₂ : braid_group 3 := presented_group.of 1

def three_braid_of : list ℤ → braid_group 3
| [] := 1
| [m] := σ₁ ^ m
| (m :: n :: rest) := σ₁ ^ m * σ₂ ^ n * three_braid_of rest

example : three_braid_of [1,2,-1] = σ₁ * σ₂^2 * σ₁^-1 := rfl

example (x : braid_group 3) : ∃ (l : list ℤ), three_braid_of l = x :=
sorry

-- Or:
example : function.surjective three_braid_of :=
sorry

end three_braids

[Kyle Miller]

Holly Liu said:

Yakov Pechersky said:

Up to the length of the shortest of the two

so you just truncate the rest of it?

He's telling you a technical detail about how zip_with works. You may as well assume la and lb in the example have the same length because of this.

[Kyle Miller]

(I updated the code I just posted to use the integers instead of natural numbers, and to include an example of three_braid_of.)

Note that it does not include conditions on the list of integers. I'm not sure why you want this theorem exactly -- what's your larger goal?

[Eric Rodriguez]

Kyle Miller said:

You can tell someone is a Haskeller (or functional programmer) if they reach for zips and maps and such so readily :smile:

(There was one time I was tempted to write flip ($) in Lean.)

what would flip ($) do? :shock:

[Holly Liu]

oh so the code with la,lb is multiplying $\sigma_1^{a_1}, ... \sigma_1^{a_n}$ to $\sigma_2^{b_1}, ..., \sigma_2^{b_n}$. that makes more sense. i was just curious if lean implements list.prod to lose elements when multiplying two differently lengthed lists together.
right now i'm just trying to code some exercises in a braid textbook. ultimately the original goal was to code enough of braid groups to PR it although that seems unlikely for now.

[Eric Wieser]

docs#list.prod only acts on a single list not on two lists

[Eric Wieser]

@Eric Rodriguez: I would imagine flip ($) = function.eval, docs#function.eval

[Holly Liu]

oh oops, i think i meant list.zip_with (*)

[Eric Wieser]

Lean is quite unforgiving if you type something different to what you mean ;).