local ring refactor

Stream: maths

[Kevin Buzzard]

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]

I think we want is_local_ring2.

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

is_local_ring, I would say.

[Kevin Buzzard]

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

[Johan Commelin]

I'm also fine with dropping all the is_ prefixes

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

[nonzero \a]

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

The proof might even be mk

[Johan Commelin]

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

[Kevin Buzzard]

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]

Whut is the diff?

[Kevin Buzzard]

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

[Johan Commelin]

It shouldn't