Theorems · Definition · category theory

Profinite.Extend.cone

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (G : CategoryTheory.Functor Profinite C) →
      (S : Profinite) →
        CategoryTheory.Limits.Cone
          ((CategoryTheory.StructuredArrow.proj S FintypeCat.toProfinite).comp (FintypeCat.toProfinite.comp G))

Given a functor G from Profinite and S : Profinite, we obtain a cone on (StructuredArrow.proj S toProfinite ⋙ toProfinite ⋙ G) with cone point G.obj S. Whiskering this cone with Profinite.Extend.functor c gives G.mapCone c as we check in the example below.

Defined in

Mathlib.Topology.Category.Profinite.Extend

Cited by

2 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category