English
If f is continuous and open, and fibers f⁻¹'{x} are preirreducible for all x, then irreducible components of Y correspond to those of X via an order isomorphism.
Русский
Если f непрерывно и открыто, и фибры преднеразложимы для всех x, то компоненты неразложимости Y соответствуют компонентам X через шероховатый порядок.
LaTeX
$$$\text{If } f \text{ is continuous and open and fibers are preirreducible, then } (\mathrm{irreducibleComponents}(Y)) \simeq_{\text{order}} (\mathrm{irreducibleComponents}(X))$$$
Lean4
theorem preimage_mem_irreducibleComponents_of_isPreirreducible_fiber {V : Set Y} (hV : V ∈ irreducibleComponents Y) :
f ⁻¹' V ∈ irreducibleComponents X :=
by
obtain ⟨Z, hZ, hWZ, H⟩ := exists_preirreducible _ (hV.1.2.preimage_of_isPreirreducible_fiber f hf₂ hf₃)
have hZ' : IsIrreducible Z := by
obtain ⟨x, hx⟩ := hV.1.1
obtain ⟨x, rfl⟩ := hf₄ x
exact ⟨⟨_, hWZ hx⟩, hZ⟩
have hWZ' : f ⁻¹' V = Z := by
refine hWZ.antisymm (Set.image_subset_iff.mp ?_)
exact
hV.2 (IsIrreducible.image hZ' f hf₁.continuousOn)
((Set.image_preimage_eq V hf₄).symm.trans_le (Set.image_mono hWZ))
rw [hWZ']
exact ⟨hZ', fun s hs hs' ↦ (H s hs.2 hs').le⟩
