SpecMapRestrictBasicOpenIso — Mathlib

English

The restriction of a Spec.map along a basic open is canonically isomorphic to the Spec.map of the localization away from that basic open.

Русский

Ограничение отображения Spec.map вдоль базового открытого пространства канонически изоморфно к отображению Spec.map локализации вне этого базового открытого.

LaTeX

$$$Arrow.mk( Spec.map f \mid_ (PrimeSpectrum.basicOpen r) ) \cong Arrow.mk( Spec.map (Localization.awayMap f.hom r) )$$$

Lean4

/-- The restriction of `Spec.map f` to a basic open `D(r)` is isomorphic to `Spec.map` of the
localization of `f` away from `r`. -/
noncomputable def SpecMapRestrictBasicOpenIso {R S : CommRingCat} (f : R ⟶ S) (r : R) :
    Arrow.mk (Spec.map f ∣_ (PrimeSpectrum.basicOpen r)) ≅
      Arrow.mk (Spec.map <| CommRingCat.ofHom (Localization.awayMap f.hom r)) :=
  by
  letI e₁ : Localization.Away r ≃ₐ[R] Γ(Spec R, basicOpen r) := IsLocalization.algEquiv (Submonoid.powers r) _ _
  letI e₂ : Localization.Away (f.hom r) ≃ₐ[S] Γ(Spec S, basicOpen (f.hom r)) :=
    IsLocalization.algEquiv (Submonoid.powers (f.hom r)) _ _
  refine Arrow.isoMk ?_ ?_ ?_
  ·
    exact
      (Spec _).isoOfEq (comap_basicOpen _ _) ≪≫
        (IsAffineOpen.Spec_basicOpen (f.hom r)).isoSpec ≪≫ Scheme.Spec.mapIso e₂.toCommRingCatIso.op
  · exact (IsAffineOpen.Spec_basicOpen r).isoSpec ≪≫ Scheme.Spec.mapIso e₁.toCommRingCatIso.op
  · have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization (S := (Localization.Away r)) r
    rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away r))))]
    simp only [Arrow.mk_left, Arrow.mk_right, Functor.id_obj, Scheme.isoOfEq_rfl, Iso.refl_trans, Iso.trans_hom,
      Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map, Quiver.Hom.unop_op, Arrow.mk_hom, Category.assoc,
      ← Spec.map_comp]
    conv =>
      congr
      · enter [2, 1];
        tactic =>
          change _ = (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (homOfLE le_top).op)
          ext
          simp only [Localization.awayMap, IsLocalization.Away.map, AlgEquiv.toRingEquiv_eq_coe,
            RingEquiv.toCommRingCatIso_hom, AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
            RingHom.comp_apply, IsLocalization.map_eq, RingHom.coe_coe, AlgEquiv.commutes,
            IsAffineOpen.algebraMap_Spec_obj]
      · enter [2, 2, 1];
        tactic =>
          change _ = (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op
          ext
          simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toCommRingCatIso_hom, AlgEquiv.toRingEquiv_toRingHom,
            CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
            AlgEquiv.commutes, IsAffineOpen.algebraMap_Spec_obj, homOfLE_leOfHom]
    simp only [IsAffineOpen.isoSpec_hom, homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_map_assoc, Scheme.Opens.toSpecΓ_top, Scheme.homOfLE_ι_assoc,
      morphismRestrict_ι_assoc]
    simp only [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Category.assoc, Iso.inv_hom_id, Category.comp_id,
      Category.id_comp]
    rfl

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