Finitely Presented Modules

Main definition

• Module.FinitePresentation: A module is finitely presented if it is generated by some finite set s and the kernel of the presentation Rˢ → M is also finitely generated.

Main results

• Module.finitePresentation_iff_finite: If R is Noetherian, then f.p. iff f.g. on R-modules.

Suppose 0 → K → M → N → 0 is an exact sequence of R-modules.

• Module.finitePresentation_of_surjective: If M is f.p., K is f.g., then N is f.p.

• Module.FinitePresentation.fg_ker: If M is f.g., N is f.p., then K is f.g.

• Module.finitePresentation_of_ker: If N and K is f.p., then M is also f.p.

• Module.FinitePresentation.isLocalizedModule_map: If M and N are R-modules and M is f.p., and S is a submonoid of R, then Hom(Mₛ, Nₛ) is the localization of Hom(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

1. If S is f.p., then M is R-f.p. implies M is S-f.p.
2. If S is both f.p. (as an algebra) and finite (as a module), then M is S-fp implies that M is R-f.p.
3. If S is f.p. as a module, then S is f.p. as an algebra. In particular,
4. S is f.p. as an R-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.lean.

class Module.FinitePresentation (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

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

@[instance 100]

instance instFiniteOfFinitePresentation (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [h : Module.FinitePresentation R M] : Module.Finite R M

theorem Module.FinitePresentation.exists_fin (R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [fp : FinitePresentation R M] : ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (x : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG

theorem Module.FinitePresentation.equiv_quotient (R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [FinitePresentation R M] [Small.{v, u} R] : ∃ (L : Type v) (x : AddCommGroup L) (x_1 : Module R L) (K : Submodule R L) (x_2 : M ≃ₗ[R] L ⧸ K), Free R L ∧ Module.Finite R L ∧ K.FG

A finitely presented module is isomorphic to the quotient of a finite free module by a finitely generated submodule.

theorem Module.finitePresentation_of_finite (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [h : Module.Finite R M] : FinitePresentation R M

theorem Module.finitePresentation_iff_finite (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] : FinitePresentation R M ↔ Module.Finite R M

theorem Module.finitePresentation_of_free_of_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Free R M] [Module.Finite R M] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) (hl' : (LinearMap.ker l).FG) : FinitePresentation R N

theorem Module.finitePresentation_of_projective (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [Projective R M] [Module.Finite R M] : FinitePresentation R M

instance instFinitePresentation {R : Type u_1} [Ring R] : Module.FinitePresentation R R

instance instFinitePresentationFinsupp {R : Type u_1} [Ring R] {ι : Type u_2} [Finite ι] : Module.FinitePresentation R (ι →₀ R)

instance instFinitePresentationForall {R : Type u_1} [Ring R] {ι : Type u_2} [Finite ι] : Module.FinitePresentation R (ι → R)

theorem Module.finitePresentation_of_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [h : FinitePresentation R M] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) (hl' : (LinearMap.ker l).FG) : FinitePresentation R N

theorem Module.FinitePresentation.fg_ker {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R M] [h : FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) : (LinearMap.ker l).FG

theorem Module.FinitePresentation.fg_ker_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [FinitePresentation R M] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) : (LinearMap.ker l).FG ↔ FinitePresentation R N

theorem Module.finitePresentation_of_ker {R : Type u_1} {M : Type u_3} {N : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective ⇑l) [FinitePresentation R ↥(LinearMap.ker l)] : FinitePresentation R M

theorem Module.finitePresentation_of_split_exact {R : Type u_2} {M : Type u_4} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_1} [AddCommGroup P] [Module R P] [FinitePresentation R N] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (l : P →ₗ[R] N) (hl : g ∘ₗ l = LinearMap.id) (hf : Function.Injective ⇑f) (H : Function.Exact ⇑f ⇑g) : FinitePresentation R M

Given a split exact sequence 0 → M → N → P → 0 with N finitely presented, then M is also finitely presented.

theorem Module.finitePresentation_of_projective_of_exact {R : Type u_2} {M : Type u_4} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : Type u_1} [AddCommGroup P] [Module R P] [FinitePresentation R N] [Projective R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (H : Function.Exact ⇑f ⇑g) : FinitePresentation R M

Given an exact sequence 0 → M → N → P → 0 with N finitely presented and P projective, then M is also finitely presented.

theorem Module.FinitePresentation.of_equiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) [FinitePresentation R M] : FinitePresentation R N

theorem LinearEquiv.finitePresentation_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.FinitePresentation R M ↔ Module.FinitePresentation R N

@[instance 900]

instance Module.FinitePresentation.of_subsingleton {R : Type u_2} (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Subsingleton M] : FinitePresentation R M

instance Module.FinitePresentation.prod {R : Type u_1} (M : Type u_2) (N : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [FinitePresentation R M] [FinitePresentation R N] : FinitePresentation R (M × N)

instance Module.FinitePresentation.pi {R : Type u_3} [Ring R] {ι : Type u_1} (M : ι → Type u_2) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), FinitePresentation R (M i)] [Finite ι] : FinitePresentation R ((i : ι) → M i)

theorem Module.FinitePresentation.trans (R : Type u_2) (M : Type u_3) [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_1) [CommRing S] [Algebra R S] [Module S M] [IsScalarTower R S M] [FinitePresentation R S] [FinitePresentation S M] : FinitePresentation R M

instance instFinitePresentationTensorProduct {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {A : Type u_1} [CommRing A] [Algebra R A] [Module.FinitePresentation R M] : Module.FinitePresentation A (TensorProduct R A M)

theorem FinitePresentation.of_isBaseChange {R : Type u_2} {M : Type u_4} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {A : Type u_1} [CommRing A] [Algebra R A] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) (h : IsBaseChange A f) [Module.FinitePresentation R M] : Module.FinitePresentation A N

instance instFinitePresentationLocalizationLocalizedModule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (S : Submonoid R) [Module.FinitePresentation R M] : Module.FinitePresentation (Localization S) (LocalizedModule S M)

theorem Module.FinitePresentation.exists_lift_of_isLocalizedModule {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup N'] [Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f] [h : FinitePresentation R M] (g : M →ₗ[R] N') : ∃ (h : M →ₗ[R] N) (s : ↥S), f ∘ₗ h = s • g

theorem Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule {R : Type u_1} {M : Type u_2} {N : Type u_3} {N' : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup N'] [Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f] [hM : Module.Finite R M] (g₁ g₂ : M →ₗ[R] N) (h : f ∘ₗ g₁ = f ∘ₗ g₂) : ∃ (s : ↥S), s • g₁ = s • g₂

theorem exists_bijective_map_powers {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] [Module.Finite R M] [Module.FinitePresentation R N] (l : M →ₗ[R] N) (hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)) : ∃ r ∈ S, ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l)

Let M be a finite R-module, and N be a finitely presented R-module. If l : M →ₗ[R] N is a linear map whose localization at S : Submonoid R is bijective, then l is already bijective under the localization at some r ∈ S.

theorem Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] [FinitePresentation R M] [FinitePresentation R N] (l : M' ≃ₗ[R] N') : ∃ (r : R) (hr : r ∈ S) (l' : LocalizedModule (Submonoid.powers r) M ≃ₗ[Localization (Submonoid.powers r)] LocalizedModule (Submonoid.powers r) N), LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯

Let M N be a finitely presented R-modules. Any Mₛ ≃ₗ[R] Nₛ between the localizations at S : Submonoid R can be lifted to an isomorphism between Mᵣ ≃ₗ[R] Nᵣ for some r ∈ S.

instance Module.FinitePresentation.isLocalizedModule_map {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] [FinitePresentation R M] : IsLocalizedModule S (IsLocalizedModule.map S f g)

instance Module.FinitePresentation.isLocalizedModule_mapExtendScalars {R : Type u_4} {M : Type u_5} {N : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) {M' : Type u_1} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {N' : Type u_2} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g] (Rₛ : Type u_3) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [Module Rₛ N'] [IsScalarTower R Rₛ M'] [IsScalarTower R Rₛ N'] [IsLocalization S Rₛ] [FinitePresentation R M] : IsLocalizedModule S (IsLocalizedModule.mapExtendScalars S f g Rₛ)

instance instIsLocalizedModuleLinearMapIdLocalizationLocalizedModuleMapOfFinitePresentation {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [Module.FinitePresentation R M] : IsLocalizedModule S (LocalizedModule.map S)

noncomputable def Module.FinitePresentation.linearEquivMap {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] : LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[R] LocalizedModule S N

Let M be a finitely presented R-module, N a R-module, S : Submonoid R. The linear equivalence between the M →ₗ[R] N localized at S and LocalizedModule S M →ₗ[R] LocalizedModule S N

Equations

• One or more equations did not get rendered due to their size.

theorem Module.FinitePresentation.linearEquivMap_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] (f : M →ₗ[R] N) : (linearEquivMap S) ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) = (IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f

@[simp]

theorem Module.FinitePresentation.linearEquivMap_symm_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] (f : M →ₗ[R] N) : (linearEquivMap S).symm ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)) f) = (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f

noncomputable def Module.FinitePresentation.linearEquivMapExtendScalars {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] : LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

Let M be a finitely presented R-module, N a R-module, S : Submonoid R. The linear equivalence between the M →ₗ[R] N localized at S and LocalizedModule S M →ₗ[Localization S] LocalizedModule S N

Equations

• One or more equations did not get rendered due to their size.

theorem Module.FinitePresentation.linearEquivMapExtendScalars_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] (f : M →ₗ[R] N) : (linearEquivMapExtendScalars S) ((LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f) = (IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) (Localization S)) f

@[simp]

theorem Module.FinitePresentation.linearEquivMapExtendScalars_symm_apply {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) [FinitePresentation R M] (f : M →ₗ[R] N) : (linearEquivMapExtendScalars S).symm ((IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) (Localization S)) f) = (LocalizedModule.mkLinearMap S (M →ₗ[R] N)) f