isAffine_of_isAffineOpen_basicOpen

English

If a spanning set s of Γ(X, U) is given with each basicOpen affine, then X is affine.

Русский

Если есть порядок s слов Γ(X, U) с каждым X.basicOpen(i) аффинным, то X аффинна.

LaTeX

$$$\\forall (s),\\; (I) \\Rightarrow IsAffine X$$$

Lean4

theorem isAffine_of_isAffineOpen_basicOpen (s : Set Γ(X, ⊤)) (hs : Ideal.span s = ⊤)
    (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) : IsAffine X :=
  by
  have : QuasiSeparatedSpace X := isAffineOpen_of_isAffineOpen_basicOpen_aux s hs hs₂
  have : CompactSpace X := by
    obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
    rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]
    simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]
    apply s'.isCompact_biUnion
    exact fun i hi ↦ (hs₂ _ (hs' hi)).isCompact
  constructor
  refine
    HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
      (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)
  · change IsAffineOpen _
    simp only [← basicOpen_eq_of_affine]
    exact (isAffineOpen_top (Scheme.Spec.obj (op _))).basicOpen _
  · rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]
  · rw [Scheme.toSpecΓ_preimage_basicOpen]
    exact hs₂ _ i.2
  · simp only [Opens.map_top, morphismRestrict_app]
    refine IsIso.comp_isIso' ?_ inferInstance
    convert isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0
    refine congr(IsIso ((ΓSpec.adjunction.unit.app X).app $(?_)))
    rw [Opens.isOpenEmbedding_obj_top]

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