Quotient of a ring by a sum of ideals

Stream: Is there code for X?

[Paul Lezeau]

Hi !

Say $R$ is a commutative ring, $I,J$ are ideals of $R$ and $J'$ is the ideal corresponding to $J$ in $R/I$.
Does anyone know of results of the form $R/(I+J) \cong (R/I)/J'$ in matlib ? (I couldn't find any when browsing through the files I thought might contain something like that).

The context is I am trying to show that for an integer $p$ (of course later I will be taking $p$ to be prime, hence the choice of notation :smile:) and a polynomial $f$ with integer coefficients, there is an isomorphism
$\mathbb{Z}[x] / (p, f(x) ) \cong \mathbb{Z}/p\mathbb{Z}[x] / ( \overline{f}(x) )$ that sends $g + (p , f(x) )$ to $(g +( p )) + (\overline{f}(x))$, where $\overline{f}$ is the reduction of $f$ mod $p$.

Many thanks in advance !

[Kevin Buzzard]

I also can't find this exact result (or anything much approaching it) in mathlib. Here's the definitions, but I've not filled in any of the proofs:

import tactic
import ring_theory.ideal.operations

-- let R be a commutative ring and let I,J be ideals of R
variables {R : Type} [comm_ring R] (I J : ideal R)

-- define f₁ to be the obvious ring hom R/I → R/(I+J)
def f₁ : I.quotient →+* (I+J).quotient := ideal.quotient.lift I (ideal.quotient.mk (I+J)) sorry

-- define f₂ to be the induced ring hom (R/I)/J' ->R/(I+J), where J' is the image of J in R/I
def f₂ : (J.map (ideal.quotient.mk I)).quotient →+* (I + J).quotient :=
ideal.quotient.lift (ideal.map (ideal.quotient.mk I) J) (f₁ I J) sorry

-- Then f₂ is an isomorphism
noncomputable example :
  (J.map (ideal.quotient.mk I)).quotient ≃+* (I + J).quotient :=
ring_equiv.of_bijective (f₂ I J) sorry

To me this indicates that we're missing some API for this sort of thing.

[Kevin Buzzard]

Actually I think I'm being overly pessimistic making it noncomputable...

[Kevin Buzzard]

import tactic
import ring_theory.ideal.operations

-- let R be a commutative ring and let I,J be ideals of R
variables {R : Type} [comm_ring R] (I J : ideal R)

-- define f₁ to be the obvious ring hom R/I → R/(I+J)
def f₁ : I.quotient →+* (I+J).quotient := ideal.quotient.lift I (ideal.quotient.mk (I+J)) sorry

-- define f₂ to be the induced ring hom (R/I)/J' ->R/(I+J), where J' is the image of J in R/I
def f₂ : (J.map (ideal.quotient.mk I)).quotient →+* (I + J).quotient :=
ideal.quotient.lift (ideal.map (ideal.quotient.mk I) J) (f₁ I J) sorry

-- define g₁ to be the composite of the maps R → (R/I) and (R/I) → (R/I)/J'
def g₁ := ring_hom.comp (ideal.quotient.mk (J.map (ideal.quotient.mk I))) (ideal.quotient.mk I)

-- define g₂ to be the induced map R/(I+J) → (R/I)/J'
def g₂ := ideal.quotient.lift (I+J) (g₁ I J) sorry

-- Then f₂ and g₂ are inverse isomorphisms
example : (J.map (ideal.quotient.mk I)).quotient ≃+* (I + J).quotient :=
{ to_fun := f₂ I J,
  inv_fun := g₂ I J,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := ring_hom.map_mul _,
  map_add' := ring_hom.map_add _ }

[Paul Lezeau]

Thanks a lot ! I'd started to try and write some code towards a proof, but had some trouble understanding how Lean works with defining maps on quotients. I'd be happy to work on a bit of API for this sort of thing, since it seems I'll be needing it for the stuff I'm working on at the minute :smile:

[Kevin Buzzard]

I found quotients In lean hard to understand so I wrote a workshop on them as part of my formalising mathematics course. The main thing to know is that quotients are defined by their universal property and what Lean calls lift is what a mathematician would think of as descent (lift is the function you use to get a map from the quotient given a map from the original ring and a proof that the ideal is in the kernel)

[Kevin Buzzard]

Some of those sorries might be a little tricky by the way, I suspect they'll all have pretty slick solutions in Lean which will only be a few lines long but they might be hard to find!

[Paul Lezeau]

Kevin Buzzard said:

I found quotients In lean hard to understand so I wrote a workshop on them as part of my formalising mathematics course. The main thing to know is that quotients are defined by their universal property and what Lean calls lift is what a mathematician would think of as descent (lift is the function you use to get a map from the quotient given a map from the original ring and a proof that the ideal is in the kernel)

I've just read through the workshop, it makes a lot more sense now. I quite like the universal property approach !

[Paul Lezeau]

Kevin Buzzard said:

Some of those sorries might be a little tricky by the way, I suspect they'll all have pretty slick solutions in Lean which will only be a few lines long but they might be hard to find!

Good to know ! My initial attempt had around 50 lines of code, and I wasn't even half way through, so I'll probably have to do some rewriting !

[Paul Lezeau]

I've been able to spell out the proofs fully, but my code is still somewhat long-ish. Do you have any tips for making it more concise ?

import ring_theory.ideal.operations
import ring_theory.ideal.basic
open ideal

namespace ideal_quot

-- let R be a commutative ring and let I,J be ideals of R
variables {R : Type} [comm_ring R] (I J : ideal R)

lemma add_comm : I+J = J+I := by {rw [ideal.add_eq_sup, sup_comm, ← ideal.add_eq_sup]}


-- a few lemmas to help shorten the proofs later
def left_proj_quot_sum (x :R) : x ∈ I →  ideal.quotient.mk (I+J) x = 0 :=
by {intro hx, apply ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_left hx)}

def right_proj_quot_sum (x : R): x ∈ J →  ideal.quotient.mk (I+J) x = 0 :=
by {intro hx, apply ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_right hx)}

lemma in_ker_proj_to_sum_left : I.map(ideal.quotient.mk(I+J)) = ⊥ :=
begin
  rw [ideal.map,ideal.span_eq_bot],
  intro y,
  rw set.mem_image,
  intro hy,
  cases hy with x hx,
  rw ← hx.2,
  exact left_proj_quot_sum I J x hx.1,
end

lemma in_ker_proj_to_sum_right : J.map(ideal.quotient.mk(I+J)) = ⊥ :=
by {rw add_comm, apply in_ker_proj_to_sum_left}

-- define f₁ to be the obvious ring hom R/I → R/(I+J)
def f₁ : I.quotient →+* (I+J).quotient :=
ideal.quotient.lift I (ideal.quotient.mk (I+J)) (left_proj_quot_sum I J)

-- one of the longer proofs. This will be used to lift f₁ to a map (R/I)/J' → R/(I+J)
def H_proj_J (x : I.quotient) : x ∈ J.map(ideal.quotient.mk I) → f₁ I J x = 0 :=
begin
  intro hx,
  have hIJmap: ((f₁ I J).comp(ideal.quotient.mk I) '' J) = (ideal.quotient.mk (I+J) '' J),
    apply set.ext,
    intro y,
    split,

    {intro hy,
    obtain ⟨z,hz⟩ := (set.mem_image ((f₁ I J).comp(ideal.quotient.mk I)) J y).1 hy,
    unfold f₁ at hz,
    rw [ring_hom.comp_apply,ideal.quotient.lift_mk] at hz,
    rw ← hz.right,
    exact set.mem_image_of_mem (ideal.quotient.mk (I+J)) hz.left},

    {intro hy,
    obtain ⟨z,hz⟩ := (set.mem_image (ideal.quotient.mk (I+J)) J y).1 hy,
    unfold f₁,
    rw set.mem_image_eq,
    use z,
    rwa [ring_hom.comp_apply,ideal.quotient.lift_mk]},

  have hJ: (J.map (ideal.quotient.mk I)).map (f₁ I J) = J.map (ideal.quotient.mk (I+J))
    := by rw [ideal.map_map,ideal.map,hIJmap,← ideal.map],

  have hf₁a : f₁ I J x ∈ (J.map (ideal.quotient.mk I)).map (f₁ I J),
  rw ideal.map,
  apply set.mem_of_subset_of_mem (ideal.subset_span),
  exact (set.mem_image_of_mem (f₁ I J) hx),
  rwa [hJ, in_ker_proj_to_sum_right I J] at hf₁a,
end


-- define f₂ to be the induced ring hom (R/I)/J' ->R/(I+J), where J' is the image of J in R/I
def f₂ : (J.map (ideal.quotient.mk I)).quotient →+* (I + J).quotient :=
ideal.quotient.lift (ideal.map (ideal.quotient.mk I) J) (f₁ I J) (H_proj_J I J)

-- define g₁ to be the composite of the maps R → (R/I) and (R/I) → (R/I)/J'
def g₁ := ring_hom.comp (ideal.quotient.mk (J.map (ideal.quotient.mk I))) (ideal.quotient.mk I)

-- Another short result for lifting map g₁ to a map R/(I+J) → (R/I)/J'
def H_sum (x : R): x ∈ I+J → g₁ I J x = 0 :=
begin
  intro hx,
  have hIJtoJ : (I+J).map(ideal.quotient.mk I) = J.map(ideal.quotient.mk I) := by {
    rw [ideal.add_eq_sup, ideal.map_sup,map_quotient_self],
    simp},
  have hJto0 : (J.map(ideal.quotient.mk I)).map(ideal.quotient.mk(J.map(ideal.quotient.mk I))) = ⊥ :=
    by rw map_quotient_self,
  have : ((I+J).map(ideal.quotient.mk I)).map(ideal.quotient.mk
    (J.map(ideal.quotient.mk I))) = ⊥ := by rw [hIJtoJ, hJto0],
  rw [g₁, ← ideal.mem_bot, ← this, ring_hom.comp_apply],
  apply ideal.mem_map_of_mem,
  apply ideal.mem_map_of_mem,
  exact hx,
end
-- define g₂ to be the induced map R/(I+J) → (R/I)/J'
def g₂ := ideal.quotient.lift (I+J) (g₁ I J) (H_sum I J)

-- Then f₂ and g₂ are inverse isomorphisms
example : (J.map (ideal.quotient.mk I)).quotient ≃+* (I + J).quotient :=
{ to_fun := f₂ I J,
  inv_fun := g₂ I J,
  left_inv :=
  begin
    unfold function.left_inverse,
    intro z,
    cases (ideal.quotient.mk_surjective z) with u hu,
    unfold f₂,
    rw [← hu,ideal.quotient.lift_mk (J.map (ideal.quotient.mk I)) (f₁ I J) (H_proj_J I J)],
    cases (ideal.quotient.mk_surjective u) with v hv,
    unfold f₁,
    rw [← hv,ideal.quotient.lift_mk I (ideal.quotient.mk (I+J)) (left_proj_quot_sum I J)],
    unfold g₂,
    rw ideal.quotient.lift_mk (I+J) (g₁ I J) (H_sum I J),
    unfold g₁,
    rw ring_hom.comp_apply,
  end,
  right_inv :=
  begin
    unfold function.right_inverse function.left_inverse,
    intro z,
    cases (ideal.quotient.mk_surjective z) with u hu,
    rw ← hu,
    unfold g₂,
    rw ideal.quotient.lift_mk (I+J) (g₁ I J) (H_sum I J),
    unfold g₁,
    rw ring_hom.comp_apply,
    unfold f₂,
    rw ideal.quotient.lift_mk (J.map (ideal.quotient.mk I)) (f₁ I J) (H_proj_J I J),
    unfold f₁,
    rw ideal.quotient.lift_mk I (ideal.quotient.mk (I+J))  (left_proj_quot_sum I J),
  end
  ,
  map_mul' := ring_hom.map_mul _,
  map_add' := ring_hom.map_add _ }

[Eric Wieser]

A general comment: in mathlib sum in a lemma name refers to an n-ary sum, not the binary addition you use there which mathlib calls add.

[Paul Lezeau]

Ah thanks that's good to know, I'll edit the names of the lemmas !

[Eric Wieser]

Here's a much shorter way to close your last example:

-- this should maybe be in mathlib
/-- Any two ring homs out of a quotient are equal if their composition with quotient.mk is equal -/
@[ext]
lemma ideal.quotient.ring_hom_ext {S} [semiring S] (f g : I.quotient →+* S)
  (h : f.comp (ideal.quotient.mk I) = g.comp (ideal.quotient.mk I)) : f = g :=
begin
  ext x,
  obtain ⟨u, rfl⟩ := ideal.quotient.mk_surjective x,
  exact (ring_hom.congr_fun h u : _),
end

-- Then f₂ and g₂ are inverse isomorphisms
example : (J.map (ideal.quotient.mk I)).quotient ≃+* (I + J).quotient :=
ring_equiv.of_hom_inv (f₂ I J) (g₂ I J) (by { ext z, refl }) (by { ext z, refl })

[Eric Wieser]

Your first two lemmas can be golfed slightly be removing the intro - if your goal state has a → in it, and the first line of your proof is an intro, then you should have used a : instead of a →:

-- as mentioned above these should have `add` not `sum` in their names.
def left_proj_quot_sum (x : R) (hx : x ∈ I) : ideal.quotient.mk (I+J) x = 0 :=
ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_left hx)

def right_proj_quot_sum (x : R) (hx : x ∈ J) : ideal.quotient.mk (I+J) x = 0 :=
ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_right hx)

[Paul Lezeau]

Eric Wieser said:

Here's a much shorter way to close your last example:

-- this should maybe be in mathlib
/-- Any two ring homs out of a quotient are equal if their composition with quotient.mk is equal -/
@[ext]
lemma ideal.quotient.ring_hom_ext {S} [semiring S] (f g : I.quotient →+* S)
  (h : f.comp (ideal.quotient.mk I) = g.comp (ideal.quotient.mk I)) : f = g :=
begin
  ext x,
  obtain ⟨u, rfl⟩ := ideal.quotient.mk_surjective x,
  exact (ring_hom.congr_fun h u : _),
end

-- Then f₂ and g₂ are inverse isomorphisms
example : (J.map (ideal.quotient.mk I)).quotient ≃+* (I + J).quotient :=
ring_equiv.of_hom_inv (f₂ I J) (g₂ I J) (by { ext z, refl }) (by { ext z, refl })

Ah, I didn't know about the ext tactic, thanks a lot for showing me that !

[Paul Lezeau]

Eric Wieser said:

Your first two lemmas can be golfed slightly be removing the intro - if your goal state has a → in it, and the first line of your proof is an intro, then you should have used a : instead of a →:

-- as mentioned above these should have `add` not `sum` in their names.
def left_proj_quot_sum (x : R) (hx : x ∈ I) : ideal.quotient.mk (I+J) x = 0 :=
ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_left hx)

def right_proj_quot_sum (x : R) (hx : x ∈ J) : ideal.quotient.mk (I+J) x = 0 :=
ideal.quotient.eq_zero_iff_mem.2 (ideal.mem_sup_right hx)

I've noticed a few other of my lemmas have a similar issue, I'll make the relevant modifications

[Alex J. Best]

Unfold's are quite often not necessary in a proof, while they are useful to see what's going on and what you want to do next of course, it can make proofs more readable / short by removing them after, so I'd recommend trying to see which ones can be removed. Doing this you can combine some rewrites onto one line too when they are only small steps.
Also the tactics tactic#rcases and tactic#rintros can be very helpful when you just want to introduce something and then split it up immediately, definitely worth looking at examples of how they are used in mathlib to see some of the tricks :smile:.

[Alex J. Best]

For example in_ker_proj_to_sum_left can be proved with:

lemma in_ker_proj_to_sum_left : I.map(ideal.quotient.mk(I+J)) = ⊥ :=
begin
  simp_rw [ideal.map, ideal.span_eq_bot, set.mem_image],
  rintros y ⟨x, hx, rfl⟩,
  exact left_proj_quot_sum I J x hx,
end

[Yaël Dillies]

rintro is a synonym of rintros and obtain makes more semantical sense than rcases when you obtain an object and its property from an exists for example.

[Paul Lezeau]

Thanks a lot for the advice ! I've been trying to expand the repertoire of tactics I know how to use so I'll try and have a go at using those !

[Paul Lezeau]

On a slightly unrelated issue I've encountered when playing around with the code, say we have two rings $R$ and $S$ which we can prove are equal (although they aren't equal by definition - in my case, this is the quotients (I+J).quotient and (J+I).quotient ). Is there :

1. An easy way of defining the identity isomorphism $R \to S$ ?
2. Given another type $T$, can we get Lean to understand $f : R \to T$ as a map $f : S \to T$ ?

For the first question, the case I am interested in seems to be approachable using quot_equiv_of_eq in ring_theory.ideals.basic, but is there a way to get an explicit description of the isomorphism ? (if possible, I would need to show that the map $x + (I+J) \mapsto x + (J+I)$ is an isomorphism. This could be done by lifting the canonical map $R \to R/(J+I)$ to a map $R/(I+J) \to R/(J+I)$, but I'm sure there's a slicker approach !)

[Eric Wieser]

docs#ideal.quot_equiv_of_eq is indeed what you want

[Eric Wieser]

It looks like it (along with docs#quotient.congr which it builds upon) is missing the lemmas about how it applies

[Paul Lezeau]

Fair enough, thanks !
Out of curiosity, how would we do this for the general case of equal rings $R$ and $S$ ?

[Eric Wieser]

You mean when you can prove R = S?

[Eric Wieser]

That's not enough, to make a ring_equiv you have to prove the ring structures agree too

[Paul Lezeau]

Oh right, of course ! Thanks !
I should be more careful when I use the equal sign, I was getting confused between equality of types and equivalence of ring structures :smile:

[Eric Wieser]

For the case of the quotients you know that the two ring structures are equal by construction

[Kevin Buzzard]

Oh I had never realised that!

[Kevin Buzzard]

The quotient only depends on the underlying equivalence relation which are equal for the two quotients.