Nakayama: Change assumption or search for lemma?

Stream: new members

[Jack J Garzella]

Hi, I'm trying to work on proving a simple corollary of Nakayama's lemma (tag 07RC, part 8). I've completed what I at first considered to be the "nontrivial" part of the proof (applying Nakayama's lemma), but am getting bogged down by something I first thought would be "elementary" (showing that if N is a submodule of M which is equal to ⊤ mod I, then N ⊔ (I • ⊤) = ⊤ as M-submodules).

In particular, I wanted to use submodule.map_mkq_eq_top to show this. However, the goal that I get once applying this lemma is about R-modules, not R/I-modules, and it's not clear to me what lemma about map or comap would solve this, seeing as the implication that I want (these things are equal as R/I-modules, so they must be equal as R-modules) is not true in general.

At this point, I'm not sure if I'm formalizing the assumption in a non-optimal way, or if I'm missing a lemma somewhere in mathlib about map and comap and quotient modules. Can someone give me some tips about how to proceed?

Here is my #mwe:

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

set_option pp.coercions true

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

open ideal

lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
(hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (S : finset M)
(hIM : submodule.span (R ⧸ I) (submodule.quotient.mk '' ↑S) =
(⊤ : submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M)))))
: (submodule.span R ↑S = (⊤ : submodule R M)) :=
begin
  let N := (submodule.span R ↑S),
  let MM := (⊤ : submodule R M),
  suffices hh : N ⊔ (I • MM) = MM,
    have htop : N ⊔ MM = MM,
      by simp only [eq_self_iff_true, sup_top_eq],
    have hItop : N ⊔ (I • MM) = N ⊔ MM,
      by exact eq.trans hh htop.symm,
    have hIineqtop : N ⊔ MM ≤ N ⊔ I • MM,
      by simp only [eq_self_iff_true, sup_top_eq, hItop, top_le_iff],
    have nakayama : I • MM ≤ N,
      apply submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot hM hIjac hIineqtop,
    have : N = N ⊔ (I • MM),
      by simp [nakayama],
    exact eq.trans this hh,
  have sup_symm : (I • MM) ⊔ N = N ⊔ (I • MM),
    by exact sup_comm,
  rw [←sup_symm],
  rw [←submodule.map_mkq_eq_top (I • MM) N],
  sorry,
  -- rw [←hIM], -- I think this should be somewhere in here
end

[Adam Topaz]

Do we have a standard way to speak about $M/IM$ as an $R/I$-module where $M$ is an $R$-module?

[Johan Commelin]

You could certainly consider restating hIM as the statement that is your goal at that sorry.

[Johan Commelin]

But nevertheless, we should have a way to go back and forth between R-submodules and R/I-submodules.

[Adam Topaz]

If you consider them as R-modules, it's easy:

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

set_option pp.coercions true

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

example (N : submodule R M) (I : ideal R)
  (h : (N.map (submodule.mkq (I • (⊤ : submodule R M)))) =
    (⊤ : submodule R (M ⧸ (I • (⊤ : submodule R M))))) :
  (I • ⊤) ⊔ N = ⊤ :=
begin
  simpa only [submodule.map_mkq_eq_top] using h,
end

[Adam Topaz]

Presumably we should also have this

def foobar (I : ideal R) : submodule R (M ⧸ (I • (⊤ : submodule R M))) ≃o
  submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M))) :=
{ to_fun := λ N, ⟨N,λ _ _, N.add_mem, N.zero_mem, by { rintro ⟨c⟩ x hx, exact N.smul_mem c hx}⟩,
  inv_fun := λ N, ⟨N, λ _ _, N.add_mem, N.zero_mem, λ c x hx, N.smul_mem ↑c hx⟩,
  left_inv := λ _, by ext ; refl,
  right_inv := λ _, by ext ; refl,
  map_rel_iff' := λ a b, iff.refl _ }

[Adam Topaz]

Well, this was a good reminder for me just how annoying lean can be. There's a lot of room for refactoring in this proof (and I abused definitional equalities with impunity). I hope it helps anyway!

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

set_option pp.coercions true
open_locale big_operators

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

def foobar (I : ideal R) : submodule R (M ⧸ (I • (⊤ : submodule R M))) ≃o
  submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M))) :=
{ to_fun := λ N, ⟨N,λ _ _, N.add_mem, N.zero_mem, by { rintro ⟨c⟩ x hx, exact N.smul_mem c hx}⟩,
  inv_fun := λ N, ⟨N, λ _ _, N.add_mem, N.zero_mem, λ c x hx, N.smul_mem ↑c hx⟩,
  left_inv := λ _, by ext ; refl,
  right_inv := λ _, by ext ; refl,
  map_rel_iff' := λ a b, iff.refl _ }

--variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

open ideal

lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
(hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (S : finset M)
(hIM : submodule.span (R ⧸ I) (submodule.quotient.mk '' ↑S) =
(⊤ : submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M)))))
: (submodule.span R ↑S = (⊤ : submodule R M)) :=
begin
  let N := (submodule.span R ↑S),
  let MM := (⊤ : submodule R M),
  suffices hh : N ⊔ (I • MM) = MM,
    have htop : N ⊔ MM = MM,
      by simp only [eq_self_iff_true, sup_top_eq],
    have hItop : N ⊔ (I • MM) = N ⊔ MM,
      by exact eq.trans hh htop.symm,
    have hIineqtop : N ⊔ MM ≤ N ⊔ I • MM,
      by simp only [eq_self_iff_true, sup_top_eq, hItop, top_le_iff],
    have nakayama : I • MM ≤ N,
      apply submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot hM hIjac hIineqtop,
    have : N = N ⊔ (I • MM),
      by simp [nakayama],
    exact eq.trans this hh,
  have sup_symm : (I • MM) ⊔ N = N ⊔ (I • MM),
    by exact sup_comm,
  rw [←sup_symm],
  rw [←submodule.map_mkq_eq_top (I • MM) N],
  apply_fun foobar I,
  rw order_iso.map_top,
  convert hIM using 1,
  ext, dsimp only [foobar, N],
  split,
  { dsimp, rintro ⟨m,hm,rfl⟩,
    apply submodule.span_induction hm,
    { intros x hx, apply submodule.subset_span, use [x,hx] },
    { simp },
    { intros x y hx hy, rw submodule.quotient.mk_add, apply submodule.add_mem _ hx hy },
    { intros a x hx, rw submodule.quotient.mk_smul,
      exact submodule.smul_mem _ (submodule.quotient.mk a) hx } },
  { intros h, rw finsupp.mem_span_iff_total at h, obtain ⟨l,hx⟩ := h,
    change x ∈ submodule.map (I • MM).mkq (submodule.span R ↑S),
    let σ : R⧸I → R := λ r, r.out',
    let π : (S : set M) → (submodule.quotient.mk '' (S : set M) : set (M ⧸ (I • MM))) :=
      set.image_factorization _ _,
    have hπ : function.surjective π := set.surjective_onto_image,
    let τ : submodule.quotient.mk '' (S : set M) → S := λ t, (hπ t).some,
    have hτ : ∀ s, π (τ s) = s := λ s, (hπ s).some_spec,
    let x' : M := ∑ s in l.support, σ (l s) • (τ s),
    refine ⟨x', _, _⟩,
    { change x' ∈ submodule.span R (S : set M),
      apply @submodule.sum_mem R M S _ _ _ _ ⊤ (λ s, σ (l ⟨_,s, s.2, rfl⟩) • s) _,
      intros c hc, dsimp,
      apply (submodule.span R (S : set M)).smul_mem (σ (l _)),
      apply submodule.subset_span,
      exact c.2 },
    { dsimp only [x'], rw ← hx,
      rw linear_map.map_sum,
      change _ = ∑ t in l.support, _,
      fapply finset.sum_bij (λ a _, a) (λ _ h, h) _ (λ a b ha hb h, h),
      { intros b hb, refine ⟨b, hb, rfl⟩ },
      { intros a ha, dsimp,
        have : submodule.quotient.mk ↑(τ a) = (a : M ⧸ I • MM),
        { exact congr_arg subtype.val (hτ a) },
        rw this, clear this,
        change (quotient.mk' (σ (l a)) : R ⧸ I) • ↑a = _,
        dsimp only [σ],
        rw quotient.out_eq' } } }
end

[Adam Topaz]

I think the right approach with this is to develop some further api that lets us consider an $R$-module $M$ as a module over $R/I$ whenever $I$ is contained in the annihilator.

[Adam Topaz]

Here's a more general result (without finiteness of S) which avoids spans (which was the most annoying part of the proof above):

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

set_option pp.coercions true
open_locale big_operators

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]


def submodule.map_mod
  (I : ideal R) (M' : Type*) [add_comm_group M'] [module (R ⧸ I) M']
  (N : submodule R M) (f : M →ₛₗ[ideal.quotient.mk I] M') :
  submodule (R ⧸ I) M' :=
{ smul_mem' := begin
    rintros ⟨c⟩ x ⟨y,h1,h2⟩, dsimp at h2,
    dsimp,
    refine ⟨(c • y), N.smul_mem _ h1, by simp [h2]⟩,
  end,
  ..(N.to_add_subgroup.map f.to_add_monoid_hom) }

def module.mkqₛₗ (I : ideal R) : M →ₛₗ[ideal.quotient.mk I] M ⧸ (I • (⊤ : submodule R M)) :=
{ ..(submodule.mkq _) }

def module.idqₛₗ (I : ideal R) : M ⧸ (I • (⊤ : submodule R M)) →ₛₗ[ideal.quotient.mk I]
  M ⧸ (I • (⊤ : submodule R M)) :=
{ ..(linear_map.id : (M ⧸ (I • (⊤ : submodule R M))) →ₗ[R] _) }

@[simps apply]
def foobar (I : ideal R) : submodule R (M ⧸ (I • (⊤ : submodule R M))) ≃o
  submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M))) :=
{ to_fun := λ N, N.map_mod _ _ $ module.idqₛₗ _,
  inv_fun := λ N, ⟨N, λ _ _, N.add_mem, N.zero_mem, λ c x hx, N.smul_mem ↑c hx⟩,
  left_inv := λ N, by { ext t, dsimp, change _ ∈ id '' _ ↔ _, simp, },
  right_inv := λ _, by { ext t, dsimp, change _ ∈ id '' _ ↔ _, simp, },
  map_rel_iff' := begin
    intros a b,
    dsimp,
    let a' : set (M ⧸ (I • (⊤ : submodule R M))) := a,
    let b' : set (M ⧸ (I • (⊤ : submodule R M))) := b,
    change id '' a' ≤ id '' b' ↔ a ≤ b,
    simp,
  end }

lemma foo (I : ideal R) (N : submodule R M) :
  submodule.map_mod I (M ⧸ I • (⊤ : submodule R M))
    (submodule.map (submodule.mkq (I • (⊤ : submodule R M))) N) (module.idqₛₗ I) =
  submodule.map_mod I (M ⧸ I • (⊤ : submodule R M)) N (module.mkqₛₗ I) :=
begin
  apply set_like.coe_injective,
  change id '' _ = _,
  simp,
  refl,
end

open ideal

lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
(hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (N : submodule R M)
(hIM : submodule.map_mod I _ N (module.mkqₛₗ I) = ⊤) : N = (⊤ : submodule R M) :=
begin
  let MM : submodule R M := ⊤,
  suffices hh : N ⊔ (I • MM) = MM,
  { have nak : I • MM ≤ N,
    { apply submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot hM hIjac _,
      simpa only [eq_self_iff_true, sup_top_eq, top_le_iff] },
    rw [(show N = N ⊔ (I • MM), by simp [nak]), hh] },
  rw [sup_comm, ← submodule.map_mkq_eq_top (I • MM) N],
  apply_fun foobar _,
  rw order_iso.map_top,
  convert hIM,
  dsimp,
  rw foo,
end

[Kevin Buzzard]

That looks much better :-)

[Adam Topaz]

Oh, it looks like docs#submodule.map already uses semilinear maps. So the above can be refactored to just use that

[Adam Topaz]

okay, cleaned up a bit:

import ring_theory.nakayama
import ring_theory.jacobson_ideal
import algebra.module.torsion

set_option pp.coercions true
open_locale big_operators

variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]

variable (M)
def submodule.mkqₛₗ (I : ideal R) : M →ₛₗ[ideal.quotient.mk I] M ⧸ (I • (⊤ : submodule R M)) :=
{ ..(submodule.mkq _) }

def submodule.idqₛₗ (I : ideal R) : M ⧸ (I • (⊤ : submodule R M)) →ₛₗ[ideal.quotient.mk I]
  M ⧸ (I • (⊤ : submodule R M)) :=
{ ..(linear_map.id : (M ⧸ (I • (⊤ : submodule R M))) →ₗ[R] _) }

@[simps apply]
def foobar (I : ideal R) : submodule R (M ⧸ (I • (⊤ : submodule R M))) ≃o
  submodule (R ⧸ I) (M ⧸ (I • (⊤ : submodule R M))) :=
{ to_fun := λ N, N.map (submodule.idqₛₗ M I),
  inv_fun := λ N, ⟨N, λ _ _, N.add_mem, N.zero_mem, λ c x hx, N.smul_mem ↑c hx⟩,
  left_inv := λ N, by { ext t, change _ ∈ id '' _ ↔ _, simp, },
  right_inv := λ _, by { ext t, change _ ∈ id '' _ ↔ _, simp, },
  map_rel_iff' := begin
    intros a b,
    dsimp,
    let a' : set (M ⧸ (I • (⊤ : submodule R M))) := a,
    let b' : set (M ⧸ (I • (⊤ : submodule R M))) := b,
    change id '' a' ≤ id '' b' ↔ a ≤ b,
    simp,
  end }

lemma foo (I : ideal R) (N : submodule R M) :
  (N.map $ submodule.mkq (I • (⊤ : submodule R M))).map (submodule.idqₛₗ M I) =
  N.map (submodule.mkqₛₗ M I) :=
begin
  apply set_like.coe_injective,
  change id '' _ = _,
  simp,
  refl,
end

open ideal

lemma generate_of_quotient_generate_of_le_jacobson (I : ideal R)
(hM : (⊤ : submodule R M).fg) (hIjac : I ≤ jacobson ⊥) (N : submodule R M)
(hIM : submodule.map (submodule.mkqₛₗ M I) N = ⊤) : N = (⊤ : submodule R M) :=
begin
  let MM : submodule R M := ⊤,
  suffices hh : N ⊔ (I • MM) = MM,
  { have nak : I • MM ≤ N,
    { apply submodule.smul_sup_le_of_le_smul_of_le_jacobson_bot hM hIjac _,
      simpa only [eq_self_iff_true, sup_top_eq, top_le_iff] },
    rw [(show N = N ⊔ (I • MM), by simp [nak]), hh] },
  rw [sup_comm, ← submodule.map_mkq_eq_top (I • MM) N],
  apply_fun foobar _ _,
  rw order_iso.map_top,
  convert hIM,
  dsimp,
  rw foo,
end

[Eric Wieser]

Isn't the reverse direction of foobar docs#submodule.restrict_scalara?

[Jack J Garzella]

Adam Topaz said:

Here's a more general result (without finiteness of S) which avoids spans (which was the most annoying part of the proof above):

What was your thought process in choosing to phrase it this way?

I feel like I often phrase lemmas in a way that makes it much harder to prove, but I can't tell the difference.

[Ruben Van de Velde]

At least part of this will be "experience"

[Adam Topaz]

yeah, experience, but in this case it was also a matter of replacing an ideal written in terms of generators by just an ideal, which is something that is perfectly natural from a mathematical perspective (regardless of the formalization)

[Jack J Garzella]

Perhaps some of the intuition is we don't want to talk about elements if possible unless all we're doing some sort of computation with equations using ring or such?

[Adam Topaz]

Sure, that's one point. The theorem is some statement about the lattice of ideals in some ring (and uses the language of lattices exclusively), so it's natural to try to stick to this language as much as possible.

[Adam Topaz]

It's hard to formalize intuition :)