rank_prime_pow_ramificationIdx — Mathlib

English

If p is maximal, P is prime, and e is the ramification exponent, then the rank of S/(P^e) over R/p equals e times the rank of S/P over R/p.

Русский

Если p максимален, P прост и e — рамфикационный показатель, то ранг $S/(P^e)$ над $R/p$ равен e умноженному на ранг $S/P$ над $R/p$.

LaTeX

$$$\\\\operatorname{Module.rank} (R \\\\backslash p) (S \\\\backslash (P^e)) = e \\\\cdot \\\\operatorname{Module.rank} (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]` is equal to `e * [S/P : R/p]`. -/
theorem rank_prime_pow_ramificationIdx [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥) (he : e ≠ 0) :
    Module.rank (R ⧸ p) (S ⧸ P ^ e) =
      e •
        @Module.rank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <| @Quotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩) :=
  by
  letI : NeZero e := ⟨he⟩
  have := rank_pow_quot p P hP0 0 (Nat.zero_le e)
  rw [pow_zero, Nat.sub_zero, Ideal.one_eq_top, Ideal.map_top] at this
  exact (rank_top (R ⧸ p) _).symm.trans this

Похожие утверждения