Zulip Chat Archive

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

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

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

Kenny Lau (Apr 01 2018 at 17:10):

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"

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

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

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

no, just n^k

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

so it's just n^omega

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

hmm

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

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

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

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

Mario Carneiro (Apr 01 2018 at 18:32):

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

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

i see

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

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

Kenny Lau (Apr 01 2018 at 18:36):

hmm

Kenny Lau (Apr 01 2018 at 18:44):

@Mario Carneiro linked list though

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?

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

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)

Kenny Lau (Apr 02 2018 at 04:22):

...

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

I'm rereading the proof now

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

Mario Carneiro (Apr 02 2018 at 04:50):

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: Dec 20 2023 at 11:08 UTC