English
If p is maximal and P is prime with nonzero ramification, then the finite dimension of R/p over S/(P^e) equals the ramification index times the inertia degree, in the appropriate quotient setup.
Русский
Если p максимален и P прост, причём рамфикационный индекс ненулевой, то размерности по модулю конечна и равна произведению рамфикационного индекса и инерцийной степени в соответствующем окружении)
LaTeX
$$$\\\\operatorname{finrank} (R \\\\backslash p) (S \\\\backslash (P^e)) = e \\\\cdot \\\\operatorname{finrank} (R \\\\backslash p) (S \\\\backslash P)$$$
Lean4
/-- If `p` is a maximal ideal of `R`, `S` extends `R` and `P^e` lies over `p`,
then the dimension `[S/(P^e) : R/p]`, as a natural number, is equal to `e * [S/P : R/p]`. -/
theorem finrank_prime_pow_ramificationIdx [IsDedekindDomain S] (hP0 : P ≠ ⊥) [p.IsMaximal] [P.IsPrime] (he : e ≠ 0) :
finrank (R ⧸ p) (S ⧸ P ^ e) =
e *
@finrank (R ⧸ p) (S ⧸ P) _ _
(@Algebra.toModule _ _ _ _ <| @Quotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩) :=
by
letI : NeZero e := ⟨he⟩
letI : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
have hdim := rank_prime_pow_ramificationIdx _ _ hP0 he
by_cases hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
· haveI := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP
apply @Nat.cast_injective Cardinal
rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]
have hPe := mt (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mp hP
simp only [finrank_of_infinite_dimensional hP, finrank_of_infinite_dimensional hPe, mul_zero]
