Theorems · Definition · algebraic geometry

AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    {x : ↥X} →
      (U : Y.Opens) →
        (hU : AlgebraicGeometry.IsAffineOpen U) →
          (V : X.Opens) →
            (hV : AlgebraicGeometry.IsAffineOpen V) →
              (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U) →
                (hx : x ∈ V) →
                  CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f x) ≅
                    CategoryTheory.Arrow.mk
                      (CommRingCat.ofHom
                        (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
                          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)) ⋯))

Given affine opens x ∈ V ⊆ f⁻¹(U), the stalk map of f at x is isomorphic to Localization.localRingHom of f.appLE U V.

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound