Theorems · Theorem · commutative algebra

Module.FinitePresentation.equiv_quotient

∀ (R : Type u) (M : Type u_1) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] [Small.{v, u} R], ∃ L x x_1 K x_2, 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.

Defined in

Mathlib.Algebra.Module.FinitePresentation

Cited by

0 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleModule.FinitePresentationSmall