Zulip Chat Archive

Stream: new members

Topic: All even integers form an integral domain


view this post on Zulip Lars Ericson (Dec 25 2020 at 02:36):

Am I setting this up right?

import algebra.algebra.subalgebra

def ℤ_even := {x :  |  y, x = 2 * y}

instance : is_submonoid ℤ_even := {
  one_mem := sorry,
  mul_mem := sorry,
}

instance : is_add_submonoid ℤ_even := {
  add_mem := sorry,
  zero_mem := sorry,
}

instance : is_add_subgroup ℤ_even := {
  neg_mem := sorry,
}

instance : is_subring ℤ_even := {}

instance : integral_domain ℤ_even := @subring.domain  _ ℤ_even _

view this post on Zulip Kevin Buzzard (Dec 25 2020 at 02:39):

Your first sorry is false

view this post on Zulip Lars Ericson (Dec 25 2020 at 06:49):

Thank you @Kevin Buzzard . It's false in a literal sense that there is no element labelled "1" in the set:

(one_mem : (1:M)  s)

On the other hand, I know we have 0 because 2 divides 0. I feel like I should have to prove that there is no unit in ℤ_even by looking at what it means to be a unit. The unit axioms are

one_mul :  (a : α), 1 * a = a
mul_one :  (a : α), a * 1 = a

I feel like I should be proving this theorem:

theorem ℤ_even_is_not_an_integral_monoid :
  ¬( (u  ℤ_even),     (x  ℤ_even),
           u * x = x   x * u = x) :=
  sorry

How do I know that, just because there is no element labelled 1 in ℤ_even, that the above theorem holds?

view this post on Zulip Kevin Buzzard (Dec 25 2020 at 11:33):

That just like like a level in the natural number game to me, the tools introduced there should do it

view this post on Zulip Lars Ericson (Dec 25 2020 at 13:30):

The question is about subsets of the reals. If I knew that 0 and 1 were unique in the reals, and the construction lost 0 or 1, then I guess I don't need to prove the non-existence of 0 or 1 in the subset, just observe that the unique 0 or 1 is gone.

theorem ℝ_0_is_unique :
   (z : ),
    ( (x : ),
      z + x = x  x + z = x   (y : ) x * y = z  x = z  y = z)
     z=0 := sorry

theorem ℝ_1_is_unique :
   (u : ),
     (x : ),
      (u * x = x  x * u = x)  u=1 := sorry

That makes the first 3 easy (no 1, no 0, no 0), and the next 3 require a little more thought:
Screenshot-from-2020-12-25-08-24-15.png

view this post on Zulip Eric Wieser (Dec 25 2020 at 13:54):

As an exercise in working with structures, it might be interesting to prove \not is_submonoid \Z_even, which amounts roughly to what you were already proving, but likely in a more clumsy way.

view this post on Zulip Johan Commelin (Dec 25 2020 at 13:56):

@Lars Ericson your first theorem statement doesn't typecheck.

view this post on Zulip Johan Commelin (Dec 25 2020 at 13:56):

I added a comma, here is a proof:

theorem ℝ_0_is_unique :
   (z : ),
    ( (x : ),
      z + x = x  x + z = x   (y : ), x * y = z  x = z  y = z)
     z=0 :=
begin
  use 1,
  contrapose!,
  simp,
end

view this post on Zulip Johan Commelin (Dec 25 2020 at 13:57):

it shows that z = 1 works

view this post on Zulip Eric Wieser (Dec 25 2020 at 14:01):

That basically constitutes a "proof" that the theorem statement isn't what was intended, right?

view this post on Zulip Lars Ericson (Dec 25 2020 at 16:51):

I think I fixed these:

theorem ℝ_1_is_unique :
   (u : ), ( (x : ), u * x = x  x * u = x)  u=1 :=
begin
  intro h1,
  intro h2,
  sorry,
end

theorem ℝ_0_is_unique :
   (z : ),
    ( (x : ),
      z + x = x 
      x + z = x 
      ( (y : ), x * y = z  (x = z  y = z)))
     z=0 :=
begin
  intro h1,
  intro h2,
  sorry,
end

For the structural theorem, I don't know how to prove a structure:

import algebra.algebra.subalgebra
import data.real.basic

def ℤ_even := {x :  |  y, x = 2 * y}

theorem ℤ_even_is_not_a_submonoid: ¬ is_submonoid ℤ_even :=
begin
  intro h,
  sorry,
end

because is_submonoid is defined as

@[to_additive]
class is_submonoid (s : set M) : Prop :=
(one_mem : (1:M)  s)
(mul_mem {a b} : a  s  b  s  a * b  s)

It says it's a Prop, but how do you prove it or disprove it? I know it as a record of two proofs. I don't know it as a proposition, and I don't know the syntax or pattern to disprove it as a proposition. That is, what is the negation of a record of two proofs?

I also have:

theorem ℤ_even_is_not_an_integral_domain_because_missing_1 :
  ¬( (u  ℤ_even),
     (x  ℤ_even),
    u * x = x 
    x * u = x) :=
begin
  intro h1,
  sorry,
end

view this post on Zulip Reid Barton (Dec 25 2020 at 16:55):

You know how to prove (or use) P ∧ Q, right? well, it is a structure too: docs#and

view this post on Zulip Mario Carneiro (Dec 25 2020 at 16:58):

you can disprove a structure by disproving any of its fields. Think of it this way: if it was a submonoid (intro h), then h.one_mem asserts that 1 \in Z_even, but that is false because [reasons], thus contradiction. So it's not a submonoid

view this post on Zulip Eric Wieser (Dec 25 2020 at 17:06):

(deleted)

view this post on Zulip Lars Ericson (Dec 25 2020 at 18:30):

I think I understand:

import tactic

def yadda :  := 1

class is_golem (s : ) : Prop :=
(three_mem : s=(3:))

#reduce yadda=3 -- 1 = 3

theorem yadda_not_golem : ¬ (is_golem yadda) :=
begin
  intro h1,
  have h2 := h1.three_mem,
  exact h2,
end

So if I complete the proof by disproving any of the component propositions of the structure, which I can extract with ., then I have disproved the structure.

I'm a little stuck in the toy example because exact h2 won't finish the proof even though h2 #reduces to 1=3. 1 and 3 are declared to be nat. Not to sound really dumb, but is there an axiom in nat which says that a=b is a false proposition if a and b are different constant integers? There's just a bit of mechanics here that is eluding me.

view this post on Zulip Eric Wieser (Dec 25 2020 at 18:32):

What error does the code above give?

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:32):

the problem is that "1=3" is not equal to "false"

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:32):

It might imply false, but it's not definitionally equal

view this post on Zulip Eric Wieser (Dec 25 2020 at 18:33):

simp at h2 is likely to help

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:34):

it doesn't, but h2 is definitionally equal to "1 = 3"

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:34):

intro h1,
have h2 := h1.three_mem,
change 1 = 3 at h2,

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:38):

You need to prove that 1 ≠ 3. It's not trivial since 1 = nat.succ 0 and 3 = nat.succ (nat.succ (nat.succ 0))

view this post on Zulip Eric Wieser (Dec 25 2020 at 18:41):

It doesn't help? I'd expect docs#nat.succ_inj whatever the lemma is actually called to kick in, leading to zero = succ x, which is (almost?) false by definition

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:45):

Here's a drawn-out proof:

theorem yadda_not_golem : ¬ (is_golem yadda) :=
begin
  intro h1,
  have h2 : 1 = 3 := h1.three_mem,
  have h3 : 0 = 2 := nat.succ.inj h2,
  have h4 : 2  0 := nat.succ_ne_zero 1,
  exact h4 h3.symm,
end

view this post on Zulip Thomas Browning (Dec 25 2020 at 18:46):

golfed:

theorem yadda_not_golem : ¬ (is_golem yadda) :=
λ h1, nat.succ_ne_zero 1 (nat.succ.inj h1.three_mem).symm

view this post on Zulip Lars Ericson (Dec 25 2020 at 18:49):

Thank you all for helping me sort this out. I now have a clear idea of how to disprove structures.


Last updated: May 11 2021 at 21:10 UTC