Playing around with module homomorphisms

Stream: new members

[Jarod Alper]

I'm trying to do basic constructions using module homomorphisms. For instance, if $f: M \to N$ is an $R$-module homomorphism and $N' \hookrightarrow N$ is an injective $R$-module homomorphism, I would like to construct the preimage $M'=f^{-1}(N')$ along with the canonical map $f|_{M'} : M' \to N'$. I was able to construct something using restrict but I feel that there ought to be an easier way.

variable {R : Type*} [CommRing R]
variable {M N N': Type*} [AddCommGroup M] [Module R M] [AddCommGroup N]  [Module R N] [AddCommGroup N']  [Module R N']
variable (f : M →ₗ[R] N)
variable (i : N' →ₗ[R] N)
let N'_sub := LinearMap.range i
let M' := Submodule.comap f N'_sub
have hf_restrictM' :  ∀ m' ∈ M', f m' ∈ N'_sub := by
  simp [M']
let f' := restrict f hf_restrictM'

I was also struggling with identifying $N'$ with the image submodule of $N' \hookrightarrow N$. For instance, is there an easy way to construct the equivalence $N' \to {\rm im}(N')$ which I can use to pass between the two?

More broadly, I would like suggestions for how I'm supposed to find these commands. Github Copilot, Lean Copilot, loogle, and moogle all came up empty.

Are there some examples out there of Lean code in commutative algebra that I can use to learn from? While I've occasionally found the proofs in Mathlib useful, I usually find them very hard to follow because (1) they use unfamiliar commands, (2) are proving foundational stuff I don't care about, or (3) they are code golfed in way that obfuscates the functionality and in some cases even the mathematics. (For an example of (3), I was trying to learn off of the Mathlib implementation of LinearMap.rTensor_surjective, where the proof introduces x, and then confusingly in the very next line redefines x as a preimage of x. What?)

[Johan Commelin]

@loogle Function.Injective, LinearEquiv, Submodule

[loogle]

:search: Submodule.equivMapOfInjective, Submodule.coe_equivMapOfInjective_apply, and 13 more

[Johan Commelin]

I think docs#LinearEquiv.ofInjective is the answer to your first question (the third result of the "13 more" that loogle found).

[Matthew Ballard]

Getting used to the naming convention for declarations is pretty helpful. With that facility, you can really narrow your search. But it does take some time

[Matthew Ballard]

I think @Brendan Seamas Murphy 's recent stuff on regular sequences is a good reference point for commutative algebra. See file#Mathlib/RingTheory/Regular/IsSMulRegular and file#Mathlib/RingTheory/Regular/RegularSequence

[Jarod Alper]

Thanks! That's helpful. I still can't locate a quick command to construct the canonical priemage map $f|_{M'} : M' \to N'$ but I was able (with far too many lines of code) to do it myself using docs#LinearEquiv.ofInjective.

Johan Commelin said:

I think docs#LinearEquiv.ofInjective is the answer to your first question (the third result of the "13 more" that loogle found).

[Jarod Alper]

Matthew Ballard said:

I think Brendan Seamas Murphy 's recent stuff on regular sequences is a good reference point for commutative algebra. See file#Mathlib/RingTheory/Regular/IsSMulRegular and file#Mathlib/RingTheory/Regular/RegularSequence

Thanks. I'll check out Brendan's code.

[Kevin Buzzard]

On mobile right now but there might be something useful in https://github.com/ImperialCollegeLondon/formalising-mathematics-2024, this is supposed to be undergraduate level comprehensible code