Skip to content

[Merged by Bors] - fix(RingTheory): correct misnamed theorem #39741

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
vlad902 wants to merge 2 commits into from
Closed

[Merged by Bors] - fix(RingTheory): correct misnamed theorem #39741

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d3ec009
fix(RingTheory): correct misnamed theorem
vlad902 May 23, 2026
f88a660
dont confuse the declaration linter
vlad902 May 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions Mathlib/RingTheory/Flat/EquationalCriterion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ that $x = y \circ a$ and $a \circ f = 0$. We recover the usual equational criter
$K = R$ and $N = R^l$. This is used in the proof of Lazard's theorem.

We conclude that every linear map from a finitely presented module to a flat module factors
through a finite free module (`Module.Flat.exists_factorization_of_isFinitelyPresented`), and
through a finite free module (`Module.Flat.exists_factorization_of_finitePresentation`), and
every finitely presented flat module is projective (`Module.Flat.projective_of_finitePresentation`).

## References
Expand Down Expand Up @@ -268,9 +268,9 @@ theorem exists_factorization_of_comp_eq_zero_of_free [Flat R M] {K N : Type*} [A
/-- 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]
theorem exists_factorization_of_finitePresentation [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
∃ (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 := .of_fg hK
have : (h₁ ∘ₗ ϕ.symm ∘ₗ K.mkQ) ∘ₗ K.subtype = 0 := by
Expand All @@ -281,9 +281,12 @@ theorem exists_factorization_of_isFinitelyPresented [Flat R M] {P : Type*} [AddC
apply (cancel_right K.mkQ_surjective).mp
simpa [comp_assoc]

@[deprecated (since := "2026-05-23")]
alias exists_factorization_of_isFinitelyPresented := exists_factorization_of_finitePresentation

@[stacks 00NX "(1) → (2)"]
theorem projective_of_finitePresentation [Flat R M] [FinitePresentation R M] : Projective R M :=
have ⟨_, f, g, eq⟩ := exists_factorization_of_isFinitelyPresented (.id (R := R) (M := M))
have ⟨_, f, g, eq⟩ := exists_factorization_of_finitePresentation (.id (R := R) (M := M))
.of_split f g eq.symm

end Module.Flat
Loading