Retracting a category onto an induced category

Let F : S → C be a map to the objects of a category C, and suppose that every object x of C comes with an isomorphism e x : x ≅ F (r x) to an object in the image of F. Conjugating by these isomorphisms defines the functor TauCeti.InducedCategory.retraction F r e from C to the induced category InducedCategory C F, sending x to r x. When the chosen isomorphisms are identities on the image of F, it is a strict retraction of the inclusion inducedFunctor F.

Under the same hypothesis the inclusion inducedFunctor F is an equivalence, but an inverse chosen by the equivalence machinery is not under control. Choosing the isomorphisms by hand allows retractions of several categories to commute strictly with given functors between them, which is what strict colimit arguments in the category of groupoids require. This is how a fundamental groupoid is retracted onto its full subgroupoid on a set of basepoints, compatibly with the fundamental groupoids of subspaces.

Main declarations

• TauCeti.InducedCategory.retraction: the functor C ⥤ InducedCategory C F given by conjugation by the chosen isomorphisms.
• TauCeti.InducedCategory.inducedFunctor_comp_retraction: it is a retraction of the inclusion when the chosen isomorphisms are identities on the image of F.

References

• R. Brown, Topology and Groupoids, 3rd ed., Section 6.7.

def TauCeti.InducedCategory.retraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {S : Type u_2} (F : S → C) (r : C → S) (e : (x : C) → x ≅ F (r x)) : CategoryTheory.Functor C (CategoryTheory.InducedCategory C F)

Conjugation by chosen isomorphisms e x : x ≅ F (r x), as a functor from C to the induced category on F: it sends x to r x and f : x ⟶ y to (e x).inv ≫ f ≫ (e y).hom.

Equations

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

@[simp]

theorem TauCeti.InducedCategory.retraction_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {S : Type u_2} (F : S → C) (r : C → S) (e : (x : C) → x ≅ F (r x)) (x : C) : (retraction F r e).obj x = r x

@[simp]

theorem TauCeti.InducedCategory.retraction_map_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {S : Type u_2} (F : S → C) (r : C → S) (e : (x : C) → x ≅ F (r x)) {x y : C} (f : x ⟶ y) : ((retraction F r e).map f).hom = CategoryTheory.CategoryStruct.comp (e x).inv (CategoryTheory.CategoryStruct.comp f (e y).hom)

theorem TauCeti.InducedCategory.inducedFunctor_comp_retraction {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {S : Type u_2} (F : S → C) (r : C → S) (e : (x : C) → x ≅ F (r x)) (hr : ∀ (s : S), r (F s) = s) (he : ∀ (s : S), (e (F s)).hom = CategoryTheory.eqToHom ⋯) : (CategoryTheory.inducedFunctor F).comp (retraction F r e) = CategoryTheory.Functor.id (CategoryTheory.InducedCategory C F)

If the chosen isomorphisms are identities on the image of F, the retraction restricts to the identity of the induced category.