isZariskiLocalAtSource — Mathlib

English

P is local on the source in the Zariski topology given a transfer of equivalence from Q across affine opens.

Русский

P является локальным по источнику в Zariski-локальности с учётом переноса через афинные открытые.

LaTeX

$$$IsZariskiLocalAtSource P$$$

Lean4

theorem isZariskiLocalAtSource
    (H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] (𝒰 : Scheme.OpenCover.{u} X), Q f ↔ ∀ i, Q (𝒰.f i ≫ f)) :
    IsZariskiLocalAtSource P := by
  refine .mk_of_iff ?_
  intro X Y f 𝒰
  simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y)]
  rw [forall_comm]
  refine forall_congr' fun U ↦ ?_
  simp_rw [HasAffineProperty.iff_of_isAffine, morphismRestrict_comp]
  exact @H _ _ (f ∣_ U.1) U.2 (Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ U.1))

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