affineOpenCoverOfSpanRangeEqTop — Mathlib

English

There is an isomorphism between a refined affine cover object and the pullback along the refinement morphisms.

Русский

Существует изоморфизм между объектом уточнённого аффинного покрытия и тягодравлением вдоль уточняющих морфизмов.

LaTeX

$$$$ \text{pullbackCoverAffineRefinementObjIso}(f, \mathcal{U}, i) $$$$

Lean4

/-- A family of elements spanning the unit ideal of `R` gives a affine open cover of `Spec R`. -/
@[simps]
noncomputable def affineOpenCoverOfSpanRangeEqTop {R : CommRingCat} {ι : Type*} (s : ι → R)
    (hs : Ideal.span (Set.range s) = ⊤) : (Spec R).AffineOpenCover
    where
  I₀ := ι
  X i := .of (Localization.Away (s i))
  f i := Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away (s i))))
  idx
    x :=
    by
    have : ∃ i, s i ∉ x.asIdeal := by by_contra! h; apply x.2.ne_top;
      rwa [← top_le_iff, ← hs, Ideal.span_le, Set.range_subset_iff]
    exact this.choose
  covers
    x := by
    generalize_proofs H
    let i := H.choose
    have := PrimeSpectrum.localization_away_comap_range (Localization.Away (s i)) (s i)
    exact (eq_iff_iff.mp congr(x ∈ $this)).mpr H.choose_spec

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