Theorems · Theorem · number theory

Ideal.rank_pow_quot_aux

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) (P : Ideal S)
  [hfp : NeZero (p.ramificationIdx' P)] [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime],
  P ≠ ⊥ →
    ∀ {i : ℕ},
      i < p.ramificationIdx' P →
        Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ i)) =
          Module.rank (R ⧸ p) (S ⧸ P) +
            Module.rank (R ⧸ p) ↥(Ideal.map (Ideal.Quotient.mk (P ^ p.ramificationIdx' P)) (P ^ (i + 1)))

Since the inclusion (P^(i + 1) / P^e) ⊂ (P^i / P^e) has a kernel isomorphic to P / S, [P^i / P^e : R / p] = [P^(i+1) / P^e : R / p] + [P / S : R / p]

Defined in

Mathlib.NumberTheory.RamificationInertia.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraNeZeroIsDedekindDomainIdeal.IsMaximalIdeal.IsPrime