Finitely Presented Modules #
Main definition #
Module.FinitePresentation
: A module is finitely presented if it is generated by some finite sets
and the kernel of the presentationRˢ → M
is also finitely generated.
Main results #
Module.finitePresentation_iff_finite
: IfR
is noetherian, then f.p. iff f.g. onR
-modules.
Suppose 0 → K → M → N → 0
is an exact sequence of R
-modules.
Module.finitePresentation_of_surjective
: IfM
is f.p.,K
is f.g., thenN
is f.p.Module.FinitePresentation.fg_ker
: IfM
is f.g.,N
is f.p., thenK
is f.g.Module.finitePresentation_of_ker
: IfN
andK
is f.p., thenM
is also f.p.Module.FinitePresentation.isLocalizedModule_map
: IfM
andN
areR
-modules andM
is f.p., andS
is a submonoid ofR
, thenHom(Mₛ, Nₛ)
is the localization ofHom(M, N)
.
Also the instances finite + free => f.p. => finite are also provided
TODO #
Suppose S
is an R
-algebra, M
is an S
-module. Then
- If
S
is f.p., thenM
isR
-f.p. impliesM
isS
-f.p. - If
S
is both f.p. (as an algebra) and finite (as a module), thenM
isS
-fp implies thatM
isR
-f.p. - If
S
is f.p. as a module, thenS
is f.p. as an algebra. In particular, S
is f.p. as anR
-module iff it is f.p. as an algebra and is finite as a module.
For finitely presented algebras, see Algebra.FinitePresentation
in file Mathlib.RingTheory.FinitePresentation
.
A module is finitely presented if it is finitely generated by some set s
and the kernel of the presentation Rˢ → M
is also finitely generated.
- out : ∃ (s : Finset M), Submodule.span R ↑s = ⊤ ∧ (LinearMap.ker (Finsupp.linearCombination R Subtype.val)).FG
Instances
Equations
- ⋯ = ⋯
A finitely presented module is isomorphic to the quotient of a finite free module by a finitely generated submodule.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯