Theorems · Definition · commutative algebra

Submodule.FG.directLimit

(R : Type u) →
  [inst : Semiring R] →
    (M : Type u_1) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : DecidableEq { P // P.FG }] →
            (Module.DirectLimit (fun P => ↥↑P) fun ⦃P Q⦄ h => Submodule.inclusion h) ≃ₗ[R] M

Any module is the direct limit of its finitely generated submodules

Defined in

Mathlib.RingTheory.TensorProduct.DirectLimitFG

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleDecidableEq