Spec_map_presheaf_map_eqToHom — Mathlib

English

If opens U,V are equal, then the Spec map induced by the presheaf map is equal to the identity composed with eqToHom: (Spec.map (X.presheaf.map (eqToHom h).op)).app W = eqToHom (by cases h; simp).

Русский

Если открытые множества U,V равны, отображение Spec, индуцируемое отображением пресшенф, равняется идентичности через eqToHom: (Spec.map ...).app W = eqToHom ...

LaTeX

$$$(\mathrm{Spec}.map (X.presheaf.map (eqToHom h).op)).app W = \mathrm{eqToHom}(...)$$$

Lean4

theorem Spec_map_presheaf_map_eqToHom {X : Scheme} {U V : X.Opens} (h : U = V) (W) :
    (Spec.map (X.presheaf.map (eqToHom h).op)).app W = eqToHom (by cases h; simp) :=
  by
  have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
  cases h
  refine (Scheme.congr_app this _).trans ?_
  simp [eqToHom_map]

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