If I,J,K,L are ideals of a comm ring R s.t. I ≅ J and K ≅ L as R-modules, then IK ≅ JL as R-modules.

ideal_prod_iso.lean

import ring_theory.ideal.operations
open submodule

variables {R M N : Type*} [comm_ring R] (I J K L : ideal R)
  [add_comm_group M] [add_comm_group N] [module R M] [module R N]
  {M₁ M₂ : submodule R M} (h : M₁ = M₂)

def eq.linear_map : M₁ →ₗ[R] M₂ :=
{ to_fun := λ x, ⟨x, h ▸ x.2⟩,
  map_add' := λ x y, rfl,
  map_smul' := λ r x, rfl }

def eq.linear_equiv : M₁ ≃ₗ[R] M₂ :=
{ inv_fun := h.symm.linear_map,
  left_inv := λ x, by { ext, refl },
  right_inv := λ x, by { ext, refl },
  .. h.linear_map }

lemma mem_submodule_submodule (M' : submodule R M) (M'' : submodule R M') (x : M') :
  x ∈ M'' ↔ x.1 ∈ map M'.subtype M'' :=
⟨λ h, ⟨x,h,rfl⟩, λ ⟨y,hy,he⟩, by { convert hy, ext, exact he.symm }⟩

lemma mul_eq_smul : (I * K : ideal R) = map K.subtype (I • ⊤ : submodule R K) :=
begin
  rw map_smul'', exact le_antisymm
    (ideal.mul_le.2 (λ r hr s hs, ideal.mul_mem_mul hr ⟨⟨s,hs⟩, trivial, rfl⟩))
    (smul_le.2 (λ r hr x ⟨⟨y,hy⟩,_,he⟩,
      ideal.mul_mem_mul hr (by { dsimp at he, exact he.subst hy }))),
end

def mul_equiv_smul : (I * K : ideal R) ≃ₗ[R] (I • ⊤ : submodule R K) :=
{ to_fun := λ x, ⟨⟨x.1, ideal.mul_le_left x.2⟩,
    by { rw [mem_submodule_submodule, ← mul_eq_smul], exact x.2 }⟩,
  inv_fun := λ x, ⟨x.1, by { erw [mul_eq_smul, ← mem_submodule_submodule], exact x.2 }⟩,
  map_add' := λ x y, rfl,
  map_smul' := λ r x, rfl,
  left_inv := λ x, by { ext, refl },
  right_inv := λ x, by { ext, refl } }

def smul_linear_map (f : M →ₗ[R] N) : (I • ⊤ : submodule R M) →ₗ[R] (I • ⊤ : submodule R N) :=
{ to_fun := λ x, ⟨f x.1,
    by { apply smul_mono_right le_top, convert mem_map_of_mem x.2, rw map_smul'' }⟩,
  map_add' := λ x y, by { ext, apply f.map_add },
  map_smul' := λ r x, by { ext, apply f.map_smul } }

variables {K L} (f : I →ₗ[R] J) (g : K →ₗ[R] L)

def mul_linear_map : (I * K : ideal R) →ₗ[R] (I * L : ideal R) :=
(mul_equiv_smul I L).symm.to_linear_map.comp
  ((smul_linear_map I g).comp (mul_equiv_smul I K).to_linear_map)

@[simp] lemma mul_linear_map_app (x : I * K) :
  ↑(mul_linear_map I g x) = (g ⟨x.1, ideal.mul_le_left x.2⟩).1 := rfl

lemma mul_linear_map_app_mul (i : I) (k : K) :
  (mul_linear_map I g ⟨i * k, mul_mem_mul i.2 k.2⟩).1 = i * g k :=
begin
  dsimp [mul_linear_map, mul_equiv_smul, smul_linear_map],
  have : i.1 • k = ⟨i * k, _⟩, ext, refl,
  erw [← this, g.map_smul], refl,
end

def mul_linear_equiv (g : K ≃ₗ[R] L) : (I * K : ideal R) ≃ₗ[R] (I * L : ideal R) :=
{ inv_fun := mul_linear_map I g.symm.to_linear_map,
  left_inv := λ ⟨x,hx⟩,
    by { ext, erw ← subtype.ext_iff.1 (g.left_inv ⟨x, ideal.mul_le_left hx⟩), simp },
  right_inv := λ ⟨x,hx⟩,
    by { ext, erw ← subtype.ext_iff.1 (g.right_inv ⟨x, ideal.mul_le_left hx⟩), simp },
  .. mul_linear_map I g.to_linear_map }

variables {I J}

def mul₂_linear_map : (I * K : ideal R) →ₗ[R] (J * L : ideal R) :=
(mul_comm L J).linear_map.comp $ (mul_linear_map L f).comp $
(mul_comm I L).linear_map.comp $ mul_linear_map I g

def mul₂_linear_equiv (f : I ≃ₗ[R] J) (g : K ≃ₗ[R] L) : (I * K : ideal R) ≃ₗ[R] (J * L : ideal R) :=
(mul_linear_equiv I g).trans $ (mul_comm I L).linear_equiv.trans $
(mul_linear_equiv L f).trans $ (mul_comm L J).linear_equiv

lemma mul₂_linear_map_app_mul (i : I) (k : K) :
  (mul₂_linear_map f g ⟨i * k, mul_mem_mul i.2 k.2⟩).1 = f i * g k :=
begin
  rw mul₂_linear_map, convert mul_linear_map_app_mul L f (g k) i using 1, swap, apply mul_comm,
  rw eq.linear_map, dsimp, congr, convert mul_linear_map_app_mul I g i k using 1, apply mul_comm,
end

lemma mul₂_linear_equiv_app_mul (f : I ≃ₗ[R] J) (g : K ≃ₗ[R] L) (i : I) (k : K) :
  (mul₂_linear_equiv f g ⟨i * k, mul_mem_mul i.2 k.2⟩).1 = f i * g k :=
by convert mul₂_linear_map_app_mul f.to_linear_map g.to_linear_map i k