proving a mul_equiv

Stream: new members

[Holly Liu]

i'm trying to prove something like def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) := sorry and am trying to use

@[to_additive "Extract the forward direction of an additive equivalence
as an addition-preserving function."]
def to_monoid_hom {M N} [mul_one_class M] [mul_one_class N] (h : M ≃* N) : (M →* N) :=
{ map_one' := h.map_one, .. h }

to somehow get a f : multiplicative ℕ →* presented_group (braid_rels σᵢ σₖ) and maybe some proof step saying these are both monoids, then using

/-- A bijective `monoid` homomorphism is an isomorphism -/
@[to_additive "A bijective `add_monoid` homomorphism is an isomorphism"]
noncomputable def of_bijective {M N} [mul_one_class M] [mul_one_class N] (f : M →* N)
  (hf : function.bijective f) : M ≃* N :=
{ map_mul' := f.map_mul',
  ..equiv.of_bijective f hf }

to finally get the multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ). however i'm not sure if i can introduce this as a function in the first place, since intro doesn't work. the error i get is Pi/let expression expected. i also think there might be some flaw to my approach, but i'm unsure.

[Yakov Pechersky]

Can you share a #mwe?

[Yakov Pechersky]

So are you constructing a (M →* N) and then proving it is bijective, to construct your mul_equiv?

[Holly Liu]

sure:

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

variables {G : Type} {σᵢ σₖ : G}

/-`σₖ⁻¹ * σᵢ⁻¹ * σₖ⁻¹ * σᵢ * σₖ * σᵢ = 1`, `σᵢ⁻¹ * σₖ⁻¹ * σᵢ * σₖ = 1`-/
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 σₖ)}

def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) :=
begin
  intro
end

[Holly Liu]

Yakov Pechersky said:

So are you constructing a (M →* N) and then proving it is bijective, to construct your mul_equiv?

yes i think that is what i'm trying to do

[Yakov Pechersky]

When you construct data, you should try to avoid doing it via tactics. So in this case, you need to provide something to fill in:

def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) :=
{ to_fun := _,
  inv_fun := _,
  left_inv := _,
  right_inv := _,
  map_mul' := _ }

[Yakov Pechersky]

I generated that skeleton by writing

def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) :=
_

Then pressing Ctrl+. or the lightbulb, and selecting Generate a skeleton for the structure under construction

[Yakov Pechersky]

If you want to do your proof via a monoid_hom and a bijectivity proof, you can do:

def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) :=
mul_equiv.of_bijective
  { to_fun := _,
    map_one' := _,
    map_mul' := _ }
  _

[Holly Liu]

oh wow ok thank you!

[Holly Liu]

Yakov Pechersky said:

If you want to do your proof via a monoid_hom and a bijectivity proof, you can do:

def braid_group (σᵢ σₖ : G) : multiplicative ℕ ≃* presented_group (braid_rels σᵢ σₖ) :=
mul_equiv.of_bijective
  { to_fun := _,
    map_one' := _,
    map_mul' := _ }
  _

how did you know we needed to generate a skeleton for the mul_equiv.of_bijective? it seems like a regular definition.

[Eric Wieser]

You start by writing mul_equiv.of_bijective _ _, and seeing what lean wants you to fill in the _s with. Lean says "I can't find the monoid_hom", and you presumably want to build it from first principles, so you tell lean to "generate a skeleton for the structure". If you try that where the type isn't a structure, lean won't generate the {} for you.

[Holly Liu]

but how do we know that we can use _ after mul_equiv.of_bijective, like what about this definition says that we can use _? i tried doing something like mul_equiv.to_monoid_hom _ just to check if the lightbulb shows up, but it doesn't.

[Ruben Van de Velde]

The _ isn't really special - it just says "I'll fill this in later", while allowing lean to figure out the structure of the term that contains the placeholder. This works here as well:

import data.real.basic
import data.equiv.mul_add

def x : ℝ →* ℝ := mul_equiv.to_monoid_hom _

[Yakov Pechersky]

Important to note that mul_equiv.to_monoid_hom isn't about constructing a mul_equiv (≃*). It is about constructing a monoid_hom (also written as ->*) from a mul_equiv. A mul_equiv is a strictly stronger definition.

[Yakov Pechersky]

how did you know we needed to generate a skeleton for the mul_equiv.of_bijective? it seems like a regular definition.

Because I knew that a ->* is a structure too. Could you clarify what you mean by "regular definition"? I think clearing up what distinction you're making will help me explain better the pieces involved.

[Holly Liu]

well, i don't actually know the difference between different definitions. they are all just a "definition" in my mind. how to_monoid_hom is constructed versus of_bijective seems identical to me, except for the fact that to_monoid_hom is constructing a ->* from a mul_equiv, while of_bijective is constructing a mul_equiv from a ->* and bijectivity proof, as you mentioned.

[Holly Liu]

i guess i should be focusing on what the definitions are saying rather than their construction.

[Eric Wieser]

You seem to be confusing functions with types. The question shouldn't be about "how to_monoid_hom (a function) is constructed", it should be about "how the arguments of type monoid_hom are constructed"

[Yakov Pechersky]

mul_equiv.to_monoid_hom is a definition that gives you a monoid_hom if you provide it a mul_equiv. The important thing to note here is that a monoid_hom is just a decorated (in mathlib lingo "bundled") function f : R -> S with the relevant proofs about f 1 = 1 and f (x * y) = f x * f y.

mul_equiv on the other hand is a bundled _pair_ of functions f : R -> S and g : S -> R with the relevant proofs that ... etc... . So a mul_equiv has more data encoded in it!

[Holly Liu]

Eric Wieser said:

"how the arguments of type monoid_hom are constructed"

what does this mean? i'm confused on what these arguments are

[Eric Wieser]

You can use #check to find out

#check @mul_equiv.to_monoid_hom
-- mul_equiv.to_monoid_hom :
--  Π {M : Type u_1} {N : Type u_2} [_inst_5 : mul_one_class M] [_inst_6 : mul_one_class N],
--    M ≃* N → M →* N

If you don't know how to read this yet, then this is what you should focus on before trying to formalize anything using parts of mathlib.

[Holly Liu]

oh, is mul_equiv.to_monoid_hom of type monoid_hom?

[Eric Wieser]

No. But mul_equiv.to_monoid_hom _ is.

[Eric Wieser]

Just like fibonacci 3 is of type ℕ, but fibonacci is not.

[Holly Liu]

oh ok, so _ is implicitly filling in the arguments?

[Eric Wieser]

_ means "work out this argument if you can, error if you can't"

[Eric Wieser]

The error will tell you what type lean needed in the gap

[Eric Wieser]

If you put your cursor before the _ as |_, then the goal view will show the type too

[Holly Liu]

got it, thanks