English
If W1 is a morphism property on C1 and W2 is a morphism property on C2, then the induced property on the product category C1 × C2 is defined pointwise: a morphism (f1, f2) lies in prod(W1, W2) iff f1 ∈ W1 and f2 ∈ W2.
Русский
Если W1 и W2 — свойства морфизмов на категориях C1 и C2 соответственно, то индуцированное свойство на произведение категорий C1 × C2 определяется поэлементно: морфизм (f1, f2) принадлежит prod(W1, W2) тогда и только тогда, когда f1 ∈ W1 и f2 ∈ W2.
LaTeX
$$$\\mathrm{prod}(W_1,W_2)(f) \\;\\coloneqq\\; W_1(f.1) \\land W_2(f.2)\\quad (f : C_1 \\times C_2 \\to \\text{...})$$$
Lean4
/-- If `W₁` and `W₂` are morphism properties on two categories `C₁` and `C₂`,
this is the induced morphism property on `C₁ × C₂`. -/
def prod {C₁ C₂ : Type*} [Category C₁] [Category C₂] (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) :
MorphismProperty (C₁ × C₂) := fun _ _ f => W₁ f.1 ∧ W₂ f.2
