# Zulip Chat Archive

## 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 }`

instead of

`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 `submodule`

s not `semimodule`

s, 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 _,
add_mem' := λ a b, is_add_submonoid.add_mem,
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},
{ rw [nat.succ_eq_add_one, add_smul, one_smul], exact s.add_mem n_ih hx },
end,
..s}
```

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

I get it now: in my mind, the distinction between the full add_comm_monoid and an add_submonoid of it were not separated, since, thinking about it in Lean term, I was already applying the coercion to simply reduce to the top element.

Thanks for spelling out this example!

Last updated: May 07 2021 at 19:12 UTC