English
For each X, the stalk map toStalk M X yields an IsLocalizedModule structure in the carrier.
Русский
Для каждого X карта stalk к MX образует структуру IsLocalizedModule.
LaTeX
$$IsLocalizedModule x.asIdeal.primeCompl (toStalk M x).hom$$
Lean4
theorem isAffineOpen_of_isAffineOpen_basicOpen_aux (s : Set Γ(X, ⊤)) (hs : Ideal.span s = ⊤)
(hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : QuasiSeparatedSpace X :=
by
rw [quasiSeparatedSpace_iff_affine]
intro U V
obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
rw [← Set.inter_univ (_ ∩ _), ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e, ← iSup_subtype'',
Opens.coe_iSup, Set.inter_iUnion]
apply isCompact_iUnion
intro i
rw [Set.inter_inter_distrib_right]
refine
(hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right (U.1.2.inter (X.basicOpen _).2) ?_
Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_
· rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
exact (U.2.basicOpen _).isCompact
· rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
exact (V.2.basicOpen _).isCompact
