English
If a base morphism is injective and all pieces in an open cover compose with f to give open immersions, then f is an open immersion.
Русский
Если базовая морфизма инъективна и все элементы открытого покрытия дают через f открытые вложения, то сам f — открытое вложение.
LaTeX
$$$ IsOpenImmersion f \Leftarrow \forall i, IsOpenImmersion(\mathcal{U}.f_i \circ f) \land Injective(f.base) $$$
Lean4
theorem of_openCover_source (f : X ⟶ Y) (𝒰 : X.OpenCover) (hf : Function.Injective f.base)
(h𝒰 : ∀ i, IsOpenImmersion (𝒰.f i ≫ f)) : IsOpenImmersion f :=
by
refine isOpenImmersion_iff_stalk.mpr ⟨.of_continuous_injective_isOpenMap f.continuous hf ?_, ?_⟩
· intro U hU
convert (⨆ i, ((𝒰.f i ≫ f) ''ᵁ (𝒰.f i ⁻¹ᵁ ⟨U, hU⟩))).2
ext x
exact ⟨fun ⟨x, _, _⟩ ↦ by have := 𝒰.exists_eq x; simp; grind, by simp; grind⟩
· intro x
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
rw [← (IsIso.comp_inv_eq _).mpr (Scheme.stalkMap_comp (𝒰.f i) f x)]
infer_instance
