Theorems · Definition · category theory

LightProfinite.Extend.functor

{F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.StructuredArrow c.pt FintypeCat.toLightProfinite)

Given a sequential cone in LightProfinite consisting of finite sets, we obtain a functor from the indexing category to StructuredArrow c.pt toLightProfinite.

Defined in

Mathlib.Topology.Category.LightProfinite.Extend

Cited by

5 results in Mathlib

Foundations

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