Functors on a groupoid with a weakly initial object

Let C be a groupoid and x₀ : C an object which admits a morphism to every object. Restricting functors F G : C ⥤ D to x₀ produces objects of D with actions of the vertex group End x₀. This file proves that an isomorphism F.obj x₀ ≅ G.obj x₀ commuting with these actions extends to a natural isomorphism F ≅ G, and the extension has the given isomorphism as its component at x₀.

The construction is the usual transport of structure. Choosing a morphism γ x : x₀ ⟶ x for every object, the component at x is F.map (γ x)⁻¹ ≫ e ≫ G.map (γ x); naturality at f : x ⟶ y holds because the discrepancy γ x ≫ f ≫ (γ y)⁻¹ between the two chosen morphisms is an endomorphism of x₀, so equivariance applies to it. Nothing depends on the choice, since the resulting natural transformation is determined by its component at x₀, and that component is e whatever γ x₀ is.

The hypothesis is exactly connectedness of the groupoid when C is nonempty, but is stated as the family of nonemptiness assertions ∀ x, Nonempty (x₀ ⟶ x) rather than through CategoryTheory.IsConnected: the intended source of that data is a path-connected topological space, whose fundamental groupoid comes with paths from a chosen basepoint, and the equivalence of the two formulations is not needed.

Main declarations

• TauCeti.Groupoid.natTrans_ext: a natural transformation is determined by its component at the weakly initial object.
• TauCeti.Groupoid.natIsoOfEnd: an equivariant isomorphism of the values at a weakly initial object of a groupoid extends to a natural isomorphism.
• TauCeti.Groupoid.natIsoOfEnd_app_self: the extension restricts to the given isomorphism.
• TauCeti.Groupoid.eq_natIsoOfEnd: the extension is the only natural isomorphism doing so.

theorem TauCeti.Groupoid.natTrans_ext {C : Type u} [CategoryTheory.Groupoid C] {D : Type w} [CategoryTheory.Category.{t, w} D] {F G : CategoryTheory.Functor C D} {x₀ : C} (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) {α β : F ⟶ G} (h : α.app x₀ = β.app x₀) : α = β

A natural transformation between functors out of a groupoid is determined by its component at a weakly initial object.

theorem TauCeti.Groupoid.natIso_ext {C : Type u} [CategoryTheory.Groupoid C] {D : Type w} [CategoryTheory.Category.{t, w} D] {F G : CategoryTheory.Functor C D} {x₀ : C} (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) {α β : F ≅ G} (h : α.app x₀ = β.app x₀) : α = β

A natural isomorphism between functors out of a groupoid is determined by its component at a weakly initial object.

noncomputable def TauCeti.Groupoid.natIsoOfEnd {C : Type u} [CategoryTheory.Groupoid C] {D : Type w} [CategoryTheory.Category.{t, w} D] {F G : CategoryTheory.Functor C D} {x₀ : C} (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) (e : F.obj x₀ ≅ G.obj x₀) (he : ∀ (g : x₀ ⟶ x₀), CategoryTheory.CategoryStruct.comp (F.map g) e.hom = CategoryTheory.CategoryStruct.comp e.hom (G.map g)) : F ≅ G

An End x₀-equivariant isomorphism between the values of two functors at a weakly initial object of a groupoid extends to a natural isomorphism.

Its component at x₀ is the given isomorphism, by natIsoOfEnd_app_self.

Equations

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

@[simp]

theorem TauCeti.Groupoid.natIsoOfEnd_app_self {C : Type u} [CategoryTheory.Groupoid C] {D : Type w} [CategoryTheory.Category.{t, w} D] {F G : CategoryTheory.Functor C D} {x₀ : C} (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) (e : F.obj x₀ ≅ G.obj x₀) (he : ∀ (g : x₀ ⟶ x₀), CategoryTheory.CategoryStruct.comp (F.map g) e.hom = CategoryTheory.CategoryStruct.comp e.hom (G.map g)) : (natIsoOfEnd hconn e he).app x₀ = e

The extension of an equivariant isomorphism restricts to that isomorphism.

theorem TauCeti.Groupoid.eq_natIsoOfEnd {C : Type u} [CategoryTheory.Groupoid C] {D : Type w} [CategoryTheory.Category.{t, w} D] {F G : CategoryTheory.Functor C D} {x₀ : C} (hconn : ∀ (x : C), Nonempty (x₀ ⟶ x)) (e : F.obj x₀ ≅ G.obj x₀) (he : ∀ (g : x₀ ⟶ x₀), CategoryTheory.CategoryStruct.comp (F.map g) e.hom = CategoryTheory.CategoryStruct.comp e.hom (G.map g)) (α : F ≅ G) (hα : α.app x₀ = e) : α = natIsoOfEnd hconn e he

The extension is the only natural isomorphism restricting to the given one at the weakly initial object.