Theorems · Definition · commutative algebra

Ideal.ramificationIdx

{S : Type u_1} → [inst : CommRing S] → Ideal S → (R : Type u_2) → [inst_1 : CommRing R] → [Algebra R S] → ℕ

Let S/R be an extension of rings, and let q be a prime ideal of S lying over a prime ideal p of R. Let Sq be the localization of S and q, and let pSq be the image of p in Sq. Then the ramification index of q over R is defined to be the length of the quotient Sq/pSq as an Sq-module. When q is not prime, we use a junk value of 0. This will eventually replace the existing definition of Ideal.ramificationIdx'.

Defined in

Mathlib.RingTheory.RamificationInertia.Ramification

Cited by

59 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra