app_eq — Mathlib

English

For e: X = Y, (eqToHom e).app U = eqToHom (by subst e; rfl).

Русский

Для e: X = Y, (eqToHom e).app U = eqToHom (by subst e; rfl).

LaTeX

$$$(eqToHom e).app U = eqToHom (\\text{by }\\; subst e; \\; rfl)$$$

Lean4

theorem app_eq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) :
    f.app U =
      Y.presheaf.map (eqToHom e.symm).op ≫ f.app V ≫ X.presheaf.map (eqToHom (congr_arg (Opens.map f.base).obj e)).op :=
  by
  rw [← IsIso.inv_comp_eq, ← Functor.map_inv, f.naturality]
  cases e
  rfl

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