## Stream: maths

### Topic: quotient by zero submodule

#### Ashwin Iyengar (May 10 2020 at 12:58):

Does Lean know how to "canonically identify" $M/0 \cong M$? And to treat the quotient map $M \to M/0$ like the identity map?

#### Ashwin Iyengar (May 10 2020 at 12:59):

I'm trying to show that a field is a Henselian local ring, and part of the definition of a Henselian ring involves lifting along $R \to R/\mathfrak{m}$. But if $R = k$ and $\mathfrak{m} = 0$ then this is just the identity...

#### Ashwin Iyengar (May 10 2020 at 13:00):

Or is the right thing to do to show that residue R is a bijection in this case (when we have [field R])?

#### Chris Hughes (May 10 2020 at 13:16):

I think perhaps the correct way to do quotients is to prove every theorem about quotients on rings that satisfy the universal property of the quotient. That way you can prove that $M$ is the quotient of $M$ at $0$. The library unfortunately hasn't been set up to make this easy, but I think it should be refactored.

#### Reid Barton (May 10 2020 at 13:17):

Ashwin Iyengar said:

Does Lean know how to "canonically identify" $M/0 \cong M$? And to treat the quotient map $M \to M/0$ like the identity map?

No. Once you write down a construction of the quotient $M/0$, it is whatever it is and it's highly unlikely to be "the same" as $M$ in Lean's eyes. There are basically two approaches:

1. Use $M \to M/0$ as an isomorphism (it's easy to write down an inverse) and then lift along this isomorphism (which is just composition with the inverse).
2. Don't work with a specific model for the quotient map $M \to M/I$, but characterize what it means to be one (e.g., surjective with kernel $I$); then the identity $M \to M$ will qualify.

#### Reid Barton (May 10 2020 at 13:26):

Also, we don't yet have the definition of a Henselian ring in mathlib, do we? I'd be very interested to see what you are working on!

#### Reid Barton (May 10 2020 at 13:27):

As much as it pains me to say it, it's usually better for technical reasons to choose definitions which don't involve quantifying over Type

#### Kevin Buzzard (May 10 2020 at 13:54):

On my job list is bundling normal_subgroup G and then rewriting quotients in group theory to use bundled normal subgroups.

#### Ashwin Iyengar (May 10 2020 at 13:54):

Reid Barton said:

Also, we don't yet have the definition of a Henselian ring in mathlib, do we? I'd be very interested to see what you are working on!

Yeah I'm working on this now! I'll push some more in a bit.

#### Kevin Buzzard (May 10 2020 at 13:54):

But I have a lot of marking and a grant application deadline to juggle right now, as well as trying to write this Mathematics in Lean book with Jeremy, Patrick and Rob.

#### Ashwin Iyengar (May 10 2020 at 14:10):

Chris Hughes said:

I think perhaps the correct way to do quotients is to prove every theorem about quotients on rings that satisfy the universal property of the quotient. That way you can prove that $M$ is the quotient of $M$ at $0$. The library unfortunately hasn't been set up to make this easy, but I think it should be refactored.

I could try defining the notion of a quotient of a nonzero_comm_ring by an ideal using the universal property. Are there already examples of things defined using universal properties in Lean that I could use as a starting point?

#### Kevin Buzzard (May 10 2020 at 14:12):

Localisation of rings was set up this way in @Ramon Fernandez Mir 's MSc thesis

#### Kevin Buzzard (May 10 2020 at 14:13):

It's available in the links on the leanprover-community website. Can I write some hashtag to link to this nowadays?

#### Kevin Buzzard (May 10 2020 at 14:14):

He defined what it meant for a homomorphism of rings to be isomorphic to a localisation, following an API idea of Strickland

#### Kevin Buzzard (May 10 2020 at 14:15):

For technical reasons this concept of being isomorphic to a localisation turned out to be very useful. Life was a lot more unbundled in those days though

#### Kevin Buzzard (May 10 2020 at 14:18):

You should make a new predicate for a ring homomorphism R -> A saying that it is surjective and its kernel is I, and then every theorem that is proved for R/I you should prove as well for all rings A equipped with a map from R satisfying the predicate

#### Kevin Buzzard (May 10 2020 at 14:18):

We are still experimenting in this area

#### Ashwin Iyengar (May 10 2020 at 14:30):

Ok. Then if I have a local ring, there should not be "the residue field $R/\mathfrak{m}$", instead there should be a predicate is_residue_field f which is an alias of is_quotient f m where f is a ring homomorphism and m is the unique maximal ideal. And then maybe one proves the lemma that $R \to R/\mathfrak{m}$ constructed in the usual way is a residue field?

#### Kevin Buzzard (May 10 2020 at 14:34):

Yeah I guess the proof of the pudding will be in the eating here. I would just experiment.

#### Ashwin Iyengar (May 10 2020 at 14:40):

fair enough, will do

#### Kevin Buzzard (May 10 2020 at 14:41):

With localisations we were well on the way to defining schemes, and then discovered that we had proved a sequence involving $R[1/fg]$ was exact, but we needed it for $R[1/f][1/g]$. We realised later on that we should have proved exactness of the sequence for any ring $A$ which was isomorphic to $R[1/fg]$.

#### Kevin Buzzard (May 10 2020 at 14:43):

This is the difference between Ramon's work and my earlier work with Kenny and Chris which we wrote after only a few months of working with Lean and which contained several serious design flaws (but which taught us a lot about Lean).

#### Johan Commelin (May 10 2020 at 14:49):

@Ashwin Iyengar After defining Henselian local rings, I think the first step to do is prove that:

1. For every Henselian local ring, you can lift along every surjective f : R → K, where K is a field.
2. If R is a local ring, and satisfies lifting for some surjective f : R → K, where K is a field, then R is local Henselian.

#### Johan Commelin (May 10 2020 at 14:55):

Or better yet, prove some lemma from the stacks project giving 11 equivalent characterisations. (But modify the statement so that it works for surjective ring maps to fields, instead of only R/m.)

#### Ashwin Iyengar (May 10 2020 at 14:58):

In that case does

variables (R : Type u)

class henselian extends local_ring R :=
(is_henselian : ∀ p : polynomial R, ∀ a₀ : residue_field R, monic p ∧ is_root (map (residue R) p) a₀ ∧ ¬is_root(derivative (map (residue R) p)) a₀ → ∃ a : R, is_root p a ∧ residue R a = a₀)


look like a sensible definition or should I define it using (2)?

#### Kenny Lau (May 10 2020 at 14:59):

if you define it using (2) you will run into universe issues

or maybe not

#### Kenny Lau (May 10 2020 at 15:00):

btw does this imply the more general Hensel theorem about factorizing polynomials, or does that require algebraic closure?

#### Reid Barton (May 10 2020 at 15:05):

The universe issues aren't a serious obstruction, but either way you are going to want to prove the equivalence of the two definitions and if you are going to do that anyways it's more ergonomic to use the one that doesn't involve quantification over Type as the definition.

#### Reid Barton (May 10 2020 at 15:07):

Typically you actually have some statements like (lifting for rings in Type u) => (some polynomial thing) => (lifting for rings in all universes), but the last one can't be expressed as the definition

#### Reid Barton (May 10 2020 at 15:08):

and in a hypothetical future world where we can automatically transfer properties from R to ulift R, it's a lot harder to do it if your definition involves quantification over types

#### Ashwin Iyengar (May 10 2020 at 15:10):

Ok I'll stick with my definition. And yes, it's equivalent to the definition which says that you can lift factorizations.

#### Reid Barton (May 10 2020 at 15:11):

One suggestion though, use more newlines!

#### Yury G. Kudryashov (May 10 2020 at 15:58):

I'm going to submit a PR including the linear equivalence between M and M/0 today or tomorrow, see here.

#### Ramon Fernandez Mir (May 10 2020 at 16:55):

If it helps, what Kevin was referring to can be found here: https://github.com/ramonfmir/lean-scheme/blob/master/src/to_mathlib/localization/localization_alt.lean

Last updated: May 18 2021 at 08:14 UTC