submodule of a submodule

Stream: Is there code for X?

[Scott Morrison]

import algebra.module.submodule

example (R M : Type) [ring R] [add_comm_group M] [module R M]
  (A : submodule R M) (B : submodule R A) :
  submodule R M := sorry -- B as a submodule of M?

[Johan Commelin]

Is it something like B.map A.incl?

[Kevin Buzzard]

For subgroups the morphism is A.subtype

[Eric Wieser]

That seems to be the preferred spelling, given how docs#submodule.equiv_subtype_map is stated

[Terence Tao]

Reviving this thread after two years because I exactly need this construction, but now in Lean4 rather than Lean3. Here I discovered a weird quirk. While the general construction

import Mathlib

example (R M : Type) [Ring R] [AddCommGroup M] [Module R M]
  (A : Submodule R M) (B : Submodule R A) : Submodule R M := B.map A.subtype

works fine, the specialization to the integers does not:

import Mathlib

example (M : Type) [AddCommGroup M] [Module ℤ M]
  (A : Submodule ℤ M) (B : Submodule ℤ A) : Submodule ℤ M := B.map A.subtype
-- failed to synthesize instance SemilinearMapClass (↥A →ₗ[ℤ] M) ?m.2597 (↥A) M

I can fix it, but only with a weird empty application of convert:

import Mathlib

example (M : Type) [AddCommGroup M] [Module ℤ M]
  (A : Submodule ℤ M) (B : Submodule ℤ A) : Submodule ℤ M := by
    convert B.map (σ₁₂ := RingHom.id ℤ) A.subtype
    convert

What is going on here??

[Yury G. Kudryashov]

My guess (not tested): Lean fails to unify universes.

[Yury G. Kudryashov]

I'll try to test it now.

[Terence Tao]

My guess is there is an instance diamond with the SemilinearMapClass on the integers. (Based on recent experience I am inclined to blame almost all weird behavior on instance diamonds.)

[Yury G. Kudryashov]

It looks like there is an instance diamond for Module Int _

[Yury G. Kudryashov]

But convert fixes it because of a Subsingleton instance.

[Terence Tao]

Ugh. Is there a workaround that allows me to express Submodule ℤ M as a term, as opposed to merely giving a proof of existence? Otherwise I can't proceed with my application.

[Yaël Dillies]

You should not be assuming [Module ℤ M]. Lean can already derive it from [AddCommGroup M].

[Terence Tao]

Ah! I got caught in this trap once before.

[Terence Tao]

But wait, there is still a diamond issue here:

import Mathlib

example (M : Type) [AddCommGroup M]
  (A : AddSubgroup M) (B : Submodule ℤ A) : Submodule ℤ M := B.map A.subtype
-- failed to synthesize instance  SemilinearMapClass (↥A →+ M) ?m.2315 (↥A) M

[Yury G. Kudryashov]

You need (A : Submodule Int M)

[Yaël Dillies]

You can get one from docs#AddSubgroup.toIntSubmodule, eg B.map A.toIntSubmodule.subtype

[Yury G. Kudryashov]

Or A.subtype.toIntLinearMap

[Yury G. Kudryashov]

The latter may work a bit better with Lean 4 simp.

[Terence Tao]

OK, to close my argument, I think I need

import Mathlib

example (M : Type) [AddCommGroup M] (A : AddSubgroup M) (B : Submodule ℤ A) : (B:Type) = B.map A.subtype.toIntLinearMap := by
  sorry

but simp didn't offer an obvious way out here.

[Terence Tao]

(or I need some equivalence betweenB and B.map A.subtype.toIntLinearMap, if they aren't identical types).

[Eric Wieser]

That's an equality of types, which is almost never a good idea

[Terence Tao]

Yeah, ignore what I just said, I applied congr way too deep.

[Terence Tao]

What I actually need is

import Mathlib

example (M : Type) [AddCommGroup M] (A : AddSubgroup M) (B : Submodule ℤ A) : B ≃ₗ[ℤ] B.map A.subtype.toIntLinearMap := by
  sorry

but I might be able to do this one on my own.

[Eric Wieser]

This works:

import Mathlib

noncomputable example
    (M : Type) [AddCommGroup M] (A : AddSubgroup M) (B : Submodule ℤ A) :
    (B:Type) ≃ₗ[ℤ] B.map A.subtype.toIntLinearMap :=
  Submodule.equivMapOfInjective _ (by simpa using Subtype.val_injective) _

[Terence Tao]

OK, that worked, and closes my use case. Thanks!

[Eric Wieser]

Or computably:

example
    (M : Type) [AddCommGroup M] (A : AddSubgroup M) (B : Submodule ℤ A) :
    (B:Type) ≃ₗ[ℤ] B.map A.subtype.toIntLinearMap where
  toFun b := ⟨b, b, b.prop, rfl⟩
  map_add' b₁ b₂ := rfl
  map_smul' c b := rfl
  invFun a := ⟨
    ⟨a.val, by obtain ⟨-, a, ha, rfl⟩ := a; exact a.prop⟩,
    by obtain ⟨-, a, ha, rfl⟩ := a; exact ha⟩
  left_inv b := rfl
  right_inv b := rfl