## Stream: Is there code for X?

### Topic: is_square/is_power

#### Damiano Testa (Mar 16 2021 at 08:20):

Dear All,

is there a predicate is_square in mathlib, similar to what is below? I would be interested in talking about squares, sums of squares and preorders (in rings), building up to Hilbert's 17th problem.

def is_square (R : Type*) [has_mul R] (r : R) : Prop :=
∃ s : R, r = s * s


#### Mario Carneiro (Mar 16 2021 at 08:22):

No, we usually just write out the existential or use s * s in theorems

#### Damiano Testa (Mar 16 2021 at 08:30):

Ok, thanks! I want to prove stuff like: if R is a comm_monoid, then the set of squares is a (sub)comm_monoid, if you take the sums of squares of a comm_semiring, you obtain a (sub)comm_semiring and then build on top of that.

#### Mario Carneiro (Mar 16 2021 at 08:32):

This might actually follow from some notion of ideals, since this is essentially saying that {n | 2 •ℤ n} is a submonoid

#### Damiano Testa (Mar 16 2021 at 08:34):

Ah, so the refactor of ideal to work with comm_semiring instead of comm_ring might prove useful! :tada:

#### Mario Carneiro (Mar 16 2021 at 08:34):

Here I think it needs to be monoids though

#### Mario Carneiro (Mar 16 2021 at 08:34):

because there is no multiplicative version of semirings

#### Damiano Testa (Mar 16 2021 at 08:35):

Yeah, this is for a single multiplicative operation, unfortunately...

#### Mario Carneiro (Mar 16 2021 at 08:35):

I think this is also called divisibility (as in divisible group)?

#### Damiano Testa (Mar 16 2021 at 08:36):

Yes, it is being 2-divisible, although I may interpret what I said, literally, as being "arbitrarily divisible by 2", depending on context.

#### Damiano Testa (Mar 16 2021 at 08:37):

I view the notion of "divisibility" more as a "typeclass" than a notion that I apply to individual elements, but this might be just me.

#### Kevin Buzzard (Mar 16 2021 at 08:40):

This should probably be some predicate on comm_monoid_with_zero (or even being an n'th power). The big theorem is that in a unique factorization monoid, if the product of two coprime elements is associated to an n'th power then so are both the elements.

#### Damiano Testa (Mar 16 2021 at 08:40):

E.g. I would find it weird to say that 2 is 2-divisible in $\mathbb{Q} [\sqrt{2}]$, but I would not object to the multiplicative group $\overline{\mathbb{Q}}^\times$ being (2-)divisible.

#### Damiano Testa (Mar 16 2021 at 08:41):

I would have said that the big theorem was that a rational function over $\mathbb{R}$ is a sum of squares if and only if its meaningful evaluations are non-negative! :wink:

I am very optimistic...

#### Damiano Testa (Mar 16 2021 at 08:43):

Actually, I have been playing with this and I started in the initial set up simply on has_mul R, building up to semigroup, monoid, comm_monoid, monoid_with_zero, and so on.

#### Kevin Buzzard (Mar 16 2021 at 08:43):

I have a really nice exposition of this stuff from some lectures of Pfister which I went to in the 90s, but unfortunately the notes are in my office. They would be perfect to formalise.

#### Damiano Testa (Mar 16 2021 at 08:44):

I am using a book by Pfister for my class on this and it is indeed perfect for formalization!

#### Damiano Testa (Mar 16 2021 at 08:44):

The only issue is that, in these notes, Pfister do not give a proof of the Artin-Lang homomorphism theorem. But assuming that, everything seems already written with the idea of formalizing it!

#### Damiano Testa (Mar 16 2021 at 12:15):

PR #6705, in case anyone wants to comment, before I generalize this to higher powers!

#### Damiano Testa (Mar 16 2021 at 14:08):

In the PR, Eric suggested using

add_submonoid.closure { r : R | is_square R r }
submodule.span ℕ { r : R | is_square R r }
for the set of all sums of squares. I now have working proofs for either one of the two, producing a comm_semiring instance on them.

Is there a reason to prefer one to the other?

#### Eric Wieser (Mar 16 2021 at 14:20):

The former is simpler, as scalar multiplication by N is probably just a distraction for you

#### Eric Wieser (Mar 16 2021 at 14:21):

We probably ought to have add_submonoid.to_nat_submodule and add_subgroup.to_int_submodule definitions somewhere

#### Damiano Testa (Mar 16 2021 at 14:26):

While you are probably right that nat-multiplication is dispensable, I do think that there should be the instances that you mention. In fact, Lean does not complain with

instance {S : Type*} [add_comm_monoid S] : semimodule ℕ S := by apply_instance


this means that the instance is already there, right?
(Sorry for the silly confirmation, I am still skeptical about my correct usage of instances.)

#### Eric Wieser (Mar 16 2021 at 14:26):

We're talking about submodules not semimodules, so instances aren't relevant here ;)

#### Damiano Testa (Mar 16 2021 at 14:28):

Ah, semimodule A B is the type of all A subsemimodules of the A-semimodule B? If this is so, then I can see why what I wrote above is not conclusive. I also do not understand why lean likes it...

#### Damiano Testa (Mar 16 2021 at 14:31):

Does this make more sense, then?

def sus {S : Type*} [add_comm_monoid S] : submodule ℕ S :=
{ carrier := set.univ,
zero_mem' := set.mem_univ _,
smul_mem' := λ a b hb, set.mem_univ (a • b) }


#### Eric Wieser (Mar 16 2021 at 14:35):

I mean, that's just ⊤, which isn't really interesting

import linear_algebra.basic
example {S : Type*} [add_comm_monoid S] : submodule ℕ S := ⊤


#### Eric Wieser (Mar 16 2021 at 14:38):

Eric Wieser said:

We probably ought to have add_submonoid.to_nat_submodule and add_subgroup.to_int_submodule definitions somewhere

To be clear, what I'm describing here is

def add_submonoid.to_nat_submodule {S : Type*} [add_comm_monoid S] (s : add_submonoid S) : submodule ℕ S :=
{ smul_mem' := λ n x hx, begin
induction n,
{ rw zero_smul, exact s.zero_mem},