Casting subgroups/submodules

Stream: new members

[Jarod Alper]

Quick question: I have a commutative ring $R$, an $R$-module $M$, and submodules $N \subseteq M$ and $N' \subseteq N$. How do I treat $N'$ as a submodule of $M$? For instance, if I have another submodule $P \subseteq M$, I would like to be able to write $P = N'$.

variable {R : Type*} [CommRing R]
variable {M: Type*} [AddCommGroup M] [Module R M]
variable {N P : Submodule R M}
variable {N' : Submodule R N}

example : P = N' := by
  sorry

[Edward van de Meent]

the way to avoid this entirely would be to rather assume N' : Submodule R M and hN' : N' ≤ N. if that's not possible, you will possibly rather want to talk about docs#Submodule.map combined with docs#Submodule.subtype

[Edward van de Meent]

that should give you N'.map (N.subtype) = P as a statement to prove

[Eric Wieser]

Edward van de Meent said:

the way to avoid this entirely would be to rather assume N' : Submodule R M and hN' : N' ⊆ N. if that's not possible, you will possibly rather want to talk about docs#Submodule.map combined with docs#Submodule.subtype

hN' : N' ≤ N is preferred here

[Jarod Alper]

Edward van de Meent said:

the way to avoid this entirely would be to rather assume N' : Submodule R M and hN' : N' ⊆ N. if that's not possible, you will possibly rather want to talk about docs#Submodule.map combined with docs#Submodule.subtype

In my case, $N'$ is given as the kernel of a map so I can't use your first suggestion. Following your second suggestion, I was able to define the inclusion from N' to N and from N to M, define the composition, and then take the range.

[Jarod Alper]

Eric Wieser said:

hN' : N' ≤ N is preferred here

Yeah, it's silly Lean doesn't recognize N' ⊆ N. There should at least be a linter that recognizes this mistake. I'm sure that I had learned in some Lean tutorials to write N' ≤ N, but I guess I had forgotten and it took me 15 minutes the other day debugging an error to realize that this was the problem.