English
Same as 37490: equivalence between global closure property and pointwise existence.
Русский
То же, что и 37490: эквивалентность глобального свойства замыкания и локального существования.
LaTeX
$$iff_forall_exists$$
Lean4
instance [P.RespectsIso] [P.RespectsLeft @IsOpenImmersion] :
IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion P) :=
by
refine .mk_of_iff fun f 𝒰 ↦ ?_
refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
· simpa [pullback.condition_assoc] using RespectsLeft.precomp (Q := @IsOpenImmersion) _ inferInstance _ (h j)
· choose 𝒱 h𝒱 using h
exact ⟨𝒰.bind 𝒱, fun i ↦ h𝒱 _ _⟩
