eval_app — Mathlib

English

In a sheaf setting, the imageι map composed with toImage recovers the original morphism.

Русский

В условиях шарфа композицию imageι с toImage восстанавливает исходный морфизм.

LaTeX

$$$ toImage f \\;\\;\\; \\text{composed with} \\;\\; imageι f = f $$$

Lean4

theorem eval_app (S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)) (f : S₁ ⟶ S₂) (α : Type u) (s : S₁.1.obj (op α))
    (x : α) : eval S₂.1 α (f.val.app (op α) s) x = f.val.app (op PUnit) (eval S₁.1 α s x) :=
  (congr_fun (f.val.naturality (↾fun _ : PUnit => x).op) s).symm

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