topologically_isZariskiLocalAtTarget'

English

A variant asserting locality for diagonal with a local property.

Русский

Вариант локальности диагонали для локального свойства.

LaTeX

$$diagonal_isLocal_variant$$

Lean4

/-- A variant of `topologically_isZariskiLocalAtTarget`
that takes one iff statement instead of two implications. -/
theorem topologically_isZariskiLocalAtTarget' [(topologically P).RespectsIso]
    (hP :
      ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β)
        (_ : IsOpenCover U) (_ : Continuous f), P f ↔ (∀ i, P ((U i).carrier.restrictPreimage f))) :
    IsZariskiLocalAtTarget (topologically P) :=
  by
  refine topologically_isZariskiLocalAtTarget P ?_ (fun f _ U hU hU' ↦ (hP f U hU hU').mpr)
  introv hf hs H
  refine (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩
  rw [IsOpenCover, ← top_le_iff]
  exact le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩

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