Direct limit of modules and abelian groups #
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.
It is constructed as a quotient of the free module instead of a quotient of the disjoint union so as to make the operations (addition etc.) "computable".
Main definitions #
theorem
Module.DirectedSystem.map_self
{ι : Type u_1}
[Preorder ι]
{F : ι → Type u_4}
{T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
(f : (i j : ι) → (h : i ≤ j) → T h)
[⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
[DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
⦃i : ι⦄
(x : F i)
:
Alias of DirectedSystem.map_self'.
A copy of DirectedSystem.map_self specialized to FunLike, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
theorem
Module.DirectedSystem.map_map
{ι : Type u_1}
[Preorder ι]
{F : ι → Type u_4}
{T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
(f : (i j : ι) → (h : i ≤ j) → T h)
[⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
[DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
⦃i j k : ι⦄
(hij : i ≤ j)
(hjk : j ≤ k)
(x : F i)
:
Alias of DirectedSystem.map_map'.
A copy of DirectedSystem.map_map specialized to FunLike, as otherwise the
fun i j h ↦ f i j h can confuse the simplifier.
inductive
Module.DirectLimit.Eqv
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
:
The relation on the direct sum that generates the additive congruence that defines the colimit as a quotient.
- of_map {R : Type u_1} [Semiring R] {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} [DecidableEq ι] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} {i j : ι} (h : i ≤ j) (x : G i) : Eqv f ((DirectSum.lof R ι G i) x) ((DirectSum.lof R ι G j) ((f i j h) x))
Instances For
noncomputable def
Module.DirectLimit
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[DecidableEq ι]
:
Type (max u_2 u_3)
The direct limit of a directed system is the modules glued together along the maps.
Equations
Instances For
noncomputable instance
Module.DirectLimit.addCommMonoid
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
:
AddCommMonoid (DirectLimit G f)
Equations
noncomputable instance
Module.DirectLimit.module
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
:
Module R (DirectLimit G f)
Equations
noncomputable instance
Module.DirectLimit.addCommGroup
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
[DecidableEq ι]
(G : ι → Type u_4)
[(i : ι) → AddCommGroup (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
:
AddCommGroup (DirectLimit G f)
Equations
noncomputable instance
Module.DirectLimit.inhabited
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
:
Inhabited (DirectLimit G f)
Equations
noncomputable instance
Module.DirectLimit.unique
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[IsEmpty ι]
:
Unique (DirectLimit G f)
Equations
noncomputable def
Module.DirectLimit.of
(R : Type u_1)
[Semiring R]
(ι : Type u_2)
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
(i : ι)
:
The canonical map from a component to the direct limit.
Equations
Instances For
theorem
Module.DirectLimit.quotMk_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
(i : ι)
(x : G i)
:
@[simp]
theorem
Module.DirectLimit.of_f
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{i j : ι}
{hij : i ≤ j}
{x : G i}
:
theorem
Module.DirectLimit.exists_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(z : DirectLimit G f)
:
Every element of the direct limit corresponds to some element in some component of the directed system.
theorem
Module.DirectLimit.exists_of₂
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
(z w : DirectLimit G f)
:
theorem
Module.DirectLimit.induction_on
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{C : DirectLimit G f → Prop}
(z : DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((of R ι G f i) x))
:
C z
noncomputable def
Module.DirectLimit.lift
(R : Type u_1)
[Semiring R]
(ι : Type u_2)
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
{P : Type u_4}
[AddCommMonoid 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)
:
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
Instances For
@[simp]
theorem
Module.DirectLimit.lift_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid 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)
:
theorem
Module.DirectLimit.hom_ext
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid P]
[Module R P]
{g₁ g₂ : DirectLimit G f →ₗ[R] P}
(h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i)
:
theorem
Module.DirectLimit.hom_ext_iff
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid P]
[Module R P]
{g₁ g₂ : DirectLimit G f →ₗ[R] P}
:
@[simp]
theorem
Module.DirectLimit.lift_comp_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid P]
[Module R P]
(F : DirectLimit G f →ₗ[R] P)
:
@[deprecated Module.DirectLimit.lift_comp_of (since := "2025-08-11")]
theorem
Module.DirectLimit.lift_unique
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid P]
[Module R P]
(F : DirectLimit G f →ₗ[R] P)
(x : DirectLimit G f)
:
@[simp]
theorem
Module.DirectLimit.lift_of'
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
:
theorem
Module.DirectLimit.lift_injective
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{P : Type u_4}
[AddCommMonoid 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 ⇑(lift R ι G f g Hg)
noncomputable def
Module.DirectLimit.map
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (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)
:
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
Instances For
@[simp]
theorem
Module.DirectLimit.map_apply_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (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)
:
@[simp]
theorem
Module.DirectLimit.map_id
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
:
theorem
Module.DirectLimit.map_comp
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
{G'' : ι → Type u_6}
[(i : ι) → AddCommMonoid (G'' i)]
[(i : ι) → Module R (G'' i)]
{f'' : (i j : ι) → i ≤ j → G'' i →ₗ[R] G'' j}
(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)
:
noncomputable def
Module.DirectLimit.congr
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
(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))
:
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
Instances For
theorem
Module.DirectLimit.congr_apply_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
(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)
:
theorem
Module.DirectLimit.congr_symm_apply_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
[(i : ι) → Module R (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j}
(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)
:
noncomputable def
Module.DirectLimit.linearEquiv
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
:
The direct limit constructed as a quotient of the direct sum is isomorphic to the direct limit constructed as a quotient of the disjoint union.
Equations
Instances For
theorem
Module.DirectLimit.linearEquiv_of
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
{i : ι}
{g : G i}
:
theorem
Module.DirectLimit.linearEquiv_symm_mk
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
(f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
{g : (i : ι) × G i}
:
theorem
Module.DirectLimit.exists_eq_of_of_eq
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{i : ι}
{x y : G i}
(h : (of R ι G f i) x = (of R ι G f i) y)
:
theorem
Module.DirectLimit.of.zero_exact
{R : Type u_1}
[Semiring R]
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[DecidableEq ι]
[(i : ι) → AddCommMonoid (G i)]
[(i : ι) → Module R (G i)]
{f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
[DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{i : ι}
{x : G i}
(H : (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 u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
[DecidableEq ι]
(f : (i j : ι) → i ≤ j → G i →+ G j)
:
Type (max u_3 u_2)
The direct limit of a directed system is the abelian groups glued together along the maps.
Equations
Instances For
theorem
AddCommGroup.DirectLimit.directedSystem
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (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).toNatLinearMap
noncomputable instance
AddCommGroup.DirectLimit.instAddCommMonoid
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
:
AddCommMonoid (DirectLimit G f)
Equations
noncomputable instance
AddCommGroup.DirectLimit.addCommGroup
{ι : Type u_2}
[Preorder ι]
[DecidableEq ι]
(G : ι → Type u_4)
[(i : ι) → AddCommGroup (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
:
AddCommGroup (DirectLimit G f)
Equations
noncomputable instance
AddCommGroup.DirectLimit.instInhabited
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
:
Inhabited (DirectLimit G f)
Equations
noncomputable instance
AddCommGroup.DirectLimit.instUniqueOfIsEmpty
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
[IsEmpty ι]
:
Unique (DirectLimit G f)
Equations
noncomputable def
AddCommGroup.DirectLimit.of
{ι : Type u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
(i : ι)
:
The canonical map from a component to the direct limit.
Equations
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.of_f
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{i j : ι}
(hij : i ≤ j)
(x : G i)
:
theorem
AddCommGroup.DirectLimit.induction_on
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
[Nonempty ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
{C : DirectLimit G f → Prop}
(z : DirectLimit G f)
(ih : ∀ (i : ι) (x : G i), C ((of G f i) x))
:
C z
theorem
AddCommGroup.DirectLimit.of.zero_exact
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (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 : (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 u_2}
[Preorder ι]
(G : ι → Type u_3)
[(i : ι) → AddCommMonoid (G i)]
(f : (i j : ι) → i ≤ j → G i →+ G j)
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid P]
(g : (i : ι) → G i →+ P)
(Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x)
:
The universal property of the direct limit: maps from the components to another abelian group that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.
Equations
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.lift_of
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid 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)
:
theorem
AddCommGroup.DirectLimit.hom_ext
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid P]
{g₁ g₂ : DirectLimit G f →+ P}
(h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i))
:
theorem
AddCommGroup.DirectLimit.hom_ext_iff
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{P : Type u_4}
[AddCommMonoid P]
{g₁ g₂ : DirectLimit G f →+ P}
:
@[simp]
theorem
AddCommGroup.DirectLimit.lift_comp_of
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid P]
(F : DirectLimit G f →+ P)
:
@[deprecated AddCommGroup.DirectLimit.lift_comp_of (since := "2025-08-11")]
theorem
AddCommGroup.DirectLimit.lift_unique
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid P]
(F : DirectLimit G f →+ P)
(x : DirectLimit G f)
:
@[simp]
theorem
AddCommGroup.DirectLimit.lift_of'
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
:
theorem
AddCommGroup.DirectLimit.lift_injective
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
(P : Type u_4)
[AddCommMonoid 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 ⇑(lift G f P g Hg)
noncomputable def
AddCommGroup.DirectLimit.map
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (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
Instances For
@[simp]
theorem
AddCommGroup.DirectLimit.map_apply_of
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (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)
:
@[simp]
theorem
AddCommGroup.DirectLimit.map_id
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
:
theorem
AddCommGroup.DirectLimit.map_comp
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
{G'' : ι → Type u_6}
[(i : ι) → AddCommMonoid (G'' i)]
{f'' : (i j : ι) → i ≤ j → G'' i →+ G'' j}
(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))
:
noncomputable def
AddCommGroup.DirectLimit.congr
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
(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
Instances For
theorem
AddCommGroup.DirectLimit.congr_apply_of
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
(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)
:
theorem
AddCommGroup.DirectLimit.congr_symm_apply_of
{ι : Type u_2}
[Preorder ι]
{G : ι → Type u_3}
[(i : ι) → AddCommMonoid (G i)]
{f : (i j : ι) → i ≤ j → G i →+ G j}
[DecidableEq ι]
{G' : ι → Type u_5}
[(i : ι) → AddCommMonoid (G' i)]
{f' : (i j : ι) → i ≤ j → G' i →+ G' j}
(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)
: