nat_trans_naturality — Mathlib

English

For a morphism f: F' ⟶ G.toPresheaf, the naturality condition holds: (f.app V (F'.map i x)).1 = F.map i (f.app U x).1.

Русский

Для морфизма f: F' ⟶ G.toPresheaf выполняется условие натуральности: (f.app V (F'.map i x)).1 = F.map i (f.app U x).1.

LaTeX

$$$(f.app V (F'.map i x)).1 = F.map i (f.app U x).1$$$

Lean4

theorem nat_trans_naturality (f : F' ⟶ G.toPresheaf) {U V : Cᵒᵖ} (i : U ⟶ V) (x : F'.obj U) :
    (f.app V (F'.map i x)).1 = F.map i (f.app U x).1 :=
  congr_arg Subtype.val (FunctorToTypes.naturality _ _ f i x)

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