Theorems · Theorem · algebraic geometry

AlgebraicGeometry.StructureSheaf.exists_const

∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (s : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)),
  ∀ x ∈ U,
    ∃ g,
      ∃ (_ : x ∈ PrimeSpectrum.basicOpen g) (i : PrimeSpectrum.basicOpen g ≤ U),
        ∃ f,
          AlgebraicGeometry.StructureSheaf.const f g (PrimeSpectrum.basicOpen g) ⋯ =
            (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.structureSheafInType R M).obj.map i.hom.op)) s

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule