Theorems · Theorem · commutative algebra

AddCommGroup.DirectLimit.map_comp

∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] {G' : ι → Type u_5}
  [inst_3 : (i : ι) → AddCommMonoid (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+ G' j} {G'' : ι → Type u_6}
  [inst_4 : (i : ι) → AddCommMonoid (G'' i)] {f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j} (g₁ : (i : ι) → G i →+ G' i)
  (g₂ : (i : ι) → G' i →+ G'' i) (hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
  (hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)),
  (AddCommGroup.DirectLimit.map g₂ hg₂).comp (AddCommGroup.DirectLimit.map g₁ hg₁) =
    AddCommGroup.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯

Defined in

Mathlib.Algebra.Colimit.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderAddCommMonoidDecidableEqAddCommMonoidAddCommMonoid