All even integers form an integral domain

Stream: new members

[Lars Ericson]

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 _

[Kevin Buzzard]

Your first sorry is false

[Lars Ericson]

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?

[Kevin Buzzard]

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

[Lars Ericson]

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

[Eric Wieser]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

it shows that z = 1 works

[Eric Wieser]

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

[Lars Ericson]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Eric Wieser]

(deleted)

[Lars Ericson]

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.

[Eric Wieser]

What error does the code above give?

[Thomas Browning]

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

[Thomas Browning]

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

[Eric Wieser]

simp at h2 is likely to help

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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))

[Eric Wieser]

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

[Thomas Browning]

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

[Thomas Browning]

golfed:

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

[Lars Ericson]

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