primesOverSpanEquivMonicFactorsMod_symm_apply

English

The inverse bijection sends a class represented by a polynomial Q modulo p back to the corresponding ideal in 𝓞_K generated by p and the evaluation of Q at θ.

Русский

Обратная биекция отображает класс, представляемый Q по модулю p, в соответствующий идеал в 𝓞_K, порожденный p и значением Q(θ).

LaTeX

$$$((\text{primesOverSpanEquivMonicFactorsMod hp}).symm \langle Q, hQ \rangle : \mathcal{O}_K) = \langle p, Q(\theta) \rangle$$$

Lean4

theorem primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬p ∣ exponent θ) {Q : (ZMod p)[X]}
    (hQ : Q ∈ monicFactorsMod θ p) :
    ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩ : Ideal (𝓞 K)) =
      (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk inferInstance (by simp [NeZero.ne p])
            (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral).symm
        ⟨Q.map (Int.quotientSpanNatEquivZMod p).symm,
          by
          rw [← primesOverSpanEquivMonicFactorsModAux_symm_apply]
          exact ((primesOverSpanEquivMonicFactorsModAux _).symm ⟨Q, hQ⟩).coe_prop⟩ :=
  rfl

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