is_square/is_power

Stream: Is there code for X?

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Mario Carneiro]

Here I think it needs to be monoids though

[Mario Carneiro]

because there is no multiplicative version of semirings

[Damiano Testa]

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

[Mario Carneiro]

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

[Damiano Testa]

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]

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]

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]

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]

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]

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]

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]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Eric Wieser]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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!