Theorems · Theorem · category theory

CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F],
  X.IsCoskeletal n ↔ CategoryTheory.IsIso ((CategoryTheory.SimplicialObject.coskAdj n).unit.app X)

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Functor.HasRightKanExtension