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 #
@[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.
theorem
module.directed_system.map_self
{R : Type u}
[ring R]
{ι : Type v}
[preorder ι]
{G : ι → Type w}
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
(i : ι)
(x : G i)
(h : i ≤ i) :
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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
{i j k : ι}
(hij : i ≤ j)
(hjk : j ≤ k)
(x : G i) :
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 : ι), module R (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
- module.direct_limit G f = (direct_sum ι G ⧸ submodule.span R {a : ⨁ (i : ι), G i | ∃ (i j : ι) (H : i ≤ j) (x : G i), ⇑(direct_sum.lof R ι G i) x - ⇑(direct_sum.lof R ι G j) (⇑(f i j H) x) = a})
@[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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)) :
Equations
- module.direct_limit.add_comm_group G f = submodule.quotient.add_comm_group (submodule.span R {a : ⨁ (i : ι), G i | ∃ (i j : ι) (H : i ≤ j) (x : G i), ⇑(direct_sum.lof R ι G i) x - ⇑(direct_sum.lof R ι G j) (⇑(f i j H) x) = a})
@[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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)) :
module R (module.direct_limit G f)
Equations
- module.direct_limit.module G f = submodule.quotient.module (submodule.span R {a : ⨁ (i : ι), G i | ∃ (i j : ι) (H : i ≤ j) (x : G i), ⇑(direct_sum.lof R ι G i) x - ⇑(direct_sum.lof R ι G j) (⇑(f i j H) x) = a})
@[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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)) :
inhabited (module.direct_limit G f)
Equations
- module.direct_limit.inhabited G f = {default := 0}
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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
(i : ι) :
G i →ₗ[R] module.direct_limit G f
The canonical map from a component to the direct limit.
Equations
- module.direct_limit.of R ι G f i = (submodule.span R {a : ⨁ (i : ι), G i | ∃ (i j : ι) (H : i ≤ j) (x : G i), ⇑(direct_sum.lof R ι G i) x - ⇑(direct_sum.lof R ι G j) (⇑(f i j H) x) = a}).mkq.comp (direct_sum.lof R ι 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
{i j : ι}
{hij : i ≤ j}
{x : G i} :
⇑(module.direct_limit.of R ι G f j) (⇑(f i j hij) x) = ⇑(module.direct_limit.of R ι 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[nonempty ι]
[is_directed ι has_le.le]
(z : module.direct_limit G f) :
∃ (i : ι) (x : G i), ⇑(module.direct_limit.of R ι 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[nonempty ι]
[is_directed ι has_le.le]
{C : module.direct_limit G f → Prop}
(z : module.direct_limit G f)
(ih : ∀ (i : ι) (x : G i), C (⇑(module.direct_limit.of R ι 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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
{P : Type u₁}
[add_comm_group P]
[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) :
module.direct_limit G f →ₗ[R] P
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
- module.direct_limit.lift R ι G f g Hg = (submodule.span R {a : ⨁ (i : ι), G i | ∃ (i j : ι) (H : i ≤ j) (x : G i), ⇑(direct_sum.lof R ι G i) x - ⇑(direct_sum.lof R ι G j) (⇑(f i j H) x) = a}).liftq (direct_sum.to_module R ι 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
{P : Type u₁}
[add_comm_group P]
[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.direct_limit.lift R ι G f g Hg) (⇑(module.direct_limit.of R ι 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
{P : Type u₁}
[add_comm_group P]
[module R P]
[nonempty ι]
[is_directed ι has_le.le]
(F : module.direct_limit G f →ₗ[R] P)
(x : module.direct_limit G f) :
⇑F x = ⇑(module.direct_limit.lift R ι G f (λ (i : ι), F.comp (module.direct_limit.of R ι 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 : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
(i 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.
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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
{i j : ι}
(h : i ≤ j) :
module.direct_limit.totalize G f i 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
{i j : ι}
(h : ¬i ≤ j) :
module.direct_limit.totalize G f i 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
{x : direct_sum ι G}
{i j : ι}
(hij : i ≤ j)
(hx : ∀ (k : ι), k ∈ dfinsupp.support x → k ≤ i) :
⇑(direct_sum.to_module R ι (G j) (λ (k : ι), module.direct_limit.totalize G f k j)) x = ⇑(f i j hij) (⇑(direct_sum.to_module R ι (G i) (λ (k : ι), module.direct_limit.totalize G f 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[nonempty ι]
[is_directed ι has_le.le]
{x : direct_sum ι G}
(H : submodule.quotient.mk x = 0) :
∃ (j : ι), (∀ (k : ι), k ∈ dfinsupp.support x → k ≤ j) ∧ ⇑(direct_sum.to_module R ι (G j) (λ (i : ι), module.direct_limit.totalize G f 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 : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
[is_directed ι has_le.le]
{i : ι}
{x : G i}
(H : ⇑(module.direct_limit.of R ι G f i) 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
- add_comm_group.direct_limit G f = module.direct_limit G (λ (i j : ι) (hij : i ≤ j), (f i j hij).to_int_linear_map)
@[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 : directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))] :
directed_system G (λ (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
- add_comm_group.direct_limit.add_comm_group G f = module.direct_limit.add_comm_group G (λ (i j : ι) (hij : i ≤ j), (f i j hij).to_int_linear_map)
@[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
- add_comm_group.direct_limit.inhabited G f = {default := 0}
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 : ι) :
G i →ₗ[ℤ] add_comm_group.direct_limit G f
The canonical map from a component to the direct limit.
Equations
- add_comm_group.direct_limit.of G f i = module.direct_limit.of ℤ ι G (λ (i j : ι) (hij : i ≤ j), (f i j hij).to_int_linear_map) i
@[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) :
⇑(add_comm_group.direct_limit.of G f j) (⇑(f i j hij) x) = ⇑(add_comm_group.direct_limit.of G f i) 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 ι]
[is_directed ι has_le.le]
{C : add_comm_group.direct_limit G f → Prop}
(z : add_comm_group.direct_limit G f)
(ih : ∀ (i : ι) (x : G i), C (⇑(add_comm_group.direct_limit.of G f i) 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}
[is_directed ι has_le.le]
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f i j h))]
(i : ι)
(x : G i)
(h : ⇑(add_comm_group.direct_limit.of G f i) 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₁)
[add_comm_group 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 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
- add_comm_group.direct_limit.lift G f P g Hg = module.direct_limit.lift ℤ ι G (λ (i j : ι) (hij : i ≤ j), (f i j hij).to_int_linear_map) (λ (i : ι), (g i).to_int_linear_map) Hg
@[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₁)
[add_comm_group 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) :
⇑(add_comm_group.direct_limit.lift G f P g Hg) (⇑(add_comm_group.direct_limit.of G f i) 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₁)
[add_comm_group P]
[nonempty ι]
[is_directed ι has_le.le]
(F : add_comm_group.direct_limit G f →+ P)
(x : add_comm_group.direct_limit G f) :
⇑F x = ⇑(add_comm_group.direct_limit.lift G f P (λ (i : ι), F.comp (add_comm_group.direct_limit.of G f i).to_add_monoid_hom) _) 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
- ring.direct_limit G f = (free_comm_ring (Σ (i : ι), G i) ⧸ ideal.span {a : free_comm_ring (Σ (i : ι), G i) | (∃ (i j : ι) (H : i ≤ j) (x : G i), free_comm_ring.of ⟨j, f 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})
@[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) :
comm_ring (ring.direct_limit G f)
Equations
- ring.direct_limit.comm_ring G f = ideal.quotient.comm_ring (ideal.span {a : free_comm_ring (Σ (i : ι), G i) | (∃ (i j : ι) (H : i ≤ j) (x : G i), free_comm_ring.of ⟨j, f 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})
@[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 (ring.direct_limit G 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) :
inhabited (ring.direct_limit G f)
Equations
- ring.direct_limit.inhabited G f = {default := 0}
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 →+* ring.direct_limit G f
The canonical map from a component to the direct limit.
Equations
- ring.direct_limit.of G f i = ring_hom.mk' {to_fun := λ (x : G i), ⇑(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, f 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})) (free_comm_ring.of ⟨i, x⟩), map_one' := _, map_mul' := _} _
@[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) :
⇑(ring.direct_limit.of G f j) (f i j hij x) = ⇑(ring.direct_limit.of G f 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 ι]
[is_directed ι has_le.le]
(z : ring.direct_limit G f) :
∃ (i : ι) (x : G i), ⇑(ring.direct_limit.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.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 ι]
[is_directed ι has_le.le]
(q : (ring.direct_limit G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h)))[X]) :
∃ (i : ι) (p : (G i)[X]), polynomial.map (ring.direct_limit.of G (λ (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 ι]
[is_directed ι has_le.le]
{C : ring.direct_limit G f → Prop}
(z : ring.direct_limit G f)
(ih : ∀ (i : ι) (x : G i), C (⇑(ring.direct_limit.of G f 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)
[directed_system G (λ (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) :
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}
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))]
[nonempty ι]
[is_directed ι has_le.le]
{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) :
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}
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))]
[is_directed ι has_le.le]
{i : ι}
{x : G i}
(hix : ⇑(ring.direct_limit.of G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h)) i) 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)
[is_directed ι has_le.le]
[directed_system G (λ (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.direct_limit.of G (λ (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) :
ring.direct_limit 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.
Equations
- ring.direct_limit.lift G f P g Hg = ideal.quotient.lift (ideal.span {a : free_comm_ring (Σ (i : ι), G i) | (∃ (i j : ι) (H : i ≤ j) (x : G i), free_comm_ring.of ⟨j, f 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}) (⇑free_comm_ring.lift (λ (x : Σ (i : ι), G i), ⇑(g x.fst) x.snd)) _
@[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) :
⇑(ring.direct_limit.lift G f P g Hg) (⇑(ring.direct_limit.of G f 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 ι]
[is_directed ι has_le.le]
(F : ring.direct_limit G f →+* P)
(x : ring.direct_limit G f) :
⇑F x = ⇑(ring.direct_limit.lift G f P (λ (i : ι), F.comp (ring.direct_limit.of G f i)) _) x
@[protected, instance]
def
field.direct_limit.nontrivial
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f' : Π (i j : ι), i ≤ j → G i →+* G j)
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))] :
nontrivial (ring.direct_limit G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h)))
theorem
field.direct_limit.exists_inv
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
{p : ring.direct_limit G f} :
p ≠ 0 → (∃ (y : ring.direct_limit G f), p * y = 1)
noncomputable
def
field.direct_limit.inv
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
(p : ring.direct_limit G f) :
Noncomputable multiplicative inverse in a direct limit of fields.
Equations
- field.direct_limit.inv G f p = dite (p = 0) (λ (H : p = 0), 0) (λ (H : ¬p = 0), classical.some _)
@[protected]
theorem
field.direct_limit.mul_inv_cancel
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
{p : ring.direct_limit G f}
(hp : p ≠ 0) :
p * field.direct_limit.inv G f p = 1
@[protected]
theorem
field.direct_limit.inv_mul_cancel
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
{p : ring.direct_limit G f}
(hp : p ≠ 0) :
(field.direct_limit.inv G f p) * p = 1
@[protected]
noncomputable
def
field.direct_limit.field
{ι : Type v}
[preorder ι]
(G : ι → Type w)
[nonempty ι]
[is_directed ι has_le.le]
[Π (i : ι), field (G i)]
(f' : Π (i j : ι), i ≤ j → G i →+* G j)
[directed_system G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))] :
field (ring.direct_limit G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h)))
Noncomputable field structure on the direct limit of fields. See note [reducible non-instances].
Equations
- field.direct_limit.field G f' = {add := comm_ring.add (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), add_assoc := _, zero := comm_ring.zero (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), sub := comm_ring.sub (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), mul_assoc := _, one := comm_ring.one (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), one_mul := _, mul_one := _, npow := comm_ring.npow (ring.direct_limit.comm_ring G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.direct_limit.inv G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h)), div := div_inv_monoid.div._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ (field.direct_limit.inv G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ (field.direct_limit.inv G (λ (i j : ι) (h : i ≤ j), ⇑(f' i j h))), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}