## 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-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 (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):

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


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 defs 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.)

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],
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

#### 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


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?

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

(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):

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 mul_equiv.symm_apply_apply or the equiv.symm_apply_apply? or does it matter nvm

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

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