affineAnd_isLocal — Mathlib

English

Let Q be a property of ring homomorphisms that respects isomorphisms, is preserved under localization away from elements of the source, and is determined by localization spans. Then the morphism property affineAnd(Q) is local on the target: to check whether a morphism f: X → Y satisfies affineAnd(Q), it suffices to verify the corresponding condition on an affine open cover of Y.

Русский

Пусть Q является свойством гомоморфизмов колец, сохраняющим изоморфимизмы, сохраняемым локализацией вдоль элементов источника и задающимся локализациями. Тогда свойство морфизмов affineAnd(Q) локально по цели: проверить, что f: X → Y удовлетворяет affineAnd(Q), достаточно проверить соответствующее условие на аффинном покрытии Y.

LaTeX

$$$\\operatorname{IsLocal}(\\operatorname{affineAnd}(Q))$$$

Lean4

/-- `affineAnd P` is local if `P` is local on the (algebraic) source. -/
theorem affineAnd_isLocal (hPi : RingHom.RespectsIso Q) (hQl : RingHom.LocalizationAwayPreserves Q)
    (hQs : RingHom.OfLocalizationSpan Q) : (affineAnd Q).IsLocal
    where
  respectsIso := affineAnd_respectsIso hPi
  to_basicOpen {X Y _} f
    r := fun ⟨hX, hf⟩ ↦ by
    simp only at hf
    constructor
    · simp only [Scheme.preimage_basicOpen, Opens.map_top]
      exact (isAffineOpen_top X).basicOpen _
    · dsimp only
      rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso]
        -- Not sure why the `show` fixes the following `rw` complaining about "motive is incorrect"

      change Q (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)).hom
      rw [Scheme.Opens.ι_image_top]
      rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X), CommRingCat.hom_comp,
        hPi.cancel_right_isIso, ← Scheme.Hom.appTop]
      dsimp only [Opens.map_top]
      haveI := (isAffineOpen_top X).isLocalization_basicOpen (f.appTop r)
      apply hQl
      exact hf
  of_basicOpenCover {X Y _} f s hs
    hf := by
    dsimp [affineAnd] at hf
    haveI : IsAffine X := by
      apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
      · apply_fun Ideal.map (f.appTop).hom at hs
        rwa [Ideal.map_span, Ideal.map_top] at hs
      · rintro - ⟨r, hr, rfl⟩
        simp_rw [Scheme.preimage_basicOpen] at hf
        exact (hf ⟨r, hr⟩).left
    refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩
    refine
      ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance, inferInstance, inferInstance,
        inferInstance, inferInstance, ?_, ?_⟩
    · exact (isAffineOpen_top X).isLocalization_basicOpen (f.appTop a.val)
    · obtain ⟨_, hf⟩ := hf a
      rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf
      have hf : Q (Scheme.Hom.app f ((Y.basicOpen a.1).ι ''ᵁ ⊤)).hom := hf
      rw [Scheme.Opens.ι_image_top] at hf
      rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map _ (isAffineOpen_top X)] at hf
      rwa [CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf

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