braid group

Stream: new members

[Holly Liu]

i've been struggling a bit to define braid group and properties. i wanted to double check that this is the way to define a braid group using presented groups:

def braid_group (σᵢ σₖ : G) : multiplicative ℤ ≃* presented_group (braid_rels σᵢ σₖ)

is this saying that multiplicative ℤ and presented_group (braid_rels σᵢ σₖ) are both braid groups?

[Yury G. Kudryashov]

Your def says that multiplicative ℤ is isomorphic to the group presented_group (braid_rels σᵢ σₖ).

[Yury G. Kudryashov]

What is braid_rels?

[Holly Liu]

those are braid relations which i tried to write as so:

/-`σₖ⁻¹ * σᵢ⁻¹ * σₖ⁻¹ * σᵢ * σₖ * σᵢ = 1` and `σᵢ⁻¹ * σₖ⁻¹ * σᵢ * σₖ = 1`
1 ≤ i - k for the second one.  -/
def braid_rels (σᵢ σₖ : G) : set (free_group G) :=
{(free_group.of σₖ)⁻¹ * (free_group.of σᵢ)⁻¹ * (free_group.of σₖ)⁻¹ *
(free_group.of σᵢ) * (free_group.of σₖ) * (free_group.of σᵢ),
(free_group.of σᵢ)⁻¹ * (free_group.of σₖ)⁻¹ * (free_group.of σᵢ) *
(free_group.of σₖ)}

[Holly Liu]

so σᵢ * σₖ * σᵢ = σₖ * σᵢ * σₖ and σᵢ * σₖ = σₖ * σᵢ for braid crossings σᵢ , σₖ

[Kyle Miller]

These aren't the correct relations for the braid group -- you're inadvertently defining the symmetric group $S_3$, and that's definitely not isomorphic to multiplicative ℤ.

[Kyle Miller]

I'm wrong, it's not $S_3$, but I'm not sure what it is.

[Kyle Miller]

I see, the relations imply that σᵢ = σₖ, and then it's an infinite cyclic group. It's not the three-strand braid group, though, which is what you'd expect from two generators.

[Yury G. Kudryashov]

Do you want to define the 3-strand braid group or the general one?

[Holly Liu]

yes i think i don't yet have 1 < i < n-2for the first relation and i - k ≥ 2 for the second one and my indexing is incorrect. how do i say that i and i + 1 are the indices rather than i, k?

[Holly Liu]

Yury G. Kudryashov said:

Do you want to define the 3-strand braid group or the general one?

i think both

[Yury G. Kudryashov]

The main problem is that σᵢ is just a notation, it has nothing to do with i.

[Yury G. Kudryashov]

You can start with

open free_group (of)
def braids_rel3 : set (free_group (fin 2)) :=
{(of 0)⁻¹ * (of 1)⁻¹ * (of 0)⁻¹ * of 1 * of 0 * of 1}

def braids_group3 := presented_group braids_rel3

[Holly Liu]

oh ok

[Yury G. Kudryashov]

In the general case you need something like

open free_group (of)

def braids_rel (n : ℕ) : set (free_group (fin n)) :=
{x | (∃ (i k : fin n), (i : ℕ) + 2 ≤ k ∧ x = (of i)⁻¹ * (of k)⁻¹ * of i * of k) ∨ ∃ i k : fin n, (i : ℕ) + 1 = k ∧ x = (of i)⁻¹ * (of k)⁻¹ * (of i)⁻¹ * of k * of i * of k}

def brais_group (n : ℕ) : presented_group (braids_rel n)

[Kyle Miller]

I see @Yury G. Kudryashov already came up with a short definition, but this is what I came up with:

import group_theory.presented_group

/-- For the n-strand braid group, we will have 1,...,n-1 be the generators. -/
def braid_gens (n : ℕ) := {i : ℕ | 1 ≤ i ∧ i < n}

def σ {n : ℕ} (i : ℕ) (h : i ∈ braid_gens n) : free_group (braid_gens n) :=
free_group.of ⟨i, h⟩

/-- Generators commute if they have to do with strands at least two away. -/
def braid_rel_A (n : ℕ) (i j k : ℕ) (h : j = i + k + 2)
  (hi : i ∈ braid_gens n)
  (hj : j ∈ braid_gens n) : free_group (braid_gens n) :=
  (σ i hi)⁻¹ * (σ j hj)⁻¹ * (σ i hi) * (σ j hj)

/-- The braid relation for adjacent generators. -/
def braid_rel_B (n : ℕ) (i : ℕ)
  (hi : i ∈ braid_gens n)
  (hj : i + 1 ∈ braid_gens n) : free_group (braid_gens n) :=
  (σ i hi)⁻¹ * (σ (i+1) hj)⁻¹ * (σ i hi)⁻¹ * (σ (i+1) hj) * (σ i hi) * (σ (i+1) hj)

def braid_rels (n : ℕ) : set (free_group (braid_gens n)) :=
{g | ∃ i j k h hi hj, g = braid_rel_A n i j k h hi hj}
  ∪ {g | ∃ i hi hj, g = braid_rel_B n i hi hj}

def braid_group (n : ℕ) := presented_group (braid_rels n)

[Yury G. Kudryashov]

If recommend using fin n instead of braid_gens n because we have more defs and theorems about fin n.

[Kyle Miller]

It looks like you defined the (n+1)-strand braid group

[Yury G. Kudryashov]

But I like your idea to split the definition into several smaller defs.

[Yakov Pechersky]

Do we have that an iso between types induces a group iso between free groups over those types?

[Yury G. Kudryashov]

Either we do, or we should.

[Kyle Miller]

It'd be nice to define Artin-Tits groups and have the braid groups be a special case.

[Kyle Miller]

Here's Artin-Tits groups and the braid group:

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 s t) 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. -/
def artin_tits (S : Type*) (m : S → S → ℕ) :=
presented_group (artin_tits_rels S m)

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

[Kyle Miller]

Walking through this, alt n s t gives an n-term product starting with s * t * s * t * .... The artin_tits group is defined using a matrix m of natural numbers with one row and column per generator, where for s and t there is a relation s * t * s * t * ... = t * s * t * s * ... with m s t terms in the first product and m t s terms in the second. In the usual definition, the matrix has entries from $2,3,\dots,\infty$, but (1) you can use $0$ instead of $\infty$ and have the same result and (2) there's no harm in allowing $1$, since it just means you could have written the group with fewer generators. Also, in the usual definition the matrix is supposed to be symmetric, but that's not used in the definition.

Then the braid group is where for neighboring generators you use 3 terms in the relation, and for non-neighboring generators you use 2 terms.

[Holly Liu]

what does m s t and m t s mean? i'm confused on what writing the matrix m next to s t does here

[Adam Topaz]

Yakov Pechersky said:

Do we have that an iso between types induces a group iso between free groups over those types?

I'm fairly sure we have this...

[Adam Topaz]

docs#free_group.free_group_congr

[Adam Topaz]

The name should be changed to free_group.congr;)

[Kyle Miller]

@Holly Liu The type of m is m : S → S → ℕ, which is a type commonly thought of as being a matrix. The two S arguments are like the two indices for the matrix.

[Holly Liu]

oh i see. i am also confused about why we want to use a matrix m of natural numbers to contain the generators

[Kyle Miller]

Braid groups are an example of Artin-Tits groups, and this is how Artin-Tits groups are defined. (Also, the matrix does not contain the generators, the entries sort of describe "how much the generators commute" so to speak.)

[Kyle Miller]

In my earlier code, braid_rel_A corresponds to a matrix entry of 2, and braid_rel_B corresponds to a matrix entry of 3

[Adam Topaz]

I like the artin-tits presentation, it's much more symmetric!

[Holly Liu]

hmm ok, i still don't know what commuting generators mean in the context of the matrix. i'll have to read up a bit on artin-tits groups

[Holly Liu]

thank you all for the input. it was incredibly helpful :big_smile:

[Kyle Miller]

@Holly Liu Here's half the proof that the 2-strand braid group is infinite cyclic.

def braid_group_2_to_mul_ℤ' : fin 1 → multiplicative ℤ := λ _, multiplicative.of_add 1

def braid_group_2_to_mul_ℤ : braid_group 2 →* multiplicative ℤ :=
@presented_group.to_group _ _ _ braid_group_2_to_mul_ℤ' _ begin
  intros r hr,
  dsimp [artin_tits_rels] at hr,
  rcases hr with ⟨s, t, rfl⟩,
  fin_cases s,
  fin_cases t,
  refl,
end

def braid_group_2_is_cyclic : braid_group 2 ≃* multiplicative ℤ :=
{ to_fun := braid_group_2_to_mul_ℤ,
  inv_fun := λ x, presented_group.of (0 : fin 1) ^ x.to_add,
  map_mul' := braid_group_2_to_mul_ℤ.map_mul,
  left_inv := begin
    sorry
  end,
  right_inv := begin
    sorry
  end }

[Kyle Miller]

(By the way, I had to make the definitions of braid_group and artin_tits reducible (I used abbreviation) to make Lean see that they're groups. I edited that message.)

[Holly Liu]

oh wow ok thanks

[Eric Wieser]

I'd recommend using docs#monoid_hom.to_mul_equiv if possible there, because usually the two proofs fall out with ext, simp

[Eric Wieser]

And if they don't, then you should add the lemmas needed so that they do!

[Kyle Miller]

Only partially following @Eric Wieser's advice (and it'd be better to follow all of it), here's an unrefined proof:

-- import algebra.group_power

def braid_group_2_to_mul_ℤ' : fin 1 → multiplicative ℤ := λ _, multiplicative.of_add 1

def braid_group_2_to_mul_ℤ : braid_group 2 →* multiplicative ℤ :=
@presented_group.to_group _ _ _ braid_group_2_to_mul_ℤ' _ begin
  intros r hr,
  dsimp [artin_tits_rels] at hr,
  rcases hr with ⟨s, t, rfl⟩,
  fin_cases s,
  fin_cases t,
  refl,
end

def mul_ℤ_to_braid_group_2 : multiplicative ℤ →* braid_group 2 :=
gpowers_hom (braid_group 2) (presented_group.of 0)

def braid_group_2_is_cyclic : braid_group 2 ≃* multiplicative ℤ :=
monoid_hom.to_mul_equiv braid_group_2_to_mul_ℤ mul_ℤ_to_braid_group_2
begin
  ext,
  simp only [braid_group_2_to_mul_ℤ, mul_ℤ_to_braid_group_2, monoid_hom.id_apply, function.comp_app, monoid_hom.coe_comp,
    gpowers_hom_apply],
  refine quotient_group.induction_on x (λ x, _),
  refine free_group.induction_on x _ (λ x, _) (λ x, _) (λ a b, _),
  { refl, },
  { fin_cases x,
    refl, },
  { fin_cases x,
    intro h,
    change _ = (quotient_group.mk (pure 0) : braid_group 2)⁻¹,
    rw ←h,
    refl, },
  { intros h1 h2,
    change _ = quotient_group.mk a * quotient_group.mk b,
    rw [←h1, ←h2],
    rw ←gpow_add,
    rw ←to_add_mul,
    congr' 2,
    simp only [presented_group.to_group, monoid_hom.map_mul, quotient_group.lift_mk'], },
end
begin
  ext, refl,
end

[Kyle Miller]

This really shouldn't be the proof -- instead it should be that it's a group presentation with to relations, so it's a free group, and it's a free group with one generator, so it's isomorphic to multiplicative ℤ.

(It doesn't apply here, but it would be nice if there were things like Tietze transformations for group presentations.)

[Kyle Miller]

A good relevant test of such transformations would be to show that braid_group 3 is isomorphic to $\langle x,y \mid x^2 = y^3\rangle$.

[Eric Wieser]

There's definitely an ext lemma missing on quotient_group that that proof would benefit from

[Eric Wieser]

Added those lemmas in #8641

[Holly Liu]

why does this result in free_group S:

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

[Eric Rodriguez]

why wouldn't it?

[Kyle Miller]

@Holly Liu Are you familiar with how to write recursive definitions in Lean? This is recursing on the natural number argument to create a product of the form free_group.of s * free_group.of t * free_group.of s * ... with n terms.

[Kyle Miller]

Well, technically it has n+1 terms with the last term being 1. For example, alt 2 s t is free_group.of s * free_group.of t * 1.

[Holly Liu]

oh ok, i think i understand the recursive part. i've been using free_group.of to define the generators but i don't actually know why we do this. this seems to be saying a generator is a free group and the product free_group.of s * free_group.of t * ... is also a free group, but this looks like a word to me.

[Kyle Miller]

Have you studied free groups and their universal property? free_group.of is the function S → free_group S that is part of the universal property.

[Kyle Miller]

The result of free_group.of s is not a free group, it's an element of the free group. A word of length 1 in particular.

[Kyle Miller]

alt n s t is creating a word of length n that looks like $ststst\dots$ in math.

[Holly Liu]

ah so if it's of type free_group S then it is an element? that makes more sense and probably something fundamental i should know...
i know a bit about free groups and haven't yet studied them rigorously. i've also just been reading the manuals on lean and lack a lot of practice coding with it, though the proofs you gave me are helpful

[Kyle Miller]

Yeah, free_group S is the free group generated by S. There's only one group (up to isomorphism) freely generated by S, so it wouldn't be very useful having a whole type of free groups. Mathlib chooses just one of them (representing elements by words) and calls it free_group S.

[Holly Liu]

so then this isn't true for sets right? if something is of type set (free_group S) then it's an element of this set of sets? i vaguely remember reading something about for U : Type, A : set U is a set.

[Kyle Miller]

an element of set (free_group S) is a subset of the free group

[Kyle Miller]

in your example, A is a subset of U. (I'm using "subset" like how we mean it in math. A type U is basically a set, and things with type set U are sets whose elements have type U, or in other words things with type set U are subsets of U. Don't take this too literally, since example (U : Type) (A : set U) : A ⊆ U := sorry gives a type error -- the subset-of relation is only for subsets of the same type. set.univ is the name for the subset of U that represents U being a subset of itself, so example (U : Type) (A : set U) : A ⊆ set.univ := sorry resolves that type error.)

[Holly Liu]

that makes sense. thanks.

[Eric Wieser]

@Kyle Miller, would you mind trying out your proof above with the now-merged ext lemmas? I don't have a mwe to hand.

[Kyle Miller]

@Eric Wieser Nice, those worked great (with a bit of heavy refling):

def braid_group_2_is_cyclic : braid_group 2 ≃* multiplicative ℤ :=
monoid_hom.to_mul_equiv braid_group_2_to_mul_ℤ mul_ℤ_to_braid_group_2
begin
  ext x,
  fin_cases x,
  refl,
end
begin
  ext, refl,
end

MWE:

import tactic
import group_theory.presented_group
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)

def braid_group_2_to_mul_ℤ' : fin 1 → multiplicative ℤ := λ _, multiplicative.of_add 1

def braid_group_2_to_mul_ℤ : braid_group 2 →* multiplicative ℤ :=
@presented_group.to_group _ _ _ braid_group_2_to_mul_ℤ' _ begin
  intros r hr,
  dsimp [artin_tits_rels] at hr,
  rcases hr with ⟨s, t, rfl⟩,
  fin_cases s,
  fin_cases t,
  refl,
end

def mul_ℤ_to_braid_group_2 : multiplicative ℤ →* braid_group 2 :=
gpowers_hom (braid_group 2) (presented_group.of 0)

def braid_group_2_is_cyclic : braid_group 2 ≃* multiplicative ℤ :=
monoid_hom.to_mul_equiv braid_group_2_to_mul_ℤ mul_ℤ_to_braid_group_2
begin
  ext x,
  fin_cases x,
  refl,
end
begin
  ext, refl,
end

[Holly Liu]

how do i resolve red underlines for fin_cases?

[Kevin Buzzard]

import tactic?

[Holly Liu]

thanks

[Eric Wieser]

I wonder if ext should know about fin 1 too...

[Holly Liu]

for the line (λ i j, if abs ((i : ℤ) - j) = 1 then 3 else 2) in this

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)

why do we have i : ℤ if i is also of type fin (n-1)?

[Scott Morrison]

The (i : ℤ) is casting from fin (n-1) to ℤ, so that the subtraction happens in ℤ, rather than in fin (n-1) (where subtraction means truncated subtraction).

[Scott Morrison]

This is not obviously the ideal way to do this!

[Scott Morrison]

I wonder if fin n has a dist function (or should have)?

[Holly Liu]

what is truncated subtraction?

[Kyle Miller]

Scott Morrison said:

in fin (n-1) (where subtraction means truncated subtraction).

(I'd thought so too, but it seems to be subtraction mod n - 1! docs#fin.sub)

[Kyle Miller]

A subtlety, by the way, with (i : ℤ) - j is that it's actually casting both i and j, so it could also have been written more clearly as (i : ℤ) - (j : ℤ). I shouldn't have saved those handful of characters since it makes it less clear.

[Holly Liu]

why would we need to cast it here? wouldn't any number in fin (n-1) subtracted by another number from fin (n-1) always be less than fin (n-1)?

[Kyle Miller]

def test (n : fin 5) := n - (2 : fin 5)

#eval test 0
-- shows 3

[Holly Liu]

oh got it, thanks

[Eric Wieser]

I'd argue (i - j : ℤ) would be the clearest way to spell the cast

[Patrick Massot]

No, that version is very confusing for beginners.

[Scott Morrison]

It is very unintuitive for most people that the casts happen as early as possible, rather than "at the moment indicated by the typography".

[Kyle Miller]

The Perl part of Lean. (It's very reminiscent of scalar/list contexts.)

[Eric Wieser]

Patrick Massot said:

No, that version is very confusing for beginners.

Yes, but if you start preferring the spelling (i : ℤ)- j instead of (i - j : ℤ) to make things "easier" for beginners, you've given those beginners exactly the wrong intuition as to how to read casts, and the non-intuitiveness is self-fulfilling. I guess the way to avoid that while also not confusing beginners is (↑i - ↑j : ℤ), which reads as (_ : ℤ) ("lean I am telling you an integer") and ↑i ("do a cast for me").

[Holly Liu]

i am getting an error here:
image.png
this is the message:
image.png

[Holly Liu]

these are my imports:

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

[Mario Carneiro]

It says it can't prove that braid_group 2 is finite. I don't know much about braid groups but considering that you are trying to prove it's isomorphic to multiplicative int I would guess this is false

[Mario Carneiro]

I see you picked this theorem from up-thread. I guess ext is finding the wrong extensionality lemma - there is probably an extensionality lemma saying that functions out of braid_group 2 are determined by their values on x : fin 2 but you are getting a more generic ext lemma

[Eric Wieser]

Perhaps the ext lemma isn't matching because Holly's braid_group isn't an abbreviation like the one upthread

[Eric Wieser]

(who can say without a #mwe)

[Adam Topaz]

The braid group is not finite.

[Holly Liu]

ah ok. how do i add the updated ext to the mathlib version on my desktop?

[Kyle Miller]

(For those who missed it, the #mwe is in the spoiler tag upthread at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/braid.20group/near/249405713 and the reason fin_cases isn't working is because @Eric Wieser added some new ext lemmas.)

[Kyle Miller]

@Holly Liu How is your project set up? Are you editing inside mathlib itself (that's what I normally do) or do you have a separate project that just uses mathlib?

[Kyle Miller]

If it's the second, I think leanproject up (short for leanproject upgrade-mathlib) will update mathlib.

[Eric Wieser]

Wait, did I break it?

[Kyle Miller]

No, the fin_cases that doesn't work is because it relies on your ext lemmas, and @Holly Liu hasn't updated mathlib. (You only broke it if somehow you're Merlin-like, living backwards in time.)

[Holly Liu]

i am still getting the error after doing leanproject up. maybe i should just copy paste the lemma into the file, or try editing inside mathlib itself?

[Holly Liu]

hello again. i am trying to prove the following

/- Every 2-braid can be written in the form `σ₁^n` for some integer `n`. -/
lemma n_form (0 : braid_group 2) (n : ℤ) (h : 0^n) : braid_group 2 :=
begin

end

i'm trying to say 0^n is a type of braid_group 2, however i'm not able to declare the generator 0. i get the error invalid binder, identifier expected. how do i go about this?

[Holly Liu]

i think the #mwe is upthread in the spoiler tag, as mentioned before

[Eric Wieser]

Your statement is nonsensical to me; do you understand how : works in a lemma statement? In particular, everything before the colon should be of the form (name : type) or similar. Lean is complaining that 0 is not a name.

[Holly Liu]

oh ok i see. is there a way to declare just the element 0 of braid_group 2?

[Eric Wieser]

It depends what you mean by declare. You can maybe write

def another_spelling_of_zero : braid_group 2 := 0

[Kyle Miller]

(0 : braid_group 2)^n would be a way to use 0 in braid_group 2 (though it doesn't have 0)

[Kyle Miller]

Maybe you mean this 0?

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

[Holly Liu]

oh yes i think that's the one i meant.

[Kyle Miller]

And maybe you mean this lemma?

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

/- Every 2-braid can be written in the form `σ₁^n` for some integer `n`. -/
lemma n_form (x : braid_group 2) : x = σ₁ ^ (braid_group_2_is_cyclic x).to_add :=
begin
end

[Holly Liu]

what is the (braid_group_2_is_cyclic x).to_add doing?

[Kyle Miller]

This proof that the braid group was equivalent to the infinite cyclic group was much stronger than just saying they're equivalent -- it is an explicit isomorphism between them.

def braid_group_2_is_cyclic : braid_group 2 ≃* multiplicative ℤ

So braid_group_2_is_cyclic x gives the image of x in the cyclic group. If you convert that element to ℤ (using to_add) you get the power you need to construct x from the generator.

The proof of n_form should probably be one line, but I'm not sure what that one line is.

[Holly Liu]

ok i think i understand. thanks!

[Eric Wieser]

Probably you want to use docs#gpowers_hom to make it an equality of monoid_homs, then use ext

[Eric Wieser]

(deleted)

[Eric Wieser]

Oh, the proof will just be braid_group_2_is_cyclic.apply_symm_apply x or braid_group_2_is_cyclic.symm_apply_apply x

[Kyle Miller]

tada:

lemma n_form (x : braid_group 2) : x = σ₁ ^ (braid_group_2_is_cyclic x).to_add :=
(braid_group_2_is_cyclic.symm_apply_apply x).symm

[Holly Liu]

is it using the mul_equiv.symm_apply_apply or the equiv.symm_apply_apply? or does it matter nvm

[Holly Liu]

i seem to be getting errors with the above code:
image.png
these are the messages:
image.png
i wonder if this is because a part of the proof in braid_group_2_is_cyclic is not working in my project?

[Kyle Miller]

Either remove the begin/end or put exact at the beginning of that line.

[Kyle Miller]

The one-line proof is a "term-mode" proof

[Holly Liu]

Kyle Miller said:

tada:

lemma n_form (x : braid_group 2) : x = σ₁ ^ (braid_group_2_is_cyclic x).to_add :=
(braid_group_2_is_cyclic.symm_apply_apply x).symm

what is braid_group_2_is_cyclic.symm_apply_apply x doing?

[Kyle Miller]

Have you followed the definition for symm_apply_apply yet?

[Holly Liu]

i think it is saying perform braid_group_2_is_cyclic.symm : multiplicative ℤ ≃* braid_group 2 then map x : braid_group 2 to it's corresponding element in multiplicative ℤ then map that back to braid_group_2_is_cyclic.symm to get x again?

[Holly Liu]

essentially i think it's saying for sets M,N, M ≃* N → N ≃* M, N(M(x)) = x and then you flip it to get x = N(M(x)) . if this is correct, i'm a bit confused about how this is of type x = 0 * 0 * ... * 0.