English
If M and N are finitely presented, then their product M × N is finitely presented.
Русский
Если M и N конечнопредставимы, то их произведение M × N тоже конечнопредставимо.
LaTeX
$$$[Module.FinitePresentation R M][Module.FinitePresentation R N] \Rightarrow Module.FinitePresentation R (M \times N)$$$
Lean4
instance prod [Module.FinitePresentation R M] [Module.FinitePresentation R N] : Module.FinitePresentation R (M × N) :=
by
have hf : Function.Surjective (LinearMap.fst R M N) := LinearMap.fst_surjective
have : FinitePresentation R ↥(LinearMap.ker (LinearMap.fst R M N)) :=
by
rw [LinearMap.ker_fst]
exact .of_equiv (LinearEquiv.ofInjective (LinearMap.inr R M N) LinearMap.inr_injective)
apply Module.finitePresentation_of_ker (.fst R M N) hf
