Theorems · Theorem · commutative algebra

Ring.DirectLimit.map_apply_of

∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (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)) {i : ι} (x : G i),
  (Ring.DirectLimit.map g hg) ((Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) x) =
    (Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) ((g i) x)

Defined in

Mathlib.Algebra.Colimit.Ring

Cited by

4 results in Mathlib

Foundations

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

Assumes

PreorderCommRingCommRing