nonzero_ring?

Stream: general

[Kenny Lau]

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

[Johan Commelin]

Probably not

[Kenny Lau]

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 α

[Kenny Lau]

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

[Kenny Lau]

#2595 created nonzero_semiring but not nonzero_ring

[Kenny Lau]

#2839

[Chris Hughes]

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

[Chris Hughes]

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

[Kenny Lau]

no, I want to refactor linear_algebra.basic

[Kenny Lau]

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

[Johan Commelin]

Shouldn't zero_ne_one_class be a prop?

[Johan Commelin]

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

[Mario Carneiro]

zero_ne_one_class is one of the things we need to delete

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

We want a non_subsingleton class :-)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Johan's class should be an instance of zero_ne_zero_class

[Reid Barton]

that's the to_additive of zero_ne_one_class right?

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

I think your idea is a good one

[Mario Carneiro]

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

[Johan Commelin]

@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]?

[Johan Commelin]

Then we can remove all the nonzero_* classes completely

[Mario Carneiro]

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

[Kenny Lau]

so what should we do?

[Mario Carneiro]

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

[Kenny Lau]

for semiring?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

do we have monoid_with_zero?

[Johan Commelin]

Yes we do

[Mario Carneiro]

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

[Johan Commelin]

But a monoid_with_zero is always nonzero

[Johan Commelin]

So I vote for your first option

[Mario Carneiro]

say what?

[Mario Carneiro]

that's definitely the wrong choice

[Johan Commelin]

Well, it worked for my one application...

[Mario Carneiro]

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

[Mario Carneiro]

In particular I would like semirings to be monoid_with_zero

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

That's why I included that assumption.

[Johan Commelin]

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

[Mario Carneiro]

luckily we now have a way to say this :)

[Johan Commelin]

s/now/almost/

[Johan Commelin]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

we haven't yet decided how much further it goes

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Johan Commelin]

Every sentence a verb

[Johan Commelin]

In other words: what the point?

[Kenny Lau]

I have started this refactor on the nonzero branch

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

The commit message?

[Bryan Gin-ge Chen]

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

[Kenny Lau]

along with the title?

[Johan Commelin]

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.

[Kenny Lau]

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

[Kenny Lau]

i.e. whether #2847 is correct

[Johan Commelin]

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

[Johan Commelin]

Kenny Lau said:

i.e. whether #2847 is correct

Yup, looks fine to me

[Kenny Lau]

@[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)

[Kenny Lau]

can we make this a Prop?

[Kenny Lau]

(by moving has_mul and has_zero before extends)

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Mario Carneiro]

no_zero_divisors looks about as useful as zero_ne_one_class and distrib

[Johan Commelin]

Unbundling FTW!

[Mario Carneiro]

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

[Johan Commelin]

But group_with_zero!

[Mario Carneiro]

aha, is that a thing?

[Johan Commelin]

Never heard of them before

[Mario Carneiro]

pre-domain

[Johan Commelin]

quasi-pseudo-demi-domain

[Mario Carneiro]

splitting semimonoid

[Mario Carneiro]

gotta keep them guessing

[Kenny Lau]

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)

• [nonzero_semiring α] becomes [semiring α] [nonzero α]
• [nonzero_comm_semiring α] becomes [comm_semiring α] [nonzero α]
• [nonzero_comm_ring α] becomes [comm_ring α] [nonzero α]
• no_zero_divisors is now a Prop
• units.ne_zero (originally for domain) merges into units.coe_ne_zero (originally for nonzero_comm_semiring)
  https://github.com/leanprover-community/mathlib/commit/f95e8090d8a02dc89c451adfa8ca10df94a56bd8

[Johan Commelin]

Thanks @Kenny Lau