# Zulip Chat Archive

## Stream: general

### Topic: maximal ideals map to maximal ideal by iso

#### Yiming Xu (May 17 2019 at 04:34):

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 (May 17 2019 at 04:35):

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 (May 17 2019 at 04:58):

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 (May 17 2019 at 06:32):

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

#### Johan Commelin (May 17 2019 at 06:35):

Shouldn't `iso_induction`

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

#### Keeley Hoek (May 17 2019 at 06:39):

At first we're building the `iso_functoriality`

instances by hand. Then we can automate how they get constructed.

#### Kevin Buzzard (May 17 2019 at 07:06):

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 (May 17 2019 at 07:07):

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

#### Yiming Xu (May 17 2019 at 07:45):

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

instance 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 (May 17 2019 at 07:53):

I would reiterate my suggestion to focus on `transfer`

style lemmas. They work in much more generality than isos

#### Kevin Buzzard (May 17 2019 at 08:06):

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 (May 17 2019 at 11:11):

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 (May 17 2019 at 11:45):

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 (May 17 2019 at 11:47):

What if `is_unit 0`

was false hehe

#### Kevin Buzzard (May 17 2019 at 11:49):

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 (May 17 2019 at 11:49):

ah, cool

#### Johan Commelin (May 17 2019 at 11:55):

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

.

#### Neil Strickland (May 17 2019 at 13:08):

Yes, sorry, you should add `0 ≠ 1`

as part of the definition of a local ring.

#### Scott Morrison (May 18 2019 at 02:09):

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...

#### Mario Carneiro (May 18 2019 at 02:12):

lol of course it's in the perfectoid thread

Last updated: Aug 03 2023 at 10:10 UTC