maximal ideals map to maximal ideal by iso

Stream: general

[Yiming Xu]

Hi,
I am attempting construct a framework of constructing instances of is_iso_functorial, and I wish to take is_local_ring as example. But there is a lemma I need which I cannot find and struggle to prove in lean.

Could someone please just give me a proof that maximal ideals are mapped to maximal ideals under an isomorphism?

Thank you!

[Yiming Xu]

Actually the version I am proving is

lemma comap_maximal_maximal (X Y : CommRing.{0}) (ix : ideal X) (f : X ≅ Y) (p : ideal.is_maximal ix):
 ideal.is_maximal (ideal.comap f.inv ix)

which requires using the category theory library, but if someone prove another version without the category theory thing, I will also very appreciate!

[Yiming Xu]

For the above to run, I did

import iso_induction
import ring_theory.ideals data.equiv.algebra
import category_theory.instances.CommRing
import category_theory.concrete_category
import category_theory.opposites
import ring_theory.ideal_operations
import ring_theory.ideals
import category_theory.core
import category_theory.elements

[Kevin Buzzard]

Maybe the set of all ideals form a lattice and you can prove something about maximal elements of a lattice

[Johan Commelin]

Shouldn't iso_induction do this recursively? If it can't do this, you set your target too high.

[Keeley Hoek]

At first we're building the iso_functoriality instances by hand. Then we can automate how they get constructed.

[Kevin Buzzard]

I've always regarded this as the statement that if you have an isomorphism of lattices then the subsets cut out by all the sensible predicates also biject with each other.

[Kevin Buzzard]

By "sensible" I mean "the ones I would allow in $maths\ mode$"

[Yiming Xu]

Sorry, I forgot mentioning the fact that I am the student of @Scott Morrison and I am currently attempt writing iso_induction with help of Scott and Keeley.

The current version of iso_induction cannot do such much thing. It can only rewrite the goal P X into P Y if it can find is_iso_functorial P and X \iso Y. The current attempt is to make constructing such instances as easy as possible, and we are attempting testing a framework of constructing a certain type of instances. And we are testing if this framework can be used to build instances of is_iso_functorialinstance of is_local_ring.

Thank you for providing thoughts about proving it! I think I basically know to prove this lemma, but sometimes the lean's behaviour is strange and does not allow me to do something and I have spent much more time on the proof of this lemma then I expected. As writing this lemma is not the main part of this project (I'd like to solve the problems I come up with, just I have other coursework so my time is quite limited, at least at this stage), so I just wish for a proof here. I will definitely return here to try to think about isomorphism of lattice when I have lower pressure from coursework. I know that it is quite ambitious to produce a good version of this tactic within such short time, I would be very happy to keep developing it after the semester and add new things to it, and perhaps find out a way to construct such instance using order of a lattice.

[Mario Carneiro]

I would reiterate my suggestion to focus on transfer style lemmas. They work in much more generality than isos

[Kevin Buzzard]

This issue keeps on coming up (unsurprisingly) and information about it is now in several threads here. I don't know what to do about this. Mario even posted some transfer code with some comment of the form "this is as far as I've got", but it was right in the middle of when I was really pushing to get perfectoids compiling and I didn't look at it at the time...I wonder if I starred it...

[Neil Strickland]

I know that this is orthogonal to your immediate question here, but I will take the opportunity to rant anyway: the correct definition of local is

∀ (x : R), (is_unit x) ∨ (is_unit (1 - x))

and one should deduce from this that {x : R // ¬ (is_unit x)} is the unique maximal ideal. This is logically preferable for many reasons, including the fact that it makes your transfer lemma easier.

[Kevin Buzzard]

o_O? As a mathematician I am not sure what the "correct" definition of anything is :-) This definition makes the zero ring local, which I think is a bad idea, but other than that it is a pretty cool way of doing it. Maybe also add 0 != 1?

[Keeley Hoek]

What if is_unit 0 was false hehe

[Kevin Buzzard]

is_unit 0 is true if 0=1. It's essential that the element of the zero ring is a unit, because you want the units of a ring to be a group (and the empty set isn't a group).

[Keeley Hoek]

ah, cool

[Johan Commelin]

Ooh, I didn't check too carefully. It is indeed standard to add 0 \ne 1.

[Neil Strickland]

Yes, sorry, you should add 0 ≠ 1 as part of the definition of a local ring.

[Scott Morrison]

Mario even posted some transfer code with some comment of the form "this is as far as I've got", but it was right in the middle of when I was really pushing to get perfectoids compiling and I didn't look at it at the time...I wonder if I starred it...

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfectoid.20spaces/near/159808751

[Mario Carneiro]

lol of course it's in the perfectoid thread