Documentation

Mathlib.Algebra.Module.FinitePresentation

Finitely Presented Modules #

Main definition #

Main results #

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

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.

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

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.

Instances
    theorem Module.FinitePresentation.out {R : Type u_1} {M : Type u_2} :
    ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} [self : Module.FinitePresentation R M], ∃ (s : Finset M), Submodule.span R s = (LinearMap.ker (Finsupp.linearCombination R Subtype.val)).FG
    @[instance 100]
    Equations
    • =
    theorem Module.FinitePresentation.equiv_quotient (R : Type u) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [fp : Module.FinitePresentation R M] :
    ∃ (L : Type u) (x : AddCommGroup L) (x_1 : Module R L) (K : Submodule R L) (x_2 : M ≃ₗ[R] L K), Module.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_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] [Module.Free R M] [Module.Finite R M] (l : M →ₗ[R] N) (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
    Equations
    • =
    instance instFinitePresentationFinsupp {R : Type u_1} [Ring R] {ι : Type u_2} [Finite ι] :
    Equations
    • =
    instance instFinitePresentationForall {R : Type u_1} [Ring R] {ι : Type u_2} [Finite ι] :
    Equations
    • =
    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 : Module.FinitePresentation R M] (l : M →ₗ[R] N) (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
    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 : Module.FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective l) :
    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 : Module.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₁ : M →ₗ[R] N) (g₂ : M →ₗ[R] N) (h : f ∘ₗ g₁ = f ∘ₗ g₂) :
    ∃ (s : S), s g₁ = s g₂
    theorem 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] [Module.FinitePresentation R M] :