New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Free groups #89
Free groups #89
Conversation
group_theory/free_group.lean
Outdated
|
||
end to_inv_type | ||
|
||
@[reducible] def word (S : Type u) : Type u := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can this not go in the global namespace?
group_theory/free_group.lean
Outdated
@@ -0,0 +1,360 @@ | |||
-- https://math.stackexchange.com/a/852661/328173 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Add a header to the file similar to other files in mathlib, with you as the author
2f0beae
to
22e671c
Compare
@kckennylau instead of closing this pull request, can you keep it and just update the branch on your side? |
oh wait is this a bug |
algebra/free_group.lean
Outdated
|
||
universes u v | ||
|
||
class inv_mon (M : Type u) extends monoid M, has_inv M := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Or involution_monoid
, inv_monoid
, etc
algebra/free_group.lean
Outdated
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 := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't we have monoid homomorphisms already?
algebra/free_group.lean
Outdated
|
||
end inv_mon.to_group | ||
|
||
class inv_type (IT : Type u) extends has_inv IT := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Move this before mon_inv
, extend mon_inv
using this than to_inv_type
is added implicitly and give it another name like: involution
?
algebra/free_group.lean
Outdated
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] := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would not introduce an extra name for it. Is there a specific reason why you don't want to use list
?
algebra/free_group.lean
Outdated
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Use list.prod
?
algebra/free_group.lean
Outdated
| [] := 1 | ||
| (h::IT) := f h * left_adjoint IT | ||
|
||
theorem left_adjoint.mul : ∀ x y, left_adjoint (x * y) = left_adjoint x * left_adjoint y |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
prod_mul
algebra/free_group.lean
Outdated
|
||
end inv_type.to_inv_mon | ||
|
||
@[reducible] def to_inv_type (T : Type u) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess α × bool
would be a better choice.
algebra/free_group.lean
Outdated
namespace to_inv_type | ||
|
||
def inv (T : Type u) : to_inv_type T → to_inv_type T | ||
| (sum.inl x) := sum.inr x |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is then just bnot
on the second argument
algebra/free_group.lean
Outdated
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
algebra/free_group.lean
Outdated
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) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you use bool
you can reduce these two cases to one.
algebra/free_group.lean
Outdated
|
||
namespace free_group | ||
|
||
variables (S : Type u) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For consistency, please change your upper case type names to α, β, γ
etc.
The new version looks great. What is the reason why you don't want to use |
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. |
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 |
Now I'm stuck on proving that "of" is injective. Before I could use quotient.exact. |
You can use |
Then I don't see the point of using |
The point is that |
@johoelzl Now that I changed the definition of free group to |
@kckennylau Does this have all your latest work on free groups? |
Also we need to have @johoelzl and @kckennylau work out the differences in their developments here |
@digama0 yes. |
My idea is to merge this PR and then gradually add my theory on transitive closure etc. |
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).