Theorems · Theorem · category theory

LightProfinite.Extend.functorOp_final

∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)],
  (LightProfinite.Extend.functorOp c).Final

If the projection maps in the cone are epimorphic and the cone is limiting, then LightProfinite.Extend.functorOp is final.

Defined in

Mathlib.Topology.Category.LightProfinite.Extend

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Epi