# mathlib3documentation

algebra.direct_limit

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• directed_system f
• module.direct_limit G f
• add_comm_group.direct_limit G f
• ring.direct_limit G f
@[class]
structure directed_system {ι : Type v} [preorder ι] (G : ι Type w) (f : Π (i j : ι), i j G i G j) :
Prop
• 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

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

Instances of this typeclass
theorem module.directed_system.map_self {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (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 directed_system.map_self specialized to linear maps, as otherwise the λ i j h, f i j h can confuse the simplifier.

theorem module.directed_system.map_map {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) [ (λ (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 directed_system.map_map specialized to linear maps, as otherwise the λ i j h, f i j h can confuse the simplifier.

def module.direct_limit {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) :
Type (max v w)

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

Equations
• = G {a : (λ (i : ι), G i) | (i j : ι) (H : i j) (x : G i), ι G i) x - ι G j) ((f i j H) x) = a})
Instances for module.direct_limit
@[protected, instance]
def module.direct_limit.add_comm_group {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) :
Equations
@[protected, instance]
def module.direct_limit.module {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) :
f)
Equations
@[protected, instance]
def module.direct_limit.inhabited {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) :
Equations
def module.direct_limit.of (R : Type u) [ring R] (ι : Type v) [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) (i : ι) :
G i →ₗ[R]

The canonical map from a component to the direct limit.

Equations
• f i = {a : (λ (i : ι), G i) | (i j : ι) (H : i j) (x : G i), ι G i) x - ι G j) ((f i j H) x) = a}).mkq.comp ι G i)
@[simp]
theorem module.direct_limit.of_f {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} {i j : ι} {hij : i j} {x : G i} :
G f j) ((f i j hij) x) = G f i) x
theorem module.direct_limit.exists_of {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} [nonempty ι] (z : f) :
(i : ι) (x : G i), G f i) x = z

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

@[protected]
theorem module.direct_limit.induction_on {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} [nonempty ι] {C : Prop} (z : f) (ih : (i : ι) (x : G i), C ( G f i) x)) :
C z
def module.direct_limit.lift (R : Type u) [ring R] (ι : Type v) [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G i →ₗ[R] G j)) {P : Type u₁} [ 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
• f g Hg = {a : (λ (i : ι), G i) | (i j : ι) (H : i j) (x : G i), ι G i) x - ι G j) ((f i j H) x) = a}).liftq P g) _
theorem module.direct_limit.lift_of {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} {P : Type u₁} [ 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) :
G f g Hg) ( G f i) x) = (g i) x
theorem module.direct_limit.lift_unique {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} {P : Type u₁} [ P] [nonempty ι] (F : →ₗ[R] P) (x : f) :
F x = G f (λ (i : ι), F.comp G f i)) _) x
noncomputable def module.direct_limit.totalize {R : Type u} [ring R] {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] (f : Π (i j : ι), i j (G 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
theorem module.direct_limit.totalize_of_le {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} {i j : ι} (h : i j) :
j = f i j h
theorem module.direct_limit.totalize_of_not_le {R : Type u} [ring R] {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} {i j : ι} (h : ¬i j) :
j = 0
theorem module.direct_limit.to_module_totalize_of_le {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} [ (λ (i j : ι) (h : i j), (f i j h))] {x : G} {i j : ι} (hij : i j) (hx : (k : ι), k i) :
(G j) (λ (k : ι), j)) x = (f i j hij) ( (G i) (λ (k : ι), i)) x)
theorem module.direct_limit.of.zero_exact_aux {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} [ (λ (i j : ι) (h : i j), (f i j h))] [nonempty ι] {x : G} (H : = 0) :
(j : ι), ( (k : ι), k j) (G j) (λ (i : ι), j)) x = 0
theorem module.direct_limit.of.zero_exact {R : Type u} [ring R] {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] [Π (i : ι), (G i)] {f : Π (i j : ι), i j (G i →ₗ[R] G j)} [ (λ (i j : ι) (h : i j), (f i j h))] {i : ι} {x : G i} (H : G f 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.

def add_comm_group.direct_limit {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G i →+ G j) :
Type (max v w)

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

Equations
Instances for add_comm_group.direct_limit
@[protected]
theorem add_comm_group.direct_limit.directed_system {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G i →+ G j) [h : (λ (i j : ι) (h : i j), (f i j h))] :
(λ (i j : ι) (hij : i j), ((f i j hij).to_int_linear_map))
@[protected, instance]
def add_comm_group.direct_limit.add_comm_group {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G i →+ G j) :
Equations
@[protected, instance]
def add_comm_group.direct_limit.inhabited {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G i →+ G j) :
Equations
def add_comm_group.direct_limit.of {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G i →+ G j) (i : ι) :

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem add_comm_group.direct_limit.of_f {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i j G i →+ G j} {i j : ι} (hij : i j) (x : G i) :
((f i j hij) x) = x
@[protected]
theorem add_comm_group.direct_limit.induction_on {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i j G i →+ G j} [nonempty ι] {C : Prop} (z : f) (ih : (i : ι) (x : G i), C ( x)) :
C z
theorem add_comm_group.direct_limit.of.zero_exact {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i j G i →+ G j} [ (λ (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.

def add_comm_group.direct_limit.lift {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] (G : ι Type w) [Π (i : ι), add_comm_group (G i)] (f : Π (i j : ι), i j G 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
@[simp]
theorem add_comm_group.direct_limit.lift_of {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i j G 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) :
g Hg) ( x) = (g i) x
theorem add_comm_group.direct_limit.lift_unique {ι : Type v} [dec_ι : decidable_eq ι] [preorder ι] {G : ι Type w} [Π (i : ι), add_comm_group (G i)] {f : Π (i j : ι), i j G i →+ G j} (P : Type u₁) [nonempty ι] (F : →+ P) (x : f) :
F x = (λ (i : ι), _) x
def ring.direct_limit {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) :
Type (max v w)

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

Equations
Instances for ring.direct_limit
@[protected, instance]
def ring.direct_limit.comm_ring {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) :
Equations
@[protected, instance]
def ring.direct_limit.ring {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) :
ring f)
Equations
@[protected, instance]
def ring.direct_limit.inhabited {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) :
Equations
def ring.direct_limit.of {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) (i : ι) :
G i →+*

The canonical map from a component to the direct limit.

Equations
@[simp]
theorem ring.direct_limit.of_f {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i j G i G j} {i j : ι} (hij : i j) (x : G i) :
j) (f i j hij x) = i) x
theorem ring.direct_limit.exists_of {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i j G i G j} [nonempty ι] (z : f) :
(i : ι) (x : G i), i) x = z

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

theorem ring.direct_limit.polynomial.exists_of {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i j G i →+* G j} [nonempty ι] (q : polynomial (λ (i j : ι) (h : i j), (f' i j h)))) :
(i : ι) (p : polynomial (G i)), polynomial.map (λ (i j : ι) (h : i j), (f' i j h)) i) p = q
theorem ring.direct_limit.induction_on {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i j G i G j} [nonempty ι] {C : Prop} (z : f) (ih : (i : ι) (x : G i), C ( i) x)) :
C z
theorem ring.direct_limit.of.zero_exact_aux2 {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f' : Π (i j : ι), i j G i →+* G j) [ (λ (i j : ι) (h : i j), (f' i j h))] {x : free_comm_ring (Σ (i : ι), G i)} {s t : set (Σ (i : ι), G i)} (hxs : x.is_supported s) {j k : ι} (hj : (z : Σ (i : ι), G i), z s z.fst j) (hk : (z : Σ (i : ι), G i), z t z.fst k) (hjk : j k) (hst : s t) :
(f' j k hjk) ((free_comm_ring.lift (λ (ix : s), (f' ix.val.fst j _) ix.val.snd)) x)) = (free_comm_ring.lift (λ (ix : t), (f' ix.val.fst k _) ix.val.snd)) x)
theorem ring.direct_limit.of.zero_exact_aux {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i j G i →+* G j} [ (λ (i j : ι) (h : i j), (f' i j h))] [nonempty ι] {x : free_comm_ring (Σ (i : ι), G i)} (H : (ideal.quotient.mk (ideal.span {a : free_comm_ring (Σ (i : ι), G i) | ( (i j : ι) (H : i j) (x : G i), free_comm_ring.of j, (λ (i j : ι) (h : i j), (f' i j h)) i j H x - free_comm_ring.of i, x⟩ = a) ( (i : ι), free_comm_ring.of i, 1⟩ - 1 = a) ( (i : ι) (x y : G i), free_comm_ring.of i, x + y - (free_comm_ring.of i, x⟩ + free_comm_ring.of i, y⟩) = a) (i : ι) (x y : G i), free_comm_ring.of i, x * y - free_comm_ring.of i, x⟩ * free_comm_ring.of i, y⟩ = a})) x = 0) :
(j : ι) (s : set (Σ (i : ι), G i)) (H : (k : Σ (i : ι), G i), k s k.fst j), x.is_supported s (free_comm_ring.lift (λ (ix : s), (f' ix.val.fst j _) ix.val.snd)) x) = 0
theorem ring.direct_limit.of.zero_exact {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f' : Π (i j : ι), i j G i →+* G j} [ (λ (i j : ι) (h : i j), (f' i j h))] {i : ι} {x : G i} (hix : (λ (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.direct_limit.of_injective {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] (f' : Π (i j : ι), i j G i →+* G j) [ (λ (i j : ι) (h : i j), (f' i j h))] (hf : (i j : ι) (hij : i j), function.injective (f' i j hij)) (i : ι) :
function.injective (λ (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.

def ring.direct_limit.lift {ι : Type v} [preorder ι] (G : ι Type w) [Π (i : ι), comm_ring (G i)] (f : Π (i j : ι), i j G i G j) (P : Type u₁) [comm_ring 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) :

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
@[simp]
theorem ring.direct_limit.lift_of {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i j G i G j} (P : Type u₁) [comm_ring 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) :
P g Hg) ( i) x) = (g i) x
theorem ring.direct_limit.lift_unique {ι : Type v} [preorder ι] {G : ι Type w} [Π (i : ι), comm_ring (G i)] {f : Π (i j : ι), i j G i G j} (P : Type u₁) [comm_ring P] [nonempty ι] (F : →+* P) (x : f) :
F x = P (λ (i : ι), F.comp i)) _) x
@[protected, instance]
def field.direct_limit.nontrivial {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f' : Π (i j : ι), i j G i →+* G j) [ (λ (i j : ι) (h : i j), (f' i j h))] :
nontrivial (λ (i j : ι) (h : i j), (f' i j h)))
theorem field.direct_limit.exists_inv {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i j G i G j) {p : f} :
p 0 ( (y : , p * y = 1)
noncomputable def field.direct_limit.inv {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i j G i G j) (p : f) :

Noncomputable multiplicative inverse in a direct limit of fields.

Equations
• = dite (p = 0) (λ (H : p = 0), 0) (λ (H : ¬p = 0),
@[protected]
theorem field.direct_limit.mul_inv_cancel {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i j G i G j) {p : f} (hp : p 0) :
p * = 1
@[protected]
theorem field.direct_limit.inv_mul_cancel {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f : Π (i j : ι), i j G i G j) {p : f} (hp : p 0) :
* p = 1
@[protected, reducible]
noncomputable def field.direct_limit.field {ι : Type v} [preorder ι] (G : ι Type w) [nonempty ι] [Π (i : ι), field (G i)] (f' : Π (i j : ι), i j G i →+* G j) [ (λ (i j : ι) (h : i j), (f' i j h))] :
field (λ (i j : ι) (h : i j), (f' i j h)))

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

Equations