Theorems · Definition · algebraic geometry

Ideal.Fiber

{R : Type u_1} →
  [inst : CommRing R] →
    (p : Ideal R) → [p.IsPrime] → (S : Type u_3) → [inst_2 : AddCommGroup S] → [Module R S] → Type (max u_3 u_1)

The fiber of a prime p of R in an R-algebra S, defined to be κ(p) ⊗ S. See PrimeSpectrum.preimageHomeomorphFiber for the homeomorphism between the spectrum of it and the actual set-theoretic fiber of PrimeSpectrum S → PrimeSpectrum R at p.

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Cited by

40 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsPrimeAddCommGroupModule