Direct limit of algebraic structures

We introduce all kinds of algebraic instances on DirectLimit, and specialize to the cases of modules and rings, showing that they are indeed colimits in the respective categories.

Implementation notes

The first 400 lines are boilerplate code that defines algebraic instances on DirectLimit from magma (Mul) to Field. To make everything "hom-polymorphic", we work with DirectedSystems of FunLikes rather than plain unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere.

In Mathlib/Algebra/Colimit/Module.lean and Mathlib/Algebra/Colimit/Ring.lean, Module.DirectLimit, AddCommGroup.DirectLimit and Ring.DirectLimit are defined as quotients of the universal objects (DirectSum and FreeCommRing). These definitions are more general and suitable for arbitrary colimits, but do not immediately provide criteria to determine when two elements in a component are equal in the direct limit.

On the other hand, the DirectLimit in this file is only defined for directed systems and does not work for general colimits, but the equivalence relation defining DirectLimit is very explicit. For colimits of directed systems there is no need to construct the universal object for each type of algebraic structure; the same type DirectLimit simply works for all of them. This file is therefore more general than the Module and Ring files in terms of the variety of algebraic structures supported.

So far we only show that DirectLimit is the colimit in the categories of modules and rings, but for the other algebraic structures the constructions and proofs will be easy following the same pattern. Since any two colimits are isomorphic, this allows us to golf proofs of equality criteria for Module/AddCommGroup/Ring.DirectLimit.

noncomputable instance DirectLimit.instOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → One (G i)] : One (DirectLimit G f)

noncomputable instance DirectLimit.instZero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Zero (G i)] : Zero (DirectLimit G f)

theorem DirectLimit.one_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (i : ι) : 1 = ⟦⟨i, 1⟩⟧

theorem DirectLimit.zero_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (i : ι) : 0 = ⟦⟨i, 0⟩⟧

theorem DirectLimit.exists_eq_one {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (x : (i : ι) × G i) : ⟦x⟧ = 1 ↔ ∃ (i : ι) (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

theorem DirectLimit.exists_eq_zero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (x : (i : ι) × G i) : ⟦x⟧ = 0 ↔ ∃ (i : ι) (h : x.fst ≤ i), (f x.fst i h) x.snd = 0

noncomputable instance DirectLimit.instMul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Mul (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : Mul (DirectLimit G f)

noncomputable instance DirectLimit.instAdd {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Add (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : Add (DirectLimit G f)

theorem DirectLimit.mul_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Mul (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] (i : ι) (x y : G i) : ⟦⟨i, x⟩⟧ * ⟦⟨i, y⟩⟧ = ⟦⟨i, x * y⟩⟧

theorem DirectLimit.add_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Add (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] (i : ι) (x y : G i) : ⟦⟨i, x⟩⟧ + ⟦⟨i, y⟩⟧ = ⟦⟨i, x + y⟩⟧

noncomputable instance DirectLimit.instCommMagmaOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → CommMagma (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : CommMagma (DirectLimit G f)

noncomputable instance DirectLimit.instAddCommMagmaOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → AddCommMagma (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddCommMagma (DirectLimit G f)

noncomputable instance DirectLimit.instSemigroupOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → Semigroup (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : Semigroup (DirectLimit G f)

noncomputable instance DirectLimit.instAddSemigroupOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → AddSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddSemigroup (DirectLimit G f)

noncomputable instance DirectLimit.instCommSemigroupOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → CommSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : CommSemigroup (DirectLimit G f)

noncomputable instance DirectLimit.instAddCommSemigroupOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → AddCommSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddCommSemigroup (DirectLimit G f)

noncomputable instance DirectLimit.instSMul {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → SMul R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : SMul R (DirectLimit G f)

noncomputable instance DirectLimit.instVAdd {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → VAdd R (G i)] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] : VAdd R (DirectLimit G f)

theorem DirectLimit.smul_def {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → SMul R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] (i : ι) (x : G i) (r : R) : r • ⟦⟨i, x⟩⟧ = ⟦⟨i, r • x⟩⟧

theorem DirectLimit.vadd_def {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → VAdd R (G i)] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] (i : ι) (x : G i) (r : R) : r +ᵥ ⟦⟨i, x⟩⟧ = ⟦⟨i, r +ᵥ x⟩⟧

noncomputable instance DirectLimit.instMulActionOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Monoid R] [(i : ι) → MulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : MulAction R (DirectLimit G f)

noncomputable instance DirectLimit.instAddActionOfAddActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [AddMonoid R] [(i : ι) → AddAction R (G i)] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] : AddAction R (DirectLimit G f)

noncomputable instance DirectLimit.instMulOneClassOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → MulOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : MulOneClass (DirectLimit G f)

noncomputable instance DirectLimit.instAddZeroClassOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddZeroClass (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddZeroClass (DirectLimit G f)

noncomputable instance DirectLimit.instMonoid {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Monoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : Monoid (DirectLimit G f)

noncomputable instance DirectLimit.instAddMonoid {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddMonoid (DirectLimit G f)

theorem DirectLimit.npow_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Monoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) (n : ℕ) : ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧

theorem DirectLimit.nsmul_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) (n : ℕ) : n • ⟦⟨i, x⟩⟧ = ⟦⟨i, n • x⟩⟧

noncomputable instance DirectLimit.instCommMonoidOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : CommMonoid (DirectLimit G f)

noncomputable instance DirectLimit.instAddCommMonoidOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddCommMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommMonoid (DirectLimit G f)

noncomputable instance DirectLimit.instGroup {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : Group (DirectLimit G f)

noncomputable instance DirectLimit.instAddGroup {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddGroup (DirectLimit G f)

theorem DirectLimit.inv_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) : (⟦⟨i, x⟩⟧)⁻¹ = ⟦⟨i, x⁻¹⟩⟧

theorem DirectLimit.neg_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) : -⟦⟨i, x⟩⟧ = ⟦⟨i, -x⟩⟧

theorem DirectLimit.div_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι) (x y : G i) : ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = ⟦⟨i, x / y⟩⟧

theorem DirectLimit.sub_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι) (x y : G i) : ⟦⟨i, x⟩⟧ - ⟦⟨i, y⟩⟧ = ⟦⟨i, x - y⟩⟧

theorem DirectLimit.zpow_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) (n : ℤ) : ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧

theorem DirectLimit.zsmul_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (i : ι) (x : G i) (n : ℤ) : n • ⟦⟨i, x⟩⟧ = ⟦⟨i, n • x⟩⟧

noncomputable instance DirectLimit.instCommGroupOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommGroup (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : CommGroup (DirectLimit G f)

noncomputable instance DirectLimit.instAddCommGroupOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddCommGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommGroup (DirectLimit G f)

noncomputable instance DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → MulZeroClass (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] : MulZeroClass (DirectLimit G f)

noncomputable instance DirectLimit.instMulZeroOneClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → MulZeroOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : MulZeroOneClass (DirectLimit G f)

instance DirectLimit.instNontrivial {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → MulZeroOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] [∀ (i : ι), Nontrivial (G i)] : Nontrivial (DirectLimit G f)

noncomputable instance DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → SemigroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] : SemigroupWithZero (DirectLimit G f)

noncomputable instance DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → MonoidWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : MonoidWithZero (DirectLimit G f)

noncomputable instance DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommMonoidWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : CommMonoidWithZero (DirectLimit G f)

noncomputable instance DirectLimit.instGroupWithZero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : GroupWithZero (DirectLimit G f)

theorem DirectLimit.inv₀_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] (i : ι) (x : G i) : (⟦⟨i, x⟩⟧)⁻¹ = ⟦⟨i, x⁻¹⟩⟧

theorem DirectLimit.div₀_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] (i : ι) (x y : G i) : ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = ⟦⟨i, x / y⟩⟧

theorem DirectLimit.zpow₀_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] (i : ι) (x : G i) (n : ℤ) : ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧

noncomputable instance DirectLimit.instCommGroupWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommGroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : CommGroupWithZero (DirectLimit G f)

noncomputable instance DirectLimit.instAddMonoidWithOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddMonoidWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddMonoidWithOne (DirectLimit G f)

theorem DirectLimit.natCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddMonoidWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (n : ℕ) (i : ι) : ↑n = ⟦⟨i, ↑n⟩⟧

noncomputable instance DirectLimit.instAddGroupWithOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroupWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddGroupWithOne (DirectLimit G f)

theorem DirectLimit.intCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroupWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (n : ℤ) (i : ι) : ↑n = ⟦⟨i, ↑n⟩⟧

noncomputable instance DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddCommMonoidWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommMonoidWithOne (DirectLimit G f)

noncomputable instance DirectLimit.instAddCommGroupWithOneOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddCommGroupWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommGroupWithOne (DirectLimit G f)

noncomputable instance DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → NonUnitalNonAssocCommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocCommSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → NonUnitalSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instNonUnitalCommSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → NonUnitalCommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalCommSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instNonAssocSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : NonAssocSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Semiring (DirectLimit G f)

noncomputable instance DirectLimit.instCommSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : CommSemiring (DirectLimit G f)

noncomputable instance DirectLimit.instRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Ring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Ring (DirectLimit G f)

noncomputable instance DirectLimit.instCommRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → CommRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : CommRing (DirectLimit G f)

noncomputable instance DirectLimit.instSMulZeroClassOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Zero (G i)] [(i : ι) → SMulZeroClass R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : SMulZeroClass R (DirectLimit G f)

noncomputable instance DirectLimit.instSMulWithZeroOfMulActionHomClassOfZeroHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [Zero R] [(i : ι) → Zero (G i)] [(i : ι) → SMulWithZero R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] : SMulWithZero R (DirectLimit G f)

noncomputable instance DirectLimit.instDistribSMulOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddZeroClass (G i)] [(i : ι) → DistribSMul R (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : DistribSMul R (DirectLimit G f)

noncomputable instance DirectLimit.instDistribMulAction {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [Monoid R] [(i : ι) → AddMonoid (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)] : DistribMulAction R (DirectLimit G f)

noncomputable instance DirectLimit.instMulDistribMulActionOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [Monoid R] [(i : ι) → Monoid (G i)] [(i : ι) → MulDistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : MulDistribMulAction R (DirectLimit G f)

noncomputable instance DirectLimit.instModule {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] : Module R (DirectLimit G f)

noncomputable instance DirectLimit.instDivisionSemiring {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → DivisionSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : DivisionSemiring (DirectLimit G f)

theorem DirectLimit.nnratCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → DivisionSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (q : ℚ≥0) (i : ι) : ↑q = ⟦⟨i, ↑q⟩⟧

noncomputable instance DirectLimit.instSemifieldOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Semifield (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Semifield (DirectLimit G f)

noncomputable instance DirectLimit.instDivisionRing {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → DivisionRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : DivisionRing (DirectLimit G f)

theorem DirectLimit.ratCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → DivisionRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (q : ℚ) (i : ι) : ↑q = ⟦⟨i, ↑q⟩⟧

noncomputable instance DirectLimit.instFieldOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] [(i : ι) → Field (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Field (DirectLimit G f)

noncomputable def DirectLimit.Module.of (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] (i : ι) : G i →ₗ[R] DirectLimit G f

The canonical map from a component to the direct limit.

@[simp]

theorem DirectLimit.Module.of_f {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {i j : ι} {hij : i ≤ j} {x : G i} : (of R ι G f j) ((f i j hij) x) = (of R ι G f i) x

noncomputable def DirectLimit.Module.lift (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_5} [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) : 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.

theorem DirectLimit.Module.lift_apply (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_5} [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) (z : DirectLimit G f) : (lift R ι G f g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.Module.lift_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_5} [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) : (lift R ι G f g Hg) ((of R ι G f i) x) = (g i) x

theorem DirectLimit.Module.hom_ext {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_5} [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) : g₁ = g₂

theorem DirectLimit.Module.hom_ext_iff {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Semiring R] [(i : ι) → AddCommMonoid (G i)] [(i : ι) → Module R (G i)] [∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_5} [AddCommMonoid P] [Module R P] {g₁ g₂ : DirectLimit G f →ₗ[R] P} : g₁ = g₂ ↔ ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i

noncomputable def DirectLimit.Ring.of {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) : G i →+* DirectLimit G f

The canonical map from a component to the direct limit.

@[simp]

theorem DirectLimit.Ring.of_f {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] {i j : ι} (hij : i ≤ j) (x : G i) : (of G f j) ((f i j hij) x) = (of G f i) x

noncomputable def DirectLimit.Ring.lift {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_5) [NonAssocSemiring 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) : 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.

@[simp]

theorem DirectLimit.Ring.lift_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_5) [NonAssocSemiring 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) : (lift G f P g Hg) ((of G f i) x) = (g i) x

theorem DirectLimit.Ring.hom_ext {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_5) [NonAssocSemiring P] {g₁ g₂ : DirectLimit G f →+* P} (h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂

theorem DirectLimit.Ring.hom_ext_iff {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] {P : Type u_5} [NonAssocSemiring P] {g₁ g₂ : DirectLimit G f →+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)