Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.comap

{R : Type u} →
  [inst : CommRing R] →
    {S : Type u} →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
            (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
              V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier →
                ↑((AlgebraicGeometry.Spec.structureSheaf R).obj.obj (Opposite.op U)) →+*
                  ↑((AlgebraicGeometry.Spec.structureSheaf S).obj.obj (Opposite.op V))

For a ring homomorphism f : R →+* S and open sets U and V of the prime spectra of R and S such that V ⊆ (comap f) ⁻¹ U, the induced ring homomorphism from the structure sheaf of R at U to the structure sheaf of S at V. Explicitly, this map is given as follows: For a point p : V, if the section s evaluates on p to the fraction a / b, its image on V evaluates on p to the fraction f(a) / f(b).

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingCommRing