English
If V is preirreducible in Y, f: X → Y is open, and V is contained in the closure of V intersected with fibers that are preirreducible, then f⁻¹'(V) is preirreducible.
Русский
Если V преднеразложимо в Y, f: X → Y открытое отображение, и V ⊆ closure(V ∩ {x | преднеразложимо (f⁻¹'( {x} ))}), то f⁻¹'(V) преднеразложимо.
LaTeX
$$$\mathrm{IsPreirreducible}(V) \rightarrow (f:X\to Y) \rightarrow \mathrm{IsOpenMap}(f) \rightarrow V \subseteq \overline{V \cap \{x : \mathrm{IsPreirreducible}(f^{-1}({x}))\}} \rightarrow \mathrm{IsPreirreducible}(f^{-1}(V))$$$
Lean4
@[stacks 004Z]
theorem preimage_of_dense_isPreirreducible_fiber {V : Set Y} (hV : IsPreirreducible V) (f : X → Y) (hf' : IsOpenMap f)
(hf'' : V ⊆ closure (V ∩ {x | IsPreirreducible (f ⁻¹' { x })})) : IsPreirreducible (f ⁻¹' V) :=
by
rintro U₁ U₂ hU₁ hU₂ ⟨x, hxV, hxU₁⟩ ⟨y, hyV, hyU₂⟩
obtain ⟨z, hzV, hz₁, hz₂⟩ := hV _ _ (hf' _ hU₁) (hf' _ hU₂) ⟨f x, hxV, x, hxU₁, rfl⟩ ⟨f y, hyV, y, hyU₂, rfl⟩
obtain ⟨z, ⟨⟨z₁, hz₁, e₁⟩, ⟨z₂, hz₂, e₂⟩⟩, hzV, hz⟩ :=
mem_closure_iff.mp (hf'' hzV) _ ((hf' _ hU₁).inter (hf' _ hU₂)) ⟨hz₁, hz₂⟩
obtain ⟨z₃, hz₃, hz₃'⟩ := hz _ _ hU₁ hU₂ ⟨z₁, e₁, hz₁⟩ ⟨z₂, e₂, hz₂⟩
refine ⟨z₃, show f z₃ ∈ _ from (show f z₃ = z from hz₃) ▸ hzV, hz₃'⟩
