## Stream: maths

### Topic: free group

#### Kenny Lau (Apr 01 2018 at 16:59):

@Kevin Buzzard here's my old version of free group https://github.com/kckennylau/Lean/blob/c6eac863b23d58d40deaab62489f6069f860407e/free_group.lean

#### Kenny Lau (Apr 01 2018 at 17:00):

is this what you wanted?

#### Kenny Lau (Apr 01 2018 at 17:00):

you see, ambient has two universe parameters

#### Kenny Lau (Apr 01 2018 at 17:02):

and this fucks up everything

Yes!

#### Kevin Buzzard (Apr 01 2018 at 17:03):

I thought Lean would somehow fix this, but the stupid issue is still there.

#### Kevin Buzzard (Apr 01 2018 at 17:04):

Maybe you can get a contradiction with a diagonal argument if you can get it to work all in the same universe :-)

#### Kevin Buzzard (Apr 01 2018 at 17:05):

It's a bit annoying though

#### Kenny Lau (Apr 01 2018 at 17:05):

it's maximally impredicative

#### Kenny Lau (Apr 01 2018 at 17:05):

it's philosophically unsound

#### Kevin Buzzard (Apr 01 2018 at 17:05):

You could be even less constructive by replacing generate with span

#### Kevin Buzzard (Apr 01 2018 at 17:06):

I never know which is which

#### Kevin Buzzard (Apr 01 2018 at 17:06):

they are synonymous in my head

#### Kenny Lau (Apr 01 2018 at 17:06):

you can't just quantify through every gorup and pretend that you have the UMP wrt every group

#### Kevin Buzzard (Apr 01 2018 at 17:07):

but the one where you say "if I am a subgroup of the big product containing S, then I contain span S"

the point is

#### Kenny Lau (Apr 01 2018 at 17:07):

you need to build the ambient group from S

#### Kenny Lau (Apr 01 2018 at 17:07):

if you want things to work

#### Kevin Buzzard (Apr 01 2018 at 17:08):

I don't really understand why you can't just quantify through every group and pretend you have the UMP. Maybe I should read Mario's posts more carefully, wherever they've gone

#### Kenny Lau (Apr 01 2018 at 17:08):

because it's cheating

#### Kevin Buzzard (Apr 01 2018 at 17:08):

I don't want to make the set of all sets

#### Kevin Buzzard (Apr 01 2018 at 17:08):

not because it's cheating

#### Kevin Buzzard (Apr 01 2018 at 17:08):

but because it leads to hell

#### Kevin Buzzard (Apr 01 2018 at 17:08):

whereas free groups won't take you to hell

#### Kevin Buzzard (Apr 01 2018 at 17:08):

because they really do exist

right

#### Kenny Lau (Apr 01 2018 at 17:09):

but that isn't the way to justify it

#### Kevin Buzzard (Apr 01 2018 at 17:10):

To build the free group in the ZFC approach, do you first build the abstract group (the subset of the product) and then say "aah it's generated by S so there's something isomorphic to it in V_kappa"?

correct

#### Kevin Buzzard (Apr 01 2018 at 17:10):

Can one prove such a theorem in Lean?

#### Kevin Buzzard (Apr 01 2018 at 17:11):

"If I am an object in some universe then sometimes you can build some object in some smaller universe which is isomorphic to me"

actually

#### Kenny Lau (Apr 01 2018 at 17:12):

what cardinality do you need?

#### Kenny Lau (Apr 01 2018 at 17:13):

if you have n letters, to make a word of length k, you have at most k! n^k ways right

no, just n^k

#### Kenny Lau (Apr 01 2018 at 17:13):

so it's just n^omega

hmm

I mean

#### Kenny Lau (Apr 01 2018 at 17:14):

now that I built it in the proper way, I don't see why we're beating a dead horse

#### Kenny Lau (Apr 01 2018 at 17:16):

@Mario Carneiro ves algum problema em o meu pull?

#### Kenny Lau (Apr 01 2018 at 17:20):

@Kevin Buzzard "but that impredicative construction is not like constructing the set of all sets because it really exists" it is actually only correct iff you can justify its existence predicatively. that's the wrong justification for the right thing, and it doesn't tell you that it actually exists

#### Kevin Buzzard (Apr 01 2018 at 18:07):

n^omega is not at all the sum of n^k as I'm sure you know. Finitely-generated groups are all countable.

#### Kevin Buzzard (Apr 01 2018 at 18:09):

The point is that if S has cardinality $\kappa$ and if $\kappa'$ is the max of $\kappa$ and $\aleph_0$ then any group generated by S has cardinality at most $\kappa'$

#### Kevin Buzzard (Apr 01 2018 at 18:09):

eew what kind of a \kappa is that

#### Kenny Lau (Apr 01 2018 at 18:19):

@Kevin Buzzard by n^omega I mean union n^k

ordinal exponent

#### Mario Carneiro (Apr 01 2018 at 18:30):

@Kevin Buzzard You can do such "arguments by cardinality" for universe resizing in lean as well. An example of this is:

theorem  lift_down {a : cardinal.{u}} {b : cardinal.{max u v}} : b ≤ lift a → ∃ a', lift a' = b


which says that a cardinal that is smaller than a cardinal lifted from a small universe is also lifted from the small universe

#### Kenny Lau (Apr 01 2018 at 18:32):

that epsilon-abstraction though @Mario Carneiro

say what?

#### Kenny Lau (Apr 01 2018 at 18:33):

so you can't find that cardinal explicitly

#### Mario Carneiro (Apr 01 2018 at 18:33):

which cardinal are you referring to? the exists in that theorem is unique

#### Kenny Lau (Apr 01 2018 at 18:34):

axiom of unique choice?

#### Mario Carneiro (Apr 01 2018 at 18:34):

cardinal theory uses choice everywhere, so meh

i see

fair enough

#### Mario Carneiro (Apr 01 2018 at 18:34):

but it is explicitly constructed

#### Kenny Lau (Apr 01 2018 at 18:34):

so do you see any problem with my pr

#### Mario Carneiro (Apr 01 2018 at 18:36):

I don't think so. The only other thing I might want is a constructive reduced word function

hmm

#### Kenny Lau (Apr 01 2018 at 18:48):

you need decidable equality

#### Kenny Lau (Apr 01 2018 at 20:10):

https://github.com/kckennylau/Lean/blob/master/free_group.lean#L266

#### Kenny Lau (Apr 01 2018 at 20:10):

@Mario Carneiro done!

#### Kenny Lau (Apr 02 2018 at 04:15):

https://github.com/kckennylau/category-theory/blob/master/src/free_group.lean

#### Kenny Lau (Apr 02 2018 at 04:15):

@Mario Carneiro could you help me prove reduce.exact?

#### Mario Carneiro (Apr 02 2018 at 04:18):

do you know that the reduced word is minimal in length in the equivalence class?

yes

#### Kenny Lau (Apr 02 2018 at 04:18):

that's reduce.min

#### Mario Carneiro (Apr 02 2018 at 04:18):

that just says that the reduced word is smaller than the input

#### Mario Carneiro (Apr 02 2018 at 04:19):

I mean if v ~~ w then length (reduce w) <= length v

#### Kenny Lau (Apr 02 2018 at 04:19):

oh, I don't know that then

#### Mario Carneiro (Apr 02 2018 at 04:21):

You may find http://us.metamath.org/mpeuni/mmtheorems154.html helpful; that's my construction of free groups in metamath by a similar method (it's more cumbersome in ZFC since it has to describe the whole reduction sequence, not just the result)

...

#### Mario Carneiro (Apr 02 2018 at 04:28):

I think I see the proof strategy. It goes by induction on the length of an extension sequence, proving that if two extension sequences (where one has length <= n) end at the same point, then they start at the same point

#### Kenny Lau (Apr 02 2018 at 04:28):

I thought you wrote it

#### Mario Carneiro (Apr 02 2018 at 04:29):

An extension sequence is a sequence that starts at a reduced word and inserts cancelling pairs one at a time

#### Mario Carneiro (Apr 02 2018 at 04:29):

and the first step in the proof shows that every word has an extension sequence that terminates with it

#### Mario Carneiro (Apr 02 2018 at 04:32):

Since the length of an extension sequence is also (half) the difference in length between the initial word and the reduced word, you could try induction on that

#### Mario Carneiro (Apr 02 2018 at 04:48):

Okay, here's a suggestion in your language: can you prove the following?

inductive red (IT : Type u) [inv_type IT] :
inv_type.to_inv_mon IT → inv_type.to_inv_mon IT → Prop
| cons : ∀ a x y, red x y → red (a :: x) (a :: y)
| cancel : ∀ a x, red (a :: a⁻¹ :: x) x

theorem eqv_gen_red (IT : Type u) [inv_type IT]
{x y : inv_type.to_inv_mon IT} : x ≈ y ↔ eqv_gen (red IT) x y :=
sorry


#### Mario Carneiro (Apr 02 2018 at 04:49):

this will considerably simplify your induction for the reduce.exact theorem

#### Kenny Lau (Apr 02 2018 at 04:49):

but I don't need to simply reduced.sound, I need to prove reduced.exact

yeah that

#### Mario Carneiro (Apr 02 2018 at 04:51):

You could also fold in the eqv_gen constructors into the constructors of red if you prefer

#### Mario Carneiro (Apr 02 2018 at 04:51):

although splitting it this way gives you the ability to talk about one step reduction

#### Kenny Lau (Apr 02 2018 at 04:55):

proving multiplication amounts to the same amount of work

#### Kenny Lau (Apr 02 2018 at 04:55):

case inv_mon.to_group.rel.mul
IT : Type u,
_inst_1 : inv_type IT,
x y c d p q : inv_type.to_inv_mon IT,
h1 : inv_mon.to_group.rel (inv_type.to_inv_mon IT) c p,
h2 : inv_mon.to_group.rel (inv_type.to_inv_mon IT) d q,
ih1 : eqv_gen (red IT) c p,
ih2 : eqv_gen (red IT) d q
⊢ eqv_gen (red IT) (c * d) (p * q)


#### Kenny Lau (Apr 02 2018 at 04:55):

i.e. I can't prove it

#### Mario Carneiro (Apr 02 2018 at 04:57):

Try proving eqv_gen (red IT) x y -> eqv_gen (red IT) (a * x * b) (a * y * b)

#### Mario Carneiro (Apr 02 2018 at 04:59):

which reduces to red IT x y -> red IT (a * x * b) (a * y * b)

#### Mario Carneiro (Apr 02 2018 at 05:00):

(You could also do the left and right multiplications as separate lemmas)

Last updated: May 12 2021 at 07:17 UTC