Direct limit of rings, and fields

See Atiyah-Macdonald PP.32-33, Matsumura PP.269-270

Generalizes the notion of "union", or "gluing", of incomparable rings or fields.

It is constructed as a quotient of the free commutative ring instead of a quotient of the disjoint union so as to make the operations (addition etc.) "computable".

Main definition

• Ring.DirectLimit G f

noncomputable def Ring.DirectLimit {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (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 rings glued together along the maps.

noncomputable instance Ring.DirectLimit.commRing {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) : CommRing (DirectLimit G f)

noncomputable instance Ring.DirectLimit.ring {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) : Ring (DirectLimit G f)

noncomputable instance Ring.DirectLimit.zero {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) : Zero (DirectLimit G f)

noncomputable instance Ring.DirectLimit.instInhabited {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) : Inhabited (DirectLimit G f)

noncomputable def Ring.DirectLimit.of {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) (i : ι) : G i →+* DirectLimit G f

The canonical map from a component to the direct limit.

theorem Ring.DirectLimit.quotientMk_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (i : ι) (x : G i) : (Ideal.Quotient.mk (Ideal.span {a : FreeCommRing ((i : ι) × G i) | (∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i), FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ (i : ι) (x : G i) (y : G i), FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ (i : ι) (x : G i) (y : G i), FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a})) (FreeCommRing.of ⟨i, x⟩) = (of G f i) x

@[simp]

theorem Ring.DirectLimit.of_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) (x : G i) : (of G f j) (f i j hij x) = (of G f i) x

theorem Ring.DirectLimit.exists_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (z : DirectLimit G f) : ∃ (i : ι) (x : G i), (of G f i) x = z

Every element of the direct limit corresponds to some element in some component of the directed system.

theorem Ring.DirectLimit.Polynomial.exists_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i ≤ j → G i →+* G j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (q : Polynomial (DirectLimit G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h))) : ∃ (i : ι) (p : Polynomial (G i)), Polynomial.map (of G (fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)) i) p = q

theorem Ring.DirectLimit.induction_on {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : DirectLimit G f → Prop} (z : DirectLimit G f) (ih : ∀ (i : ι) (x : G i), C ((of G f i) x)) : C z

noncomputable def Ring.DirectLimit.lift {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i ≤ j → G i → G j) (P : Type u_3) [CommRing P] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) : DirectLimit G f →+* P

The universal property of the direct limit: maps from the components to another ring that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

@[simp]

theorem Ring.DirectLimit.lift_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [CommRing P] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) (i : ι) (x : G i) : (lift G f P g Hg) ((of G f i) x) = (g i) x

theorem Ring.DirectLimit.hom_ext {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [CommRing P] {g₁ g₂ : DirectLimit G f →+* P} (h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂

theorem Ring.DirectLimit.hom_ext_iff {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} {P : Type u_3} [CommRing P] {g₁ g₂ : DirectLimit G f →+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

@[simp]

theorem Ring.DirectLimit.lift_comp_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [CommRing P] (F : DirectLimit G f →+* P) : lift G f P (fun (i : ι) => F.comp (of G f i)) ⋯ = F

@[deprecated Ring.DirectLimit.lift_comp_of (since := "2025-08-11")]

theorem Ring.DirectLimit.lift_unique {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [CommRing P] (F : DirectLimit G f →+* P) (x : DirectLimit G f) : F x = (lift G f P (fun (i : ι) => F.comp (of G f i)) ⋯) x

@[simp]

theorem Ring.DirectLimit.lift_of' {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} : lift G f (DirectLimit G f) (of G f) ⋯ = RingHom.id (DirectLimit G f)

theorem Ring.DirectLimit.lift_injective {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [CommRing P] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (injective : ∀ (i : ι), Function.Injective ⇑(g i)) : Function.Injective ⇑(lift G f P g Hg)

noncomputable def Ring.DirectLimit.ringEquiv {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] : (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)) ≃+* _root_.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.

theorem Ring.DirectLimit.ringEquiv_of {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {i : ι} {g : G i} : (ringEquiv G f') ((of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)) i) g) = ⟦⟨i, g⟩⟧

theorem Ring.DirectLimit.ringEquiv_symm_mk {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] {g : (i : ι) × G i} : (ringEquiv G f').symm ⟦g⟧ = (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)) g.fst) g.snd

theorem Ring.DirectLimit.of.zero_exact {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i ≤ j → G i →+* G j} [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {i : ι} {x : G i} (hix : (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)) i) x = 0) : ∃ (j : ι) (hij : i ≤ j), (f' i j hij) x = 0

A component that corresponds to zero in the direct limit is already zero in some bigger module in the directed system.

theorem Ring.DirectLimit.of_injective {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)] (hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)) (i : ι) : Function.Injective ⇑(of G (fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)) i)

If the maps in the directed system are injective, then the canonical maps from the components to the direct limits are injective.

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

Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of ring homomorphisms gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a ring homomorphism lim G ⟶ lim G'.

@[simp]

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

@[simp]

theorem Ring.DirectLimit.map_id {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} : map (fun (x : ι) => RingHom.id (G x)) ⋯ = RingHom.id (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h))

theorem Ring.DirectLimit.map_comp {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+* G' j} {G'' : ι → Type u_5} [(i : ι) → CommRing (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)) : (map g₂ hg₂).comp (map g₁ hg₁) = map (fun (i : ι) => (g₂ i).comp (g₁ i)) ⋯

noncomputable def Ring.DirectLimit.congr {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) : (DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) ≃+* DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)

Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence lim G ⟶ lim G'.

theorem Ring.DirectLimit.congr_apply_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G i) : (congr e he) ((of G (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) i) g) = (of G' (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)) i) ((e i) g)

theorem Ring.DirectLimit.congr_symm_apply_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i) (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G' i) : (congr e he).symm ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)) i) g) = (of G (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) i) ((e i).symm g)

instance Field.DirectLimit.nontrivial {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)] : Nontrivial (Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3))

theorem Field.DirectLimit.exists_inv {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f} : p ≠ 0 → ∃ (y : Ring.DirectLimit G f), p * y = 1

noncomputable def Field.DirectLimit.inv {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) (p : Ring.DirectLimit G f) : Ring.DirectLimit G f

Noncomputable multiplicative inverse in a direct limit of fields.

theorem Field.DirectLimit.mul_inv_cancel {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f} (hp : p ≠ 0) : p * inv G f p = 1

theorem Field.DirectLimit.inv_mul_cancel {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f : (i j : ι) → i ≤ j → G i → G j) {p : Ring.DirectLimit G f} (hp : p ≠ 0) : inv G f p * p = 1

@[reducible, inline]

noncomputable abbrev Field.DirectLimit.field {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Field (G i)] (f' : (i j : ι) → i ≤ j → G i →+* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3)] : Field (Ring.DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f' x1 x2 x3))

Noncomputable field structure on the direct limit of fields. See note [reducible non-instances].