English
The ideal computed via the inverse bijection is the span of p and Q(θ).
Русский
Идеал, полученный через обратную биекцию, равен порождению p и Q(θ).
LaTeX
$$$((\text{primesOverSpanEquivMonicFactorsMod hp}).symm \langle Q.map (Int.castRingHom (ZMod p)), hQ \rangle : \mathcal{O}_K) = \operatorname{span}\{p, Q(\theta)\}$$$
Lean4
/-- The residual degree of the ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is equal to the degree of `Q mod p`.
-/
theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬p ∣ exponent θ) {Q : ℤ[X]}
(hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
inertiaDeg (span {(p : ℤ)})
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞 K)) =
natDegree (Q.map (Int.castRingHom (ZMod p))) :=
by
-- This is needed for `inertiaDeg_algebraMap` below to work
have := liesOver_primesOverSpanEquivMonicFactorsMod_symm hp hQ
rw [primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, inertiaDeg_algebraMap, ←
finrank_quotient_span_eq_natDegree]
refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)
exact (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm
