Filtered colimits of amenable groups

The colimit of a filtered diagram of amenable groups is amenable. The transition maps need not be injective. Every finite subset of the apex of a colimit cocone over a filtered diagram in GrpCat lies in the image of a single leg, so the criterion TauCeti.Amenable.of_forall_finset_subset_range, which pushes left-invariant means forward along the legs, applies as soon as the legs are continuous.

The stages of the diagram are arbitrary groups, so their topologies are supplied as instances. In the discrete setting every leg is continuous, and the apex may carry any group topology. A nonempty directed preorder is a filtered category, so this covers colimits of directed systems of groups indexed by such a preorder.

For Mathlib's concrete model DirectLimit G f of the colimit of a directed system of groups, the same argument applies directly: every finite subset of DirectLimit G f lies in the image of a single canonical map DirectLimit.Monoid.of G f i (DirectLimit.Monoid.exists_subset_range_of). This needs neither that the groups live in a common universe with the index set, nor that the transition maps be injective. The identification of DirectLimit G f with the colimit in GrpCat is TauCeti.GrpCat.directLimitIsColimit.

Main results

• TauCeti.Amenable.of_isColimit: the apex of a colimit cocone over a filtered diagram of amenable topological groups is amenable, provided the legs are continuous.
• TauCeti.Amenable.of_isColimit_of_discreteTopology: the apex of a colimit cocone over a filtered diagram of discrete amenable groups is amenable for every group topology.
• TauCeti.Amenable.directLimit: the direct limit of a directed system of amenable topological groups is amenable, provided the canonical maps are continuous.
• TauCeti.Amenable.directLimit_of_discreteTopology: the direct limit of a directed system of discrete amenable groups is amenable for every group topology.

References

• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Proposition G.2.2.
• A. Garrido, An introduction to amenable groups, Proposition 2.2.

theorem TauCeti.Amenable.of_isColimit {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J GrpCat} [(j : J) → TopologicalSpace ↑(F.obj j)] {c : CategoryTheory.Limits.Cocone F} [TopologicalSpace ↑c.pt] [IsTopologicalGroup ↑c.pt] [∀ (j : J), IsTopologicalGroup ↑(F.obj j)] [∀ (j : J), Amenable ↑(F.obj j)] (hc : CategoryTheory.Limits.IsColimit c) (hcont : ∀ (j : J), Continuous ⇑(GrpCat.Hom.hom (c.ι.app j))) : Amenable ↑c.pt

The apex of a colimit cocone over a filtered diagram of amenable topological groups in GrpCat is amenable, provided the legs of the cocone are continuous.

theorem TauCeti.Amenable.of_isColimit_of_discreteTopology {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J GrpCat} [(j : J) → TopologicalSpace ↑(F.obj j)] {c : CategoryTheory.Limits.Cocone F} [TopologicalSpace ↑c.pt] [IsTopologicalGroup ↑c.pt] [∀ (j : J), DiscreteTopology ↑(F.obj j)] [∀ (j : J), Amenable ↑(F.obj j)] (hc : CategoryTheory.Limits.IsColimit c) : Amenable ↑c.pt

The apex of a colimit cocone over a filtered diagram of discrete amenable groups in GrpCat is amenable, for every group topology on the apex.

theorem TauCeti.Amenable.directLimit {ι : Type u_2} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] {G : ι → Type u_3} [(i : ι) → Group (G i)] {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [(i : ι) → TopologicalSpace (G i)] [TopologicalSpace (DirectLimit G f)] [IsTopologicalGroup (DirectLimit G f)] [∀ (i : ι), IsTopologicalGroup (G i)] [∀ (i : ι), Amenable (G i)] (hcont : ∀ (i : ι), Continuous ⇑(DirectLimit.Monoid.of G f i)) : Amenable (DirectLimit G f)

The direct limit of a directed system of amenable topological groups is amenable, provided the canonical maps from the groups of the system are continuous.

theorem TauCeti.Amenable.directLimit_of_discreteTopology {ι : Type u_2} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι] {G : ι → Type u_3} [(i : ι) → Group (G i)] {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] [DirectedSystem G fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [(i : ι) → TopologicalSpace (G i)] [TopologicalSpace (DirectLimit G f)] [IsTopologicalGroup (DirectLimit G f)] [∀ (i : ι), DiscreteTopology (G i)] [∀ (i : ι), Amenable (G i)] : Amenable (DirectLimit G f)

The direct limit of a directed system of discrete amenable groups is amenable, for every group topology on the direct limit.