# Zulip Chat Archive

## Stream: new members

### Topic: braid group

#### Holly Liu (Aug 11 2021 at 17:45):

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 (Aug 11 2021 at 17:49):

Your `def`

says that `multiplicative ℤ`

is isomorphic to the group `presented_group (braid_rels σᵢ σₖ)`

.

#### Yury G. Kudryashov (Aug 11 2021 at 17:50):

What is `braid_rels`

?

#### Holly Liu (Aug 11 2021 at 17:52):

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 (Aug 11 2021 at 17:54):

so `σᵢ * σₖ * σᵢ = σₖ * σᵢ * σₖ `

and `σᵢ * σₖ = σₖ * σᵢ`

for braid crossings `σᵢ `

,` σₖ`

#### Kyle Miller (Aug 11 2021 at 17:55):

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 (Aug 11 2021 at 17:55):

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

#### Kyle Miller (Aug 11 2021 at 17:59):

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 (Aug 11 2021 at 18:00):

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

#### Holly Liu (Aug 11 2021 at 18:00):

yes i think i don't yet have `1 < i < n-2`

for 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 (Aug 11 2021 at 18:01):

Yury G. Kudryashov said:

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

i think both

#### Yury G. Kudryashov (Aug 11 2021 at 18:01):

The main problem is that `σᵢ`

is just a notation, it has nothing to do with `i`

.

#### Yury G. Kudryashov (Aug 11 2021 at 18:04):

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 (Aug 11 2021 at 18:08):

oh ok

#### Yury G. Kudryashov (Aug 11 2021 at 18:08):

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 (Aug 11 2021 at 18:11):

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 (Aug 11 2021 at 18:12):

If recommend using `fin n`

instead of `braid_gens n`

because we have more `def`

s and theorems about `fin n`

.

#### Kyle Miller (Aug 11 2021 at 18:13):

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

#### Yury G. Kudryashov (Aug 11 2021 at 18:14):

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

#### Yakov Pechersky (Aug 11 2021 at 18:16):

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

#### Yury G. Kudryashov (Aug 11 2021 at 18:16):

Either we do, or we should.

#### Kyle Miller (Aug 11 2021 at 18:17):

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

#### Kyle Miller (Aug 11 2021 at 18:30):

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 (Aug 11 2021 at 18:40):

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 (Aug 11 2021 at 18:48):

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 (Aug 11 2021 at 18:49):

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 (Aug 11 2021 at 18:50):

docs#free_group.free_group_congr

#### Adam Topaz (Aug 11 2021 at 18:50):

The name should be changed to `free_group.congr`

;)

#### Kyle Miller (Aug 11 2021 at 18:51):

@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 (Aug 11 2021 at 18:53):

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 (Aug 11 2021 at 18:57):

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 (Aug 11 2021 at 18:58):

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 (Aug 11 2021 at 19:00):

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

#### Holly Liu (Aug 11 2021 at 19:01):

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 (Aug 11 2021 at 19:11):

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

#### Kyle Miller (Aug 11 2021 at 19:14):

@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 (Aug 11 2021 at 19:25):

(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 (Aug 11 2021 at 22:19):

oh wow ok thanks

#### Eric Wieser (Aug 11 2021 at 22:59):

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 (Aug 11 2021 at 23:01):

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

#### Kyle Miller (Aug 12 2021 at 01:04):

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 (Aug 12 2021 at 01:10):

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 (Aug 12 2021 at 01:35):

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 (Aug 12 2021 at 06:53):

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

#### Eric Wieser (Aug 12 2021 at 08:40):

Added those lemmas in #8641

#### Holly Liu (Aug 12 2021 at 22:38):

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 (Aug 12 2021 at 22:57):

why wouldn't it?

#### Kyle Miller (Aug 12 2021 at 23:06):

@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 (Aug 12 2021 at 23:07):

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 (Aug 13 2021 at 00:14):

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 (Aug 13 2021 at 00:18):

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 (Aug 13 2021 at 00:19):

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 (Aug 13 2021 at 00:21):

`alt n s t`

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

#### Holly Liu (Aug 13 2021 at 00:29):

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 (Aug 13 2021 at 00:33):

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 (Aug 13 2021 at 00:51):

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 (Aug 13 2021 at 01:04):

an element of `set (free_group S)`

is a subset of the free group

#### Kyle Miller (Aug 13 2021 at 01:09):

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 (Aug 13 2021 at 01:16):

that makes sense. thanks.

#### Eric Wieser (Aug 13 2021 at 19:11):

@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 (Aug 13 2021 at 19:53):

@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:

#### Holly Liu (Aug 13 2021 at 20:08):

how do i resolve red underlines for `fin_cases`

?

#### Kevin Buzzard (Aug 13 2021 at 20:14):

`import tactic`

?

#### Holly Liu (Aug 13 2021 at 20:19):

thanks

#### Eric Wieser (Aug 13 2021 at 20:32):

I wonder if `ext`

should know about `fin 1`

too...

#### Holly Liu (Aug 17 2021 at 01:00):

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 (Aug 17 2021 at 01:07):

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 (Aug 17 2021 at 01:07):

This is not obviously the ideal way to do this!

#### Scott Morrison (Aug 17 2021 at 01:08):

I wonder if `fin n`

has a `dist`

function (or should have)?

#### Holly Liu (Aug 17 2021 at 01:25):

what is truncated subtraction?

#### Kyle Miller (Aug 17 2021 at 01:25):

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 (Aug 17 2021 at 01:28):

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 (Aug 17 2021 at 01:35):

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 (Aug 17 2021 at 01:37):

```
def test (n : fin 5) := n - (2 : fin 5)
#eval test 0
-- shows 3
```

#### Holly Liu (Aug 17 2021 at 01:40):

oh got it, thanks

#### Eric Wieser (Aug 17 2021 at 07:39):

I'd argue `(i - j : ℤ)`

would be the clearest way to spell the cast

#### Patrick Massot (Aug 17 2021 at 08:35):

No, that version is very confusing for beginners.

#### Scott Morrison (Aug 17 2021 at 08:37):

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 (Aug 17 2021 at 08:50):

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

#### Eric Wieser (Aug 17 2021 at 09:10):

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 (Aug 19 2021 at 00:19):

i am getting an error here:

image.png

this is the message:

image.png

#### Holly Liu (Aug 19 2021 at 00:20):

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 (Aug 19 2021 at 00:22):

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 (Aug 19 2021 at 00:25):

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 (Aug 19 2021 at 00:42):

Perhaps the ext lemma isn't matching because Holly's `braid_group`

isn't an abbreviation like the one upthread

#### Eric Wieser (Aug 19 2021 at 00:43):

(who can say without a #mwe)

#### Adam Topaz (Aug 19 2021 at 01:20):

The braid group is not finite.

#### Holly Liu (Aug 19 2021 at 20:49):

ah ok. how do i add the updated `ext`

to the mathlib version on my desktop?

#### Kyle Miller (Aug 19 2021 at 21:09):

(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 (Aug 19 2021 at 21:10):

@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 (Aug 19 2021 at 21:16):

If it's the second, I think `leanproject up`

(short for `leanproject upgrade-mathlib`

) will update mathlib.

#### Eric Wieser (Aug 19 2021 at 21:29):

Wait, did I break it?

#### Kyle Miller (Aug 19 2021 at 21:32):

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 (Aug 19 2021 at 22:41):

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 (Aug 20 2021 at 16:31):

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 (Aug 20 2021 at 16:32):

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

#### Eric Wieser (Aug 20 2021 at 16:46):

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 (Aug 20 2021 at 16:53):

oh ok i see. is there a way to declare just the element `0`

of `braid_group 2`

?

#### Eric Wieser (Aug 20 2021 at 16:54):

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

```
def another_spelling_of_zero : braid_group 2 := 0
```

#### Kyle Miller (Aug 20 2021 at 16:54):

`(0 : braid_group 2)^n`

would be a way to use `0`

in `braid_group 2`

(though it doesn't have `0`

)

#### Kyle Miller (Aug 20 2021 at 16:55):

Maybe you mean this `0`

?

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

#### Holly Liu (Aug 20 2021 at 16:56):

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

#### Kyle Miller (Aug 20 2021 at 16:56):

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 (Aug 20 2021 at 17:00):

what is the `(braid_group_2_is_cyclic x).to_add`

doing?

#### Kyle Miller (Aug 20 2021 at 17:03):

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 (Aug 20 2021 at 17:09):

ok i think i understand. thanks!

#### Eric Wieser (Aug 20 2021 at 17:33):

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

#### Eric Wieser (Aug 20 2021 at 17:34):

(deleted)

#### Eric Wieser (Aug 20 2021 at 17:36):

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 (Aug 20 2021 at 17:38):

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 (Aug 20 2021 at 17:53):

~~is it using the ~~ nvm`mul_equiv.symm_apply_apply`

or the `equiv.symm_apply_apply`

? or does it matter

#### Holly Liu (Aug 20 2021 at 19:40):

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 (Aug 20 2021 at 19:52):

Either remove the begin/end or put `exact`

at the beginning of that line.

#### Kyle Miller (Aug 20 2021 at 19:52):

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

#### Holly Liu (Aug 21 2021 at 19:54):

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 (Aug 21 2021 at 20:17):

Have you followed the definition for `symm_apply_apply`

yet?

#### Holly Liu (Aug 21 2021 at 20:38):

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 (Aug 21 2021 at 21:23):

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`

.

Last updated: Dec 20 2023 at 11:08 UTC