Left orthogonals are closed under colimits

A map out of a colimit is determined by its components, so if every object of a diagram is left orthogonal to P, so is the colimit: the induced map and the zero map agree on every leg.

Mathlib's Mathlib/CategoryTheory/ObjectProperty/Orthogonal.lean gives both orthogonals IsClosedUnderIsomorphisms and ContainsZero, and its Triangulated/Orthogonal.lean gives them IsTriangulatedClosed₂. Closure under colimits is the one hypothesis of ObjectProperty.coprodClosure_le that neither file supplies, which is why two compactly-generated t-structure proofs each re-derived it by hand as three branches of an induction over coprodClosure. With this instance both collapse to a single coprodClosure_le application.

The statement is for an arbitrary shape J, not just Discrete ι, because nothing in the argument uses the shape: IsColimit.hom_ext is the whole proof. There is no dual instance for rightOrthogonal under limits here, because no consumer needs one yet.

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeLeftOrthogonal {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (J : Type u') [Category.{v', u'} J] : P.leftOrthogonal.IsClosedUnderColimitsOfShape J