Free groups by kckennylau · Pull Request #89 · leanprover-community/mathlib3

kckennylau · 2018-04-01T07:41:22Z

Local copy: https://github.com/kckennylau/Lean/blob/master/free_group.lean

Construction given by https://math.stackexchange.com/a/852661/328173

A three-step approach to constructing the free group over a set (type).

digama0 · 2018-04-05T04:26:47Z

group_theory/free_group.lean

+
+end to_inv_type
+
+@[reducible] def word (S : Type u) : Type u :=


Can this not go in the global namespace?

digama0 · 2018-04-05T04:28:03Z

group_theory/free_group.lean

@@ -0,0 +1,360 @@
+-- https://math.stackexchange.com/a/852661/328173


Add a header to the file similar to other files in mathlib, with you as the author

johoelzl · 2018-04-05T07:52:26Z

@kckennylau instead of closing this pull request, can you keep it and just update the branch on your side?

kckennylau · 2018-04-05T08:33:04Z

oh wait is this a bug

johoelzl · 2018-04-05T08:58:26Z

algebra/free_group.lean

+
+universes u v
+
+class inv_mon (M : Type u) extends monoid M, has_inv M :=


inv_mon doesn't seam to be a very informative name, especially since it is a global name I would prefer something longer: monoid_with_involution or monoid_with_inv?

Or involution_monoid, inv_monoid, etc

johoelzl · 2018-04-05T08:59:10Z

algebra/free_group.lean

+  one_inv := one_inv,
+  inv_inv := inv_inv }
+
+class inv_mon.is_hom (M : Type u) (N : Type v) [inv_mon M] [inv_mon N] (f : M → N) : Prop :=


Don't we have monoid homomorphisms already?

johoelzl · 2018-04-05T09:02:06Z

algebra/free_group.lean

+
+end inv_mon.to_group
+
+class inv_type (IT : Type u) extends has_inv IT :=


Move this before mon_inv, extend mon_inv using this than to_inv_type is added implicitly and give it another name like: involution?

johoelzl · 2018-04-05T09:03:19Z

algebra/free_group.lean

+instance inv_mon.to_inv_type (M : Type u) [inv_mon M] : inv_type M :=
+{ inv_inv := inv_mon.inv_inv }
+
+@[reducible] def inv_type.to_inv_mon (IT : Type u) [inv_type IT] :=


I would not introduce an extra name for it. Is there a specific reason why you don't want to use list?

johoelzl · 2018-04-05T09:03:32Z

algebra/free_group.lean

+parameters (f : IT → M) -- IT → Forgetful(M)
+parameters (Hinv : ∀ x, f x⁻¹ = (f x)⁻¹)
+
+def left_adjoint : inv_type.to_inv_mon IT → M -- Free(IT) → M


Use list.prod?

johoelzl · 2018-04-05T09:04:05Z

algebra/free_group.lean

+| []     := 1
+| (h::IT) := f h * left_adjoint IT
+
+theorem left_adjoint.mul : ∀ x y, left_adjoint (x * y) = left_adjoint x * left_adjoint y


johoelzl · 2018-04-05T09:04:51Z

algebra/free_group.lean

+
+end inv_type.to_inv_mon
+
+@[reducible] def to_inv_type (T : Type u) :=


I guess α × bool would be a better choice.

johoelzl · 2018-04-05T09:05:12Z

algebra/free_group.lean

+namespace to_inv_type
+
+def inv (T : Type u) : to_inv_type T → to_inv_type T
+| (sum.inl x) := sum.inr x


This is then just bnot on the second argument

johoelzl · 2018-04-05T09:06:30Z

algebra/free_group.lean

+def reduce : word S → word S
+| ((sum.inl x)::(sum.inr y)::t) := if x = y then reduce t else ((sum.inl x)::(sum.inr y)::reduce t)
+| ((sum.inr x)::(sum.inl y)::t) := if x = y then reduce t else ((sum.inr x)::(sum.inl y)::reduce t)
+| (h1::h2::t)                   := h1::h2::reduce t


This looks wrong to me, shouldn't reduce [a, b, b⁻¹] evaluate to [a]? As far as I see it this is not the case.

johoelzl · 2018-04-05T09:15:47Z

algebra/free_group.lean

+variable [decidable_eq S]
+
+def reduce : word S → word S
+| ((sum.inl x)::(sum.inr y)::t) := if x = y then reduce t else ((sum.inl x)::(sum.inr y)::reduce t)


If you use bool you can reduce these two cases to one.

johoelzl · 2018-04-05T09:17:03Z

algebra/free_group.lean

+
+namespace free_group
+
+variables (S : Type u)


For consistency, please change your upper case type names to α, β, γ etc.

rebase

Patch 8

johoelzl · 2018-04-19T18:29:54Z

The new version looks great.

What is the reason why you don't want to use quot on red.step to define free_group? Then the lifting proofs should be easier as there is no transitivity necessary.

kckennylau · 2018-04-20T00:56:05Z

I find quotient to be more user-friendly than quot, and more mathematical to be honest (I don't remember the last time someone quotiented by a non-transitive relation). However, I'm now experimenting with quot to see how it goes.

digama0 · 2018-04-20T00:58:21Z

It's not uncommon to define a quotient by saying what things are related, where implicitly you are supposed to take the equivalence closure of the given relation. That is exactly what quot does, it's not really a quotient by a non-transitive relation so much as a quotient by the equivalence relation generated by a non-transitive relation.

kckennylau · 2018-04-20T01:43:50Z

Now I'm stuck on proving that "of" is injective. Before I could use quotient.exact.

johoelzl · 2018-04-20T06:05:29Z

You can use quot.exact. You will need to prove eqv_gen red.step L₁ L₂ is the same as ∃ L₃, red L₁ L₃ ∧ red L₂ L₃ . But this is essentially what you have in https://github.com/leanprover/mathlib/pull/89/files#diff-5f7e06d86429e56d8e516817d14026d1R131

kckennylau · 2018-04-20T08:44:10Z

Then I don't see the point of using quot instead of quotient.

johoelzl · 2018-04-20T08:46:39Z

The point is that quot.lift on red.step is easier to use than quotient.lift on the setoid.r defined in your file.
When definining mul, inv, etc. one just need to show that your definitions are invariant under exactly one reduction step, and not a sequence of reduction steps.

kckennylau · 2018-04-21T15:05:01Z

@johoelzl Now that I changed the definition of free group to quot $ @free_group.red.step α, I don't really feel like I have removed a lot of lemmas. For example, consider the lemma red.append that says red commutes with list.append, which was used to prove that multiplication is well-defined. Well, now it is used in reduce.red to show that there is a sequence of reduction from L to reduce L, which is one of the two interface theorems of reduce (the other being reduce.min). By that, I mean that every other theorem of reduce are proved from these two theorems, i.e. they characterise the reduce function.

digama0 · 2018-04-24T18:31:34Z

@kckennylau Does this have all your latest work on free groups?

digama0 · 2018-04-24T18:32:12Z

Also we need to have @johoelzl and @kckennylau work out the differences in their developments here

kckennylau · 2018-04-25T00:48:19Z

@digama0 yes.

johoelzl · 2018-04-25T11:31:30Z

My idea is to merge this PR and then gradually add my theory on transitive closure etc.

digama0 reviewed Apr 5, 2018

View reviewed changes

digama0 force-pushed the master branch 2 times, most recently from 2f0beae to 22e671c Compare April 5, 2018 05:29

kckennylau closed this Apr 5, 2018

kckennylau deleted the patch-6 branch April 5, 2018 07:53

Create free_group.lean

0d2d312

kckennylau mentioned this pull request Apr 5, 2018

Create free_group.lean #92

Closed

kckennylau restored the patch-6 branch April 5, 2018 08:32

kckennylau reopened this Apr 5, 2018

johoelzl force-pushed the patch-6 branch from 20126d4 to 0d2d312 Compare April 5, 2018 08:46

johoelzl changed the title ~~Create free_group.lean~~ Free groups Apr 5, 2018

johoelzl reviewed Apr 5, 2018

View reviewed changes

kckennylau added 4 commits April 20, 2018 00:04

Merge pull request #9 from leanprover/master

53c99eb

rebase

Update free_group.lean

b6511ac

Update subgroup.lean

d1cd117

Merge pull request #10 from kckennylau/patch-8

9ece2d7

Patch 8

Update free_group.lean

af1bb2c

Update free_group.lean

1bef421

johoelzl merged commit 716decc into leanprover-community:master Apr 25, 2018

kckennylau deleted the patch-6 branch November 16, 2018 11:58


		end to_inv_type

		@[reducible] def word (S : Type u) : Type u :=

		@@ -0,0 +1,360 @@
		-- https://math.stackexchange.com/a/852661/328173


		universes u v

		class inv_mon (M : Type u) extends monoid M, has_inv M :=


		end inv_mon.to_group

		class inv_type (IT : Type u) extends has_inv IT :=


		end inv_type.to_inv_mon

		@[reducible] def to_inv_type (T : Type u) :=


		namespace free_group

		variables (S : Type u)

Conversation

kckennylau commented Apr 1, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

johoelzl commented Apr 5, 2018

Uh oh!

kckennylau commented Apr 5, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

johoelzl commented Apr 19, 2018

Uh oh!

kckennylau commented Apr 20, 2018

Uh oh!

digama0 commented Apr 20, 2018

Uh oh!

kckennylau commented Apr 20, 2018

Uh oh!

johoelzl commented Apr 20, 2018

Uh oh!

kckennylau commented Apr 20, 2018

Uh oh!

johoelzl commented Apr 20, 2018

Uh oh!

kckennylau commented Apr 21, 2018

Uh oh!

digama0 commented Apr 24, 2018

Uh oh!

digama0 commented Apr 24, 2018

Uh oh!

kckennylau commented Apr 25, 2018

Uh oh!

johoelzl commented Apr 25, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants