Prove equality of ideals, related by some function

Stream: general

[Arnoud van der Leer]

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]

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

[Scott Morrison]

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

[Arnoud van der Leer]

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

Search for ideal.map and ideal.comap.

[Arnoud van der Leer]

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

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]

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

[Riccardo Brasca]

The first isomorphism theorem is docs#ring_hom.quotient_ker_equiv_of_surjective

[Riccardo Brasca]

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

[Arnoud van der Leer]

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]

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]

Riccardo Brasca Thanks!

[Kevin Buzzard]

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

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

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]

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

[Arnoud van der Leer]

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]

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]

Actually, #7319 does that. :-)

[Scott Morrison]

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]

That's much harder for a beginner though

[Eric Wieser]

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

[Scott Morrison]

No.

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Kevin Buzzard]

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

[Scott Morrison]

Yes.

[Eric Wieser]

What is the former notation for?

[Kevin Buzzard]

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

[Scott Morrison]

That notation in category_theory is for biproducts.

[Kevin Buzzard]

With \O+? The big O?

[Scott Morrison]

Yes

[Eric Wieser]

docs#category_theory.biproduct? nope, wrong guess

[Scott Morrison]

docs#category_theory.limits.biproduct ?

[Hanting Zhang]

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

[Floris van Doorn]

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]

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

[Arnoud van der Leer]

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