Monoidal object properties on tensor words

A monoidal property of objects holds on the interpretation of every formal tensor word as soon as it holds on the generating objects. This lets interpretations of a monoidal presentation be restricted to properties needed only on their image, rather than imposed on the whole target category. The interpretation is Mathlib's FreeMonoidalCategory.projectObj; no new tensor-word carrier or evaluation function is introduced.

theorem CategoryTheory.ObjectProperty.prop_projectObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (P : ObjectProperty C) [P.IsMonoidal] {A : Type w} {f : A → C} (h : ∀ (a : A), P (f a)) (W : FreeMonoidalCategory A) : P (FreeMonoidalCategory.projectObj f W)

A monoidal property holding on the generators holds on every interpreted tensor word, including the empty word and every parenthesization.