## Stream: maths

### Topic: zero ring

#### Kevin Buzzard (Sep 09 2018 at 14:56):

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 (Sep 09 2018 at 15:11):

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

Is this a real example, including the fintype part?

#### Reid Barton (Sep 09 2018 at 15:12):

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

#### Chris Hughes (Sep 09 2018 at 15:12):

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

#### Reid Barton (Sep 09 2018 at 15:12):

You can also use subsingleton in this case, yeah

#### Kevin Buzzard (Sep 09 2018 at 15:13):

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 (Sep 09 2018 at 15:14):

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

#### Kevin Buzzard (Sep 09 2018 at 15:14):

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

#### Kevin Buzzard (Sep 09 2018 at 15:15):

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

#### Reid Barton (Sep 09 2018 at 15:16):

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 (Sep 09 2018 at 15:17):

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

#### Kevin Buzzard (Sep 09 2018 at 15:18):

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 (Sep 09 2018 at 15:18):

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

#### Kevin Buzzard (Sep 09 2018 at 15:26):

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

Not computably.

#### Chris Hughes (Sep 09 2018 at 15:27):

It will for rings though

#### Kevin Buzzard (Sep 09 2018 at 15:41):

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 (Sep 12 2018 at 11:54):

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 (Sep 12 2018 at 11:55):

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

#### Kevin Buzzard (Sep 12 2018 at 12:14):

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 (Sep 12 2018 at 12:15):

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 (Sep 12 2018 at 12:17):

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

#### Mario Carneiro (Sep 12 2018 at 17:10):

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

#### Kevin Buzzard (Jul 10 2019 at 22:49):

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 (Jul 10 2019 at 22:50):

I really want "import all of mathlib" here.

#### Kevin Buzzard (Jul 10 2019 at 23:11):

instance : comm_ring unit :=
{ add := λ _ _, (),
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 (Jul 10 2019 at 23:12):

I wrote that algorithmically.

#### Kevin Buzzard (Jul 10 2019 at 23:13):

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 (Jul 10 2019 at 23:22):

I thought I remembered it from somewhere. algebra.punit_instances

#### Kevin Buzzard (Jul 10 2019 at 23:25):

topological_ring unit missing?

#### Kevin Buzzard (Jul 10 2019 at 23:59):

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 (Jul 11 2019 at 00:01):

got it, i'd made a diamond

#### Kevin Buzzard (Jul 11 2019 at 00:05):

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

#### Mario Carneiro (Jul 11 2019 at 01:25):

I thought the zero ring was added to pi_instances

#### Mario Carneiro (Jul 11 2019 at 01:25):

(which should be renamed btw)

#### Johan Commelin (Jul 11 2019 at 04:26):

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

#### Heather Macbeth (Jun 27 2020 at 19:13):

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 (Jun 27 2020 at 19:18):

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

Aha, thank you!

#### Heather Macbeth (Jun 27 2020 at 19:20):

Is there a reason that there is no unique_of_zero_eq_one?

#### Johan Commelin (Jun 27 2020 at 19:20):

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

#### Heather Macbeth (Jun 27 2020 at 19:20):

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

#### Kevin Buzzard (Jun 27 2020 at 19:20):

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 (Jun 27 2020 at 19:20):

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

#### Alex J. Best (Jun 27 2020 at 19:20):

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 (Jun 27 2020 at 19:22):

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

Yup, I agree

#### Johan Commelin (Jun 27 2020 at 19:22):

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

#### Johan Commelin (Jun 27 2020 at 19:22):

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

#### Johan Commelin (Jun 27 2020 at 19:23):

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

#### Johan Commelin (Jun 27 2020 at 19:23):

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

#### Kevin Buzzard (Jun 27 2020 at 19:23):

haveI right?

#### Johan Commelin (Jun 27 2020 at 19:24):

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

#### Johan Commelin (Jun 27 2020 at 19:24):

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

#### Johan Commelin (Jun 27 2020 at 19:24):

The rest will be done by tc

#### Heather Macbeth (Jun 27 2020 at 19:31):

Sorry, had to step away for a sec

#### Heather Macbeth (Jun 27 2020 at 19:34):

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 (Jun 27 2020 at 19:35):

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 (Jun 27 2020 at 19:48):

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 (Jun 27 2020 at 19:48):

I'll build another one that uses unique

#### Johan Commelin (Jun 27 2020 at 19:54):

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 (Jun 27 2020 at 19:54):

Yes, these look great!

#### Johan Commelin (Jun 27 2020 at 19:54):

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 (Jun 27 2020 at 19:55):

@Heather Macbeth Feel free to incorporate this into a PR

#### Johan Commelin (Jun 27 2020 at 19:55):

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

#### Johan Commelin (Jun 27 2020 at 19:56):

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

#### Johan Commelin (Jun 27 2020 at 19:56):

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

#### Heather Macbeth (Jun 27 2020 at 19:56):

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 (Jun 27 2020 at 20:24):

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 (Jun 27 2020 at 20:55):

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 (Jun 27 2020 at 20:56):

that's the sumtype?

#### Heather Macbeth (Jun 27 2020 at 20:59):

@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 (Jun 27 2020 at 21:02):

hmm, how about psum (if it exists)?

#### Heather Macbeth (Jun 27 2020 at 21:04):

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

#### Kenny Lau (Jun 27 2020 at 21:12):

I think p just means universere polymorphic

#### Scott Olson (Jun 28 2020 at 02:55):

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 (Jun 28 2020 at 02:59):

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

#### Johan Commelin (Jun 28 2020 at 04:09):

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 (Jun 28 2020 at 04:10):

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

#### Heather Macbeth (Jun 28 2020 at 12:17):

#3210

Last updated: May 06 2021 at 18:20 UTC