quotient by zero submodule

Stream: maths

[Ashwin Iyengar]

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]

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]

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]

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]

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]

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]

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]

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

[Ashwin Iyengar]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

We are still experimenting in this area

[Ashwin Iyengar]

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]

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

[Ashwin Iyengar]

fair enough, will do

[Kevin Buzzard]

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]

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]

@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]

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]

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]

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

[Kenny Lau]

or maybe not

[Kenny Lau]

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

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

One suggestion though, use more newlines!

[Yury G. Kudryashov]

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

[Ramon Fernandez Mir]

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