Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.const

{R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        M →
          (g : R) →
            (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
              U ≤ PrimeSpectrum.basicOpen g → (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)

The section of structureSheaf R on an open U sending each x ∈ U to the element f/g in the localization of R at x.

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

20 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule