English
A variant giving a one-way iff statement for topological localization at target.
Русский
Вариант даёт одностороннюю эквивалентность локальности по цели.
LaTeX
$$topologically_isZarisaniLocalAtTarget'(...)$$
Lean4
/-- To check that a topologically defined morphism property is local at the target,
we may check the corresponding properties on topological spaces. -/
theorem topologically_isZariskiLocalAtTarget [(topologically P).RespectsIso]
(hP₂ :
∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set β) (_ : Continuous f)
(_ : IsOpen s), P f → P (s.restrictPreimage f))
(hP₃ :
∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β)
(_ : IsOpenCover U) (_ : Continuous f), (∀ i, P ((U i).carrier.restrictPreimage f)) → P f) :
IsZariskiLocalAtTarget (topologically P) :=
by
apply IsZariskiLocalAtTarget.mk'
· intro X Y f U hf
simp_rw [topologically, morphismRestrict_base]
exact hP₂ f.base U.carrier f.base.hom.2 U.2 hf
· intro X Y f ι U hU hf
apply hP₃ f.base U hU f.base.hom.continuous fun i ↦ ?_
rw [← morphismRestrict_base]
exact hf i
