English
Let U be an open cover of X by opens. Then X is Jacobson if and only if every open piece U_i is Jacobson.
Русский
Пусть U — открытое покрытие X набором открытых открытых множеств. Тогда X является пространством Якобсона тогда и только тогда, когда каждый элемент покрытия U_i является пространством Якобсона.
LaTeX
$$$ \operatorname{JacobsonSpace}(X) \iff \forall i, \operatorname{JacobsonSpace}(U_i) $$$
Lean4
theorem jacobsonSpace_iff {ι : Type*} {U : ι → Opens X} (hU : IsOpenCover U) :
JacobsonSpace X ↔ ∀ i, JacobsonSpace (U i) :=
by
refine ⟨fun H i ↦ .of_isOpenEmbedding (U i).2.isOpenEmbedding_subtypeVal, fun H ↦ ?_⟩
rw [jacobsonSpace_iff_locallyClosed]
intro Z hZ hZ'
rw [← hU.iUnion_inter Z, Set.nonempty_iUnion] at hZ
obtain ⟨i, x, hx, hx'⟩ := hZ
obtain ⟨y, hy, hy'⟩ :=
(jacobsonSpace_iff_locallyClosed.mp (H i)) _ ⟨⟨x, hx'⟩, hx⟩ (hZ'.preimage continuous_subtype_val)
refine ⟨y, hy, hU.isClosed_iff_coe_preimage.mpr fun j ↦ ?_⟩
by_cases h : (y : X) ∈ U j
· convert_to IsClosed {(⟨y, h⟩ : U j)}
· ext; simp [← Subtype.coe_inj]
apply isClosed_singleton_of_isLocallyClosed_singleton
convert
(hy'.isLocallyClosed.image IsEmbedding.subtypeVal.isInducing
(U i).2.isOpenEmbedding_subtypeVal.isOpen_range.isLocallyClosed).preimage
continuous_subtype_val
ext
simp [← Subtype.coe_inj]
· convert isClosed_empty
rw [Set.eq_empty_iff_forall_notMem]
intro z (hz : z.1 = y.1)
exact h (hz ▸ z.2)
