Theorems · Definition · commutative algebra

Module.DirectLimit

{R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              ((i j : ι) → i ≤ j → G i →ₗ[R] G j) → [DecidableEq ι] → Type (max u_2 u_3)

The direct limit of a directed system is the modules glued together along the maps.

Defined in

Mathlib.Algebra.Colimit.Module

Cited by

41 results in Mathlib

Foundations

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

Assumes

SemiringPreorderAddCommMonoidModuleDecidableEq