# Zulip Chat Archive

## 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 := {
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 (Dec 25 2020 at 02:39):

Your first sorry is false

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

#### Eric Wieser (Dec 25 2020 at 17:06):

(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
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`

`#reduce`

s 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