Documentation

TauCeti.Algebra.Category.Grp.DirectLimit

The direct limit of groups is a colimit in GrpCat #

A directed system of groups G i, indexed by a directed preorder ι, with transition maps f i j : G i →* G j, is a diagram ι ⥤ GrpCat. Mathlib's generic DirectLimit G f, with the canonical maps DirectLimit.Monoid.of G f i, is a cocone over it, and the universal property DirectLimit.Monoid.lift shows that this cocone is a colimit. Results about colimits of filtered diagrams in GrpCat therefore apply to DirectLimit G f, and conversely DirectLimit G f is a concrete model of the colimit of a directed system of groups.

Main definitions #

This follows ModuleCat.directLimitIsColimit, the corresponding statement for modules.

source
def TauCeti.GrpCat.directLimitDiagram {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] :
CategoryTheory.Functor ι GrpCat

The diagram in GrpCat of a directed system of groups.

Instances For
    source
    @[simp]
    theorem TauCeti.GrpCat.directLimitDiagram_obj_coe {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] (i : ι) :
    ↑((directLimitDiagram G f).obj i) = G i
    source
    @[simp]
    theorem TauCeti.GrpCat.directLimitDiagram_map {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] {X✝ Y✝ : ι} (hij : X✝ ⟶ Y✝) :
    (directLimitDiagram G f).map hij = GrpCat.ofHom (f X✝ Y✝ ⋯)
    source
    noncomputable def TauCeti.GrpCat.directLimitCocone {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] :
    CategoryTheory.Limits.Cocone (directLimitDiagram G f)

    The cocone over the diagram of a directed system of groups with apex the direct limit DirectLimit G f and legs the canonical maps DirectLimit.Monoid.of G f i.

    Instances For
      source
      @[simp]
      theorem TauCeti.GrpCat.directLimitCocone_ι_app {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] (i : ι) :
      (directLimitCocone G f).ι.app i = GrpCat.ofHom (DirectLimit.Monoid.of G f i)
      source
      @[simp]
      theorem TauCeti.GrpCat.directLimitCocone_pt_coe {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] :
      ↑(directLimitCocone G f).pt = DirectLimit G f
      source
      noncomputable def TauCeti.GrpCat.directLimitIsColimit {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] :
      CategoryTheory.Limits.IsColimit (directLimitCocone G f)

      The direct limit of a directed system of groups is a colimit in GrpCat.

      Instances For
        source
        @[simp]
        theorem TauCeti.GrpCat.directLimitIsColimit_desc {ι : Type v} [Preorder ι] (G : ι → Type (max u v)) [(i : ι) → Group (G i)] (f : (i j : ι) → i ≤ j → G i →* G j) [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirectedOrder ι] [Nonempty ι] (s : CategoryTheory.Limits.Cocone (directLimitDiagram G f)) :
        (directLimitIsColimit G f).desc s = GrpCat.ofHom (DirectLimit.Monoid.lift G f (fun (i : ι) => GrpCat.Hom.hom (s.ι.app i)) ⋯)