Images of the legs of a colimit of groups

The images of the legs c.ι.app j of a colimit cocone c in GrpCat generate its apex: a subgroup containing all of them receives a cocone, so by the universal property its inclusion has a right inverse. Over a filtered index category, the images form a directed family of subgroups, so every finite subset of the apex already lies in the image of a single leg. This is how properties defined by finitely many elements at a time pass to filtered colimits of groups.

Main declarations

• TauCeti.GrpCat.iSup_range_eq_top_of_isColimit: the images of the legs of a colimit cocone generate its apex.
• TauCeti.GrpCat.range_le_range: the image of the leg at j is contained in the image of the leg at any object receiving a morphism from j.
• TauCeti.GrpCat.directed_range: over a filtered index category, the images of the legs of a cocone form a directed family of subgroups.
• TauCeti.GrpCat.exists_subset_range_of_isColimit: over a filtered index category, every finite subset of the apex of a colimit cocone lies in the image of a single leg.

theorem TauCeti.GrpCat.iSup_range_eq_top_of_isColimit {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J GrpCat} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : ⨆ (j : J), (GrpCat.Hom.hom (c.ι.app j)).range = ⊤

The images of the legs of a colimit cocone in GrpCat generate its apex.

theorem TauCeti.GrpCat.range_le_range {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J GrpCat} (c : CategoryTheory.Limits.Cocone F) {j k : J} (f : j ⟶ k) : (GrpCat.Hom.hom (c.ι.app j)).range ≤ (GrpCat.Hom.hom (c.ι.app k)).range

The image of the leg at j of a cocone in GrpCat is contained in the image of the leg at any object receiving a morphism from j.

theorem TauCeti.GrpCat.directed_range {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J GrpCat} [CategoryTheory.IsFilteredOrEmpty J] (c : CategoryTheory.Limits.Cocone F) : Directed (fun (x1 x2 : Subgroup ↑c.pt) => x1 ≤ x2) fun (j : J) => (GrpCat.Hom.hom (c.ι.app j)).range

Over a filtered index category, the images of the legs of a cocone in GrpCat form a directed family of subgroups.

theorem TauCeti.GrpCat.exists_subset_range_of_isColimit {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {F : CategoryTheory.Functor J GrpCat} [CategoryTheory.IsFiltered J] {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) (s : Finset ↑c.pt) : ∃ (j : J), ↑s ⊆ Set.range ⇑(GrpCat.Hom.hom (c.ι.app j))

Over a filtered index category, every finite subset of the apex of a colimit cocone in GrpCat lies in the image of a single leg.