Theorems · Theorem · commutative algebra

Ideal.inertiaDeg_eq_of_isFractionRing

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [p.IsPrime] [q.IsPrime] (K : Type u_4) (L : Type u_5) [inst_6 : Field K]
  [inst_7 : Field L] [inst_8 : Algebra (R ⧸ p) K] [IsFractionRing (R ⧸ p) K] [inst_10 : Algebra (S ⧸ q) L]
  [IsFractionRing (S ⧸ q) L] [inst_12 : Algebra R K] [IsScalarTower R (R ⧸ p) K] [inst_14 : Algebra S L]
  [IsScalarTower S (S ⧸ q) L] [inst_16 : Algebra R L] [IsScalarTower R S L] [inst_18 : Algebra K L]
  [IsScalarTower R K L], q.inertiaDeg R = Module.finrank K L

Defined in

Mathlib.RingTheory.RamificationInertia.Inertia

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIdeal.LiesOverIdeal.IsPrimeIdeal.IsPrimeFieldFieldAlgebraIsFractionRingAlgebraIsFractionRingAlgebraIsScalarTowerAlgebraIsScalarTowerAlgebraIsScalarTowerAlgebraIsScalarTower