sourceAffineLocally_isLocal — Mathlib

English

The local behavior of P on affine opens induces a local property on morphisms.

Русский

Локальное поведение P на аффинных открытых подмножеств порождает локальное свойство для морфизмов.

LaTeX

$$(sourceAffineLocally P).IsLocal$$

Lean4

theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso P) (h₂ : RingHom.LocalizationAwayPreserves P)
    (h₃ : RingHom.OfLocalizationSpan P) : (sourceAffineLocally P).IsLocal :=
  by
  constructor
  · exact sourceAffineLocally_respectsIso P h₁
  · intro X Y _ f r H
    rw [sourceAffineLocally_morphismRestrict]
    intro U hU
    have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U :=
      by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU
    rw [← f.appLE_congr (by simp [Scheme.Hom.appLE]) rfl this (fun f => P f.hom),
      IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]
    simp only [CommRingCat.hom_ofHom]
    apply (config := { allowSynthFailures := true }) h₂
    exact H U
  · introv hs hs' U
    apply h₃ _ _ hs
    intro r
    simp_rw [sourceAffineLocally_morphismRestrict] at hs'
    have :=
      hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩ (by simp [Scheme.Hom.appLE])
    rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom, ←
      h₁.isLocalization_away_iff] at this

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