groups

Stream: general

[Michael Melesse]

Hey everyone, I just finished the Naturals number game. It was great. Does anyone know if there are any resources on working with groups in lean.

[Yury G. Kudryashov]

Math library has docs#group and many other definitions/theorems.

[Michael Melesse]

Got it thank you. I will take a look.

[Michael Melesse]

Would you know where I can find an example of some one proving something simple about groups using lean.

[Michael Melesse]

nvm, just found https://cocalc.com/share/public_paths/f014cd1885a22e8665a728be825e563fc79b7e1f/README.md

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib/tree/master/src/algebra/group

[Yury G. Kudryashov]

and https://github.com/leanprover-community/mathlib/tree/master/src/group_theory

[Kevin Buzzard]

These links to mathlib are not really useful here -- the mathlib proofs are incomprehensible to someone who has only played NNG

[Kevin Buzzard]

Here's a link to a workshop I ran about group theory for lean beginners: https://xenaproject.wordpress.com/2021/01/28/formalising-mathematics-workshop-2/

[Yaël Dillies]

For having learnt Lean using this, I can attest of this workshop's quality.

[Kevin Buzzard]

The mathlib links on the other hand do give you some kind of feeling as to "how far we have got" in group theory. For example the names of the files indicate what is covered and the module docstrings (the text at the top of each file) explains what definitions are made and what theorems are proved in the files

[Michael Melesse]

Thank you all. Looking forward to going through the workshop

[Michael Melesse]

How would I go about defining a custom group in lean? For example if I wanted to define a group on a subset of the reals and a custom op.

[Yaël Dillies]

Fill those in :smile:

def my_group (S : set ℝ) : group S :=
{ mul := _,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  inv := _,
  mul_left_inv := _ }

[Yaël Dillies]

To quickly get this list of fields, you can do

def my_group (S : set ℝ) : group S :=
{!!}

and click on the lightbulb.

[Adam Topaz]

Yaël Dillies said:

Fill those in :smile:

def my_group (S : set ℝ) : group S :=

This won't work -- this will ask you to define a group structure on any given set S of reals. I assume you have a specific set Sin mind?

[Yaël Dillies]

Yeah of course, I don't know what Michael wants.

[Michael Melesse]

Yes, I was hoping to define on ℝ\{-1}

[Adam Topaz]

what's the operation?

[Yaël Dillies]

Then replace S with {x : ℝ // x ≠ -1}.

[Michael Melesse]

The op is a*b :=(a+b)^2 where a,b are in the set ℝ\{-1}

[Michael Melesse]

Thank you both

[Eric Rodriguez]

Yaël Dillies said:

Fill those in :smile:

def my_group (S : set ℝ) : group S :=
{ mul := _,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  inv := _,
  div := _,
  div_eq_mul_inv := _,
  mul_left_inv := _ }

Div and Div eq mul inv are impl details right?

[Yaël Dillies]

Whoops, yeah

[Bolton Bailey]

Michael Melesse said:

The op is a*b :=(a+b)^2 where a,b are in the set ℝ\{-1}

I don't actually see how this operation defines a group. Is there any identity element e such that a = (a + e)^2 for all a in your set?

[Michael Melesse]

oops this is the op, ab + a + b

[Yaël Dillies]

Aah, makes more sense

[Yaël Dillies]

You can also instead define a group_with_zero ℝ. That'll probably be more pleasant.

[Mario Carneiro]

The nicest way to prove that is to prove that a -> a - 1 is a bijection from units ℝ to ℝ\{-1} such that the image of * under the bijection is a,b -> ab+a+b

[Michael Melesse]

@Yaël Dillies When you say replace S with {x : ℝ // x ≠ -1}. Do you mean define a variable? Just plugging it in doesnot seem to work

[Yaël Dillies]

I mean

def my_group : group {x : ℝ // x ≠ -1} := ...

[Michael Melesse]

Got it. Thanks.

[Michael Melesse]

When I define the mul like this mul := ∀(a b:{x : ℝ // x ≠ -1}), a+a*b+b, I get an error about the addition

[Michael Melesse]

failed to synthesize type class instance for
a b : {x // x ≠ -1}
⊢ has_add {x // x ≠ -1}

[Michael Melesse]

I cannot seem to define an add op. The group structure doesnot have it to overwrite

[Michael Melesse]

looking through docs non of the flavors have add and mul at the same time

[Yaël Dillies]

Welcome to subtyping hell. :smiling_devil: Enjoy you stay.

[Yaël Dillies]

{x : ℝ // x ≠ -1} is an entirely new type, so Lean doesn't know anything about it besides its definition. And it certainly doesn't know the inexistent addition you're trying to define: -1/2 : {x : ℝ // x ≠ -1} but you cannot make -1/2 + -1/2 have the meaningful value -1 as it's not in the type!

[Yaël Dillies]

The answer is to define your operations through ℝ and show they preserve ≠ -1. An element of {x : ℝ // x ≠ -1} is ⟨an element of ℝ, a proof that it's ≠ -1⟩.

[Yaël Dillies]

So your operation will look like λ a b, ⟨(a : ℝ) * b + a + b, some_proof⟩.

[Yaël Dillies]

(a : ℝ) telling Lean to consider a as a real.

[Yaël Dillies]

You probably start getting why we use group_with_zero. Removing 0 to provide a group structure is simply too much of a pain.

[Eric Wieser]

I'm not sure this really counts as subtyping hell; this seems like exactly what you would expect to have to do on paper.