group with zero

Stream: general

[Johan Commelin]

For the perfectoid project we need gadgets of the form $\Gamma \cup \{0\}$, and we formalised this using a type class group_with_zero. Examples are (i) fields and division rings, (ii) nnreal, (iii) with_zero G for any group G.

It would be very helpful if we could inject this structure below field in the algebraic hierarchy. What is the best way to do this? Should I make a PR to core lean? Can this be done without touching core? Should fields be moved out of core to mathlib?

[Mario Carneiro]

Would it suffice to have a typeclass instance?

[Mario Carneiro]

instance [field F] : group_with_zero F := ...

[Mario Carneiro]

(also, I think this should assume division_ring instead, no? field would give you a comm_group_with_zero)

[Johan Commelin]

Yes, division_ring is better.

[Mario Carneiro]

what are the axioms of group_with_zero?

[Johan Commelin]

class group_with_zero (α : Type*)
  extends monoid α, has_inv α, zero_ne_one_class α, mul_zero_class α :=
[has_decidable_eq : decidable_eq α]
(inv_zero : (0 : α)⁻¹ = 0)
(mul_inv_cancel : ∀ a:α, a ≠ 0 → a * a⁻¹ = 1)

[Johan Commelin]

The decidable_eq is an artifact

[Mario Carneiro]

I forget where we ended up regarding decidable_eq for division_ring

[Mario Carneiro]

I think we just use classical logic, in which case it would be consistent to do the same here

[Johan Commelin]

Yes, this is old code

[Johan Commelin]

@Mario Carneiro The reason that it would be really nice to inject it below division_ring is that lemmas like inv_zero could have a nice name and work for both of the cases. Currently we need to use group_with_zero.inv_zero because the assumptions on inv_zero are "too strong".

[Mario Carneiro]

meh, that's already done in core in a few places

[Johan Commelin]

Idem dito for

@[simp] lemma mul_inv_cancel' (a : G) (h : a ≠ 0) : a * a⁻¹ = 1 :=
group_with_zero.mul_inv_cancel a h

@[simp] lemma mul_inv_cancel_assoc_left (a b : G) (h : b ≠ 0) :
  (a * b) * b⁻¹ = a :=
calc (a * b) * b⁻¹ = a * (b * b⁻¹) : mul_assoc _ _ _
               ... = a             : by simp [h]

@[simp] lemma mul_inv_cancel_assoc_right (a b : G) (h : a ≠ 0) :
  a * (a⁻¹ * b) = b :=
calc a * (a⁻¹ * b) = (a * a⁻¹) * b : (mul_assoc _ _ _).symm
               ... = b             : by simp [h]

lemma inv_ne_zero' (a : G) (h : a ≠ 0) : a⁻¹ ≠ 0 :=
assume a_eq_0, by simpa [a_eq_0] using mul_inv_cancel' a h

@[simp] lemma inv_mul_cancel' (a : G) (h : a ≠ 0) : a⁻¹ * a = 1 :=
calc a⁻¹ * a = (a⁻¹ * a) * a⁻¹ * a⁻¹⁻¹ : by simp [inv_ne_zero' _ h]
         ... = a⁻¹ * a⁻¹⁻¹             : by simp [h]
         ... = 1                       : by simp [inv_ne_zero' _ h]

@[simp] lemma inv_mul_cancel_assoc_left (a b : G) (h : b ≠ 0) :
  (a * b⁻¹) * b = a :=
calc (a * b⁻¹) * b = a * (b⁻¹ * b) : mul_assoc _ _ _
               ... = a             : by simp [h]

@[simp] lemma inv_mul_cancel_assoc_right (a b : G) (h : a ≠ 0) :
  a⁻¹ * (a * b) = b :=
calc a⁻¹ * (a * b) = (a⁻¹ * a) * b : (mul_assoc _ _ _).symm
               ... = b             : by simp [h]

[Mario Carneiro]

for example most of the division_ring lemmas have namespace division_ring because they conflict with group lemmas

[Johan Commelin]

Is there a reason why field and division_ring should stay in core?

[Johan Commelin]

Mario Carneiro said:

for example most of the division_ring lemmas have namespace division_ring because they conflict with group lemmas

Right, and now we'll have a third conflict. Why not reduce them?

[Johan Commelin]

mk0 will also be duplicated.

[Johan Commelin]

Although that one is in mathlib. So we could deduplicate, I guess.

[Kevin Buzzard]

Johan Commelin said:

Mario Carneiro said:

for example most of the division_ring lemmas have namespace division_ring because they conflict with group lemmas

Right, and now we'll have a third conflict. Why not reduce them?

I don't think there will be a third conflict. For lemmas about division there are two kinds -- those that work under no assumptions about zero-ness (perhaps because they are theorems about monoids or groups, which don't have a zero) and those which have explicit assumptions that something has to be non-zero. The group ones v the field ones, basically.

In fact can you just load all the group_with_zero lemmas into monoid but just ask for the typeclass with_zero on your monoid, and also with_inv if you want it to be a group with 0. How many of them work with that set-up?

[Johan Commelin]

I meant a third naming conflict.

[Johan Commelin]

@Mario Carneiro We will get two definitions of has_div on division rings...

[Mario Carneiro]

that are defeq?

[Kevin Buzzard]

You can't just do some old structure command magic?

[Johan Commelin]

The fields of the has_div structure are defeq

[Johan Commelin]

But that's not good enough, right?

[Johan Commelin]

What is the reason that we try to keep fields in core?

[Johan Commelin]

I understand that nat has to be in core. And hence add_monoid must be in core. But everything starting from rings and beyond?? Could go in mathlib, I think.

[Yury G. Kudryashov]

nat is a linear_ordered_semiring. Not sure if core needs to know about this.

[Bryan Gin-ge Chen]

My impression from this thread is that it's not a big deal to move stuff out of core now and indeed might be a good idea given that Lean 4 core will have much less math. If there's some consensus on what should be done, I'd be happy to help out too.

[Kevin Buzzard]

ring is to monoid as division_ring is to group_with_zero as comm_ring is to comm_monoid as field is to comm_group_with_zero. This makes it sound like all of them are fundamental. Johan has just basically discovered a fundamental structure which is often ignored by mathematicians but which is helpful for formalisation.

[Kevin Buzzard]

@Cyril Cohen have you ever heard of a group with 0? Could you just drop them into Coq's algebra heirarchy without any difficulty?

[Mario Carneiro]

There isn't any problem adding a new element in the middle of the hierarchy later, you just add a couple instances and that's it

[Mario Carneiro]

The main reason you might not want to do this is because some theorems will generalize and there will be duplication there

[Johan Commelin]

@Mario Carneiro So you say it's not a problem that there are two paths to has_div?

[Mario Carneiro]

not if they are defeq

[Johan Commelin]

def div {G : Type*} [group_with_zero G] (g h : G) := g * h⁻¹

/-- The division operation on a group with zero element. -/
instance group_with_zero.has_div {G : Type*} [group_with_zero G] :
  has_div G := ⟨div⟩

[Johan Commelin]

And exactly the same definition exists for division rings in core.

[Mario Carneiro]

What's the definition in core?

[Johan Commelin]

Also, the "some theorems" turn out to be several hundreds lines of duplication...

[Mario Carneiro]

I think the definition in core could be generalized to a has_mul has_inv

[Mario Carneiro]

well, that's expensive...

[Johan Commelin]

What do you think of taking all of it out of core and putting it in mathlib?

[Mario Carneiro]

It is used by tactic.norm_num

[Mario Carneiro]

and possibly some bits of algebraic normalizer that no one has touched in years

[Johan Commelin]

What? division_rings are used in core?

[Johan Commelin]

But can't we move the stuff that uses it to mathlib as well?

[Johan Commelin]

I can't imagine that there is C++ code that depends on division_ring

[Mario Carneiro]

there is

[Johan Commelin]

Oooh, wow

[Mario Carneiro]

There are examples of using norm_num to do numeric simplification in fields

[Mario Carneiro]

this bit of C++ uses this theorem about fields

[Johan Commelin]

#2240

[Bryan Gin-ge Chen]

Monoids with zero appear in some approaches to "the field with one element" (see 2.1.1 on page 12 of "F_1 for everyone"). (I found this stuff via a paper by Baker and Lorscheid about the moduli spaces of matroids.)

[Patrick Massot]

By the way, what happened to your matroid formalization? Was it ever PR'ed to mathlib?

[Bryan Gin-ge Chen]

It's still pending some big refactor. I'm still not happy with the way I deal with submatroids.

[Johan Commelin]

@Bryan Gin-ge Chen In group_with_zero I require that 0 ≠ 1. Should that also be done for monoid_with_zero?

[Johan Commelin]

It seems that the page you linked to doesn't want that requirement.

[Johan Commelin]

But it would be satisfied by F_1

[Bryan Gin-ge Chen]

Should that also be done for monoid_with_zero?

Hmm, I'm not sure. I think ease of doing things in Lean would be most important here, and I don't have enough experience with algebra to say.

[Bryan Gin-ge Chen]

Chapter 3 of Lorscheid's lecture notes "Blueprints and tropical scheme theory" does algebra over monoids with zero, including prime ideals and localization.

[Johan Commelin]

@Bryan Gin-ge Chen Thanks. I can try to refactor to include monoid_with_zero in the hierarchy.

[Kevin Buzzard]

Then you can start on diistrib_with_zero

[Kevin Buzzard]

Asking if 0 ne 1 feels a bit like asking if the zero ring is a field

[Kevin Buzzard]

But my instincts are not helping. I guess the idea is that we should just concentrate on the objects which are of use to us, and for group_with_zero we definitely want 0 ne 1 because I don't want to the zero ring to have any valuations

[Kevin Buzzard]

For monoid_with_zero I don't think I care -- the issue is simply what people need. I guess if you don't assume it then you can prove that every ring is a monoid with 0

[Kevin Buzzard]

So this seems natural.

[Johan Commelin]

So... I changed some things, and now I get this build error

mathlib/src/data/complex/basic.lean:28:4: error: definition 'of_real' is noncomputable, it depends on 'real.division_ring'

[Johan Commelin]

But as far as I know, I didn't change the computability of anything

[Johan Commelin]

How do I debug this issue?

[Gabriel Ebner]

I think it pulls in the wrong type class instance somewhere. I'd add noncomputable to of_real and then stare at the term with pp.all enabled. Is this in the PR that you've just closed?

[Johan Commelin]

Let me try.

[Johan Commelin]

noncomputable def complex.of_real : real → complex :=
λ (r : real),
  {re := r,
   im := @has_zero.zero.{0} real
           (@no_zero_divisors.to_has_zero.{0} real
              (@gwz.no_zero_divisors.{0} real (@division_ring.to_group_with_zero.{0} real real.division_ring)))}

[Johan Commelin]

So, it's now using this group_with_zero stuff

[Johan Commelin]

Hmm, I guess I should lower some instance priorities?

[Gabriel Ebner]

We've had similar problems when we removed the decidable_eq parent from fields.

[Gabriel Ebner]

The problem there was that every field with decidable equality is a Euclidean ring (and every Euclidean ring is a ring, etc.). But if you use this instance with open_locale classical, then you get instances using classical decidability. And suddenly multiplication is noncomputable.

[Gabriel Ebner]

I've put low priority on that instance and it seems to work.

[Gabriel Ebner]

Ok, this can be a bit subtle. I lowered the priority of euclidean_domain.to_nonzero_comm_ring instead: https://github.com/leanprover-community/mathlib/blob/e719f8ee3b0de0f02e3e32ff2a196f9703b63083/src/algebra/euclidean_domain.lean#L14

[Johan Commelin]

Ok, I've lowered some priorities. Let's see what happens

[Gabriel Ebner]

Do you know which one of the instances is noncomputable? They all seem fine to me.

[Johan Commelin]

I have no clue

[Johan Commelin]

But lowering the priorities helped

[Gabriel Ebner]

That said, both no_zero_divisors.to_has_zero and gwz.no_zero_divisors should have a lower priority. I believe #lint should complain.

[Johan Commelin]

@Bryan Gin-ge Chen I've factored out monoid with zero. But I didn't prove many lemmas for them.

[Bryan Gin-ge Chen]

OK, thanks! To be quite honest the algebraic hierarchy intimidates me still so I don't know that I'll have any intelligent comments on your code.