Zulip Chat Archive

Stream: Is there code for X?

Topic: is_square/is_power


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:22):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:34):

Here I think it needs to be monoids though

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:34):

because there is no multiplicative version of semirings

view this post on Zulip Damiano Testa (Mar 16 2021 at 08:35):

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

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Mar 16 2021 at 08:40):

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

view this post on Zulip Damiano Testa (Mar 16 2021 at 08:41):

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

I am very optimistic...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Mar 16 2021 at 12:15):

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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 16 2021 at 14:20):

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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip Eric Wieser (Mar 16 2021 at 14:26):

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

view this post on Zulip 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...

view this post on Zulip 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) }

view this post on Zulip 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 := 

view this post on Zulip 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}

view this post on Zulip 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