group

Stream: new members

[Amaury Hayat]

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]

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

[Eric Rodriguez]

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

[Anne Baanen]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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]

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

[Anne Baanen]

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

[Horatiu Cheval]

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

[Mario Carneiro]

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

[Riccardo Brasca]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

ah, here it is: docs#gpow.is_group_hom

[Amaury Hayat]

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]

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

[Amaury Hayat]

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

[Johan Commelin]

We have all been there (-;

[Kevin Buzzard]

Everyone is bikeshedding about $\mathbb{N}^*$ but the statement is true for $\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]

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]

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

[Amaury Hayat]

Great, thanks! I'll use monoid_hom then.

[Eric Wieser]

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

[Eric Wieser]

This also works:

import data.real.basic

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

[Kevin Buzzard]

Lean knows that the units of $\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]

Lean knows that the units of $\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]

Great, thank you for the explanation