stalkwise_isZariskiLocalAtSource_of_respectsIso

English

Stalkwise P is local at the source provided P respects isos.

Русский

Stalkwise P локально по источнику при условии, что P сохраняет изоморфизмы.

LaTeX

$$stalkwise_isZariskiLocalAtSource_of_respectsIso$$

Lean4

/-- If `P` respects isos, then `stalkwise P` is local at the source. -/
theorem stalkwise_isZariskiLocalAtSource_of_respectsIso (hP : RingHom.RespectsIso P) :
    IsZariskiLocalAtSource (stalkwise P) :=
  by
  letI := stalkwise_respectsIso hP
  apply IsZariskiLocalAtSource.mk'
  · intro X Y f U hf x
    rw [Scheme.stalkMap_comp, CommRingCat.hom_comp, hP.cancel_right_isIso]
    exact hf _
  · intro X Y f ι U hU hf x
    have hy : x ∈ iSup U := by rw [hU]; trivial
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp hy
    rw [← hP.cancel_right_isIso _ ((U i).ι.stalkMap ⟨x, hi⟩)]
    simpa [Scheme.stalkMap_comp] using hf i ⟨x, hi⟩

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