congr_app — Mathlib

English

If f = g, then f.app U equals g.app U followed by a suitable map on the presheaf induced by the equality; more precisely, f.app U = g.app U ≫ X.presheaf.map (eqToHom (by subst e; rfl)).op.

Русский

Если f = g, то f.app U = g.app U ∘ соответствующее отображение на пирсешфе по равенству; конкретно f.app U = g.app U ∘ eqToHom (by subst e; rfl).op.

LaTeX

$$$f.app U = g.app U \\; \\circ \\; X.presheaf.map (eqToHom (by \\; subst e; \\; rfl)).op$$$

Lean4

theorem congr_app {X Y : Scheme} {f g : X ⟶ Y} (e : f = g) (U) :
    f.app U = g.app U ≫ X.presheaf.map (eqToHom (by subst e; rfl)).op := by subst e; simp

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