Theorems · Definition · commutative algebra
Ring.DirectLimit
{ι : Type u_1} →
[inst : Preorder ι] →
(G : ι → Type u_2) → [(i : ι) → CommRing (G i)] → ((i j : ι) → i ≤ j → G i → G j) → Type (max (max u_1 u_2) u_2 u_1)The direct limit of a directed system is the ring obtained by gluing the components along the maps.
- Defined in
- Mathlib.Algebra.Colimit.Ring
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Preorderstatement and proof · cited by 7,952
- Set.ofPredproof · cited by 6,101
- HasQuotient.Quotientproof · cited by 2,301
- Ideal.spanproof · cited by 948
- FreeCommRingproof · cited by 43
- FreeCommRing.ofproof · cited by 34
Cited by33
Results whose statement or proof uses this declaration.
- Ring.DirectLimit.ofstatement · cited by 21
- Ring.DirectLimit.liftstatement · cited by 6
- Ring.DirectLimit.hom_extstatement and proof · cited by 5
- Ring.DirectLimit.lift_ofstatement · cited by 5
- Ring.DirectLimit.mapstatement and proof · cited by 5
- Ring.DirectLimit.ringEquivstatement and proof · cited by 5
- Ring.DirectLimit.map_apply_ofstatement and proof · cited by 4
- Ring.DirectLimit.congrstatement · cited by 2
- Ring.DirectLimit.exists_ofstatement and proof · cited by 2
- Field.DirectLimit.invstatement and proof · cited by 2
- Ring.DirectLimit.induction_onstatement and proof · cited by 2
- Ring.DirectLimit.of_fstatement · cited by 2