Ring.DirectLimit.of.zero_exact
theorem Ring.DirectLimit.of.zero_exact :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → CommRing (G i)]
{f' : (i j : ι) → i ≤ j → G i →+* G j} [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)]
[inst_3 : IsDirected ι fun x x_1 => x ≤ x_1] {i : ι} {x : G i},
(Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0
The theorem `Ring.DirectLimit.of.zero_exact` states that for any directed system of commutative rings (indexed by a preordered set), if a component maps to zero in the direct limit of this system, then there exists a larger or equal index in the system such that the component also maps to zero at this larger index. In other words, if an element becomes zero in the limit, it will already be zero in some sufficiently large module in the original directed system.
More concisely: If $f:\mathcal{I} \to \text{Rings}$ is a directed system of commutative rings and $x \in \mathop{\lim}\limits^{} f.I$ with $x = 0$ in the limit, then there exists $i \in \mathcal{I}$ such that $f.i(x) = 0$.
|
Module.DirectLimit.of.zero_exact
theorem Module.DirectLimit.of.zero_exact :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] {G : ι → Type w}
[inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} [inst_4 : DecidableEq ι]
[inst_5 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_6 : IsDirected ι fun x x_1 => x ≤ x_1] {i : ι}
{x : G i}, (Module.DirectLimit.of R ι G f i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
This theorem states that for any ring R, any preorder ι, and any directed system G of modules over R indexed by ι, if a component x in a module of the directed system maps to zero in the direct limit of the system, then there exists a module in the directed system (denoted by some j), further up in the order, such that the image of x under the morphism from the module of x to the module j is already zero. Various conditions are assumed including that for any two elements of the index set, we can decide if they are equal, and that the directed system and the preorder are directed in the sense that for any two elements in the system or the index set, there is a third element that is greater than or equal to them.
More concisely: For any ring R, preorder ι, and directed system G of R-modules indexed by ι, if an element x in a module maps to zero in the direct limit, then there exists a module in G with an index greater than the current one, such that x maps to zero in this module.
|
AddCommGroup.DirectLimit.of.zero_exact
theorem AddCommGroup.DirectLimit.of.zero_exact :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j} [inst_3 : IsDirected ι fun x x_1 => x ≤ x_1]
[inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι) (x : G i),
(AddCommGroup.DirectLimit.of G f i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f i j hij) x = 0
This theorem, `AddCommGroup.DirectLimit.of.zero_exact`, states that for any type `ι` that forms a preorder, with `DecidableEq ι` implying that equality within the type `ι` is decidable, and for any function `G` that maps `ι` to an additive commutative group, along with a directed system `f` that maps an element of `G i` to `G j` for `i ≤ j`, it holds that if the canonical map from a component to the direct limit yields zero for an element `x` from `G i`, then there exists some `j` greater than or equal to `i` such that the mapping of `x` under the directed system `f` from `G i` to `G j` is zero. This theorem essentially guarantees that a zero element in the direct limit corresponds to a zero element in one of the larger modules in the directed system.
More concisely: For any preorder ι with decidable equality, any function G from ι to an additive commutative group, and any directed system f with zero-preserving maps, if an element x in Gi maps to zero in the direct limit, then there exists a j ≥ i such that x maps to zero in Gj.
|
Module.DirectedSystem.map_map
theorem Module.DirectedSystem.map_map :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] {G : ι → Type w}
[inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [inst_4 : DirectedSystem G fun i j h => ⇑(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
This theorem, `Module.DirectedSystem.map_map`, is a version of the `DirectedSystem.map_map` theorem specifically crafted for linear maps in the context of Module theory. It states that for any given ring `R`, an indexed type `ι` with a preorder, an indexed type `G` where each `G i` is an additive commutative group and also an `R`-module, and a system of linear maps `f` from `G i` to `G j` for each pair `(i, j)` with `i ≤ j`, if the `G`'s form a directed system under these maps, then for any `i`, `j`, and `k` in `ι` with `i ≤ j ≤ k` and any element `x` of `G i`, applying `f i j` to `x` and then `f j k` to the result is the same as applying a certain linear map `f i k` to `x` directly.
More concisely: For any ring `R`, directed system `(G i, ≤, (f ij : G i → G j))` of `R`-modules `G i` with `ι` as index, and any element `x` in `G i` with `i ≤ j ≤ k`, we have `f i k (x) = f i j (x) ∣∣ f j k`.
|
Ring.DirectLimit.induction_on
theorem Ring.DirectLimit.induction_on :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j} [inst_2 : Nonempty ι] [inst_3 : IsDirected ι fun x x_1 => x ≤ x_1]
{C : Ring.DirectLimit G f → Prop} (z : Ring.DirectLimit G f),
(∀ (i : ι) (x : G i), C ((Ring.DirectLimit.of G f i) x)) → C z
This theorem is about direct limits in the category of rings. It states that for any preorder `ι`, any indexed family of commutative rings `G : ι → Type w`, any transition maps `f : (i j : ι) → i ≤ j → G i → G j`, and a property `C` of elements in the direct limit ring, if `C` holds for every element in the image of the canonical map `Ring.DirectLimit.of G f i` for each `i`, then `C` holds for every element in the direct limit ring `Ring.DirectLimit G f`. In essence, it provides a principle of induction on the construction of the direct limit. This theorem is fundamental in the theory of direct limits and allows one to prove properties of the whole direct limit based on the properties of its parts.
More concisely: If `C` is a property of elements in the direct limit of an indexed family of commutative rings `G : ι → Type w` and `C` holds for the image of the canonical map for each `i`, then `C` holds for every element in the direct limit ring.
|
AddCommGroup.DirectLimit.map_apply_of
theorem AddCommGroup.DirectLimit.map_apply_of :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j} {G' : ι → Type v'} [inst_3 : (i : ι) → AddCommGroup (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j} (g : (i : ι) → G i →+ G' i)
(hg : ∀ (i j : ι) (h : i ≤ j), (g j).comp (f i j h) = (f' i j h).comp (g i)) {i : ι} (x : G i),
(AddCommGroup.DirectLimit.map g hg) ((AddCommGroup.DirectLimit.of G f i) x) =
(AddCommGroup.DirectLimit.of G' f' i) ((g i) x)
This theorem states that for any type `ι` with a preorder, and families of additive commutative groups `G` and `G'` indexed by `ι`, if we have morphisms `f` and `f'` between elements of these families respecting the preorder, and a family of morphisms `g` from `G` to `G'` such that the composition of `g` and `f` yields the same result as the composition of `f'` and `g`, then for any `i` in `ι` and any element `x` of `G i`, the result of applying the direct limit map from `G` to `G'` to the image of `x` under the direct limit map of `G` is equal to the result of applying the direct limit map of `G'` to the image of `x` under `g i`. In more mathematical terms, this theorem essentially verifies that a certain diagram in the category of additive commutative groups commutes.
More concisely: Given additive commutative groups indexed by a preordered type `ι`, if morphisms `f`, `f'`, and a family of morphisms `g` respect the preorder and commute, then the direct limit of `g` applied to the direct limit of `G` is equal to the direct limit of `g` applied to the direct limit of `G'` when applied to any element of `G`.
|
Ring.DirectLimit.of_injective
theorem Ring.DirectLimit.of_injective :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → CommRing (G i)]
(f' : (i j : ι) → i ≤ j → G i →+* G j) [inst_2 : IsDirected ι fun x x_1 => x ≤ x_1]
[inst_3 : DirectedSystem G fun i j h => ⇑(f' i j h)],
(∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)) →
∀ (i : ι), Function.Injective ⇑(Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i)
This theorem states that if all the maps in a directed system of rings are injective (a map `f` is injective if whenever `f(x) = f(y)` then `x = y`), then the canonical maps from the components of this system to their direct limit are also injective.
Here, a directed system of rings is a collection of rings indexed by a preorder (a set with a binary relation that is reflexive and transitive) such that for any two indices there exists an index that is greater than or equal to both, and a family of ring homomorphisms that respects this ordering. The direct limit of this system is a way of 'collapsing' the system into a single ring in a way that respects the directed structure.
More concisely: If every map in a directed system of rings is injective, then the canonical maps from the components to their direct limit are also injective.
|
Ring.DirectLimit.exists_of
theorem Ring.DirectLimit.exists_of :
∀ {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j} [inst_2 : Nonempty ι] [inst_3 : IsDirected ι fun x x_1 => x ≤ x_1]
(z : Ring.DirectLimit G f), ∃ i x, (Ring.DirectLimit.of G f i) x = z
This theorem states that for any element in the direct limit of a directed system of commutative rings indexed by a preorder, there exists an element in a component of the directed system that corresponds to this element in the direct limit. More specifically, given a directed system of rings described by a function `f` that maps elements from ring `G i` to `G j` for `i ≤ j`, and an element `z` in the direct limit of this system, there is some index `i` and element `x` in `G i` such that the image of `x` under the canonical map `Ring.DirectLimit.of G f i` is `z`.
More concisely: For any element in the direct limit of a directed system of commutative rings, there exists an element in some component and a map from that component to the direct limit that maps the element to the given element in the direct limit.
|
Module.DirectedSystem.map_self
theorem Module.DirectedSystem.map_self :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] {G : ι → Type w}
[inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)] (i : ι) (x : G i)
(h : i ≤ i), (f i i h) x = x
This theorem, `Module.DirectedSystem.map_self`, is specialized for linear maps in a directed system of modules. It states that for any ring `R`, index type `ι` with a preorder, and a type function `G` mapping each index to an additive commutative group that also forms a `R`-module, if we have a family of linear maps `f` that honors the order and forms a directed system, then for any index `i` and any element `x` in the module `G i`, applying the linear map `f` that maps `i` to itself does not change `x`, i.e., `(f i i h) x = x`, where `h` is the proof that `i` is less than or equal to itself (which is always true by reflexivity of the preorder).
More concisely: For any ring `R`, index type `ι` with a preorder, and a family of linear maps `f` in a directed system of `R`-modules `(G i : Type _)` over `ι`, given an element `x` in `G i`, we have `f i i x = x`.
|
Module.DirectLimit.exists_of
theorem Module.DirectLimit.exists_of :
∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] {G : ι → Type w}
[inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} [inst_4 : DecidableEq ι] [inst_5 : Nonempty ι]
[inst_6 : IsDirected ι fun x x_1 => x ≤ x_1] (z : Module.DirectLimit G f),
∃ i x, (Module.DirectLimit.of R ι G f i) x = z
This theorem asserts that for any direct limit module of a directed system, each element of the direct limit corresponds to an element in some component of the directed system. Specifically, given a ring `R`, a preorder `ι`, a function `G` from `ι` to a type, where each type in the image of `G` is an additive commutative group and a module over `R`, and a function `f` providing a linear map between each pair of modules in the directed order, any element `z` in the direct limit of this system can be expressed as the image of an element `x` from the module `G i` for some `i` in `ι` under the direct limit map. This statement is true under the assumption that `ι` has decidable equality, is nonempty, and is directed with respect to the order.
More concisely: Given a direct system of additive commutative `R`-modules indexed by a decidable, nonempty, and directed preorder `ι`, every element in the direct limit can be expressed as the image of an element from some module in the system under the direct limit map.
|