Theorems · Definition · algebraic geometry

AlgebraicGeometry.StructureSheaf.Localizations

{R : Type u} →
  (M : Type u) →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [Module R M] → ↑(AlgebraicGeometry.PrimeSpectrum.Top R) → Type u

The type family over PrimeSpectrum R consisting of the localization over each point.

Defined in

Mathlib.AlgebraicGeometry.StructureSheaf

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule