exists_open_ne_empty_le_irreducibleComponent

English

For any irreducible component Z in a Noetherian space, there exists a nonempty open set contained in Z.

Русский

Для любой неприводимой компоненты Z в Noetherian-пространстве существует непустое открытое множество, contained в Z.

LaTeX

$$$\forall Z \in \operatorname{irreducibleComponents}(X), \exists \; o \subseteq X: \; \text{IsOpen}(o) \wedge o \neq \emptyset \wedge o \le Z.$$$

Lean4

@[stacks 0052 "(3)"]
theorem exists_open_ne_empty_le_irreducibleComponent [NoetherianSpace α] (Z : Set α) (H : Z ∈ irreducibleComponents α) :
    ∃ o : Set α, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z := by
  classical
  let ι : Set (Set α) := irreducibleComponents α \ { Z }
  have hι : ι.Finite := NoetherianSpace.finite_irreducibleComponents.subset Set.diff_subset
  have hι' : Finite ι := by rwa [Set.finite_coe_iff]
  let U := Z \ ⋃ (x : ι), x
  have hU0 : U ≠ ∅ := fun r ↦
    by
    obtain ⟨Z', hZ'⟩ :=
      isIrreducible_iff_sUnion_isClosed.mp H.1 hι.toFinset
        (fun z hz ↦ by
          simp only [Set.Finite.mem_toFinset] at hz
          exact isClosed_of_mem_irreducibleComponents _ hz.1)
        (by
          rw [Set.Finite.coe_toFinset, Set.sUnion_eq_iUnion]
          rw [Set.diff_eq_empty] at r
          exact r)
    simp only [Set.Finite.mem_toFinset] at hZ'
    exact hZ'.1.2 <| le_antisymm (H.2 hZ'.1.1.1 hZ'.2) hZ'.2
  have hU1 : U = (⋃ (x : ι), x.1)ᶜ := by
    rw [Set.compl_eq_univ_diff]
    refine le_antisymm (Set.diff_subset_diff le_top subset_rfl) ?_
    rw [← Set.compl_eq_univ_diff]
    refine Set.compl_subset_iff_union.mpr (le_antisymm le_top ?_)
    rw [Set.union_comm, ← Set.sUnion_eq_iUnion, ← Set.sUnion_insert]
    rintro a -
    by_cases h : a ∈ U
    · exact ⟨U, Set.mem_insert _ _, h⟩
    · rw [Set.mem_diff, Decidable.not_and_iff_not_or_not, not_not, Set.mem_iUnion] at h
      rcases h with (h | ⟨i, hi⟩)
      · refine ⟨irreducibleComponent a, Or.inr ?_, mem_irreducibleComponent⟩
        simp only [ι, Set.mem_diff, Set.mem_singleton_iff]
        refine ⟨irreducibleComponent_mem_irreducibleComponents _, ?_⟩
        rintro rfl
        exact h mem_irreducibleComponent
      · exact ⟨i, Or.inr i.2, hi⟩
  refine ⟨U, hU1 ▸ isOpen_compl_iff.mpr ?_, hU0, sdiff_le⟩
  exact isClosed_iUnion_of_finite fun i ↦ isClosed_of_mem_irreducibleComponents i.1 i.2.1

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