opensRange_subschemeCover_map — Mathlib

English

For an affine open U, the opensRange of I.subschemeCover.f U equals the preimage of U under I.subschemeι.base.

Русский

Для аффинного открытого множества U открытые области образа I.subschemeCover.f U равны предобразу U по I.subschemeι.base.

LaTeX

$$$(I.subschemeCover.f U).opensRange = I.subschemeι^{-1}^\! U$$$

Lean4

@[simp]
theorem opensRange_subschemeCover_map (U : X.affineOpens) : (I.subschemeCover.f U).opensRange = I.subschemeι ⁻¹ᵁ U :=
  I.opensRange_glueData_ι_subschemeIso_inv U

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