Theorems · Theorem · number theory

Ideal.finrank_quotient_map

Deprecated since 2026-07-01Mathlib marks this declaration as deprecated.

∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (K : Type u_1) [inst_3 : Field K] [inst_4 : Algebra R K] (L : Type u_2) [inst_5 : Field L] [inst_6 : Algebra S L]
  [IsFractionRing S L] [hRK : IsFractionRing R K] [IsDomain S] [IsDedekindDomain R] [inst_10 : Algebra K L]
  [inst_11 : Algebra R L] [IsScalarTower R K L] [IsScalarTower R S L] [hp : p.IsMaximal] [Module.Finite R S],
  Module.finrank (R ⧸ p) (S ⧸ Ideal.map (algebraMap R S) p) = Module.finrank K L

If p is a maximal ideal of R, and S is the integral closure of R in L, then the dimension [S/pS : R/p] is equal to [Frac(S) : Frac(R)].

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFieldAlgebraFieldAlgebraIsFractionRingIsFractionRingIsDomainIsDedekindDomainAlgebraAlgebraIsScalarTowerIsScalarTowerIdeal.IsMaximalModule.Finite