w_obj — Mathlib

English

For a based functor F: X ⇢ Y and an object a in X, the base object of F(a) equals the base object of a: p_Y(F(a)) = p_X(a).

Русский

Для основанного функторa F: X ⥤ᵇ Y и объекта a в X базовый объект F(a) равен базовому объекту a: p_Y(F(a)) = p_X(a).

LaTeX

$$$\\forall a:\\\, X.obj,\\; Y.p.obj(F.obj(a)) = X.p.obj(a)$$$

Lean4

@[simp]
theorem w_obj (F : 𝒳 ⥤ᵇ 𝒴) (a : 𝒳.obj) : 𝒴.p.obj (F.obj a) = 𝒳.p.obj a := by rw [← Functor.comp_obj, F.w]

Похожие утверждения