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 #
theorem
Module.DirectedSystem.map_self
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
(i : ι)
(x : G i)
(h : i ≤ i)
:
(f i i h) x = x
A copy of DirectedSystem.map_self specialized to linear maps, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
theorem
Module.DirectedSystem.map_map
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
{i j k : ι}
(hij : i ≤ j)
(hjk : j ≤ k)
(x : G i)
:
(f j k hjk) ((f i j hij) x) = (f i k ⋯) x
A copy of DirectedSystem.map_map specialized to linear maps, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
noncomputable def
Module.DirectLimit
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
:
Type (max v w)
The direct limit of a directed system is the modules glued together along the maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
Module.DirectLimit.addCommGroup
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
Module.DirectLimit.module
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
:
Module R (Module.DirectLimit G f)
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
Module.DirectLimit.inhabited
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
:
Inhabited (Module.DirectLimit G f)
Equations
- Module.DirectLimit.inhabited G f = { default := 0 }
noncomputable instance
Module.DirectLimit.unique
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
[IsEmpty ι]
:
Unique (Module.DirectLimit G f)
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
Module.DirectLimit.of
(R : Type u)
[Ring R]
(ι : Type v)
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
(i : ι)
:
G i →ₗ[R] Module.DirectLimit G f
The canonical map from a component to the direct limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Module.DirectLimit.of_f
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{i j : ι}
{hij : i ≤ j}
{x : G i}
:
(Module.DirectLimit.of R ι G f j) ((f i j hij) x) = (Module.DirectLimit.of R ι G f i) x
theorem
Module.DirectLimit.exists_of
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(z : Module.DirectLimit G f)
:
∃ (i : ι) (x : G i), (Module.DirectLimit.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.DirectLimit.induction_on
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{C : Module.DirectLimit G f → Prop}
(z : Module.DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((Module.DirectLimit.of R ι G f i) x))
:
C z
noncomputable def
Module.DirectLimit.lift
(R : Type u)
[Ring R]
(ι : Type v)
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
{P : Type u₁}
[AddCommGroup 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.DirectLimit 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
Module.DirectLimit.lift_of
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{P : Type u₁}
[AddCommGroup 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.DirectLimit.lift R ι G f g Hg) ((Module.DirectLimit.of R ι G f i) x) = (g i) x
theorem
Module.DirectLimit.lift_unique
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{P : Type u₁}
[AddCommGroup P]
[Module R P]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(F : Module.DirectLimit G f →ₗ[R] P)
(x : Module.DirectLimit G f)
:
F x = (Module.DirectLimit.lift R ι G f (fun (i : ι) => F ∘ₗ Module.DirectLimit.of R ι G f i) ⋯) x
theorem
Module.DirectLimit.lift_injective
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{P : Type u₁}
[AddCommGroup 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)
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(injective : ∀ (i : ι), Function.Injective ⇑(g i))
:
Function.Injective ⇑(Module.DirectLimit.lift R ι G f g Hg)
noncomputable def
Module.DirectLimit.map
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
(g : (i : ι) → G i →ₗ[R] G' i)
(hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i)
:
Module.DirectLimit G f →ₗ[R] Module.DirectLimit G' f'
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of linear maps gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a linear map
lim G ⟶ lim G'.
Equations
- Module.DirectLimit.map g hg = Module.DirectLimit.lift R ι G f (fun (i : ι) => Module.DirectLimit.of R ι G' f' i ∘ₗ g i) ⋯
Instances For
@[simp]
theorem
Module.DirectLimit.map_apply_of
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
(g : (i : ι) → G i →ₗ[R] G' i)
(hg : ∀ (i j : ι) (h : i ≤ j), g j ∘ₗ f i j h = f' i j h ∘ₗ g i)
{i : ι}
(x : G i)
:
(Module.DirectLimit.map g hg) ((Module.DirectLimit.of R ι G f i) x) = (Module.DirectLimit.of R ι G' f' i) ((g i) x)
@[simp]
theorem
Module.DirectLimit.map_id
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
:
Module.DirectLimit.map (fun (x : ι) => LinearMap.id) ⋯ = LinearMap.id
theorem
Module.DirectLimit.map_comp
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
{G'' : ι → Type v''}
[(i : ι) → AddCommGroup (G'' i)]
[(i : ι) → Module R (G'' i)]
{f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(g₁ : (i : ι) → G i →ₗ[R] G' i)
(g₂ : (i : ι) → G' i →ₗ[R] G'' i)
(hg₁ : ∀ (i j : ι) (h : i ≤ j), g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i)
(hg₂ : ∀ (i j : ι) (h : i ≤ j), g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i)
:
Module.DirectLimit.map g₂ hg₂ ∘ₗ Module.DirectLimit.map g₁ hg₁ = Module.DirectLimit.map (fun (i : ι) => g₂ i ∘ₗ g₁ i) ⋯
noncomputable def
Module.DirectLimit.congr
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃ₗ[R] G' i)
(he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i))
:
Module.DirectLimit G f ≃ₗ[R] Module.DirectLimit G' f'
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence
lim G ≅ lim G'.
Equations
- Module.DirectLimit.congr e he = LinearEquiv.ofLinear (Module.DirectLimit.map (fun (x : ι) => ↑(e x)) he) (Module.DirectLimit.map (fun (i : ι) => ↑(e i).symm) ⋯) ⋯ ⋯
Instances For
theorem
Module.DirectLimit.congr_apply_of
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃ₗ[R] G' i)
(he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i))
{i : ι}
(g : G i)
:
(Module.DirectLimit.congr e he) ((Module.DirectLimit.of R ι G f i) g) = (Module.DirectLimit.of R ι G' f' i) ((e i) g)
theorem
Module.DirectLimit.congr_symm_apply_of
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃ₗ[R] G' i)
(he : ∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i))
{i : ι}
(g : G' i)
:
(Module.DirectLimit.congr e he).symm ((Module.DirectLimit.of R ι G' f' i) g) = (Module.DirectLimit.of R ι G f i) ((e i).symm g)
noncomputable def
Module.DirectLimit.totalize
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (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.
Equations
- Module.DirectLimit.totalize G f i j = if h : i ≤ j then f i j h else 0
Instances For
theorem
Module.DirectLimit.totalize_of_le
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{i j : ι}
(h : i ≤ j)
:
Module.DirectLimit.totalize G f i j = f i j h
theorem
Module.DirectLimit.toModule_totalize_of_le
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[(i : ι) → (k : G i) → Decidable (k ≠ 0)]
{x : DirectSum ι G}
{i j : ι}
(hij : i ≤ j)
(hx : ∀ k ∈ DFinsupp.support x, k ≤ i)
:
(DirectSum.toModule R ι (G j) fun (k : ι) => Module.DirectLimit.totalize G f k j) x = (f i j hij) ((DirectSum.toModule R ι (G i) fun (k : ι) => Module.DirectLimit.totalize G f k i) x)
theorem
Module.DirectLimit.of.zero_exact_aux
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[(i : ι) → (k : G i) → Decidable (k ≠ 0)]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{x : DirectSum ι G}
(H : Submodule.Quotient.mk x = 0)
:
∃ (j : ι),
(∀ k ∈ DFinsupp.support x, k ≤ j) ∧ (DirectSum.toModule R ι (G j) fun (i : ι) => Module.DirectLimit.totalize G f i j) x = 0
theorem
Module.DirectLimit.of.zero_exact
{R : Type u}
[Ring R]
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DecidableEq ι]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{i : ι}
{x : G i}
(H : (Module.DirectLimit.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.
noncomputable def
AddCommGroup.DirectLimit
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
[DecidableEq ι]
(f : (i j : ι) → i ≤ j → G i →+ G j)
:
Type (max w v)
The direct limit of a directed system is the abelian groups glued together along the maps.
Equations
- AddCommGroup.DirectLimit G f = Module.DirectLimit G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toIntLinearMap
Instances For
theorem
AddCommGroup.DirectLimit.directedSystem
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[h : DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
:
DirectedSystem G fun (i j : ι) (hij : i ≤ j) => ⇑(f i j hij).toIntLinearMap
noncomputable instance
AddCommGroup.DirectLimit.inst
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
:
Equations
- AddCommGroup.DirectLimit.inst G f = Module.DirectLimit.addCommGroup G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toIntLinearMap
noncomputable instance
AddCommGroup.DirectLimit.instInhabited
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
:
Equations
- AddCommGroup.DirectLimit.instInhabited G f = { default := 0 }
noncomputable instance
AddCommGroup.DirectLimit.instUniqueOfIsEmpty
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
[IsEmpty ι]
:
Equations
- AddCommGroup.DirectLimit.instUniqueOfIsEmpty G f = Module.DirectLimit.unique G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toIntLinearMap
noncomputable def
AddCommGroup.DirectLimit.of
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
(i : ι)
:
G i →+ AddCommGroup.DirectLimit G f
The canonical map from a component to the direct limit.
Equations
- AddCommGroup.DirectLimit.of G f i = (Module.DirectLimit.of ℤ ι G (fun (i j : ι) (hij : i ≤ j) => (f i j hij).toIntLinearMap) i).toAddMonoidHom
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.of_f
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{i j : ι}
(hij : i ≤ j)
(x : G i)
:
(AddCommGroup.DirectLimit.of G f j) ((f i j hij) x) = (AddCommGroup.DirectLimit.of G f i) x
theorem
AddCommGroup.DirectLimit.induction_on
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{C : AddCommGroup.DirectLimit G f → Prop}
(z : AddCommGroup.DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((AddCommGroup.DirectLimit.of G f i) x))
:
C z
theorem
AddCommGroup.DirectLimit.of.zero_exact
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f i j h)]
(i : ι)
(x : G i)
(h : (AddCommGroup.DirectLimit.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.
noncomputable def
AddCommGroup.DirectLimit.lift
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
(P : Type u₁)
[AddCommGroup 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)
:
AddCommGroup.DirectLimit 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
- AddCommGroup.DirectLimit.lift G f P g Hg = (Module.DirectLimit.lift ℤ ι G (fun (i j : ι) (hij : i ≤ j) => (f i j hij).toIntLinearMap) (fun (i : ι) => (g i).toIntLinearMap) Hg).toAddMonoidHom
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.lift_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u₁)
[AddCommGroup 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)
:
(AddCommGroup.DirectLimit.lift G f P g Hg) ((AddCommGroup.DirectLimit.of G f i) x) = (g i) x
theorem
AddCommGroup.DirectLimit.lift_unique
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u₁)
[AddCommGroup P]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(F : AddCommGroup.DirectLimit G f →+ P)
(x : AddCommGroup.DirectLimit G f)
:
F x = (AddCommGroup.DirectLimit.lift G f P (fun (i : ι) => F.comp (AddCommGroup.DirectLimit.of G f i)) ⋯) x
theorem
AddCommGroup.DirectLimit.lift_injective
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u₁)
[AddCommGroup 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)
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(injective : ∀ (i : ι), Function.Injective ⇑(g i))
:
Function.Injective ⇑(AddCommGroup.DirectLimit.lift G f P g Hg)
noncomputable def
AddCommGroup.DirectLimit.map
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(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))
:
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of group homomorphisms gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a group
homomorphism lim G ⟶ lim G'.
Equations
- AddCommGroup.DirectLimit.map g hg = AddCommGroup.DirectLimit.lift G f (AddCommGroup.DirectLimit G' f') (fun (i : ι) => (AddCommGroup.DirectLimit.of G' f' i).comp (g i)) ⋯
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.map_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(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)
@[simp]
theorem
AddCommGroup.DirectLimit.map_id
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
:
AddCommGroup.DirectLimit.map (fun (x : ι) => AddMonoidHom.id (G x)) ⋯ = AddMonoidHom.id (AddCommGroup.DirectLimit G f)
theorem
AddCommGroup.DirectLimit.map_comp
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
{G'' : ι → Type v''}
[(i : ι) → AddCommGroup (G'' i)]
{f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(g₁ : (i : ι) → G i →+ G' i)
(g₂ : (i : ι) → G' i →+ G'' i)
(hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
(hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i))
:
(AddCommGroup.DirectLimit.map g₂ hg₂).comp (AddCommGroup.DirectLimit.map g₁ hg₁) = AddCommGroup.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i)) ⋯
noncomputable def
AddCommGroup.DirectLimit.congr
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+ G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i))
:
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence
lim G ⟶ lim G'.
Equations
- AddCommGroup.DirectLimit.congr e he = (AddCommGroup.DirectLimit.map (fun (x : ι) => ↑(e x)) he).toAddEquiv (AddCommGroup.DirectLimit.map (fun (i : ι) => ↑(e i).symm) ⋯) ⋯ ⋯
Instances For
theorem
AddCommGroup.DirectLimit.congr_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+ G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i))
{i : ι}
(g : G i)
:
(AddCommGroup.DirectLimit.congr e he) ((AddCommGroup.DirectLimit.of G f i) g) = (AddCommGroup.DirectLimit.of G' f' i) ((e i) g)
theorem
AddCommGroup.DirectLimit.congr_symm_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → AddCommGroup (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type v'}
[(i : ι) → AddCommGroup (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+ G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i))
{i : ι}
(g : G' i)
:
(AddCommGroup.DirectLimit.congr e he).symm ((AddCommGroup.DirectLimit.of G' f' i) g) = (AddCommGroup.DirectLimit.of G f i) ((e i).symm g)
noncomputable def
Ring.DirectLimit
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
Ring.DirectLimit.commRing
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
:
CommRing (Ring.DirectLimit G f)
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
Ring.DirectLimit.ring
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
:
Ring (Ring.DirectLimit G f)
Equations
- Ring.DirectLimit.ring G f = CommRing.toRing
noncomputable instance
Ring.DirectLimit.zero
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
:
Zero (Ring.DirectLimit G f)
Equations
- Ring.DirectLimit.zero G f = id { zero := 0 }
noncomputable instance
Ring.DirectLimit.instInhabited
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
:
Inhabited (Ring.DirectLimit G f)
Equations
- Ring.DirectLimit.instInhabited G f = { default := 0 }
noncomputable def
Ring.DirectLimit.of
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
(i : ι)
:
G i →+* Ring.DirectLimit G f
The canonical map from a component to the direct limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Ring.DirectLimit.of_f
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
{i j : ι}
(hij : i ≤ j)
(x : G i)
:
(Ring.DirectLimit.of G f j) (f i j hij x) = (Ring.DirectLimit.of G f i) x
theorem
Ring.DirectLimit.exists_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(z : Ring.DirectLimit G f)
:
∃ (i : ι) (x : G i), (Ring.DirectLimit.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.DirectLimit.Polynomial.exists_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f' : (i j : ι) → i ≤ j → G i →+* G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(q : Polynomial (Ring.DirectLimit G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)))
:
∃ (i : ι) (p : Polynomial (G i)),
Polynomial.map (Ring.DirectLimit.of G (fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)) i) p = q
theorem
Ring.DirectLimit.induction_on
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{C : Ring.DirectLimit G f → Prop}
(z : Ring.DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((Ring.DirectLimit.of G f i) x))
:
C z
theorem
Ring.DirectLimit.of.zero_exact_aux2
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f' : (i j : ι) → i ≤ j → G i →+* G j)
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
{x : FreeCommRing ((i : ι) × G i)}
{s t : Set ((i : ι) × G i)}
[DecidablePred fun (x : (i : ι) × G i) => x ∈ s]
[DecidablePred fun (x : (i : ι) × G i) => x ∈ t]
(hxs : x.IsSupported s)
{j k : ι}
(hj : ∀ z ∈ s, z.fst ≤ j)
(hk : ∀ z ∈ t, z.fst ≤ k)
(hjk : j ≤ k)
(hst : s ⊆ t)
:
(f' j k hjk) ((FreeCommRing.lift fun (ix : ↑s) => (f' (↑ix).fst j ⋯) (↑ix).snd) ((FreeCommRing.restriction s) x)) = (FreeCommRing.lift fun (ix : ↑t) => (f' (↑ix).fst k ⋯) (↑ix).snd) ((FreeCommRing.restriction t) x)
theorem
Ring.DirectLimit.of.zero_exact_aux
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f' : (i j : ι) → i ≤ j → G i →+* G j}
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{x : FreeCommRing ((i : ι) × G i)}
(H :
(Ideal.Quotient.mk
(Ideal.span
{a : FreeCommRing ((i : ι) × G i) |
(∃ (i : ι) (j : ι) (H : i ≤ j) (x : G i),
FreeCommRing.of ⟨j, (fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)) i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨ (∃ (i : ι), FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨ (∃ (i : ι) (x : G i) (y : G i),
FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨ ∃ (i : ι) (x : G i) (y : G i),
FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a}))
x = 0)
:
∃ (j : ι) (s : Set ((i : ι) × G i)) (H : ∀ k ∈ s, k.fst ≤ j),
x.IsSupported s ∧ ∀ [inst : DecidablePred fun (x : (i : ι) × G i) => x ∈ s],
(FreeCommRing.lift fun (ix : ↑s) => (f' (↑ix).fst j ⋯) (↑ix).snd) ((FreeCommRing.restriction s) x) = 0
theorem
Ring.DirectLimit.of.zero_exact
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f' : (i j : ι) → i ≤ j → G i →+* G j}
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{i : ι}
{x : G i}
(hix : (Ring.DirectLimit.of G (fun (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.DirectLimit.of_injective
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
(f' : (i j : ι) → i ≤ j → G i →+* G j)
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
(hf : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij))
(i : ι)
:
Function.Injective ⇑(Ring.DirectLimit.of G (fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)) i)
If the maps in the directed system are injective, then the canonical maps from the components to the direct limits are injective.
noncomputable def
Ring.DirectLimit.lift
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[(i : ι) → CommRing (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
(P : Type u₁)
[CommRing 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.DirectLimit 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
- One or more equations did not get rendered due to their size.
Instances For
theorem
Ring.DirectLimit.lift_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
(P : Type u₁)
[CommRing 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.DirectLimit.lift G f P g Hg) ((Ring.DirectLimit.of G f i) x) = (g i) x
theorem
Ring.DirectLimit.lift_unique
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
(P : Type u₁)
[CommRing P]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(F : Ring.DirectLimit G f →+* P)
(x : Ring.DirectLimit G f)
:
F x = (Ring.DirectLimit.lift G f P (fun (i : ι) => F.comp (Ring.DirectLimit.of G f i)) ⋯) x
theorem
Ring.DirectLimit.lift_injective
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i → G j}
(P : Type u₁)
[CommRing 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)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(injective : ∀ (i : ι), Function.Injective ⇑(g i))
:
Function.Injective ⇑(Ring.DirectLimit.lift G f P g Hg)
noncomputable def
Ring.DirectLimit.map
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (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))
:
(Ring.DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) →+* Ring.DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of ring homomorphisms gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a ring
homomorphism lim G ⟶ lim G'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Ring.DirectLimit.map_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (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)
:
(Ring.DirectLimit.map g hg) ((Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) i) x) = (Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)) i) ((g i) x)
@[simp]
theorem
Ring.DirectLimit.map_id
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
:
Ring.DirectLimit.map (fun (x : ι) => RingHom.id (G x)) ⋯ = RingHom.id (Ring.DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h))
theorem
Ring.DirectLimit.map_comp
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+* G' j}
{G'' : ι → Type v''}
[(i : ι) → CommRing (G'' i)]
{f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(g₁ : (i : ι) → G i →+* G' i)
(g₂ : (i : ι) → G' i →+* G'' i)
(hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
(hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i))
:
(Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) = Ring.DirectLimit.map (fun (i : ι) => (g₂ i).comp (g₁ i)) ⋯
noncomputable def
Ring.DirectLimit.congr
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+* G' j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+* G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i))
:
(Ring.DirectLimit G fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) ≃+* Ring.DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)
Consider direct limits lim G and lim G' with direct system f and f' respectively, any
family of equivalences eᵢ : Gᵢ ≅ G'ᵢ such that e ∘ f = f' ∘ e induces an equivalence
lim G ⟶ lim G'.
Equations
- Ring.DirectLimit.congr e he = RingEquiv.ofHomInv (Ring.DirectLimit.map (fun (x : ι) => ↑(e x)) he) (Ring.DirectLimit.map (fun (i : ι) => ↑(e i).symm) ⋯) ⋯ ⋯
Instances For
theorem
Ring.DirectLimit.congr_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+* G' j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+* G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i))
{i : ι}
(g : G i)
:
(Ring.DirectLimit.congr e he) ((Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) i) g) = (Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)) i) ((e i) g)
theorem
Ring.DirectLimit.congr_symm_apply_of
{ι : Type v}
[Preorder ι]
{G : ι → Type w}
[(i : ι) → CommRing (G i)]
{f : (i j : ι) → i ≤ j → G i →+* G j}
{G' : ι → Type v'}
[(i : ι) → CommRing (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+* G' j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(e : (i : ι) → G i ≃+* G' i)
(he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i))
{i : ι}
(g : G' i)
:
(Ring.DirectLimit.congr e he).symm ((Ring.DirectLimit.of G' (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f' x x_1 h)) i) g) = (Ring.DirectLimit.of G (fun (x x_1 : ι) (h : x ≤ x_1) => ⇑(f x x_1 h)) i) ((e i).symm g)
noncomputable instance
Field.DirectLimit.nontrivial
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f' : (i j : ι) → i ≤ j → G i →+* G j)
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
:
Nontrivial (Ring.DirectLimit G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h))
Equations
- ⋯ = ⋯
theorem
Field.DirectLimit.exists_inv
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
{p : Ring.DirectLimit G f}
:
p ≠ 0 → ∃ (y : Ring.DirectLimit G f), p * y = 1
noncomputable def
Field.DirectLimit.inv
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
(p : Ring.DirectLimit G f)
:
Ring.DirectLimit G f
Noncomputable multiplicative inverse in a direct limit of fields.
Equations
- Field.DirectLimit.inv G f p = if H : p = 0 then 0 else Classical.choose ⋯
Instances For
theorem
Field.DirectLimit.mul_inv_cancel
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
{p : Ring.DirectLimit G f}
(hp : p ≠ 0)
:
p * Field.DirectLimit.inv G f p = 1
theorem
Field.DirectLimit.inv_mul_cancel
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f : (i j : ι) → i ≤ j → G i → G j)
{p : Ring.DirectLimit G f}
(hp : p ≠ 0)
:
Field.DirectLimit.inv G f p * p = 1
@[reducible, inline]
noncomputable abbrev
Field.DirectLimit.field
{ι : Type v}
[Preorder ι]
(G : ι → Type w)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[(i : ι) → Field (G i)]
(f' : (i j : ι) → i ≤ j → G i →+* G j)
[DirectedSystem G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h)]
:
Field (Ring.DirectLimit G fun (i j : ι) (h : i ≤ j) => ⇑(f' i j h))
Noncomputable field structure on the direct limit of fields. See note [reducible non-instances].