Theorems · Theorem · category theory

ModuleCat.directLimitDiagram_obj_carrier

∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] (G : ι → Type v)
  [inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι), ↑((ModuleCat.directLimitDiagram G f).obj i) = G i

Defined in

Mathlib.Algebra.Category.ModuleCat.Limits

Cited by

0 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Quot.sound

Assumes

RingPreorderAddCommGroupModuleDirectedSystem