Zulip Chat Archive

Stream: maths

Topic: quotient by zero submodule


view this post on Zulip Ashwin Iyengar (May 10 2020 at 12:58):

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

view this post on Zulip 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 RR/mR \to R/\mathfrak{m}. But if R=kR = k and m=0\mathfrak{m} = 0 then this is just the identity...

view this post on Zulip 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])?

view this post on Zulip 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 MM is the quotient of MM at 00. The library unfortunately hasn't been set up to make this easy, but I think it should be refactored.

view this post on Zulip Reid Barton (May 10 2020 at 13:17):

Ashwin Iyengar said:

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

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

  1. Use MM/0M \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 MM/IM \to M/I, but characterize what it means to be one (e.g., surjective with kernel II); then the identity MMM \to M will qualify.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 MM is the quotient of MM at 00. 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?

view this post on Zulip Kevin Buzzard (May 10 2020 at 14:12):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 10 2020 at 14:18):

We are still experimenting in this area

view this post on Zulip Ashwin Iyengar (May 10 2020 at 14:30):

Ok. Then if I have a local ring, there should not be "the residue field R/mR/\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 RR/mR \to R/\mathfrak{m} constructed in the usual way is a residue field?

view this post on Zulip 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.

view this post on Zulip Ashwin Iyengar (May 10 2020 at 14:40):

fair enough, will do

view this post on Zulip 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]R[1/fg] was exact, but we needed it for R[1/f][1/g]R[1/f][1/g]. We realised later on that we should have proved exactness of the sequence for any ring AA which was isomorphic to R[1/fg]R[1/fg].

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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)?

view this post on Zulip Kenny Lau (May 10 2020 at 14:59):

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

view this post on Zulip Kenny Lau (May 10 2020 at 14:59):

or maybe not

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 10 2020 at 15:11):

One suggestion though, use more newlines!

view this post on Zulip 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.

view this post on Zulip 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