Theorems · Definition · commutative algebra

AddCommGroup.DirectLimit

{ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] → [DecidableEq ι] → ((i j : ι) → i ≤ j → G i →+ G j) → Type (max u_3 u_2)

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

Defined in

Mathlib.Algebra.Colimit.Module

Cited by

16 results in Mathlib

Foundations

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

Assumes

PreorderAddCommMonoidDecidableEq