Stream: maths

Topic: local ring refactor

Kevin Buzzard (Jun 25 2020 at 12:00):

My understanding is that we're now coming round to the idea that there should be a predicate either called local_ring or is_local_ring on commutative rings, and that this predicate should also be a class. Currently in mathlib we have

class local_ring (α : Type u) extends comm_ring α, nonzero α :=
(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))


(a class but not a Prop) and

def is_local_ring (α : Type u) [comm_ring α] : Prop :=
((0:α) ≠ 1) ∧ ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a))


(a Prop but not a class). My understanding of the type class system is poor. Note that we also have nonzero R:

@[protect_proj] class nonzero (α : Type u) [has_zero α] [has_one α] : Prop :=
(zero_ne_one : 0 ≠ (1:α))


which is a class and a Prop. I realise now that I am not sure about the relationship between nonzero and our dream class Prop is_local_ring predicate. Which of these do we want:

class is_local_ring1 (α : Type u) [comm_ring α] [nonzero α] : Prop :=
(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))

class is_local_ring2 (α : Type u) [comm_ring α] extends nonzero α : Prop :=
(is_local : ∀ (a : α), (is_unit a) ∨ (is_unit (1 - a)))


Or do we want something else? And if I introduce this prop class, which, if either, of the current local_ring and is_local_ring should I remove? I'm hoping that this is not too big a refactor; local_ring(including is_local_ring) only gets 61 hits in mathlib.

Sebastien Gouezel (Jun 25 2020 at 12:03):

I think we want is_local_ring2.

Sebastien Gouezel (Jun 25 2020 at 12:06):

And we want to remove both local_ring and the current is_local_ring.

Kevin Buzzard (Jun 25 2020 at 12:10):

Thanks! Any comments on the name of the new class predicate? :-)

Sebastien Gouezel (Jun 25 2020 at 12:12):

is_local_ring, I would say.

Kevin Buzzard (Jun 25 2020 at 12:13):

And the name of the namespace for all the local ring lemmas?

Johan Commelin (Jun 25 2020 at 12:14):

I'm also fine with dropping all the is_ prefixes

Kevin Buzzard (Jun 25 2020 at 12:16):

This is a decision which needs to be made. It's going to come up again and again. I'm doing is_DVR next, then is_Dedekind_domain, then...

Sebastien Gouezel (Jun 25 2020 at 12:16):

Yes, local_ring is fine. The only ambiguity (which is not present with the is_) is that you don't know if it takes ring as a parameter or if it extends it, but I agree it is uselessly (is this a word?) verbose. For topological spaces, we have dropped the is_ on space predicates.

Sebastien Gouezel (Jun 25 2020 at 12:17):

We have complete_space or proper_space, which take toplogical_space as a parameter. So, I vote for dropping the is_.

Kevin Buzzard (Jun 25 2020 at 12:18):

Whether or not it's a word, it's clear what you mean. Another advantage of dropping the is is that we then can work in the local_ring namespace and not have to open is_local_ring or copy the definition of is_local_ring.is_local into a local_ring namespace

Johan Commelin (Jun 25 2020 at 12:19):

The name of the class and the name of the namespace should be the same, I think

Kevin Buzzard (Jun 25 2020 at 14:11):

The below result should not be a def (any more). But I'm assuming there's no point making it an instance? The target is a typeclass but I can't imagine type class inference ever being able to find h and hnze. Am I thinking about this in the correct way?

lemma local_of_is_local_ring [comm_ring α] (hnze : (0:α) ≠ 1)
(h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α := ...


Patrick Massot (Jun 25 2020 at 14:13):

In this form it won't. But you could use the fact typeclass.

Johan Commelin (Jun 25 2020 at 14:28):

[nonzero \a]

Kevin Buzzard (Jun 25 2020 at 14:28):

I cannot see the point of this lemma at all and it is not used anywhere else.

Johan Commelin (Jun 25 2020 at 14:28):

@Kevin Buzzard nonzero is one of the classes that went through the "make it a predicate refactor" already

Johan Commelin (Jun 25 2020 at 14:29):

It can't be an instance, because of h, but hnze is fine.

Kevin Buzzard (Jun 25 2020 at 14:29):

This just literally says "if I can prove all the fields of this structure, I can make an instance of the structure". When would one want to use this? The proof is {nonzero := hnze, is_local := h}

Kevin Buzzard (Jun 25 2020 at 14:30):

The proof might even be mk

Johan Commelin (Jun 25 2020 at 14:32):

Well, in that case, you might as well remove it, I guess

Kevin Buzzard (Jun 25 2020 at 14:34):

Sorry, I have conflated two definitions, adding to the confusion. The one I posted seems completely pointless. There is also

lemma local_of_nonunits_ideal [comm_ring α] (hnze : (0:α) ≠ 1)
(h : ∀ x y ∈ nonunits α, x + y ∈ nonunits α) : local_ring α :=


which is a cooler result and is the one we should be talking about. Here I could change hnze to nonzero \alpha but leave it as a lemma.

Johan Commelin (Jun 25 2020 at 14:35):

Whut is the diff?

Kevin Buzzard (Jun 25 2020 at 14:39):

I'm just checking it shouldn't be an instance

Johan Commelin (Jun 25 2020 at 14:39):

It shouldn't

Last updated: May 18 2021 at 06:15 UTC