image_mem_irreducibleComponents_of_isPreirreducible_fiber

English

If V is an irreducible component in Y, then f⁻¹'(V) is an irreducible component in X.

Русский

Если V — неразложимая компонентa в Y, то f⁻¹'(V) — неразложимая компонента в X.

LaTeX

$$$V \in \mathrm{irreducibleComponents}(Y) \rightarrow f^{-1}(V) \in \mathrm{irreducibleComponents}(X)$$$

Lean4

theorem image_mem_irreducibleComponents_of_isPreirreducible_fiber {V : Set X} (hV : V ∈ irreducibleComponents X) :
    f '' V ∈ irreducibleComponents Y :=
  ⟨hV.1.image _ hf₁.continuousOn, fun Z hZ hWZ ↦
    by
    have :=
      hV.2
        ⟨(by obtain ⟨x, hx⟩ := hV.1.1; exact ⟨x, hWZ ⟨x, hx, rfl⟩⟩), hZ.2.preimage_of_isPreirreducible_fiber f hf₂ hf₃⟩
        (Set.image_subset_iff.mp hWZ)
    rw [← Set.image_preimage_eq Z hf₄]
    exact Set.image_mono this⟩

Похожие утверждения