English
If V is irreducible in X, then f''V is an irreducible component in Y.
Русский
Если V неразложимо в X, то образ f[V] является компонентой неразложимости в Y.
LaTeX
$$$V \in \mathrm{irreducibleComponents}(X) \rightarrow f''V \in \mathrm{irreducibleComponents}(Y)$$$
Lean4
/-- If `f : X → Y` is continuous, open, and has irreducible fibers, then it induces an
bijection between irreducible components -/
@[stacks 037A]
def irreducibleComponentsEquivOfIsPreirreducibleFiber : irreducibleComponents Y ≃o irreducibleComponents X
where
invFun W := ⟨f '' W.1, image_mem_irreducibleComponents_of_isPreirreducible_fiber f hf₁ hf₂ hf₃ hf₄ W.2⟩
toFun W := ⟨f ⁻¹' W.1, preimage_mem_irreducibleComponents_of_isPreirreducible_fiber f hf₁ hf₂ hf₃ hf₄ W.2⟩
right_inv
W :=
Subtype.ext <|
by
refine (Set.subset_preimage_image _ _).antisymm' (W.2.2 ?_ (Set.subset_preimage_image _ _))
refine ⟨?_, (W.2.1.image _ hf₁.continuousOn).2.preimage_of_isPreirreducible_fiber _ hf₂ hf₃⟩
obtain ⟨x, hx⟩ := W.2.1.1
exact ⟨_, x, hx, rfl⟩
left_inv _ := Subtype.ext <| Set.image_preimage_eq _ hf₄
map_rel_iff'
{W Z} := by
refine ⟨fun H ↦ ?_, Set.preimage_mono⟩
simpa only [Equiv.coe_fn_mk, Set.image_preimage_eq _ hf₄] using Set.image_mono (f := f) H
