topologically_isZariskiLocalAtSource

English

A variant stating HasAffineProperty for diagonals is stable under local checks.

Русский

Вариант: диагональ (P.diagonal) обладает локальной аффинной свойностью.

LaTeX

$$HasAffineProperty(P.diagonal, Q.diagonal)$$

Lean4

theorem topologically_isZariskiLocalAtSource [(topologically P).RespectsIso]
    (hP₁ :
      ∀ {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (_ : Continuous f) (U : Opens X),
        P f → P (f ∘ ((↑) : U → X)))
    (hP₂ :
      ∀ {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (_ : Continuous f) {ι : Type u}
        (U : ι → Opens X), IsOpenCover U → (∀ i, P (f ∘ ((↑) : U i → X))) → P f) :
    IsZariskiLocalAtSource (topologically P) :=
  by
  apply IsZariskiLocalAtSource.mk'
  · introv hf
    exact hP₁ f.base f.continuous _ hf
  · introv hU hf
    exact hP₂ f.base f.continuous _ hU hf

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