Directed colimits of monoids and algebras

Basic API for Mathlib's generic DirectLimit G f of a directed system of monoids or groups G i with monoid homomorphisms as transition maps, and of a directed system of A-algebras with A-algebra transition maps.

Mathlib equips DirectLimit G f with its monoid and group structures and bundles the canonical maps from the components as linear maps and ring homomorphisms. Here they are bundled as monoid homomorphisms TauCeti.DirectLimit.Monoid.of G f i : G i →* DirectLimit G f, with the universal property TauCeti.DirectLimit.Monoid.lift. The canonical map, its universal property, their compatibility lemmas and TauCeti.DirectLimit.Monoid.hom_ext follow Mathlib's DirectLimit.Ring.of, DirectLimit.Ring.lift and DirectLimit.Ring.hom_ext in Mathlib/Algebra/Colimit/DirectLimit.lean, with monoid homomorphisms in place of ring homomorphisms. Every element of the direct limit comes from some component, and the index set is directed, so every finite subset of the direct limit lies in the image of a single component (TauCeti.DirectLimit.Monoid.exists_subset_range_of). This is how properties defined by finitely many elements at a time pass to direct limits.

Main declarations

• TauCeti.DirectLimit.Monoid.of: the canonical map from a component, as a monoid homomorphism.
• TauCeti.DirectLimit.Monoid.lift: the universal property of the direct limit of monoids.
• TauCeti.DirectLimit.Monoid.hom_ext: monoid homomorphisms out of the direct limit agree when they agree on every component.
• TauCeti.DirectLimit.Monoid.exists_subset_range_of: every finite subset of the direct limit lies in the image of a single component.
• TauCeti.DirectLimit.Algebra.of_comp_f: the canonical maps into a direct limit of algebras are compatible with the transition maps. This is the algebra version of Ring.DirectLimit.of_comp_f in TauCeti/Algebra/Colimit/Ring.lean.

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

The canonical map from a component to the direct limit, as a monoid homomorphism.

@[simp]

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

theorem TauCeti.DirectLimit.Monoid.of_f {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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 j : ι} (hij : i ≤ j) (x : G i) : (of G f j) ((f i j hij) x) = (of G f i) x

def TauCeti.DirectLimit.Monoid.lift {ι : Type u_1} [Preorder ι] (G : ι → Type u_2) {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} (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)] {P : Type u_4} [MulOneClass 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 of monoids: monoid homomorphisms from the components which are compatible with the transition maps induce a monoid homomorphism out of the direct limit.

@[simp]

theorem TauCeti.DirectLimit.Monoid.lift_mk {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] {P : Type u_4} [MulOneClass 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 g Hg) ⟦⟨i, x⟩⟧ = (g i) x

theorem TauCeti.DirectLimit.Monoid.lift_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] {P : Type u_4} [MulOneClass 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 g Hg) ((of G f i) x) = (g i) x

@[simp]

theorem TauCeti.DirectLimit.Monoid.lift_comp_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] {P : Type u_4} [MulOneClass 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 g Hg).comp (of G f i) = g i

theorem TauCeti.DirectLimit.Monoid.hom_ext {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] {P : Type u_4} [MulOneClass P] {g₁ g₂ : DirectLimit G f →* P} (h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)) : g₁ = g₂

theorem TauCeti.DirectLimit.Monoid.hom_ext_iff {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] {P : Type u_4} [MulOneClass P] {g₁ g₂ : DirectLimit G f →* P} : g₁ = g₂ ↔ ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)

theorem TauCeti.DirectLimit.Monoid.exists_subset_range_of {ι : Type u_1} [Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3} {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)] (s : Finset (DirectLimit G f)) : ∃ (i : ι), ↑s ⊆ Set.range ⇑(of G f i)

Every finite subset of the direct limit of a directed system of monoids lies in the image of a single component.

@[simp]

theorem TauCeti.DirectLimit.Algebra.of_comp_f {A : Type u_1} {ι : Type u_2} [CommSemiring A] [Preorder ι] {B : ι → Type u_3} [(i : ι) → Semiring (B i)] [(i : ι) → Algebra A (B i)] {f : (i j : ι) → i ≤ j → B i →ₐ[A] B j} [DirectedSystem B fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] {i j : ι} (hij : i ≤ j) : (DirectLimit.Algebra.of B f j).comp (f i j hij) = DirectLimit.Algebra.of B f i

The canonical maps into a direct limit of algebras are compatible with the transition maps.