zero ring

Stream: maths

[Kevin Buzzard]

I'm working with polynomials and the zero ring is constantly a special case. There is a class nonzero_comm_ring extending comm_ring with the proposition that 0 \ne 1, and several of Chris' results on polynomials need this as a hypothesis (for example the fact that degree of X is 1, and every corollary of this). Of course everything is true (and trivial) for the zero ring, but often the proofs need to be separate because of this. Because of the constructor for nonzero_comm_ring I am coming around to the idea to be splitting on (0 : R) = 1 for lemmas which are true in the case R=0 but where the proof in the non-zero case is far from working for the zero ring.

So I now find myself wanting to prove things such as "if R is a ring and 0 = 1 then R is a fintype". I don't really know how to make that an instance, and I am not sure whether it should be an instance. On the other hand if I made a new class zero_ring then in some sense my life would be easier. Having said that, making a class for such a silly edge case seems a bit ridiculous. Should I just stick to proving lemmas rather than making this a class? I am slightly concerned that really I should be working with zero_semiring or something.

Another issue is that if I put 0 = 1 -> fintype R into ring.lean then I have to add an import to ring.lean and I have this vague worry that I don't really know "which comes first" out of rings and fintypes.

[Reid Barton]

"if R is a ring and 0 = 1 then R is a fintype"

Is this a real example, including the fintype part?

[Reid Barton]

Your zero_ring could be "lifted" all the way up to is_singleton, except we don't have it.

[Chris Hughes]

Rings definitely come before fintype. A more useful instance would perhaps be 0 = 1 -> subsingleton R

[Reid Barton]

You can also use subsingleton in this case, yeah

[Kevin Buzzard]

lemma ring.zero_of_zero_eq_one {α} [ring α] (h01 : (0 : α) = 1) (a : α) : a = 0 :=
by rw [←one_mul a,←h01,zero_mul]

noncomputable definition ring.fintype_of_zero_eq_one {α} [ring α] (h01 : (0 : α) = 1) : fintype α := {
  elems := {0},
  complete := λ x, begin
    suffices: x = 0, by simpa,
    exact ring.zero_of_zero_eq_one h01 x,
  end
}

theorem ring.is_noetherian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_noetherian_ring R :=
@ring.is_noetherian_of_fintype R R _ _ $ ring.fintype_of_zero_eq_one h01

[Reid Barton]

Aha I see. I was wondering how you were using the fintype, but this makes sense.

[Kevin Buzzard]

I am trying to prove the Hilbert basis theorem for the zero ring :-)

[Kevin Buzzard]

I've proved that if a module is a fintype then it's Noetherian so I figured I'd use that.

[Reid Barton]

So you could use case analysis on whether R is a subsingleton, and show that if it isn't then $0 \ne 1$.
Then also make an instance that says that if R is a subsingleton then so is R[X].

[Reid Barton]

Or write a lemma ∀ R, subsingleton R ∨ ((0 : R) ≠ 1)

[Kevin Buzzard]

I see. You're suggesting that I use what we currently have in the type class system by using a different class to convey what I'm trying to say, rather than making a new class. Thanks!

[Reid Barton]

Well, I would actually prefer that you make a new class but that it should be called is_singleton :)

[Kevin Buzzard]

Hmm. subsingleton is a Prop. Does this mean that type class inference won't get me from it to fintype?

[Chris Hughes]

Not computably.

[Chris Hughes]

It will for rings though

[Kevin Buzzard]

Proof now looks like

theorem ring.is_noetherian_of_zero_eq_one {R} [ring R] (h01 : (0 : R) = 1) : is_noetherian_ring R :=
by haveI := ring.subsingleton_of_zero_eq_one h01; exact ring.is_noetherian_of_fintype R R

[Patrick Massot]

I read that Kevin fights the zero ring. But what's the point of allowing this ring? Why don't we defined a ring with the assumption that 0 and 1 are different? Is it a trick in order to totalize certain constructions? Or is it needed from a categorical point of view (I guess it's a terminal object)?

[Johan Commelin]

I've never thought this through carefully, but I think it is indeed useful from a categorical point of view.

[Kevin Buzzard]

Funnily enough in my undergraduate ring theory course the lecturer made 0 not= 1 an axiom, and it caused them all sorts of problems. Whenever they formed a quotient ring R / I I would put my hand up and point out that they needed to assume that I was not R (which was not a natural thing to do on many occasions). On the other hand I was only an undergraduate and just assumed that this was an axiom of rings. It was only when I learnt algebraic geometry that I found out that it wasn't. Assuming 0 isn't 1 is a disastrous idea. In a separated scheme, the intersection of two affines is affine -- this sort of thing is used all the time. It would not be true if the empty scheme were not affine.

[Patrick Massot]

The quotient case is one of the examples I had in mind when I wrote "totalizing construction". The same probably happens with localization

[Patrick Massot]

and i̶t̶ Kevin caused them all sorts of problems

[Mario Carneiro]

of course, Kevin's behavior there is exactly what lean would do to you if you tried to formalize it

[Kevin Buzzard]

Where do I find the zero ring? I want to offer it promotion to topological ring. Patrick, did you already do this?

If it was already there, what was the algorithm I should have used to find it?

-- desperation imports
import tactic.linarith

import topology.metric_space.gromov_hausdorff

instance : comm_ring unit := by apply_instance -- fails

[Kevin Buzzard]

I really want "import all of mathlib" here.

[Kevin Buzzard]

instance : comm_ring unit :=
{ add := λ _ _, (),
  add_assoc := by simp,
  zero := (),
  zero_add := λ x, by cases x; refl,
  add_zero := λ x, by cases x; refl,
  neg := λ _, (),
  add_left_neg := λ x, by cases x; refl,
  add_comm := λ a b, by cases a; cases b; refl,
  mul := λ _ _, (),
  mul_assoc := λ a b c, by cases a; cases b; cases c; refl,
  one := (),
  one_mul := λ a, by cases a; refl,
  mul_one := λ a, by cases a; refl,
  left_distrib := λ a b c, by cases a; cases b; cases c; refl,
  right_distrib := λ a b c, by cases a; cases b; cases c; refl,
  mul_comm := λ a b, by cases a; cases b; refl }

[Kevin Buzzard]

I wrote that algorithmically.

[Kevin Buzzard]

I'm about to put a topology on this ring pretty algorithmically as well and then prove it's a topological ring in an equally trivial way. What is the automation that does all this for me?

[Kevin Buzzard]

I thought I remembered it from somewhere. algebra.punit_instances

[Kevin Buzzard]

topological_ring unit missing?

[Kevin Buzzard]

My goal is now

⊢ topological_space.lattice.complete_lattice = tmp_complete_lattice

That's some officially-sanctioned mathlib name is it?

A little earlier:

invalid type ascription, term has type
  @topological_ring unit (@uniform_space.to_topological_space unit unit.uniform_space)
    (@comm_ring.to_ring unit punit.comm_ring)
but is expected to have type
  @topological_ring unit ⊤ (@comm_ring.to_ring unit punit.comm_ring)
state:
U : topological_space.opens empty
⊢ topological_ring unit

[Kevin Buzzard]

got it, i'd made a diamond

[Kevin Buzzard]

valuation := by rintro ⟨⟩, -- thanks @Rob Lewis ;-)

[Mario Carneiro]

I thought the zero ring was added to pi_instances

[Mario Carneiro]

(which should be renamed btw)

[Johan Commelin]

No it's all in the file punit_instances. But topological_ring is probably missing.

[Heather Macbeth]

I would like to use the fact that if a normed ring is stupid (by which I mean that 0 = 1), then all subsets are open. Here is what I have:

import analysis.normed_space.basic
variables {α : Type*}

instance test [semiring α] (h : (0:α) = 1) : unique α :=
{ to_inhabited := {default := 0},
  uniq         := eq_zero_of_zero_eq_one α h}

instance test2 [normed_ring α] (h : (0:α) = 1) : discrete_topology α :=
@subsingleton.discrete_topology α _ (@unique.subsingleton α (test h))

example [normed_ring α] (h : (0:α) = 1) (s : set α) : is_open s :=
@is_open_discrete α _ (test2 h) s

Can this be cleaned up (for example, to avoid all the @s)? What should the instances test and test2 be called, and in what files do they belong? (I was surprised that test did not already exist; is there a reason for this?)

[Alex J. Best]

Did you see docs#subsingleton_of_zero_eq_one , it might cut test out of your proof?

[Heather Macbeth]

Aha, thank you!

[Heather Macbeth]

Is there a reason that there is no unique_of_zero_eq_one?

[Johan Commelin]

For test2, I would replace h with [unique \a]

[Heather Macbeth]

Johan, I am doing a proof by cases on 0 = 1

[Kevin Buzzard]

I want the proof of this to be that if 0=1 then the underlying topological space is isomorphic to punit and hence all sets are open by transfer because it's true for punit by dec_trivial. @Mario Carneiro is that the way to do it?

[Johan Commelin]

@Heather Macbeth I think that test and co cannot be instances, because typeclass search can't figure out 0 = 1.

[Alex J. Best]

Heather Macbeth said:

Is there a reason that there is no unique_of_zero_eq_one?

I don't know, it seems to me there should be.

[Heather Macbeth]

If 0 = 1, I get [unique α] and access to one set of theorems; if 0 ≠ 1, I get [nonzero α] and another set of theorems

[Johan Commelin]

Yup, I agree

[Johan Commelin]

But you can't get unique \a without writing something (as in, tc search won't figure it out for you).

[Johan Commelin]

If you use [fact (0 = 1)] then it can work

[Johan Commelin]

But then... how will you get fact (0 = 1) in you hypotheses?

[Johan Commelin]

It will still require writing a line. So I'm not sure if it's worth it.

[Kevin Buzzard]

haveI right?

[Johan Commelin]

@Heather Macbeth I think test2 shouldn't be necessary.

[Johan Commelin]

Just letI : unique \a := test _ in your proof.

[Johan Commelin]

The rest will be done by tc

[Heather Macbeth]

Sorry, had to step away for a sec

[Heather Macbeth]

To summarize the suggestions of all three of you, I can get the result I need from

example [normed_ring α] (h : (0:α) = 1) (s : set α) : is_open s :=
begin
  letI : subsingleton α := subsingleton_of_zero_eq_one α h,
  exact is_open_discrete s,
end

[Heather Macbeth]

Remaining questions: Is there a way to do letI in term mode? And, must I be a good citizen and add unique_of_zero_eq_one?

[Johan Commelin]

I think we want something like this:

import ring_theory.noetherian

variables (R : Type*) [semiring R]

lemma subsingleton_or_nonzero : subsingleton R ∨ nonzero R :=
begin
  classical,
  by_cases h : (0 : R) = 1,
  { left, exact subsingleton_of_zero_eq_one R h },
  { right, exact ⟨h⟩ }
end

-- use like this
example (r : R) : true :=
begin
  rcases subsingleton_or_nonzero R with _i|_i, resetI,
end

[Johan Commelin]

I'll build another one that uses unique

[Johan Commelin]

def unique_of_zero_eq_one (h : (0:R) = 1) : unique R :=
{ default := 0,
  uniq :=
  begin
    haveI := subsingleton_of_zero_eq_one R h,
    intro r, exact subsingleton.elim r _
  end }

inductive data_xor (X : Sort*) (Y : Sort*)
| left (x : X)  : data_xor
| right (y : Y) : data_xor

noncomputable def unique_or_nonzero : data_xor (unique R) (nonzero R) :=
begin
  classical,
  by_cases h : (0 : R) = 1,
  { exact data_xor.left (unique_of_zero_eq_one R h) },
  { exact data_xor.right (⟨h⟩) }
end

example (r : R) : true :=
begin
  rcases unique_or_nonzero R with _i|_i, resetI,
end

[Heather Macbeth]

Yes, these look great!

[Johan Commelin]

I think this is how you generally want to split cases, and this way it's a one liner.
The resetI is important though! Because it adds the result or rcases to the type class cache.

[Johan Commelin]

@Heather Macbeth Feel free to incorporate this into a PR

[Johan Commelin]

If nobody else does it, I'll do it next week.

[Johan Commelin]

Note that unique is data. We have to choose a default element, and I choose 0.

[Johan Commelin]

So 1 is only provably equal to default R, not defeq.

[Heather Macbeth]

OK, thanks a lot. I have a nearly-ready PR it can go in, but if "nearly-ready" is not "ready" by Monday, I'll pass back to you.

[Heather Macbeth]

Johan Commelin said:

def unique_of_zero_eq_one (h : (0:R) = 1) : unique R :=
{ default := 0,
  uniq :=
  begin
    haveI := subsingleton_of_zero_eq_one R h,
    intro r, exact subsingleton.elim r _
  end }

@Johan Commelin , is there a reason you did this instead of

def unique_of_zero_eq_one (h : (0:R) = 1) : unique R :=
{ default := 0,
  uniq    := eq_zero_of_zero_eq_one R h }

[Heather Macbeth]

And one more question: what file should

inductive data_xor (X : Sort*) (Y : Sort*)
| left (x : X)  : data_xor
| right (y : Y) : data_xor

go in?

[Kenny Lau]

that's the sumtype?

[Heather Macbeth]

@Kenny Lau , can you elaborate? If I naively replace all uses of data_xor with sum in Johan's example
noncomputable def unique_or_nonzero : data_xor (unique R) (nonzero R), I get the following error:

type mismatch at application
  unique α ⊕ nonzero α
term
  nonzero α
has type
  Prop : Type
but is expected to have type
  Type ? : Type (?+1)

[Kenny Lau]

hmm, how about psum (if it exists)?

[Heather Macbeth]

Seems to work, thanks! What's a psum?

[Kenny Lau]

I think p just means universere polymorphic

[Scott Olson]

I interpreted the p in psum as "proposition", since sum : Type u → Type v → Type (max u v) and psum : Sort u → Sort v → Sort (max 1 u v) are both universe polymorphic, but only psum accepts Prop components (because Sort u is like saying "Prop or any Type level").

[Scott Olson]

A bunch of the core types come in threes, like or/sum/psum, and/prod/pprod, and Exists/sigma/psigma.

[Johan Commelin]

Heather Macbeth said:

Johan Commelin said:

def unique_of_zero_eq_one (h : (0:R) = 1) : unique R :=
{ default := 0,
  uniq :=
  begin
    haveI := subsingleton_of_zero_eq_one R h,
    intro r, exact subsingleton.elim r _
  end }

Johan Commelin , is there a reason you did this instead of

def unique_of_zero_eq_one (h : (0:R) = 1) : unique R :=
{ default := 0,
  uniq    := eq_zero_of_zero_eq_one R h }

Yes, but the reason is silly: I didn't think of using eq_zero_of_zero_eq_one... So, it's just a stupid mistake on my side.

[Johan Commelin]

@Heather Macbeth psum is better. I didn't know about it.

[Heather Macbeth]

#3210