Theorems · Theorem · commutative algebra

Ideal.sum_ramification_inertia_eq_finrank

∀ {R : Type u_1} [inst : CommRing R] (p : Ideal R) [p.IsPrime] (S : Type u_2) [inst_2 : CommRing S]
  [inst_3 : Algebra R S] [IsDomain R] [Module.Finite R S] [Module.Flat R S] [inst_7 : Fintype ↑(p.primesOver S)],
  ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Module.finrank R S

Let R be an integral domain, let S be a finite flat R-algebra, and let p be a prime ideal of R. Then the sum over all prime ideals q of S lying over p of the ramification index of q times the inertia degree of q equals the rank of S as an R-module.

Defined in

Mathlib.RingTheory.RamificationInertia.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIdeal.IsPrimeCommRingAlgebraIsDomainModule.FiniteModule.FlatFintype