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

• Module.DirectLimit G f
• AddCommGroup.DirectLimit G f

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) : (f i i ⋯) x = x

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) : (f j k hjk) ((f i j hij) x) = (f i k ⋯) x

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) : DirectSum ι G → DirectSum ι G → Prop

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) : Module.DirectLimit.Eqv f ((DirectSum.lof R ι G i) x) ((DirectSum.lof R ι G j) ((f i j h) x))

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

• Module.DirectLimit G f = (addConGen (Module.DirectLimit.Eqv f)).Quotient

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 (Module.DirectLimit G f)

Equations

• Module.DirectLimit.addCommMonoid G f = (addConGen (Module.DirectLimit.Eqv f)).addCommMonoid

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 (Module.DirectLimit G f)

Equations

• Module.DirectLimit.module G f = Module.mk ⋯ ⋯

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 (Module.DirectLimit G f)

Equations

• Module.DirectLimit.addCommGroup G f = inferInstanceAs (AddCommGroup (addConGen (Module.DirectLimit.Eqv f)).Quotient)

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 (Module.DirectLimit G f)

Equations

• Module.DirectLimit.inhabited G f = { default := 0 }

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 (Module.DirectLimit G f)

Equations

• Module.DirectLimit.unique G f = inferInstanceAs (Unique (Quotient (addConGen (Module.DirectLimit.Eqv f)).toSetoid))

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 : ι) : G i →ₗ[R] Module.DirectLimit G f

The canonical map from a component to the direct limit.

Equations

• Module.DirectLimit.of R ι G f i = (let __spread.0 := (addConGen (Module.DirectLimit.Eqv f)).mk'; { toFun := (↑__spread.0).toFun, map_add' := ⋯, map_smul' := ⋯ }) ∘ₗ DirectSum.lof R ι G i

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) : Quot.mk (⇑(addConGen (Module.DirectLimit.Eqv f)).toSetoid) ((DirectSum.of G i) x) = (Module.DirectLimit.of R ι G f i) x

@[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} : (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_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 : 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.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 : Module.DirectLimit G f) : ∃ (i : ι) (x : G i) (y : G i), (Module.DirectLimit.of R ι G f i) x = z ∧ (Module.DirectLimit.of R ι G f i) y = w

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 : 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_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) : 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

• Module.DirectLimit.lift R ι G f g Hg = { toFun := (↑((addConGen (Module.DirectLimit.Eqv f)).lift ↑(DirectSum.toModule R ι P g) ⋯)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[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) : (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_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 : 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_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 ⇑(Module.DirectLimit.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) : 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) ⋯

@[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) : (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_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.DirectLimit.map (fun (x : ι) => LinearMap.id) ⋯ = LinearMap.id

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) : 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_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)) : 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) ⋯) ⋯ ⋯

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) : (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_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) : (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.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)] : Module.DirectLimit G f ≃ₗ[R] DirectLimit G f

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

• One or more equations did not get rendered due to their size.

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} : (Module.DirectLimit.linearEquiv G f) ((Module.DirectLimit.of R ι G f i) g) = ⟦⟨i, g⟩⟧

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} : (Module.DirectLimit.linearEquiv G f).symm ⟦g⟧ = (Module.DirectLimit.of R ι G f g.fst) g.snd

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 : (Module.DirectLimit.of R ι G f i) x = 0) : ∃ (j : ι) (hij : i ≤ j), (f i j hij) 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

• AddCommGroup.DirectLimit G f = Module.DirectLimit G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toNatLinearMap

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 (AddCommGroup.DirectLimit G f)

Equations

• AddCommGroup.DirectLimit.instAddCommMonoid G f = Module.DirectLimit.addCommMonoid G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toNatLinearMap

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 (AddCommGroup.DirectLimit G f)

Equations

• AddCommGroup.DirectLimit.addCommGroup G f = Module.DirectLimit.addCommGroup G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toNatLinearMap

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 (AddCommGroup.DirectLimit G f)

Equations

• AddCommGroup.DirectLimit.instInhabited G f = { default := 0 }

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 (AddCommGroup.DirectLimit G f)

Equations

• AddCommGroup.DirectLimit.instUniqueOfIsEmpty G f = Module.DirectLimit.unique G fun (i j : ι) (hij : i ≤ j) => (f i j hij).toNatLinearMap

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 : ι) : 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).toNatLinearMap) i).toAddMonoidHom

@[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) : (AddCommGroup.DirectLimit.of G f j) ((f i j hij) x) = (AddCommGroup.DirectLimit.of G f i) x

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 : 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 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 : (AddCommGroup.DirectLimit.of G f i) x = 0) : ∃ (j : ι) (hij : i ≤ j), (f i j hij) 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) : 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).toNatLinearMap) (fun (i : ι) => (g i).toNatLinearMap) Hg).toAddMonoidHom

@[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) : (AddCommGroup.DirectLimit.lift G f P g Hg) ((AddCommGroup.DirectLimit.of G f i) x) = (g i) x

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 : 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 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 ⇑(AddCommGroup.DirectLimit.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)) : AddCommGroup.DirectLimit G f →+ AddCommGroup.DirectLimit G' f'

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)) ⋯

@[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) : (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 u_2} [Preorder ι] {G : ι → Type u_3} [(i : ι) → AddCommMonoid (G i)] {f : (i j : ι) → i ≤ j → G i →+ G j} [DecidableEq ι] : AddCommGroup.DirectLimit.map (fun (x : ι) => AddMonoidHom.id (G x)) ⋯ = AddMonoidHom.id (AddCommGroup.DirectLimit G f)

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)) : (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 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)) : AddCommGroup.DirectLimit G f ≃+ AddCommGroup.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

• AddCommGroup.DirectLimit.congr e he = (AddCommGroup.DirectLimit.map (fun (x : ι) => ↑(e x)) he).toAddEquiv (AddCommGroup.DirectLimit.map (fun (i : ι) => ↑(e i).symm) ⋯) ⋯ ⋯

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) : (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 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) : (AddCommGroup.DirectLimit.congr e he).symm ((AddCommGroup.DirectLimit.of G' f' i) g) = (AddCommGroup.DirectLimit.of G f i) ((e i).symm g)