English
If P is a finitely presented module and h1: P → M is a linear map, then there exist a finite free module and maps h2, h3 making h1 = h3 ∘ h2.
Русский
Если P — конечно представимый модуль и h1: P → M линейно, то существует конечный свободный модуль и линейные отображения h2, h3 такие, что h1 = h3 ∘ h2.
LaTeX
$$$[Module.Flat\ R\ M] \Rightarrow \forall P, [FinitePresentation\ R\ P], \forall h_1: P \to M, \ Exists k, h_2: P \to R^k, h_3: R^k \to M, h_1 = h_3 \circ h_2$$$
Lean4
/-- Every homomorphism from a finitely presented module to a flat module factors through a finite
free module. -/
@[stacks 058E "only if"]
theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type*} [AddCommGroup P] [Module R P]
[FinitePresentation R P] (h₁ : P →ₗ[R] M) :
∃ (k : ℕ) (h₂ : P →ₗ[R] (Fin k →₀ R)) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂ :=
by
have ⟨_, K, ϕ, hK⟩ := FinitePresentation.exists_fin R P
haveI : Module.Finite R K := Module.Finite.iff_fg.mpr hK
have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
simp_rw [comp_assoc, (LinearMap.exact_subtype_mkQ K).linearMap_comp_eq_zero, comp_zero]
obtain ⟨k, a, y, hay, ha⟩ := exists_factorization_of_comp_eq_zero_of_free this
use k, (K.liftQ a (by rwa [← range_le_ker_iff, Submodule.range_subtype] at ha)) ∘ₗ ϕ, y
apply (cancel_right ϕ.symm.surjective).mp
apply (cancel_right K.mkQ_surjective).mp
simpa [comp_assoc]
