basicOpen_fromSpec_app — Mathlib

English

A compatibility relation between ΓSpecIso and fromSpec isomorphisms holds in the affine setting.

Русский

В афинной настройке выполняется совместимость между ΓSpecIso и изоморфизмами fromSpec.

LaTeX

$$$(Scheme.\,ΓSpecIso(X))^{\mathrm{hom}} \circ h_U^{fromSpec}(U) = (\mathrm{Spec}(X.presheaf.obj{ unop := U })).presheaf.map( eqToHom(h_U.fromSpec_preimage_self).op)$$$

Lean4

@[simp]
theorem basicOpen_fromSpec_app : (Spec Γ(X, U)).basicOpen (hU.fromSpec.app U f) = PrimeSpectrum.basicOpen f := by
  rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]

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