The type of even integers

Stream: new members

[Lars Ericson]

I am working on an exercise "are all even integers an integral domain". In Lean, I think this means I need to create the type of even integers as opposed to creating the set of even integers, because my sense so far is that sets can't be used in place of types, more or less. So I want to do this to set the problem up, but I am worried that it is not correct:

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

instance : integral_domain ℕ_even := sorry

I will need to make more of these somewhat ad hoc set-types which don't necessarily have any structure, for example "all rational numbers whose denominators are a power of 2".

[Yury G. Kudryashov]

You can use either {x : ℕ | ∃ y, x = 2 * y} or {x : ℕ // ∃ y, x = 2 * y}. In the former case, it is a set ℕ but it has an automatic coercion to Type. In the latter case, it is already a Type.

[Mario Carneiro]

you can also use {n | even n} by the way

[Yury G. Kudryashov]

If you want some instances to be deduced automatically (e.g., add_comm_monoid), then you might want to use docs#add_submonoid.closure like in add_submonoid.closure {2}

[Mario Carneiro]

the easiest way to get the full result by abstract nonsense is to express it as the span of {2}

[Mario Carneiro]

we should have the theorem that says that you are in the span of a singleton iff you divide the element

[Lars Ericson]

Thanks I will follow your suggestions. This is the exercise. Some will be integral domains and some won't. The ones that are will fit into the "instance" pattern. For the ones that aren't I guess I have to show an example where an integral domain axiom is violated:
Screenshot-from-2020-12-23-20-44-18.png

[Yury G. Kudryashov]

Do you mean docs#add_submonoid.closure or docs#subalgebra.span?

[Mario Carneiro]

certainly (d) and (e) are best expressed as spans

[Yury G. Kudryashov]

docs#integral_domain says that you need 1

[Mario Carneiro]

you could use an add_submonoid.closure but we're after a ring structure here

[Yury G. Kudryashov]

docs#subalgebra.span pulls in at least all integers

[Mario Carneiro]

Well in those cases I suppose the theorem is false so it doesn't matter

[Mario Carneiro]

if you want to prove it's not an integral domain the proof strategy is different

[Yury G. Kudryashov]

First, you need to define a predicate is_integral_subdomain on a set R provided [ring R]

[Yury G. Kudryashov]

It should say that you have a subring + the natural ring structure on the subtype defines an integral domain.

[Yury G. Kudryashov]

Otherwise you can't formalize arguments like "this set does not contain 1, so it's not an integral domain".

[Mario Carneiro]

You don't need the same 1

[Mario Carneiro]

you can still reason that the set does not contain any idempotent element and hence can't have a 1-alike

[Mario Carneiro]

do we have a notion of subring that doesn't require that 1 come along? I guess that's a subrng

[Yury G. Kudryashov]

Yes, the problem is ill-formulated. Each of those sets is an integral domain (w.r.t. some *, +, 0, and 1) because there exist a countable integral domain. The problem doesn't say what operations/constants must agree with those in real

[Yury G. Kudryashov]

AFAIK, subrng is not in mathlib

[Mario Carneiro]

it might be nice to have something like that even if we don't have non-unital rings, because I think they come up in banach spaces

[Mario Carneiro]

you can have two rings which share the same operations but are not in a subring relation because the unit of the subobject is different