Theorems · Definition · category theory

LightProfinite.Extend.isLimitCone

{F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} →
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        (G : CategoryTheory.Functor LightProfinite C) →
          CategoryTheory.Limits.IsLimit c →
            [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] →
              CategoryTheory.Limits.IsLimit (G.mapCone c) →
                CategoryTheory.Limits.IsLimit (LightProfinite.Extend.cone G c.pt)

If c and G.mapCone c are limit cones and the projection maps in c are epimorphic, then cone G c.pt is a limit cone.

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.CategoryCategoryTheory.Epi