Ideals, monic polynomials and finitely presented rings over directed colimits of rings

Let I i be a compatible family of ideals in a directed system of commutative rings G i, indexed by a nonempty directed preorder: the transition maps f i j carry I i into I j. The colimit ideal of Ring.DirectLimit G f is ⨆ i, (I i).map (of G f i). This file shows that its elements are exactly the images of elements of the I i, and that membership in it, and being a unit modulo it, descend to a finite stage. It also shows that monic polynomials over the colimit come from monic polynomials over some stage, and that ring homomorphisms from a finitely presented ring into the colimit factor through some stage.

Main results

• Ring.DirectLimit.mem_iSup_map_of_iff: membership in the colimit ideal.
• Ring.DirectLimit.exists_f_mem_of_of_mem_iSup_map, Ring.DirectLimit.exists_isUnit_mk_f_of_isUnit_mk_of: descent of membership in the colimit ideal, and of units modulo it, to a finite stage.
• Ring.DirectLimit.Polynomial.exists_monic_of: a monic polynomial over the colimit comes from a monic polynomial over some stage.
• Ring.DirectLimit.exists_of_comp_eq_of_finitePresentation: a ring homomorphism from a finitely presented ring into the colimit factors through some stage.

@[simp]

theorem Ring.DirectLimit.of_comp_f {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {i j : ι} (hij : i ≤ j) : (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) j).comp (f i j hij) = of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i

The canonical maps into a direct limit are compatible with the transition maps.

@[simp]

theorem Ring.DirectLimit.mem_iSup_map_of_iff {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {I : (i : ι) → Ideal (G i)} [Nonempty ι] [IsDirectedOrder ι] (hI : ∀ (i j : ι) (hij : i ≤ j), I i ≤ Ideal.comap (f i j hij) (I j)) {z : DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)} : z ∈ ⨆ (i : ι), Ideal.map (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) (I i) ↔ ∃ (i : ι), ∃ x ∈ I i, (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) x = z

In a directed colimit of rings, the ideal generated by the images of a compatible family of ideals consists of the images of their elements.

theorem Ring.DirectLimit.exists_f_mem_of_of_mem_iSup_map {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {I : (i : ι) → Ideal (G i)} [IsDirectedOrder ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (hI : ∀ (i j : ι) (hij : i ≤ j), I i ≤ Ideal.comap (f i j hij) (I j)) {i : ι} {x : G i} (hx : (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) x ∈ ⨆ (i : ι), Ideal.map (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) (I i)) : ∃ (j : ι) (hij : i ≤ j), (f i j hij) x ∈ I j

If the image of an element of a stage lies in the colimit of a compatible family of ideals, then the element is carried into the ideal at some later stage.

theorem Ring.DirectLimit.exists_isUnit_mk_f_of_isUnit_mk_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {I : (i : ι) → Ideal (G i)} [IsDirectedOrder ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (hI : ∀ (i j : ι) (hij : i ≤ j), I i ≤ Ideal.comap (f i j hij) (I j)) {i : ι} {x : G i} (hx : IsUnit ((Ideal.Quotient.mk (⨆ (i : ι), Ideal.map (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) (I i))) ((of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) x))) : ∃ (j : ι) (hij : i ≤ j), IsUnit ((Ideal.Quotient.mk (I j)) ((f i j hij) x))

If an element of a stage is a unit modulo the colimit of a compatible family of ideals, then it is a unit modulo the ideal at some later stage.

theorem Ring.DirectLimit.Polynomial.exists_monic_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} [Nonempty ι] [IsDirectedOrder ι] {P : Polynomial (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3))} (hP : P.Monic) : ∃ (i : ι) (p : Polynomial (G i)), p.Monic ∧ Polynomial.map (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i) p = P

A monic polynomial over a directed colimit of rings is the image of a monic polynomial over some stage.

theorem Ring.DirectLimit.exists_of_comp_eq_of_finitePresentation {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} [Nonempty ι] [IsDirectedOrder ι] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {A : Type u_3} [CommRing A] [Algebra.FinitePresentation ℤ A] (g : A →+* DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) : ∃ (i : ι) (g' : A →+* G i), (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)) i).comp g' = g

A ring homomorphism from a finitely presented ring into a directed colimit of rings factors through some stage. This is the surjectivity half of the statement that Hom(A, -) commutes with directed colimits for a finitely presented ring A.

The proof adapts Mathlib's RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit (Mathlib/Algebra/Category/Ring/FinitePresentation.lean), which is stated for IsColimit cocones in CommRingCat, to Ring.DirectLimit.