topologically_isZariskiLocalAtSource'

English

Independent of site, diagonal is local at the source under certain assumptions.

Русский

Диагональ локальна у источника при некоторых предпосылках.

LaTeX

$$HasAffineProperty.diagonal_isLocal_at_source$$

Lean4

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

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