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".
@[class]
structure
directed_system
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
(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 the category (directed poset) to another category. This is used for abelian groups and rings and fields because their maps are not bundled. See module.directed_system
@[class]
structure
module.directed_system
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] 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 the category (directed poset) to the category of R-modules.
def
module.direct_limit
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f] :
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 = (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}).quotient
@[instance]
def
module.direct_limit.add_comm_group
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f] :
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})
@[instance]
def
module.direct_limit.semimodule
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f] :
semimodule R (module.direct_limit G f)
Equations
- module.direct_limit.semimodule G f = submodule.quotient.semimodule (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})
def
module.direct_limit.of
(R : Type u)
[ring R]
(ι : Type v)
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f]
(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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
(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.
theorem
module.direct_limit.induction_on
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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)
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{P : Type u₁}
[add_comm_group P]
[module R P]
(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
def
module.direct_limit.totalize
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
(f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j))
[module.directed_system G f]
(i j : ι) :
theorem
module.direct_limit.totalize_apply
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
(i j : ι)
(x : G i) :
theorem
module.direct_limit.to_module_totalize_of_le
{R : Type u}
[ring R]
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
[Π (i : ι), module R (G i)]
{f : Π (i j : ι), i ≤ j → (G i →ₗ[R] G j)}
[module.directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f] :
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), (add_monoid_hom.of (f i j hij)).to_int_linear_map)
theorem
add_comm_group.direct_limit.directed_system
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f] :
module.directed_system G (λ (i j : ι) (hij : i ≤ j), (add_monoid_hom.of (f i j hij)).to_int_linear_map)
@[instance]
def
add_comm_group.direct_limit.add_comm_group
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f] :
Equations
- add_comm_group.direct_limit.add_comm_group G f = module.direct_limit.add_comm_group G (λ (i j : ι) (hij : i ≤ j), (add_monoid_hom.of (f i j hij)).to_int_linear_map)
def
add_comm_group.direct_limit.of
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι)
(a : G i) :
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), (add_monoid_hom.of (f i j hij)).to_int_linear_map) i)
@[instance]
def
add_comm_group.direct_limit.of.is_add_group_hom
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι) :
@[simp]
theorem
add_comm_group.direct_limit.of_f
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
{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
@[simp]
theorem
add_comm_group.direct_limit.of_zero
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι) :
add_comm_group.direct_limit.of G f i 0 = 0
@[simp]
theorem
add_comm_group.direct_limit.of_add
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x y : G i) :
add_comm_group.direct_limit.of G f i (x + y) = add_comm_group.direct_limit.of G f i x + add_comm_group.direct_limit.of G f i y
@[simp]
theorem
add_comm_group.direct_limit.of_neg
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x : G i) :
add_comm_group.direct_limit.of G f i (-x) = -add_comm_group.direct_limit.of G f i x
@[simp]
theorem
add_comm_group.direct_limit.of_sub
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x y : G i) :
add_comm_group.direct_limit.of G f i (x - y) = add_comm_group.direct_limit.of G f i x - add_comm_group.direct_limit.of G f i y
theorem
add_comm_group.direct_limit.induction_on
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(a : add_comm_group.direct_limit G f) :
P
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), (add_monoid_hom.of (f i j hij)).to_int_linear_map) (λ (i : ι), (add_monoid_hom.of (g i)).to_int_linear_map) Hg)
@[instance]
def
add_comm_group.direct_limit.lift.is_add_group_hom
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x) :
is_add_group_hom (add_comm_group.direct_limit.lift G f P g Hg)
@[simp]
theorem
add_comm_group.direct_limit.lift_of
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(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
@[simp]
theorem
add_comm_group.direct_limit.lift_zero
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x) :
add_comm_group.direct_limit.lift G f P g Hg 0 = 0
@[simp]
theorem
add_comm_group.direct_limit.lift_add
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x y : add_comm_group.direct_limit G f) :
add_comm_group.direct_limit.lift G f P g Hg (x + y) = add_comm_group.direct_limit.lift G f P g Hg x + add_comm_group.direct_limit.lift G f P g Hg y
@[simp]
theorem
add_comm_group.direct_limit.lift_neg
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x : add_comm_group.direct_limit G f) :
add_comm_group.direct_limit.lift G f P g Hg (-x) = -add_comm_group.direct_limit.lift G f P g Hg x
@[simp]
theorem
add_comm_group.direct_limit.lift_sub
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_add_group_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x y : add_comm_group.direct_limit G f) :
add_comm_group.direct_limit.lift G f P g Hg (x - y) = add_comm_group.direct_limit.lift G f P g Hg x - add_comm_group.direct_limit.lift G f P g Hg y
theorem
add_comm_group.direct_limit.lift_unique
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), add_comm_group (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_add_group_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[add_comm_group P]
(F : add_comm_group.direct_limit G f → P)
[is_add_group_hom F]
(x : add_comm_group.direct_limit G f) :
F x = add_comm_group.direct_limit.lift G f P (λ (i : ι) (x : G i), F (add_comm_group.direct_limit.of G f i x)) _ x
def
ring.direct_limit
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f] :
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 = (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}).quotient
@[instance]
def
ring.direct_limit.comm_ring
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f] :
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})
@[instance]
def
ring.direct_limit.ring
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f] :
ring (ring.direct_limit G f)
Equations
def
ring.direct_limit.of
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x : G i) :
The canonical map from a component to the direct limit.
Equations
- ring.direct_limit.of G f i x = ⇑(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⟩)
@[instance]
def
ring.direct_limit.of.is_ring_hom
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι) :
is_ring_hom (ring.direct_limit.of G f i)
@[simp]
theorem
ring.direct_limit.of_f
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{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
@[simp]
theorem
ring.direct_limit.of_zero
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι) :
ring.direct_limit.of G f i 0 = 0
@[simp]
theorem
ring.direct_limit.of_one
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι) :
ring.direct_limit.of G f i 1 = 1
@[simp]
theorem
ring.direct_limit.of_add
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x y : G i) :
ring.direct_limit.of G f i (x + y) = ring.direct_limit.of G f i x + ring.direct_limit.of G f i y
@[simp]
theorem
ring.direct_limit.of_neg
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x : G i) :
ring.direct_limit.of G f i (-x) = -ring.direct_limit.of G f i x
@[simp]
theorem
ring.direct_limit.of_sub
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x y : G i) :
ring.direct_limit.of G f i (x - y) = ring.direct_limit.of G f i x - ring.direct_limit.of G f i y
@[simp]
theorem
ring.direct_limit.of_mul
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x y : G i) :
ring.direct_limit.of G f i (x * y) = (ring.direct_limit.of G f i x) * ring.direct_limit.of G f i y
@[simp]
theorem
ring.direct_limit.of_pow
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(i : ι)
(x : G i)
(n : ℕ) :
ring.direct_limit.of G f i (x ^ n) = ring.direct_limit.of G f i x ^ n
theorem
ring.direct_limit.exists_of
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(q : polynomial (ring.direct_limit G f)) :
∃ (i : ι) (p : polynomial (G i)), polynomial.map (ring_hom.of (ring.direct_limit.of G f i)) p = q
theorem
ring.direct_limit.induction_on
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{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}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{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)) (⇑(free_comm_ring.restriction s) x)) = ⇑(free_comm_ring.lift (λ (ix : ↥t), f ix.val.fst k _ ix.val.snd)) (⇑(free_comm_ring.restriction t) x)
theorem
ring.direct_limit.of.zero_exact_aux
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{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, 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})) x = 0) :
theorem
ring.direct_limit.of.zero_exact
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{i : ι}
{x : G i}
(hix : ring.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.
theorem
ring.direct_limit.of_injective
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(hf : ∀ (i j : ι) (hij : i ≤ j), function.injective (f i j hij))
(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_hom
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(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.
We don't use this function as the canonical form because Lean 3 fails to automatically coerce
it to a function; use lift instead.
Equations
- ring.direct_limit.lift_hom 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)) _
def
ring.direct_limit.lift
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(a : 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 = ⇑(ring.direct_limit.lift_hom G f P g Hg)
@[instance]
def
ring.direct_limit.lift_is_ring_hom
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x) :
is_ring_hom (ring.direct_limit.lift G f P g Hg)
@[simp]
theorem
ring.direct_limit.lift_of
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(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
@[simp]
theorem
ring.direct_limit.lift_zero
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x) :
ring.direct_limit.lift G f P g Hg 0 = 0
@[simp]
theorem
ring.direct_limit.lift_one
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x) :
ring.direct_limit.lift G f P g Hg 1 = 1
@[simp]
theorem
ring.direct_limit.lift_add
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x + y) = ring.direct_limit.lift G f P g Hg x + ring.direct_limit.lift G f P g Hg y
@[simp]
theorem
ring.direct_limit.lift_neg
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (-x) = -ring.direct_limit.lift G f P g Hg x
@[simp]
theorem
ring.direct_limit.lift_sub
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x - y) = ring.direct_limit.lift G f P g Hg x - ring.direct_limit.lift G f P g Hg y
@[simp]
theorem
ring.direct_limit.lift_mul
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x y : ring.direct_limit G f) :
ring.direct_limit.lift G f P g Hg (x * y) = (ring.direct_limit.lift G f P g Hg x) * ring.direct_limit.lift G f P g Hg y
@[simp]
theorem
ring.direct_limit.lift_pow
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(g : Π (i : ι), G i → P)
[∀ (i : ι), is_ring_hom (g i)]
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), g j (f i j hij x) = g i x)
(x : ring.direct_limit G f)
(n : ℕ) :
ring.direct_limit.lift G f P g Hg (x ^ n) = ring.direct_limit.lift G f P g Hg x ^ n
theorem
ring.direct_limit.lift_unique
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
{G : ι → Type w}
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), comm_ring (G i)]
{f : Π (i j : ι), i ≤ j → G i → G j}
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(P : Type u₁)
[comm_ring P]
(F : ring.direct_limit G f → P)
[is_ring_hom F]
(x : ring.direct_limit G f) :
F x = ring.direct_limit.lift G f P (λ (i : ι) (x : G i), F (ring.direct_limit.of G f i x)) _ x
@[instance]
def
field.direct_limit.nontrivial
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f] :
nontrivial (ring.direct_limit G f)
theorem
field.direct_limit.exists_inv
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{p : ring.direct_limit G f}
(a : p ≠ 0) :
∃ (y : ring.direct_limit G f), p * y = 1
def
field.direct_limit.inv
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
(p : ring.direct_limit G f) :
Equations
- field.direct_limit.inv G f p = dite (p = 0) (λ (H : p = 0), 0) (λ (H : ¬p = 0), classical.some _)
theorem
field.direct_limit.mul_inv_cancel
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{p : ring.direct_limit G f}
(hp : p ≠ 0) :
p * field.direct_limit.inv G f p = 1
theorem
field.direct_limit.inv_mul_cancel
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f]
{p : ring.direct_limit G f}
(hp : p ≠ 0) :
(field.direct_limit.inv G f p) * p = 1
def
field.direct_limit.field
{ι : Type v}
[nonempty ι]
[decidable_eq ι]
[directed_order ι]
(G : ι → Type w)
[Π (i : ι), decidable_eq (G i)]
[Π (i : ι), field (G i)]
(f : Π (i j : ι), i ≤ j → G i → G j)
[∀ (i j : ι) (hij : i ≤ j), is_ring_hom (f i j hij)]
[directed_system G f] :
field (ring.direct_limit G f)
Equations
- field.direct_limit.field G f = {add := comm_ring.add (ring.direct_limit.comm_ring G f), add_assoc := _, zero := comm_ring.zero (ring.direct_limit.comm_ring G f), zero_add := _, add_zero := _, neg := comm_ring.neg (ring.direct_limit.comm_ring G f), add_left_neg := _, add_comm := _, mul := comm_ring.mul (ring.direct_limit.comm_ring G f), mul_assoc := _, one := comm_ring.one (ring.direct_limit.comm_ring G f), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.direct_limit.inv G f _inst_8, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}