Zulip Chat Archive

Stream: general

Topic: Prove equality of ideals, related by some function


Arnoud van der Leer (Apr 24 2021 at 07:36):

Hi there, my latest attempt at doing something remotely useful is formalizing Atiyah & Macdonald, Introduction to Commutative Algebra. I am kind of stuck at the first theorem. More specifically: I was able to prove that we can lift and project an ideal from and to a quotient by an ideal I, but now I am trying to prove that this is a "bijection" (from ideals containing I):

import algebra.ring
import ring_theory.ideal.basic

lemma project_ideal_to_quotient {R: Type} [comm_ring R] (I: ideal R) :  (J: ideal R), ideal I.quotient := assume J, {
  carrier   := (ideal.quotient.mk I)'' J,
  zero_mem' := by { use 0, simp [J.zero_mem'] },
  add_mem'  := begin
    rintros a b  a',  ha1, ha2    b',  hb1, hb2  ⟩,
    use a' + b',
    simp,
    split,
      apply J.add_mem'; assumption,
      rw [ha2, hb2],
  end,
  smul_mem' := begin
    rintros c x  x',  hx1, hx2  ⟩,
    cases ideal.quotient.mk_surjective c with c' hc,
    simp,
    use c'  x',
    split,
      apply J.smul_mem'; assumption,
      { simp,
        rw [hx2, hc]},
  end,
}

lemma lift_ideal_from_quotient {R: Type} [comm_ring R] (I: ideal R) :  (J: ideal I.quotient), ideal R := assume J, {
  carrier   := (ideal.quotient.mk I)⁻¹' J,
  zero_mem' := by simp,
  add_mem'  := assume ha hb, by apply J.add_mem',
  smul_mem' := begin
    simp,
    intros c x hx,
    have h :  c x (h: x  J), c * x = c  x, by simp,
    rw h _ _ hx,
    apply J.smul_mem',
    assumption,
  end
}

lemma project_lift (R: Type) [comm_ring R] (I: ideal R) :  (J: ideal I.quotient), project_ideal_to_quotient I (lift_ideal_from_quotient I J) = J := begin
  intros,
  sorry
end

How can I start proving that J equals some_lemma _ (some_other_lemma _ J)? When I try cases J and cases project_ideal_to_quotient _ _, I lose the information about how they are related (namely, that the carrier of the latter is the projection of the preimage of the former).

Johan Commelin (Apr 24 2021 at 08:43):

@Arnoud van der Leer Just to be sure: you are aware that a lot of this is already in mathlib, right?

Scott Morrison (Apr 24 2021 at 08:44):

One worry here is that you are defining data inside a lemma, rather than a def.

Arnoud van der Leer (Apr 24 2021 at 08:47):

@Johan Commelin I am kind of new at this. I found out yesterday where ideals and quotients by ideals are located. And no, I am not aware that a lot of this is already in mathlib :flushed:
Is it?

Johan Commelin (Apr 24 2021 at 08:48):

Search for ideal.map and ideal.comap.

Arnoud van der Leer (Apr 24 2021 at 08:48):

@Scott Morrison Hm... Right. I was aware that there was some difference between them, but I don't know exactly which difference. (Lemma and Theorem are equivalent though, right?)

Johan Commelin (Apr 24 2021 at 08:49):

I don't know if the "bijection" you mention is there in exactly this form. But certainly a lot of the ingredients are there.

Johan Commelin (Apr 24 2021 at 08:49):

I think @Riccardo Brasca did that "bijection" as some form of one of the isomorphism theorems

Riccardo Brasca (Apr 24 2021 at 08:52):

The first isomorphism theorem is docs#ring_hom.quotient_ker_equiv_of_surjective

Riccardo Brasca (Apr 24 2021 at 08:53):

In that file there are several results about ideals, map and comap

Arnoud van der Leer (Apr 24 2021 at 08:57):

Ah, right. Thanks!
So is all of the information in there about the correspondence between the ideals J in R8 containing an ideal I and the ideals J / I in R / I`?

Riccardo Brasca (Apr 24 2021 at 09:15):

I am with my phone and it's not easy to search, but of you are interested in the bijection between ideals of R/I and ideals that contain I, I would look for something about submodules

Arnoud van der Leer (Apr 24 2021 at 09:20):

Riccardo Brasca Thanks!

Kevin Buzzard (Apr 24 2021 at 09:45):

@Arnoud van der Leer I wouldn't worry about a lot of it being done already. Doing stuff like this is a great way to learn Lean, however quotients can be complicated so it's a bit of a tricky place to start.

Note that mathlib thinks about stuff like "canonical bijections" in quite an abstract way and is very careful with what we mean by it: for example what you might think of as (and what is constantly explained to us as) a "theorem" is sometimes a definition in Lean. For example the first isomorphism "theorem" that a quotient by a kernel "is isomorphic to" or "is canonically isomorphic to" an image, would in Lean be expressed as a definition giving the explicit construction, because this is what we mathematicians actually need in practice rather than just the abstract statement that there is an isomorphism.

Thinking about Atiyah-Macdonald, I'm not sure if we have primary decomposition in Lean, but although I'm not a commutative algebraist my impression is that that chapter hasn't aged well and people now emphasize different definitions. I also don't think we have Krull's intersection theorem but I might be wrong. Everything else is I think covered by what we have although sometimes you have to know what you're looking for, eg we might have some incomprehensible-looking definition involving a morphism of lattices and this turns out to me some way of expressing the third isomorphism theorem.

If you're looking to do commutative algebra in general then we have essentially nothing on flat or projective modules beyond the definitions (and note that as a mathematician you might have several definitions of these ideas; we may only have one so there might even be work to do proving that various other definitions are equivalent to the one we have). Note however that homological algebra is currently being actively worked on, and until we've got the basics sorted out in some vast generality there is unlikely to be any access to Ext or Tor.

Arnoud van der Leer (Apr 24 2021 at 09:54):

@Kevin Buzzard Thanks for your comment.

Right. So why do we also have lemmas and theorems then? Are these really only useful for nonconstructive mathematics?

Summarizing, a lot of A&M has either already been implemented, or has become almost obsolete.

Okay, so I think I will still try to formalize a part of the book, just to get a bit of practice. However, now with the healthy expectation that this will not yet be my great contribution to mathlib ^^ (and, maybe, if I succeed before I get bored or otherwise distracted, to have most of the mathematics of the book in one, structured place, for those who still use the book for lectures and stuff)

Kevin Buzzard (Apr 24 2021 at 09:56):

Because some theorems are theorems! For example the statement that the sum of 1/n^2 is pi^2/6 is a theorem. I'm just pointing out that the first isomorphism theorem is the statement that an explicit construction (a definition) is an isomorphism, not the statement that two things happen to be isomorphic as it is usually presented to us.

Kevin Buzzard (Apr 24 2021 at 09:58):

The theorem mathematicians use in practice is "this construction is an isomorphism" not "there exists an isomorphism"

Arnoud van der Leer (Apr 24 2021 at 09:59):

Ah, that makes sense. I am not sure whether I will always be able to pick the correct one, but I get the general idea. Thank you for your time!

Kevin Buzzard (Apr 24 2021 at 10:00):

If you want to make a contribution to mathlib you could prove that a direct sum of two projective modules is projective and that an arbitrary direct sum of projective modules is projective.

Scott Morrison (Apr 24 2021 at 10:00):

Actually, #7319 does that. :-)

Scott Morrison (Apr 24 2021 at 10:01):

We still need the glue that the definition of a projective module agrees with that of a projective object in the category of modules, which is waiting on some other PR.

Kevin Buzzard (Apr 24 2021 at 10:01):

That's much harder for a beginner though

Eric Wieser (Apr 24 2021 at 10:02):

Do we have the glue between the category theory direct sum and direct_sum?

Scott Morrison (Apr 24 2021 at 10:03):

No.

Scott Morrison (Apr 24 2021 at 10:03):

We actually don't have categorical direct sum at all, in the sense of https://ncatlab.org/nlab/show/direct+sum

Scott Morrison (Apr 24 2021 at 10:04):

On the categorical side we have biproducts, which are slightly "better" (= harder to have exist, typically you only get to have finite biproducts).

Eric Wieser (Apr 24 2021 at 10:04):

Oh, does ⨁ g not mean something similar to ⨁ i, g i (with open_locale direct_sum)?

Kevin Buzzard (Apr 24 2021 at 10:06):

Surely those are the same, at least for concrete categories such as monoids, groups and modules

Scott Morrison (Apr 24 2021 at 10:06):

Yes.

Eric Wieser (Apr 24 2021 at 10:06):

What is the former notation for?

Kevin Buzzard (Apr 24 2021 at 10:07):

I think Scott is just saying that we don't have this construction in general categories

Scott Morrison (Apr 24 2021 at 10:07):

That notation in category_theory is for biproducts.

Kevin Buzzard (Apr 24 2021 at 10:08):

With \O+? The big O?

Scott Morrison (Apr 24 2021 at 10:08):

Yes

Eric Wieser (Apr 24 2021 at 10:09):

docs#category_theory.biproduct? nope, wrong guess

Scott Morrison (Apr 24 2021 at 10:10):

docs#category_theory.limits.biproduct ?

Hanting Zhang (Apr 24 2021 at 15:33):

@Arnoud van der Leer docs#ideal.rel_iso_of_surjective gives the correspondence.

Floris van Doorn (Apr 24 2021 at 15:40):

Arnoud van der Leer said:

Ah, that makes sense. I am not sure whether I will always be able to pick the correct one, but I get the general idea. Thank you for your time!

If you're talking about choosing the correct one between def and lemma, we have a tool for that: Write #lint a the bottom of your file, and it will complain about any def/lemma mistakes you made (and potentially about some other stuff). You might need to import tactic at the top.

Arnoud van der Leer (Apr 24 2021 at 15:50):

@Hanting Zhang Ooooh, right, I see. Thanks!

Arnoud van der Leer (Apr 24 2021 at 15:50):

@Floris van Doorn That sounds like a good idea. Thanks!


Last updated: Dec 20 2023 at 11:08 UTC