Theorems · Definition · commutative algebra

Ideal.inertiaDeg

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

Given a prime ideal q of an R-algebra S, the inertia degree of q over R is defined to be the degree of the residue field of q over the residue field of its preimage p in R. When q is not prime, we use a junk value of 0. This will eventually replace the existing definition of Ideal.inertiaDeg'.

Defined in

Mathlib.RingTheory.RamificationInertia.Inertia

Cited by

60 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra