----- > [!proposition] Proposition. ([[computing colimits with cofinals]]) > Let $\mathsf{C}$ be a [[category]]. Let $I,J$ be [[filtered poset|filtered]] [[poset|posets]], and $f:I \to J$ a [[cofinal monotone map]] — "$I$ contains an upper bound for all $j \in J$." > Then for any [[diagram|directed system]] in $\mathsf{C}$ indexed by $J$, we have $\operatorname{colim}_{i \in I} G_{f(i)} \cong \operatorname{colim}_{j \in J} G_{j},$ if the relevant [[categorical colimit|colimits]] exist (as they do, e.g. if $\mathsf{C}$ is $\mathsf{Set}, \mathsf{Ab}, R\mathsf{Mod}, \text{etc.}$). This matters because often the LHS is much easier to compute. ^proposition > [!proof]- Proof. ([[computing colimits with cofinals]]) > ~ - [ ] todo (not a part of the course) ----- #### ---- #### References > [!backlink] > ```dataview > TABLE rows.file.link as "Further Reading" > FROM [[]] > FLATTEN file.tags as Tag > WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom" > GROUP BY Tag > ``` > [!frontlink] > ```dataview > TABLE rows.file.link as "Further Reading" > FROM outgoing([[]]) > FLATTEN file.tags as Tag > WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom" > GROUP BY Tag > ```