Zulip Chat Archive

Stream: general

Topic: nonzero_ring?


view this post on Zulip Kenny Lau (May 27 2020 at 08:51):

We have nonzero_comm_ring and nonzero_comm_semiring and nonzero_semiring but not nonzero_ring. Is this deliberate?

view this post on Zulip Johan Commelin (May 27 2020 at 08:53):

Probably not

view this post on Zulip Kenny Lau (May 27 2020 at 08:57):

https://github.com/leanprover-community/mathlib/blob/2792c93ac5ad99a82945caad1110e6e284fd6ff7/src/algebra/ring.lean#L669-L676

/-- Predicate for semirings in which zero does not equal one. -/
class nonzero_semiring (α : Type*) extends semiring α, zero_ne_one_class α

/-- Predicate for commutative semirings in which zero does not equal one. -/
class nonzero_comm_semiring (α : Type*) extends comm_semiring α, zero_ne_one_class α

/-- Predicate for commutative rings in which zero does not equal one. -/
class nonzero_comm_ring (α : Type*) extends comm_ring α, zero_ne_one_class α

view this post on Zulip Kenny Lau (May 27 2020 at 09:00):

https://github.com/leanprover-community/mathlib/pull/2595/files#diff-997c56fe87e1352880681d783e610a7f

view this post on Zulip Kenny Lau (May 27 2020 at 09:00):

#2595 created nonzero_semiring but not nonzero_ring

view this post on Zulip Kenny Lau (May 27 2020 at 09:17):

#2839

view this post on Zulip Chris Hughes (May 27 2020 at 10:43):

The point of the commutative versions was to deal with polynomials. Nobody's found a point of the non commutative versions yet.

view this post on Zulip Chris Hughes (May 27 2020 at 10:44):

Is this related to codewars? I wanted this class for a Kata.

view this post on Zulip Kenny Lau (May 27 2020 at 10:47):

no, I want to refactor linear_algebra.basic

view this post on Zulip Kenny Lau (May 27 2020 at 10:47):

there are a lot of theorems with rings and 0 ne 1 assumption

view this post on Zulip Johan Commelin (May 27 2020 at 10:48):

Shouldn't zero_ne_one_class be a prop?

view this post on Zulip Johan Commelin (May 27 2020 at 10:49):

We could have a class [nonzero R], and then we can get rid of nonzero_* for all versions of *.

view this post on Zulip Mario Carneiro (May 27 2020 at 10:49):

zero_ne_one_class is one of the things we need to delete

view this post on Zulip Mario Carneiro (May 27 2020 at 10:50):

it makes sense for an algebraic hierarchy that isn't mathlib's

view this post on Zulip Mario Carneiro (May 27 2020 at 10:51):

If you use mixins for making classes, a la the mathcomp hierarchy, it makes sense

view this post on Zulip Kevin Buzzard (May 27 2020 at 10:54):

We want a non_subsingleton class :-)

view this post on Zulip Mario Carneiro (May 27 2020 at 10:55):

are those always the same thing in all classes where zero_ne_one makes sense?

view this post on Zulip Mario Carneiro (May 27 2020 at 10:56):

I guess it's true as long as 0 * x = 0 and 1 * x = x

view this post on Zulip Mario Carneiro (May 27 2020 at 10:57):

which seem like pretty safe bets in an algebraic class with a thing called 0

view this post on Zulip Johan Commelin (May 27 2020 at 10:57):

Is it true in with_zero \a if \a is an ordered_add_comm_monoid?

view this post on Zulip Johan Commelin (May 27 2020 at 10:57):

To bad... we don't have a 1 there :sad:

view this post on Zulip Kevin Buzzard (May 27 2020 at 10:58):

so 1 is definitely not 0, because we have two of those!

view this post on Zulip Mario Carneiro (May 27 2020 at 10:58):

It's not true in a add_monoid has_one, which is the context where nat.cast is stated

view this post on Zulip Kevin Buzzard (May 27 2020 at 10:58):

Johan's class should be an instance of zero_ne_zero_class

view this post on Zulip Reid Barton (May 27 2020 at 11:00):

that's the to_additive of zero_ne_one_class right?

view this post on Zulip Mario Carneiro (May 27 2020 at 11:01):

I feel like it should be possible to to_additive a semiring and get a tropical ring

view this post on Zulip Johan Commelin (May 27 2020 at 11:02):

Back on topic: what do we do with nonzero_*?

view this post on Zulip Johan Commelin (May 27 2020 at 11:02):

I wouldn't want to waste Kenny's refactor energy

view this post on Zulip Mario Carneiro (May 27 2020 at 11:02):

I think your idea is a good one

view this post on Zulip Mario Carneiro (May 27 2020 at 11:04):

although I think that we should still have things like domain and field containing nonzero as part of the structure

view this post on Zulip Johan Commelin (May 27 2020 at 20:46):

@Mario Carneiro what do you think of just using [fact (0:R) ≠ 1] whenever we need it, and adding an instance for this fact for [domain R]?

view this post on Zulip Johan Commelin (May 27 2020 at 20:46):

Then we can remove all the nonzero_* classes completely

view this post on Zulip Mario Carneiro (May 27 2020 at 20:56):

You can do this kind of encoding for anything. The big downside is that all facts end up in a single class, which means that typeclass inference is going to have to sort through all facts in all contexts when trying to prove this. So no, I think we should try to not have any instances of fact other than local instances and hypotheses

view this post on Zulip Kenny Lau (May 27 2020 at 21:11):

so what should we do?

view this post on Zulip Mario Carneiro (May 27 2020 at 21:11):

have a nonzero R class, which was Johan's original suggestion

view this post on Zulip Kenny Lau (May 27 2020 at 21:12):

for semiring?

view this post on Zulip Mario Carneiro (May 27 2020 at 21:13):

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

view this post on Zulip Mario Carneiro (May 27 2020 at 21:13):

it could also be class nonzero (R) [semiring R]

view this post on Zulip Mario Carneiro (May 27 2020 at 21:14):

do we have monoid_with_zero?

view this post on Zulip Johan Commelin (May 27 2020 at 21:14):

Yes we do

view this post on Zulip Mario Carneiro (May 27 2020 at 21:15):

ah, I should get in the habit of using that for stuff with 0 and 1

view this post on Zulip Johan Commelin (May 27 2020 at 21:15):

But a monoid_with_zero is always nonzero

view this post on Zulip Johan Commelin (May 27 2020 at 21:15):

So I vote for your first option

view this post on Zulip Mario Carneiro (May 27 2020 at 21:15):

say what?

view this post on Zulip Mario Carneiro (May 27 2020 at 21:15):

that's definitely the wrong choice

view this post on Zulip Johan Commelin (May 27 2020 at 21:16):

Well, it worked for my one application...

view this post on Zulip Mario Carneiro (May 27 2020 at 21:16):

If monoid_with_zero is to group_with_zero as ring is to division_ring then it shouldn't have nonzero

view this post on Zulip Mario Carneiro (May 27 2020 at 21:17):

In particular I would like semirings to be monoid_with_zero

view this post on Zulip Johan Commelin (May 27 2020 at 21:17):

Yup, but I'm not sure that analogy should hold

view this post on Zulip Johan Commelin (May 27 2020 at 21:17):

Apparently in tropical geometry people study monoid_with_zero Ms and they are all nonzero by assumption.

view this post on Zulip Johan Commelin (May 27 2020 at 21:17):

That's why I included that assumption.

view this post on Zulip Johan Commelin (May 27 2020 at 21:17):

But it's probably a 2-line refactor to drop that assumption from mathlib

view this post on Zulip Mario Carneiro (May 27 2020 at 21:17):

luckily we now have a way to say this :)

view this post on Zulip Johan Commelin (May 27 2020 at 21:18):

s/now/almost/

view this post on Zulip Johan Commelin (May 27 2020 at 21:18):

I need to refill my 'refactor-mathlib' battery. So I would like to take a pass on this one.

view this post on Zulip Mario Carneiro (May 27 2020 at 21:18):

It seems awkward that group_with_zero and semiring currently have no greatest lower bound

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:19):

The mathematical world is still reeling from the introduction of this new group_with_zero concept

view this post on Zulip Johan Commelin (May 27 2020 at 21:19):

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:19):

we haven't yet decided how much further it goes

view this post on Zulip Mario Carneiro (May 27 2020 at 21:20):

Johan Commelin said:

But a complete refactor of the algebraic hierarchy... I wouldn't want to do that without more supporting tools

It's not a complete refactor, just one new class

view this post on Zulip Mario Carneiro (May 27 2020 at 21:20):

some theorems will transfer to the weaker assumption, other stuff won't

view this post on Zulip Mario Carneiro (May 27 2020 at 21:20):

since it's a GLB class there will be no conflicts

view this post on Zulip Kenny Lau (May 28 2020 at 07:32):

Mario Carneiro said:

class nonzero (R) [has_zero R] [has_one R] := (zero_ne_one : 0 != 1)

https://github.com/leanprover-community/mathlib/commit/d1df1780ff89b8c023847b97119411601448f74c
https://github.com/leanprover-community/mathlib/tree/nonzero

view this post on Zulip Johan Commelin (May 28 2020 at 07:34):

Every sentence a verb

view this post on Zulip Johan Commelin (May 28 2020 at 07:35):

In other words: what the point?

view this post on Zulip Kenny Lau (May 28 2020 at 07:35):

I have started this refactor on the nonzero branch

view this post on Zulip Kenny Lau (May 28 2020 at 07:42):

[nonzero_semiring α] becomes [semiring α] [nonzero α]
[nonzero_comm_semiring α] becomes [comm_semiring α] [nonzero α]
[nonzero_comm_ring α] becomes [comm_ring α] [nonzero α]

view this post on Zulip Kenny Lau (May 28 2020 at 07:42):

(is there a place where I can put information like this?)

view this post on Zulip Johan Commelin (May 28 2020 at 07:43):

The commit message?

view this post on Zulip Bryan Gin-ge Chen (May 28 2020 at 07:45):

Note that when you make a PR, the contents of the first post become the commit message of the final squashed and merged commit.

view this post on Zulip Kenny Lau (May 28 2020 at 07:46):

along with the title?

view this post on Zulip Johan Commelin (May 28 2020 at 07:47):

When you create the PR it suggests a title, but it's usually crappy. It might also suggest a message, but you might want to change it.

view this post on Zulip Kenny Lau (May 28 2020 at 07:48):

I'm just asking whether the title also becomes the commit message

view this post on Zulip Kenny Lau (May 28 2020 at 07:48):

i.e. whether #2847 is correct

view this post on Zulip Johan Commelin (May 28 2020 at 07:48):

The title becomes the first line of the message, and will afterwards typically be formatted as a title.

view this post on Zulip Johan Commelin (May 28 2020 at 07:49):

Kenny Lau said:

i.e. whether #2847 is correct

Yup, looks fine to me

view this post on Zulip Kenny Lau (May 28 2020 at 07:50):

@[ancestor has_mul has_zero]
class no_zero_divisors (α : Type u) extends has_mul α, has_zero α :=
(eq_zero_or_eq_zero_of_mul_eq_zero :  a b : α, a * b = 0  a = 0  b = 0)

view this post on Zulip Kenny Lau (May 28 2020 at 07:50):

can we make this a Prop?

view this post on Zulip Kenny Lau (May 28 2020 at 07:50):

(by moving has_mul and has_zero before extends)

view this post on Zulip Kenny Lau (May 28 2020 at 07:50):

class domain (α : Type u) extends ring α, no_zero_divisors α, nonzero α

view this post on Zulip Kenny Lau (May 28 2020 at 07:51):

because the nonzero is problematic in "old_str_cmd true" and the no_zero_divisors is problematic in "false"

view this post on Zulip Johan Commelin (May 28 2020 at 07:51):

Yup, I would like that one to become a prop as well

view this post on Zulip Mario Carneiro (May 28 2020 at 07:51):

no_zero_divisors looks about as useful as zero_ne_one_class and distrib

view this post on Zulip Johan Commelin (May 28 2020 at 07:52):

Unbundling FTW!

view this post on Zulip Mario Carneiro (May 28 2020 at 07:52):

I think it should just be deleted (and merged into domain)

view this post on Zulip Johan Commelin (May 28 2020 at 07:52):

But group_with_zero!

view this post on Zulip Mario Carneiro (May 28 2020 at 07:53):

aha, is that a thing?

view this post on Zulip Johan Commelin (May 28 2020 at 07:53):

Never heard of them before

view this post on Zulip Mario Carneiro (May 28 2020 at 07:53):

pre-domain

view this post on Zulip Johan Commelin (May 28 2020 at 07:54):

quasi-pseudo-demi-domain

view this post on Zulip Mario Carneiro (May 28 2020 at 07:54):

splitting semimonoid

view this post on Zulip Mario Carneiro (May 28 2020 at 07:54):

gotta keep them guessing

view this post on Zulip Kenny Lau (May 30 2020 at 06:55):

rss-bot said:

chore(algebra): displace zero_ne_one_class with nonzero and make no_z…
chore(algebra): displace zero_ne_one_class with nonzero and make no_zero_divisors a Prop (#2847)

view this post on Zulip Johan Commelin (May 30 2020 at 07:12):

Thanks @Kenny Lau


Last updated: May 15 2021 at 00:39 UTC