Zulip Chat Archive

Stream: maths

Topic: free group


view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:00):

is this what you wanted?

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:00):

you see, ambient has two universe parameters

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:02):

and this fucks up everything

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:03):

Yes!

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:03):

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

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:04):

I didn't read all of what Mario had to say about this.

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:05):

It's a bit annoying though

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:05):

it's maximally impredicative

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:05):

it's philosophically unsound

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:05):

You could be even less constructive by replacing generate with span

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:06):

I never know which is which

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:06):

they are synonymous in my head

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:07):

the point is

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:07):

you need to build the ambient group from S

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:07):

if you want things to work

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:08):

because it's cheating

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:08):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:08):

not because it's cheating

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:08):

but because it leads to hell

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:08):

whereas free groups won't take you to hell

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:08):

because they really do exist

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:09):

right

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:09):

but that isn't the way to justify it

view this post on Zulip 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"?

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:10):

correct

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 17:10):

Can one prove such a theorem in Lean?

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:12):

actually

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:12):

what cardinality do you need?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:13):

no, just n^k

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:13):

so it's just n^omega

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:14):

hmm

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:14):

I mean

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 17:16):

@Mario Carneiro ves algum problema em o meu pull?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 0\aleph_0 then any group generated by S has cardinality at most κ\kappa'

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 18:09):

eew what kind of a \kappa is that

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:19):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:19):

ordinal exponent

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:32):

that epsilon-abstraction though @Mario Carneiro

view this post on Zulip Mario Carneiro (Apr 01 2018 at 18:32):

say what?

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:33):

so you can't find that cardinal explicitly

view this post on Zulip Mario Carneiro (Apr 01 2018 at 18:33):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:34):

axiom of unique choice?

view this post on Zulip Mario Carneiro (Apr 01 2018 at 18:34):

cardinal theory uses choice everywhere, so meh

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:34):

i see

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:34):

fair enough

view this post on Zulip Mario Carneiro (Apr 01 2018 at 18:34):

but it is explicitly constructed

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:34):

so do you see any problem with my pr

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:36):

hmm

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:44):

@Mario Carneiro linked list though

view this post on Zulip Kenny Lau (Apr 01 2018 at 18:48):

you need decidable equality

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:10):

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

view this post on Zulip Kenny Lau (Apr 01 2018 at 20:10):

@Mario Carneiro done!

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:15):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:15):

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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:18):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:18):

yes

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:18):

that's reduce.min

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:18):

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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:19):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:19):

oh, I don't know that then

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:22):

...

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:28):

I thought you wrote it

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:28):

I'm rereading the proof now

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:49):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:49):

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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:50):

yeah that

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:51):

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

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:55):

proving multiplication amounts to the same amount of work

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 02 2018 at 04:55):

i.e. I can't prove it

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 02 2018 at 04:59):

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

view this post on Zulip 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