fromOfGlobalSections_resLE — Mathlib

English

The restriction map on the open cover induced by fromOfGlobalSections matches the standard restriction map on the localized open subschemes, giving a compatible pullback of basic opens.

Русский

Ограничение по открытой подсборке, индуцированное fromOfGlobalSections, согласуется со стандартным ограничением локализованных открытых подсхем и тяготеет к совместному вытягиванию базовых открытых.

LaTeX

$$$\mathrm{resLE} = \mathrm{toBasicOpenOfGlobalSections}$ on the compatible opens.$$

Lean4

theorem fromOfGlobalSections_resLE {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) :
    (fromOfGlobalSections 𝒜 f hf).resLE _ _ (fromOfGlobalSections_preimage_basicOpen _ _ _ hn hr).ge =
      toBasicOpenOfGlobalSections 𝒜 f rfl hn hr :=
  by
  rw [← (Iso.inv_comp_eq _).mpr (fromOfGlobalSections_morphismRestrict 𝒜 f hf hn hr), ←
    Scheme.Hom.resLE_eq_morphismRestrict]
  simp [Scheme.isoOfEq_inv]

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