# Zulip Chat Archive

## 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`

?

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

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 := λ _ _, (), 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 (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?

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

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

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

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 `sum`

type?

#### 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 **p**olymorphic

#### 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):

Last updated: May 06 2021 at 18:20 UTC