## Stream: new members

### Topic: All even integers form an integral domain

#### 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 := {
zero_mem := sorry,
}

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

instance : is_subring ℤ_even := {}

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


#### 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?

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

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

#### 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.

#### Johan Commelin (Dec 25 2020 at 13:56):

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

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


#### Johan Commelin (Dec 25 2020 at 13:57):

it shows that z = 1 works

#### Eric Wieser (Dec 25 2020 at 14:01):

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

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


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

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

(deleted)

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

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 (Dec 25 2020 at 18:32):

What error does the code above give?

#### Thomas Browning (Dec 25 2020 at 18:32):

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

#### Thomas Browning (Dec 25 2020 at 18:32):

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

#### Eric Wieser (Dec 25 2020 at 18:33):

simp at h2 is likely to help

#### Thomas Browning (Dec 25 2020 at 18:34):

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

#### Thomas Browning (Dec 25 2020 at 18:34):

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


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

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

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


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


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