Zulip Chat Archive

Stream: new members

Topic: group


Amaury Hayat (May 17 2021 at 10:17):

Hi all,
My name is Amaury Hayat, I am a mathematician just beginning with Lean, and I am very happy to join this community! I read the doc and played at the very nice Natural Number Game. I am trying to write some theorems, and I am still struggling with some maths notations in Lean: for instance I am trying to write that for n\in\mathbb{N}^{*}, f : x |-> x^{n} is a group homomorphism from (\mathbb{R}^{*}, \times) in itself and was wondering whether there is already some code to show that (\mathbb{R}^{*}, \times) is a multiplicative group. Thanks a lot in advance, I hope I'll be able to contribute to this project :)

Anne Baanen (May 17 2021 at 10:19):

You can write R\mathbb{R}^* as units ℝ

Eric Rodriguez (May 17 2021 at 10:19):

also, you can write LaTeX in Zulip by surrounding it with $$, e.g. nN,f:xxnn\in\mathbb{N}^{*}, f : x \mapsto x^{n}

Anne Baanen (May 17 2021 at 10:20):

(Or is N\mathbb{N}^{*} something different from the invertible elements, i.e. {1}?)

Eric Rodriguez (May 17 2021 at 10:22):

Maybe it's notation for the positive natural numbers? I haven't seen it before either

Eric Rodriguez (May 17 2021 at 10:23):

And the fact that it's a group is registered through the type-class system; for example see here for the proof/instance that the units of a monoid (like ℝ) also form a group

Eric Rodriguez (May 17 2021 at 10:24):

So you can just start doing group stuff with it and it'll be fine with it

Anne Baanen (May 17 2021 at 10:24):

Ah, it's probably where * is actually addition, so multiplicative ℕ in mathlib

Horatiu Cheval (May 17 2021 at 10:28):

I always thought N\mathbb{N}^* was a standard notation for the naturals without 0. Maybe it's a regional thing.

Mario Carneiro (May 17 2021 at 10:28):

The syntax RR^* usually means "without zero", so in this case N\mathbb{N}^* means the positive natural numbers pnat. It is also used on other rings like R\mathbb{R}^*, in which case we are usually interested in the multiplicative structure; this is what (R,×)(\mathbb{R}^{*}, \times) means (which we would write units ℝ)

Riccardo Brasca (May 17 2021 at 10:30):

I had this exact discussion with some friends (they are french and working in analysis). They were shocked that for me Z\mathbb{Z}^\ast does not mean Z{0}\mathbb{Z} \setminus \{0\}.

Mario Carneiro (May 17 2021 at 10:33):

Regarding the question, we already know that units R is an abelian group, so I would generalize this to the statement that λ x, n • x is a group hom on any abelian group

Johan Commelin (May 17 2021 at 10:35):

Which as of recently is part of the axioms of (additive) abelian groups

Mario Carneiro (May 17 2021 at 10:40):

ah, here it is: docs#gpow.is_group_hom

Amaury Hayat (May 17 2021 at 11:50):

Thanks a lot for all these answers ! It's very helpful :) Yes I used $\mathbb{N}^{*}$ for the positive natural numbers, sorry for the confusion I should have remembered that this is just a regional thing.

Johan Commelin (May 17 2021 at 11:53):

@Amaury Hayat Confusingly, you need to use $$ for inline math on Zulip.

Amaury Hayat (May 17 2021 at 12:05):

Ok, thanks ! Seems like I'm a beginner on Zulip as well.

Johan Commelin (May 17 2021 at 12:06):

We have all been there (-;

Kevin Buzzard (May 17 2021 at 12:51):

Everyone is bikeshedding about N\mathbb{N}^* but the statement is true for N\mathbb{N} ;-)

@Amaury Hayat here are the two sorrys which Lean would like you to fill in for your result:

import data.real.basic

def real.nat_pow_hom (n : ) : units  →* units  :=
{ to_fun := λ u, u^n,
  map_one' := begin
    sorry
  end,
  map_mul' := begin
    sorry
  end }

I suspect that there is a way to do it with just one sorry, there should be a constructor for group homs which only demands a proof of map_mul.

Amaury Hayat (May 17 2021 at 15:37):

Thanks a lot @Kevin Buzzard for this answer ! Indeed, the statement was conservative. Do you think there would be a way to state it as a theorem (for the sole purpose of exercising in writing statements) like:

def f (n: ) (x : units ):=x^n
theorem my_test_th (n : ) : is_group_hom (f n) :=
begin
    sorry
end

Would this formulation be too naïve (as it implicitly uses that units \br is a group) ? Apologies in advance if this is a silly question: I literally just started writing in Lean this morning.

Johan Commelin (May 17 2021 at 16:02):

@Amaury Hayat Yes, some think like that looks fine. Although mathlib no longer uses is_group_hom.

Amaury Hayat (May 17 2021 at 16:04):

Great, thanks! I'll use monoid_hom then.

Eric Wieser (May 17 2021 at 16:21):

I think we have this in the library as (powers_mul_hom (units ℝ)).to_monoid_hom.flip n (docs#powers_mul_hom)

Eric Wieser (May 17 2021 at 16:28):

This also works:

import data.real.basic

def real.nat_pow_hom (n : ) : units  →* units  :=
monoid_hom.of (^ n)

Kevin Buzzard (May 17 2021 at 16:43):

Lean knows that the units of R\R (or indeed of any ring) are a group under multiplication -- this "therorem" (as a mathematician would call it), or, more precisely, construction (as Lean would call it), is part of Lean's type class inference system. Eric's proof is just saying "it's in mathlib already" which of course is not surprising.

Kevin Buzzard (May 17 2021 at 16:43):

Lean knows that the units of R\R (or indeed of any ring) are a group under multiplication -- this "therorem" (as a mathematician would call it), or, more precisely, construction (as Lean would call it), is part of Lean's type class inference system. Eric's proof is just saying "it's in mathlib already" which of course is not surprising.

Amaury Hayat (May 17 2021 at 17:38):

Great, thank you for the explanation


Last updated: Dec 20 2023 at 11:08 UTC