# Direct limit of modules, abelian groups, rings, and fields. #

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

Generalizes the notion of "union", or "gluing", of incomparable modules over the same ring, or incomparable abelian groups, or rings, or fields.

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

## Main definitions #

• DirectedSystem f
• Module.DirectLimit G f
• AddCommGroup.DirectLimit G f
• Ring.DirectLimit G f
class DirectedSystem {ι : Type v} [] (G : ιType w) (f : (i j : ι) → i jG iG j) :

A directed system is a functor from a category (directed poset) to another category.

• map_self' : ∀ (i : ι) (x : G i) (h : i i), f i i h x = x
• map_map' : ∀ {i j k : ι} (hij : i j) (hjk : j k) (x : G i), f j k hjk (f i j hij x) = f i k x
Instances
theorem DirectedSystem.map_self' {ι : Type v} [] {G : ιType w} {f : (i j : ι) → i jG iG j} [self : ] (i : ι) (x : G i) (h : i i) :
f i i h x = x
theorem DirectedSystem.map_map' {ι : Type v} [] {G : ιType w} {f : (i j : ι) → i jG iG j} [self : ] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
f j k hjk (f i j hij x) = f i k x
theorem DirectedSystem.map_self {ι : Type v} [] {G : ιType w} (f : (i j : ι) → i jG iG j) [DirectedSystem G fun (i j : ι) (h : i j) => f i j h] (i : ι) (x : G i) (h : i i) :
f i i h x = x
theorem DirectedSystem.map_map {ι : Type v} [] {G : ιType w} (f : (i j : ι) → i jG iG j) [DirectedSystem G fun (i j : ι) (h : i j) => f i j h] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
f j k hjk (f i j hij x) = f i k x
theorem Module.DirectedSystem.map_self {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) (x : G i) (h : i i) :
(f i i h) x = x

A copy of DirectedSystem.map_self specialized to linear maps, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

theorem Module.DirectedSystem.map_map {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] {i : ι} {j : ι} {k : ι} (hij : i j) (hjk : j k) (x : G i) :
(f j k hjk) ((f i j hij) x) = (f i k ) x

A copy of DirectedSystem.map_map specialized to linear maps, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

noncomputable def Module.DirectLimit {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] :
Type (max v w)

The direct limit of a directed system is the modules glued together along the maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Module.DirectLimit.addCommGroup {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Module.DirectLimit.module {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] :
Module R ()
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Module.DirectLimit.inhabited {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] :
Equations
• = { default := 0 }
noncomputable instance Module.DirectLimit.unique {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] [] :
Equations
• One or more equations did not get rendered due to their size.
noncomputable def Module.DirectLimit.of (R : Type u) [Ring R] (ι : Type v) [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] (i : ι) :
G i →ₗ[R]

The canonical map from a component to the direct limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Module.DirectLimit.of_f {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {i : ι} {j : ι} {hij : i j} {x : G i} :
() ((f i j hij) x) = () x
theorem Module.DirectLimit.exists_of {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [] [IsDirected ι fun (x x_1 : ι) => x x_1] (z : ) :
∃ (i : ι) (x : G i), () x = z

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

theorem Module.DirectLimit.induction_on {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [] [IsDirected ι fun (x x_1 : ι) => x x_1] {C : } (z : ) (ih : ∀ (i : ι) (x : G i), C (() x)) :
C z
noncomputable def Module.DirectLimit.lift (R : Type u) [Ring R] (ι : Type v) [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) [] {P : Type u₁} [] [Module R P] (g : (i : ι) → G i →ₗ[R] P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Module.DirectLimit.lift_of {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {P : Type u₁} [] [Module R P] (g : (i : ι) → G i →ₗ[R] P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι} (x : G i) :
(Module.DirectLimit.lift R ι G f g Hg) (() x) = (g i) x
theorem Module.DirectLimit.lift_unique {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {P : Type u₁} [] [Module R P] [IsDirected ι fun (x x_1 : ι) => x x_1] (F : →ₗ[R] P) (x : ) :
F x = (Module.DirectLimit.lift R ι G f (fun (i : ι) => F ∘ₗ ) ) x
theorem Module.DirectLimit.lift_injective {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {P : Type u₁} [] [Module R P] (g : (i : ι) → G i →ₗ[R] P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) [IsDirected ι fun (x x_1 : ι) => x x_1] (injective : ∀ (i : ι), Function.Injective (g i)) :
noncomputable def Module.DirectLimit.map {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ (i j : ι) (h : i j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) :

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

Equations
Instances For
@[simp]
theorem Module.DirectLimit.map_apply_of {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} (g : (i : ι) → G i →ₗ[R] G' i) (hg : ∀ (i j : ι) (h : i j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i) {i : ι} (x : G i) :
() (() x) = (Module.DirectLimit.of R ι G' f' i) ((g i) x)
@[simp]
theorem Module.DirectLimit.map_id {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] :
Module.DirectLimit.map (fun (i : ι) => LinearMap.id) = LinearMap.id
theorem Module.DirectLimit.map_comp {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} {G'' : ιType v''} [(i : ι) → AddCommGroup (G'' i)] [(i : ι) → Module R (G'' i)] {f'' : (i j : ι) → i jG'' i →ₗ[R] G'' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (g₁ : (i : ι) → G i →ₗ[R] G' i) (g₂ : (i : ι) → G' i →ₗ[R] G'' i) (hg₁ : ∀ (i j : ι) (h : i j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i) (hg₂ : ∀ (i j : ι) (h : i j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i) :
∘ₗ = Module.DirectLimit.map (fun (i : ι) => g₂ i ∘ₗ g₁ i)
noncomputable def Module.DirectLimit.congr {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) :

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'.

Equations
Instances For
theorem Module.DirectLimit.congr_apply_of {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) {i : ι} (g : G i) :
() (() g) = (Module.DirectLimit.of R ι G' f' i) ((e i) g)
theorem Module.DirectLimit.congr_symm_apply_of {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] [(i : ι) → Module R (G' i)] {f' : (i j : ι) → i jG' i →ₗ[R] G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃ₗ[R] G' i) (he : ∀ (i j : ι) (h : i j), (e j) ∘ₗ f i j h = f' i j h ∘ₗ (e i)) {i : ι} (g : G' i) :
().symm ((Module.DirectLimit.of R ι G' f' i) g) = () ((e i).symm g)
noncomputable def Module.DirectLimit.totalize {R : Type u} [Ring R] {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] (f : (i j : ι) → i jG i →ₗ[R] G j) (i : ι) (j : ι) :
G i →ₗ[R] G j

totalize G f i j is a linear map from G i to G j, for every i and j. If i ≤ j, then it is the map f i j that comes with the directed system G, and otherwise it is the zero map.

Equations
• = if h : i j then f i j h else 0
Instances For
theorem Module.DirectLimit.totalize_of_le {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {i : ι} {j : ι} (h : i j) :
= f i j h
theorem Module.DirectLimit.totalize_of_not_le {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} {i : ι} {j : ι} (h : ¬i j) :
= 0
theorem Module.DirectLimit.toModule_totalize_of_le {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [(i : ι) → (k : G i) → Decidable (k 0)] {x : } {i : ι} {j : ι} (hij : i j) (hx : k, k i) :
(DirectSum.toModule R ι (G j) fun (k : ι) => ) x = (f i j hij) ((DirectSum.toModule R ι (G i) fun (k : ι) => ) x)
theorem Module.DirectLimit.of.zero_exact_aux {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [(i : ι) → (k : G i) → Decidable (k 0)] [] [IsDirected ι fun (x x_1 : ι) => x x_1] {x : } (H : ) :
∃ (j : ι), (k, k j) (DirectSum.toModule R ι (G j) fun (i : ι) => ) x = 0
theorem Module.DirectLimit.of.zero_exact {R : Type u} [Ring R] {ι : Type v} [] {G : ιType w} [(i : ι) → AddCommGroup (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i jG i →ₗ[R] G j} [] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} {x : G i} (H : () 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.

noncomputable def AddCommGroup.DirectLimit {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
Type (max w v)

The direct limit of a directed system is the abelian groups glued together along the maps.

Equations
Instances For
theorem AddCommGroup.DirectLimit.directedSystem {ι : Type v} [] (G : ιType w) [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [h : DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] :
DirectedSystem G fun (i j : ι) (hij : i j) => (f i j hij).toIntLinearMap
noncomputable instance AddCommGroup.DirectLimit.inst {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
Equations
noncomputable instance AddCommGroup.DirectLimit.instInhabited {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) :
Equations
• = { default := 0 }
noncomputable instance AddCommGroup.DirectLimit.instUniqueOfIsEmpty {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) [] :
Equations
noncomputable def AddCommGroup.DirectLimit.of {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) (i : ι) :
G i →+

The canonical map from a component to the direct limit.

Equations
Instances For
@[simp]
theorem AddCommGroup.DirectLimit.of_f {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {i : ι} {j : ι} (hij : i j) (x : G i) :
() ((f i j hij) x) = () x
theorem AddCommGroup.DirectLimit.induction_on {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] {C : } (z : ) (ih : ∀ (i : ι) (x : G i), C (() x)) :
C z
theorem AddCommGroup.DirectLimit.of.zero_exact {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [IsDirected ι fun (x x_1 : ι) => x x_1] [DirectedSystem G fun (i j : ι) (h : i j) => (f i j h)] (i : ι) (x : G i) (h : () 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.

noncomputable def AddCommGroup.DirectLimit.lift {ι : Type v} [] (G : ιType w) [] [(i : ι) → AddCommGroup (G i)] (f : (i j : ι) → i jG i →+ G j) (P : Type u₁) [] (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) :

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

Equations
• = (Module.DirectLimit.lift ι G (fun (i j : ι) (hij : i j) => (f i j hij).toIntLinearMap) (fun (i : ι) => (g i).toIntLinearMap) Hg).toAddMonoidHom
Instances For
@[simp]
theorem AddCommGroup.DirectLimit.lift_of {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} (P : Type u₁) [] (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) :
() (() x) = (g i) x
theorem AddCommGroup.DirectLimit.lift_unique {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} (P : Type u₁) [] [IsDirected ι fun (x x_1 : ι) => x x_1] (F : ) (x : ) :
F x = (AddCommGroup.DirectLimit.lift G f P (fun (i : ι) => F.comp ()) ) x
theorem AddCommGroup.DirectLimit.lift_injective {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} (P : Type u₁) [] (g : (i : ι) → G i →+ P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) ((f i j hij) x) = (g i) x) [IsDirected ι fun (x x_1 : ι) => x x_1] (injective : ∀ (i : ι), Function.Injective (g i)) :
noncomputable def AddCommGroup.DirectLimit.map {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' 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)) :

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

Equations
Instances For
@[simp]
theorem AddCommGroup.DirectLimit.map_apply_of {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' 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) :
() (() x) = () ((g i) x)
@[simp]
theorem AddCommGroup.DirectLimit.map_id {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} [IsDirected ι fun (x x_1 : ι) => x x_1] :
theorem AddCommGroup.DirectLimit.map_comp {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} {G'' : ιType v''} [(i : ι) → AddCommGroup (G'' i)] {f'' : (i j : ι) → i jG'' i →+ G'' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (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)) :
().comp () = AddCommGroup.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i))
noncomputable def AddCommGroup.DirectLimit.congr {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) :

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'.

Equations
Instances For
theorem AddCommGroup.DirectLimit.congr_apply_of {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G i) :
(() g) = () ((e i) g)
theorem AddCommGroup.DirectLimit.congr_symm_apply_of {ι : Type v} [] {G : ιType w} [] [(i : ι) → AddCommGroup (G i)] {f : (i j : ι) → i jG i →+ G j} {G' : ιType v'} [(i : ι) → AddCommGroup (G' i)] {f' : (i j : ι) → i jG' i →+ G' j} [IsDirected ι fun (x x_1 : ι) => x x_1] (e : (i : ι) → G i ≃+ G' i) (he : ∀ (i j : ι) (h : i j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G' i) :
.symm (() g) = () ((e i).symm g)
noncomputable def Ring.DirectLimit {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
Type (max v w)

The direct limit of a directed system is the rings glued together along the maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable instance Ring.DirectLimit.commRing {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
Equations
• One or more equations did not get rendered due to their size.
noncomputable instance Ring.DirectLimit.ring {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
Ring ()
Equations
• = CommRing.toRing
noncomputable instance Ring.DirectLimit.zero {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
Zero ()
Equations
• = id { zero := 0 }
noncomputable instance Ring.DirectLimit.instInhabited {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) :
Equations
• = { default := 0 }
noncomputable def Ring.DirectLimit.of {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) (i : ι) :
G i →+*

The canonical map from a component to the direct limit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ring.DirectLimit.of_f {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} {i : ι} {j : ι} (hij : i j) (x : G i) :
() (f i j hij x) = () x
theorem Ring.DirectLimit.exists_of {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (z : ) :
∃ (i : ι) (x : G 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 v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (q : Polynomial (Ring.DirectLimit G fun (i j : ι) (h : i j) => (f' i j h))) :
∃ (i : ι) (p : Polynomial (G i)), Polynomial.map (Ring.DirectLimit.of G (fun (i j : ι) (h : i j) => (f' i j h)) i) p = q
theorem Ring.DirectLimit.induction_on {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] {C : Prop} (z : ) (ih : ∀ (i : ι) (x : G i), C (() x)) :
C z
theorem Ring.DirectLimit.of.zero_exact_aux2 {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] {x : FreeCommRing ((i : ι) × G i)} {s : Set ((i : ι) × G i)} {t : Set ((i : ι) × G i)} [DecidablePred fun (x : (i : ι) × G i) => x s] [DecidablePred fun (x : (i : ι) × G i) => x t] (hxs : x.IsSupported s) {j : ι} {k : ι} (hj : zs, z.fst j) (hk : zt, z.fst k) (hjk : j k) (hst : s t) :
(f' j k hjk) ((FreeCommRing.lift fun (ix : s) => (f' (ix).fst j ) (ix).snd) ()) = (FreeCommRing.lift fun (ix : t) => (f' (ix).fst k ) (ix).snd) ()
theorem Ring.DirectLimit.of.zero_exact_aux {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [] [IsDirected ι fun (x x_1 : ι) => x x_1] {x : FreeCommRing ((i : ι) × G i)} (H : (Ideal.Quotient.mk (Ideal.span {a : FreeCommRing ((i : ι) × G i) | (∃ (i : ι) (j : ι) (H : i j) (x : G i), FreeCommRing.of j, (fun (i j : ι) (h : i j) => (f' i j h)) 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})) x = 0) :
∃ (j : ι) (s : Set ((i : ι) × G i)) (H : ks, k.fst j), x.IsSupported s ∀ [inst : DecidablePred fun (x : (i : ι) × G i) => x s], (FreeCommRing.lift fun (ix : s) => (f' (ix).fst j ) (ix).snd) () = 0
theorem Ring.DirectLimit.of.zero_exact {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f' : (i j : ι) → i jG i →+* G j} [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] [IsDirected ι fun (x x_1 : ι) => x x_1] {i : ι} {x : G i} (hix : (Ring.DirectLimit.of G (fun (i j : ι) (h : i j) => (f' i j h)) 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 v} [] {G : ιType w} [(i : ι) → CommRing (G i)] (f' : (i j : ι) → i jG i →+* G j) [IsDirected ι fun (x x_1 : ι) => x x_1] [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 (Ring.DirectLimit.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.lift {ι : Type v} [] (G : ιType w) [(i : ι) → CommRing (G i)] (f : (i j : ι) → i jG iG j) (P : Type u₁) [] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) (f i j hij x) = (g i) x) :

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Ring.DirectLimit.lift_of {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} (P : Type u₁) [] (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) :
(Ring.DirectLimit.lift G f P g Hg) (() x) = (g i) x
theorem Ring.DirectLimit.lift_unique {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} (P : Type u₁) [] [IsDirected ι fun (x x_1 : ι) => x x_1] (F : →+* P) (x : ) :
F x = (Ring.DirectLimit.lift G f P (fun (i : ι) => F.comp ()) ) x
theorem Ring.DirectLimit.lift_injective {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG iG j} (P : Type u₁) [] (g : (i : ι) → G i →+* P) (Hg : ∀ (i j : ι) (hij : i j) (x : G i), (g j) (f i j hij x) = (g i) x) [] [IsDirected ι fun (x x_1 : ι) => x x_1] (injective : ∀ (i : ι), Function.Injective (g i)) :
noncomputable def Ring.DirectLimit.map {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' 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)) :
(Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) →+* Ring.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'.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Ring.DirectLimit.map_apply_of {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' 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.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) x) = (Ring.DirectLimit.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 v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] :
Ring.DirectLimit.map (fun (i : ι) => RingHom.id (G i)) = RingHom.id (Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h))
theorem Ring.DirectLimit.map_comp {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} {G'' : ιType v''} [(i : ι) → CommRing (G'' i)] {f'' : (i j : ι) → i jG'' i →+* G'' j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (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)) :
(Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) = Ring.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i))
noncomputable def Ring.DirectLimit.congr {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (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)) :
(Ring.DirectLimit G fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) ≃+* Ring.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'.

Equations
Instances For
theorem Ring.DirectLimit.congr_apply_of {ι : Type v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (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) :
() ((Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) g) = (Ring.DirectLimit.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 v} [] {G : ιType w} [(i : ι) → CommRing (G i)] {f : (i j : ι) → i jG i →+* G j} {G' : ιType v'} [(i : ι) → CommRing (G' i)] {f' : (i j : ι) → i jG' i →+* G' j} [] [IsDirected ι fun (x x_1 : ι) => x x_1] (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) :
().symm ((Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x x_1) => (f' x x_1 h)) i) g) = (Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x x_1) => (f x x_1 h)) i) ((e i).symm g)
noncomputable instance Field.DirectLimit.nontrivial {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] :
Nontrivial (Ring.DirectLimit G fun (i j : ι) (h : i j) => (f' i j h))
Equations
• =
theorem Field.DirectLimit.exists_inv {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : } :
p 0∃ (y : ), p * y = 1
noncomputable def Field.DirectLimit.inv {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) (p : ) :

Noncomputable multiplicative inverse in a direct limit of fields.

Equations
• = if H : p = 0 then 0 else
Instances For
theorem Field.DirectLimit.mul_inv_cancel {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : } (hp : p 0) :
p * = 1
theorem Field.DirectLimit.inv_mul_cancel {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f : (i j : ι) → i jG iG j) {p : } (hp : p 0) :
* p = 1
@[reducible, inline]
noncomputable abbrev Field.DirectLimit.field {ι : Type v} [] (G : ιType w) [] [IsDirected ι fun (x x_1 : ι) => x x_1] [(i : ι) → Field (G i)] (f' : (i j : ι) → i jG i →+* G j) [DirectedSystem G fun (i j : ι) (h : i j) => (f' i j h)] :
Field (Ring.DirectLimit G fun (i j : ι) (h : i j) => (f' i j h))

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

Equations
• One or more equations did not get rendered due to their size.
Instances For