Theorems · Definition · commutative algebra

Ring.DirectLimit.ringEquiv

{ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] →
        (f' : (i j : ι) → i ≤ j → G i →+* G j) →
          [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)] →
            [inst_3 : IsDirectedOrder ι] →
              [Nonempty ι] → (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f' x1 x2 x3)) ≃+* DirectLimit G f'

The direct limit constructed as a quotient of the free commutative ring is isomorphic to the direct limit constructed as a quotient of the disjoint union.

Defined in

Mathlib.Algebra.Colimit.Ring

Cited by

5 results in Mathlib

Foundations

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

Assumes

PreorderCommRingDirectedSystemIsDirectedOrderNonempty