Theorems · Theorem · category theory

ModuleCat.directLimitIsColimit_desc

∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι] (G : ι → Type v)
  [inst_3 : (i : ι) → AddCommGroup (G i)] [inst_4 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)]
  (s : CategoryTheory.Limits.Cocone (ModuleCat.directLimitDiagram G f)),
  (ModuleCat.directLimitIsColimit G f).desc s =
    ModuleCat.ofHom (Module.DirectLimit.lift R ι G f (fun i => ModuleCat.Hom.hom (s.ι.app i)) ⋯)

Defined in

Mathlib.Algebra.Category.ModuleCat.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingDecidableEqPreorderAddCommGroupModuleDirectedSystem