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 following categories:

• modules
• non-unital semirings
• rings
• (non-unital) star rings
• R-algebras

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.

@[implicit_reducible]

noncomputable instance DirectLimit.instOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → One (G i)] : One (DirectLimit G f)

Equations

• DirectLimit.instOne = { one := DirectLimit.map₀ f fun (x : ι) => 1 }

@[implicit_reducible]

noncomputable instance DirectLimit.instZero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Zero (G i)] : Zero (DirectLimit G f)

Equations

• DirectLimit.instZero = { zero := DirectLimit.map₀ f fun (x : ι) => 0 }

theorem DirectLimit.one_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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

@[simp]

theorem DirectLimit.lift_one {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → One (G i)] [One C] [∀ (i : ι), OneHomClass (H i) (G i) C] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h 1 = 1

@[simp]

theorem DirectLimit.lift_zero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Zero (G i)] [Zero C] [∀ (i : ι), ZeroHomClass (H i) (G i) C] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h 0 = 0

@[simp]

theorem DirectLimit.map₀_one {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → One (G i)] [∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)] : map₀ f 1 = 1

@[simp]

theorem DirectLimit.map₀_zero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Zero (G i)] [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] : map₀ f 0 = 0

@[implicit_reducible]

noncomputable instance DirectLimit.instStar {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Star (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] : Star (DirectLimit G f)

Equations

• DirectLimit.instStar = { star := DirectLimit.map f f (fun (x : ι) (x_1 : G x) => star x_1) ⋯ }

theorem DirectLimit.star_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Star (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] (i : ι) (x : G i) : star ⟦⟨i, x⟩⟧ = ⟦⟨i, star x⟩⟧

@[simp]

theorem DirectLimit.lift_star {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → Star (G i)] [Star C] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [∀ (i : ι), StarHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (star x) = star (DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x)

@[implicit_reducible]

noncomputable instance DirectLimit.instInvolutiveStar {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → InvolutiveStar (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] : InvolutiveStar (DirectLimit G f)

Equations

• DirectLimit.instInvolutiveStar = { toStar := DirectLimit.instStar, star_involutive := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Mul (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : Mul (DirectLimit G f)

Equations

• DirectLimit.instMul = { mul := DirectLimit.map₂ f f f (fun (x : ι) (x1 x2 : G x) => x1 * x2) ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAdd {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Add (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : Add (DirectLimit G f)

Equations

• DirectLimit.instAdd = { add := DirectLimit.map₂ f f f (fun (x : ι) (x1 x2 : G x) => x1 + x2) ⋯ }

theorem DirectLimit.mul_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(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_6} {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)] [IsDirectedOrder ι] [(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⟩⟧

@[simp]

theorem DirectLimit.lift_mul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → Mul (G i)] [Mul C] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [∀ (i : ι), MulHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x y : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x * y) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x * DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h y

@[simp]

theorem DirectLimit.lift_add {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → Add (G i)] [Add C] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] [∀ (i : ι), AddHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x y : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x + y) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x + DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h y

@[simp]

theorem DirectLimit.map₀_mul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Mul (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [Nonempty ι] (r s : (i : ι) → G i) : map₀ f (r * s) = map₀ f r * map₀ f s

@[simp]

theorem DirectLimit.map₀_add {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Add (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] [Nonempty ι] (r s : (i : ι) → G i) : map₀ f (r + s) = map₀ f r + map₀ f s

@[implicit_reducible]

noncomputable instance DirectLimit.instCommMagmaOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → CommMagma (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : CommMagma (DirectLimit G f)

Equations

• DirectLimit.instCommMagmaOfMulHomClass = { toMul := DirectLimit.instMul, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommMagmaOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → AddCommMagma (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddCommMagma (DirectLimit G f)

Equations

• DirectLimit.instAddCommMagmaOfAddHomClass = { toAdd := DirectLimit.instAdd, add_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instSemigroupOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Semigroup (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : Semigroup (DirectLimit G f)

Equations

• DirectLimit.instSemigroupOfMulHomClass = { toMul := DirectLimit.instMul, mul_assoc := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddSemigroupOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → AddSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddSemigroup (DirectLimit G f)

Equations

• DirectLimit.instAddSemigroupOfAddHomClass = { toAdd := DirectLimit.instAdd, add_assoc := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instCommSemigroupOfMulHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → CommSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] : CommSemigroup (DirectLimit G f)

Equations

• DirectLimit.instCommSemigroupOfMulHomClass = { toSemigroup := DirectLimit.instSemigroupOfMulHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommSemigroupOfAddHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → AddCommSemigroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] : AddCommSemigroup (DirectLimit G f)

Equations

• DirectLimit.instAddCommSemigroupOfAddHomClass = { toAddSemigroup := DirectLimit.instAddSemigroupOfAddHomClass, add_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instStarMul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → Mul (G i)] [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] [(i : ι) → StarMul (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] : StarMul (DirectLimit G f)

Equations

• DirectLimit.instStarMul = { toInvolutiveStar := DirectLimit.instInvolutiveStar, star_mul := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instSMul {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → SMul R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : SMul R (DirectLimit G f)

Equations

• DirectLimit.instSMul = { smul := fun (r : R) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => r • x_1) ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instVAdd {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → VAdd R (G i)] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] : VAdd R (DirectLimit G f)

Equations

• DirectLimit.instVAdd = { vadd := fun (r : R) => DirectLimit.map f f (fun (x : ι) (x_1 : G x) => r +ᵥ x_1) ⋯ }

theorem DirectLimit.smul_def {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(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_6} {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)] [IsDirectedOrder ι] [(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⟩⟧

@[simp]

theorem DirectLimit.lift_smul {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → SMul R (G i)] [SMul R C] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] [∀ (i : ι), MulActionHomClass (H i) R (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (r : R) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (r • x) = r • DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x

@[simp]

theorem DirectLimit.lift_vadd {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [(i : ι) → VAdd R (G i)] [VAdd R C] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] [∀ (i : ι), AddActionHomClass (H i) R (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (r : R) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (r +ᵥ x) = r +ᵥ DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x

instance DirectLimit.instStarModule {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Star R] [(i : ι) → Star (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [(i : ι) → SMul R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] [∀ (i : ι), StarModule R (G i)] : StarModule R (DirectLimit G f)

@[implicit_reducible]

noncomputable instance DirectLimit.instMulActionOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instMulActionOfMulActionHomClass = { toSMul := DirectLimit.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddActionOfAddActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instAddActionOfAddActionHomClass = { toVAdd := DirectLimit.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMulOneClassOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → MulOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : MulOneClass (DirectLimit G f)

Equations

• DirectLimit.instMulOneClassOfMonoidHomClass = { toOne := DirectLimit.instOne, toMul := DirectLimit.instMul, one_mul := ⋯, mul_one := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddZeroClassOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddZeroClass (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddZeroClass (DirectLimit G f)

Equations

• DirectLimit.instAddZeroClassOfAddMonoidHomClass = { toZero := DirectLimit.instZero, toAdd := DirectLimit.instAdd, zero_add := ⋯, add_zero := ⋯ }

noncomputable def DirectLimit.map₀MonoidHom {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → MulOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : ((i : ι) → G i) →* DirectLimit G f

map₀ as a MonoidHom.

Equations

• DirectLimit.map₀MonoidHom f = { toFun := fun (x : (i : ι) → G i) => DirectLimit.map₀ f x, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def DirectLimit.map₀AddMonoidHom {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddZeroClass (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : ((i : ι) → G i) →+ DirectLimit G f

map₀ as an AddMonoidHom.

Equations

• DirectLimit.map₀AddMonoidHom f = { toFun := fun (x : (i : ι) → G i) => DirectLimit.map₀ f x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.map₀MonoidHom_apply {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → MulOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (x : (i : ι) → G i) : (map₀MonoidHom f) x = map₀ f x

@[simp]

theorem DirectLimit.map₀AddMonoidHom_apply {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddZeroClass (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] (x : (i : ι) → G i) : (map₀AddMonoidHom f) x = map₀ f x

@[implicit_reducible]

noncomputable instance DirectLimit.instMonoid {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Monoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : Monoid (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instAddMonoid {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddMonoid (DirectLimit G f)

Equations

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

theorem DirectLimit.npow_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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⟩⟧

@[simp]

theorem DirectLimit.lift_npow {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Monoid (G i)] [Monoid C] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) (n : ℕ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x ^ n) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x ^ n

@[simp]

theorem DirectLimit.lift_nsmul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [AddMonoid C] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) (n : ℕ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (n • x) = n • DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x

@[implicit_reducible]

noncomputable instance DirectLimit.instCommMonoidOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : CommMonoid (DirectLimit G f)

Equations

• DirectLimit.instCommMonoidOfMonoidHomClass = { toMonoid := DirectLimit.instMonoid, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommMonoidOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddCommMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommMonoid (DirectLimit G f)

Equations

• DirectLimit.instAddCommMonoidOfAddMonoidHomClass = { toAddMonoid := DirectLimit.instAddMonoid, add_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instStarAddMonoid {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [(i : ι) → StarAddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] : StarAddMonoid (DirectLimit G f)

Equations

• DirectLimit.instStarAddMonoid = { toInvolutiveStar := DirectLimit.instInvolutiveStar, star_add := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instGroup {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : Group (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instAddGroup {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddGroup (DirectLimit G f)

Equations

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

theorem DirectLimit.inv_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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⟩⟧

@[simp]

theorem DirectLimit.lift_inv {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Group (G i)] [Group C] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x⁻¹ = (DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x)⁻¹

@[simp]

theorem DirectLimit.lift_neg {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddGroup (G i)] [AddGroup C] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (-x) = -DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x

@[simp]

theorem DirectLimit.lift_div {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Group (G i)] [Group C] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x y : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x / y) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x / DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h y

@[simp]

theorem DirectLimit.lift_sub {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddGroup (G i)] [AddGroup C] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x y : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x - y) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x - DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h y

@[simp]

theorem DirectLimit.lift_zpow {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Group (G i)] [Group C] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) (z : ℤ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x ^ z) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x ^ z

@[simp]

theorem DirectLimit.lift_zsmul {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddGroup (G i)] [AddGroup C] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) (z : ℤ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (z • x) = z • DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x

@[implicit_reducible]

noncomputable instance DirectLimit.instCommGroupOfMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommGroup (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : CommGroup (DirectLimit G f)

Equations

• DirectLimit.instCommGroupOfMonoidHomClass = { toGroup := DirectLimit.instGroup, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommGroupOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddCommGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommGroup (DirectLimit G f)

Equations

• DirectLimit.instAddCommGroupOfAddMonoidHomClass = { toAddGroup := DirectLimit.instAddGroup, add_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass = { toMul := DirectLimit.instMul, toZero := DirectLimit.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMulZeroOneClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → MulZeroOneClass (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : MulZeroOneClass (DirectLimit G f)

Equations

• DirectLimit.instMulZeroOneClass = { toMulOneClass := DirectLimit.instMulOneClassOfMonoidHomClass, toZero := DirectLimit.instZero, zero_mul := ⋯, mul_zero := ⋯ }

instance DirectLimit.instNontrivial {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

@[implicit_reducible]

noncomputable instance DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass = { toSemigroup := DirectLimit.instSemigroupOfMulHomClass, toZero := DirectLimit.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → MonoidWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : MonoidWithZero (DirectLimit G f)

Equations

• DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass = { toMonoid := DirectLimit.instMonoid, toZero := DirectLimit.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommMonoidWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : CommMonoidWithZero (DirectLimit G f)

Equations

• DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass = { toCommMonoid := DirectLimit.instCommMonoidOfMonoidHomClass, toZero := DirectLimit.instZero, zero_mul := ⋯, mul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instGroupWithZero {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : GroupWithZero (DirectLimit G f)

Equations

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

theorem DirectLimit.inv₀_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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_6} {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)] [IsDirectedOrder ι] [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⟩⟧

@[simp]

theorem DirectLimit.lift_inv₀ {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [GroupWithZero C] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x⁻¹ = (DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x)⁻¹

@[simp]

theorem DirectLimit.lift_div₀ {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [GroupWithZero C] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x y : DirectLimit G f) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x / y) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x / DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h y

@[simp]

theorem DirectLimit.lift_zpow₀ {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → GroupWithZero (G i)] [GroupWithZero C] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (x : DirectLimit G f) (z : ℤ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h (x ^ z) = DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h x ^ z

@[implicit_reducible]

noncomputable instance DirectLimit.instCommGroupWithZeroOfMonoidWithZeroHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommGroupWithZero (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] : CommGroupWithZero (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instAddMonoidWithOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddMonoidWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddMonoidWithOne (DirectLimit G f)

Equations

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

theorem DirectLimit.natCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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⟩⟧

@[implicit_reducible]

noncomputable instance DirectLimit.instAddGroupWithOne {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddGroupWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddGroupWithOne (DirectLimit G f)

Equations

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

theorem DirectLimit.intCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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⟩⟧

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddCommMonoidWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommMonoidWithOne (DirectLimit G f)

Equations

• DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass = { toAddMonoidWithOne := DirectLimit.instAddMonoidWithOne, add_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instAddCommGroupWithOneOfAddMonoidHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → AddCommGroupWithOne (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : AddCommGroupWithOne (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocSemiring (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instStarRingOfStarHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] : StarRing (DirectLimit G f)

Equations

• DirectLimit.instStarRingOfStarHomClass = { toStarMul := DirectLimit.instStarMul, star_add := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalSemiring (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass = { toNonUnitalNonAssocSemiring := DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass, mul_assoc := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonAssocSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : NonAssocSemiring (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Semiring (DirectLimit G f)

Equations

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

noncomputable def DirectLimit.map₀RingHom {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : ((i : ι) → G i) →+* DirectLimit G f

map₀ as a RingHom.

Equations

• DirectLimit.map₀RingHom f = { toFun := fun (r : (i : ι) → G i) => DirectLimit.map₀ f r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.map₀RingHom_apply {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (r : (i : ι) → G i) : (map₀RingHom f) r = map₀ f r

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalNonAssocCommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocCommSemiring (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass = { toNonUnitalNonAssocSemiring := DirectLimit.instNonUnitalNonAssocSemiringOfNonUnitalRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalCommSemiringOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalCommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalCommSemiring (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalCommSemiringOfNonUnitalRingHomClass = { toNonUnitalSemiring := DirectLimit.instNonUnitalSemiringOfNonUnitalRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonAssocCommSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocCommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : NonAssocCommSemiring (DirectLimit G f)

Equations

• DirectLimit.instNonAssocCommSemiringOfRingHomClass = { toNonAssocSemiring := DirectLimit.instNonAssocSemiringOfRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instCommSemiringOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : CommSemiring (DirectLimit G f)

Equations

• DirectLimit.instCommSemiringOfRingHomClass = { toSemiring := DirectLimit.instSemiringOfRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalNonAssocRingOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalNonAssocRing (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocRing (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalRingOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalRing (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalRing (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalRingOfNonUnitalRingHomClass = { toNonUnitalNonAssocRing := DirectLimit.instNonUnitalNonAssocRingOfNonUnitalRingHomClass, mul_assoc := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonAssocRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : NonAssocRing (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Ring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Ring (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalNonAssocCommRing (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalNonAssocCommRing (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalNonAssocCommRingOfNonUnitalRingHomClass = { toNonUnitalNonAssocRing := DirectLimit.instNonUnitalNonAssocRingOfNonUnitalRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonUnitalCommRingOfNonUnitalRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonUnitalCommRing (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] : NonUnitalCommRing (DirectLimit G f)

Equations

• DirectLimit.instNonUnitalCommRingOfNonUnitalRingHomClass = { toNonUnitalRing := DirectLimit.instNonUnitalRingOfNonUnitalRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instNonAssocCommRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → NonAssocCommRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : NonAssocCommRing (DirectLimit G f)

Equations

• DirectLimit.instNonAssocCommRingOfRingHomClass = { toNonAssocRing := DirectLimit.instNonAssocRingOfRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instCommRingOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → CommRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : CommRing (DirectLimit G f)

Equations

• DirectLimit.instCommRingOfRingHomClass = { toRing := DirectLimit.instRingOfRingHomClass, mul_comm := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instSMulZeroClassOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instSMulZeroClassOfMulActionHomClass = { toSMul := DirectLimit.instSMul, smul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instSMulWithZeroOfMulActionHomClassOfZeroHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instSMulWithZeroOfMulActionHomClassOfZeroHomClass = { toSMulZeroClass := DirectLimit.instSMulZeroClassOfMulActionHomClass, zero_smul := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instDistribSMulOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instDistribSMulOfMulActionHomClass = { toSMulZeroClass := DirectLimit.instSMulZeroClassOfMulActionHomClass, smul_add := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instDistribMulAction {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instDistribMulAction = { toMulAction := DirectLimit.instMulActionOfMulActionHomClass, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instMulDistribMulActionOfMulActionHomClass {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instMulDistribMulActionOfMulActionHomClass = { toMulAction := DirectLimit.instMulActionOfMulActionHomClass, smul_one := ⋯, smul_mul := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instModule {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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)

Equations

• DirectLimit.instModule = { toDistribMulAction := DirectLimit.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

noncomputable instance DirectLimit.instDivisionSemiring {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : DivisionSemiring (DirectLimit G f)

Equations

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

theorem DirectLimit.nnratCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (q : ℚ≥0) (i : ι) : ↑q = ⟦⟨i, ↑q⟩⟧

@[simp]

theorem DirectLimit.lift_nnratCast {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionSemiring (G i)] [DivisionSemiring C] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [∀ (i : ι), RingHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (q : ℚ≥0) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h ↑q = ↑q

@[implicit_reducible]

noncomputable instance DirectLimit.instSemifieldOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Semifield (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Semifield (DirectLimit G f)

Equations

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

@[implicit_reducible]

noncomputable instance DirectLimit.instDivisionRing {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : DivisionRing (DirectLimit G f)

Equations

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

theorem DirectLimit.ratCast_def {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionRing (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] (q : ℚ) (i : ι) : ↑q = ⟦⟨i, ↑q⟩⟧

@[simp]

theorem DirectLimit.lift_ratCast {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [(i : ι) → FunLike (H i) (G i) C] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → DivisionRing (G i)] [DivisionRing C] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [∀ (i : ι), RingHomClass (H i) (G i) C] (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (fun (x : ι) => ⇑(g x)) i x = (fun (x : ι) => ⇑(g x)) j ((f i j h) x)) (q : ℚ) : DirectLimit.lift f (fun (x : ι) => ⇑(g x)) h ↑q = ↑q

@[implicit_reducible]

noncomputable instance DirectLimit.instFieldOfRingHomClass {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [(i : ι) → Field (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] : Field (DirectLimit G f)

Equations

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

theorem DirectLimit.map₀_algebraMap {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] (i : ι) (r : R) : (map₀ f fun (i : ι) => (algebraMap R (G i)) r) = ⟦⟨i, (algebraMap R (G i)) r⟩⟧

@[implicit_reducible]

noncomputable instance DirectLimit.instAlgebra {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] : Algebra R (DirectLimit G f)

Equations

• DirectLimit.instAlgebra = { toSMul := DistribMulAction.toDistribSMul.toSMul, algebraMap := (DirectLimit.map₀RingHom f).comp (algebraMap R ((i : ι) → G i)), commutes' := ⋯, smul_def' := ⋯ }

theorem DirectLimit.algebraMap_def {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [Nonempty ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] (i : ι) (r : R) : (algebraMap R (DirectLimit G f)) r = ⟦⟨i, (algebraMap R (G i)) r⟩⟧

noncomputable def DirectLimit.Module.of (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [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.

Equations

• DirectLimit.Module.of R ι G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DirectLimit.Module.of_apply (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [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 : ι) (x : G i) : (of R ι G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.Module.of_f {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_6} (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)] [IsDirectedOrder ι] [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_7} [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.

Equations

• DirectLimit.Module.lift R ι G f g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem DirectLimit.Module.lift_apply (R : Type u_1) (ι : Type u_2) [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [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_7} [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_comp_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_7} [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 : ι} : lift R ι G f g Hg ∘ₗ of R ι G f i = g i

theorem DirectLimit.Module.lift_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [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_7} [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_6} {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)] [IsDirectedOrder ι] [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_7} [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_6} {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)] [IsDirectedOrder ι] [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_7} [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.NonUnitalRing.of {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) : G i →ₙ+* DirectLimit G f

The canonical map from a component to the direct limit.

Equations

• DirectLimit.NonUnitalRing.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalRing.of_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.NonUnitalRing.of_f {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (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.NonUnitalRing.lift {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring 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 NonUnitalNonAsssocSemiRing that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

Equations

• DirectLimit.NonUnitalRing.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalRing.lift_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring 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) (z : DirectLimit G f) : (lift G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.NonUnitalRing.lift_comp_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring 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 : ι} : (lift G f P g Hg).comp (of G f i) = g i

theorem DirectLimit.NonUnitalRing.lift_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring 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.NonUnitalRing.hom_ext {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring 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.NonUnitalRing.hom_ext_iff {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonUnitalNonAssocSemiring P] {g₁ g₂ : DirectLimit G f →ₙ+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

noncomputable def DirectLimit.Ring.of {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(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.

Equations

• DirectLimit.Ring.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.Ring.of_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.Ring.of_f {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(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_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [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.

Equations

• DirectLimit.Ring.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DirectLimit.Ring.lift_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [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) (z : DirectLimit G f) : (lift G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.Ring.lift_comp_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [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 : ι} : (lift G f P g Hg).comp (of G f i) = g i

theorem DirectLimit.Ring.lift_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [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_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [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_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonAssocSemiring P] {g₁ g₂ : DirectLimit G f →+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

noncomputable def DirectLimit.NonUnitalStarRing.of {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) : G i →⋆ₙ+* DirectLimit G f

The canonical map from a component to the direct limit.

Equations

• DirectLimit.NonUnitalStarRing.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_star' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalStarRing.of_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.NonUnitalStarRing.of_f {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (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.NonUnitalStarRing.lift {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [StarRing 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 StarRing that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

Equations

• DirectLimit.NonUnitalStarRing.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_star' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalStarRing.lift_apply {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [StarRing 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) (z : DirectLimit G f) : (lift G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.NonUnitalStarRing.lift_comp_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [StarRing 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 : ι} : (lift G f P g Hg).comp (of G f i) = g i

theorem DirectLimit.NonUnitalStarRing.lift_of {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [StarRing 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.NonUnitalStarRing.hom_ext {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [StarRing 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.NonUnitalStarRing.hom_ext_iff {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [(i : ι) → StarRing (G i)] [∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonUnitalNonAssocSemiring P] [StarRing P] {g₁ g₂ : DirectLimit G f →⋆ₙ+* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

noncomputable def DirectLimit.Algebra.of {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (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.

Equations

• DirectLimit.Algebra.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem DirectLimit.Algebra.of_apply {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.Algebra.of_f {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (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.Algebra.lift {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [Semiring P] [Algebra 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 R-algebra that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

Equations

• DirectLimit.Algebra.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem DirectLimit.Algebra.lift_apply {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [Semiring P] [Algebra 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 G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.Algebra.lift_comp_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [Semiring P] [Algebra 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 : ι} : (lift G f P g Hg).comp (of G f i) = g i

theorem DirectLimit.Algebra.lift_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [Semiring P] [Algebra 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 G f P g Hg) ((of G f i) x) = (g i) x

theorem DirectLimit.Algebra.hom_ext {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [Semiring P] [Algebra R P] {g₁ g₂ : DirectLimit G f →ₐ[R] P} (h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂

theorem DirectLimit.Algebra.hom_ext_iff {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → Semiring (G i)] [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [(i : ι) → Algebra R (G i)] [∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_7} [Semiring P] [Algebra R P] {g₁ g₂ : DirectLimit G f →ₐ[R] P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

noncomputable def DirectLimit.NonUnitalAlgebra.of {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (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.

Equations

• DirectLimit.NonUnitalAlgebra.of G f i = { toFun := fun (x : G i) => ⟦⟨i, x⟩⟧, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalAlgebra.of_apply {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

@[simp]

theorem DirectLimit.NonUnitalAlgebra.of_toFun {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (i : ι) (x : G i) : (of G f i) x = ⟦⟨i, x⟩⟧

theorem DirectLimit.NonUnitalAlgebra.of_f {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (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.NonUnitalAlgebra.lift {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction 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 R-algebra that respect the directed system structure (i.e. make some diagram commute) give rise to a unique map out of the direct limit.

Equations

• DirectLimit.NonUnitalAlgebra.lift G f P g Hg = { toFun := DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem DirectLimit.NonUnitalAlgebra.lift_toFun {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction 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 G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.NonUnitalAlgebra.lift_apply {R : Type u_1} {ι : Type u_2} [Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} (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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction 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 G f P g Hg) z = DirectLimit.lift f (fun (x1 : ι) (x2 : G x1) => (g x1) x2) ⋯ z

@[simp]

theorem DirectLimit.NonUnitalAlgebra.lift_comp_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction 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 : ι} : (lift G f P g Hg).comp (of G f i) = g i

theorem DirectLimit.NonUnitalAlgebra.lift_of {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction 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 G f P g Hg) ((of G f i) x) = (g i) x

theorem DirectLimit.NonUnitalAlgebra.hom_ext {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] (P : Type u_7) [NonUnitalNonAssocSemiring P] [DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P} (h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂

theorem DirectLimit.NonUnitalAlgebra.hom_ext_iff {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {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)] [IsDirectedOrder ι] [CommSemiring R] [(i : ι) → NonUnitalNonAssocSemiring (G i)] [(i : ι) → DistribMulAction R (G i)] [∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)] [Nonempty ι] {P : Type u_7} [NonUnitalNonAssocSemiring P] [DistribMulAction R P] {g₁ g₂ : DirectLimit G f →ₙₐ[R] P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)