toSpec_base_apply_eq — Mathlib

English

In the same graded setting, the base map of the Spec after restriction to the top component D(f) coincides with the Spec map associated to the top component ProjIsoSpecTopComponent; explicitly, the base morphism matches the isomorphism-induced Spec map on the corresponding top component.

Русский

В той же конфигурации градации базовое отображение Spec после ограничения к верхним компонентам D(f) совпадает с отображением Spec, полученным от изоморфизма верхней компоненты ProjIsoSpecTopComponent; явным образом основание отображения совпадает с отображением Spec, индуцированным изоморфизмом над соответствующей верхней компонентой.

LaTeX

$$$(toSpec\;\mathcal{A}f).base\;x = \text{ProjIsoSpecTopComponent.toSpec}\;\mathcal{A}f\;x$$$

Lean4

theorem toSpec_base_apply_eq {f} (x : Proj| pbo f) : (toSpec 𝒜 f).base x = ProjIsoSpecTopComponent.toSpec 𝒜 f x :=
  toSpec_base_apply_eq_comap 𝒜 x |>.trans <|
    PrimeSpectrum.ext <|
      Ideal.ext fun z =>
        show ¬IsUnit _ ↔ z ∈ ProjIsoSpecTopComponent.ToSpec.carrier _
          by
          obtain ⟨z, rfl⟩ := z.mk_surjective
          rw [← HomogeneousLocalization.isUnit_iff_isUnit_val, ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier,
            HomogeneousLocalization.map_mk, HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
            IsLocalization.AtPrime.isUnit_mk'_iff]
          exact not_not

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