Zulip Chat Archive

Stream: new members

Topic: The type of even integers


view this post on Zulip Lars Ericson (Dec 24 2020 at 01:37):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:44):

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.

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:44):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:45):

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}

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:45):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:46):

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

view this post on Zulip Lars Ericson (Dec 24 2020 at 01:47):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:47):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:48):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:48):

docs#integral_domain says that you need 1

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:48):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:49):

docs#subalgebra.span pulls in at least all integers

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:49):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:50):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:50):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:51):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:52):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:52):

You don't need the same 1

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:53):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:55):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:55):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 01:55):

AFAIK, subrng is not in mathlib

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:56):

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

view this post on Zulip Mario Carneiro (Dec 24 2020 at 01:57):

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


Last updated: May 14 2021 at 07:19 UTC