feat: port CategoryTheory.Idempotents.SimplicialObject (#3411)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -403,6 +403,7 @@ import Mathlib.CategoryTheory.Idempotents.FunctorCategories
 import Mathlib.CategoryTheory.Idempotents.FunctorExtension
 import Mathlib.CategoryTheory.Idempotents.Karoubi
 import Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
+import Mathlib.CategoryTheory.Idempotents.SimplicialObject
 import Mathlib.CategoryTheory.IsConnected
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.IsomorphismClasses

Mathlib/CategoryTheory/Idempotents/SimplicialObject.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+
+! This file was ported from Lean 3 source module category_theory.idempotents.simplicial_object
+! leanprover-community/mathlib commit 163d1a6d98caf9f0431704169027e49c5c6c6cc0
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.AlgebraicTopology.SimplicialObject
+import Mathlib.CategoryTheory.Idempotents.FunctorCategories
+
+/-!
+
+# Idempotent completeness of categories of simplicial objects
+
+In this file, we provide an instance expressing that `SimplicialObject C`
+and `CosimplicialObject C` are idempotent complete categories when the
+category `C` is.
+
+-/
+
+
+namespace CategoryTheory
+
+namespace Idempotents
+
+variable {C : Type _} [Category C] [IsIdempotentComplete C]
+
+instance : IsIdempotentComplete (SimplicialObject C) :=
+  Idempotents.functor_category_isIdempotentComplete _ _
+
+instance : IsIdempotentComplete (CosimplicialObject C) :=
+  Idempotents.functor_category_isIdempotentComplete _ _
+
+end Idempotents
+
+end CategoryTheory