isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime

English

Let h be a hypothesis: if for all ⦃I⦄ with I prime and absNorm(I) ≤ M(K) one has Submodule.IsPrincipal(I), then 𝓞_K is a PID.

Русский

Пусть дано условие: если для каждого простого идеала I над 𝓞_K с absNorm(I) ≤ M(K) выполняется Submodule.IsPrincipal(I), то 𝓞_K является ПИД.

LaTeX

$$$\left( \forall \{I:(Ideal(\mathcal{O}_K))^{\circ}\}, I(\.val).IsPrime \Rightarrow \mathrm{absNorm}(I) \le M(K) \Rightarrow \mathrm{Submodule.IsPrincipal}(I) \right) \Rightarrow \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$

Lean4

theorem isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime
    (h :
      ∀ ⦃I : (Ideal (𝓞 K))⁰⦄,
        (I : Ideal (𝓞 K)).IsPrime → absNorm (I : Ideal (𝓞 K)) ≤ M K → Submodule.IsPrincipal (I : Ideal (𝓞 K))) :
    IsPrincipalIdealRing (𝓞 K) :=
  by
  refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)
  rw [← mem_isPrincipalSubmonoid_iff, ← prod_normalizedFactors_eq_self (nonZeroDivisors.coe_ne_zero I)]
  refine Submonoid.multiset_prod_mem _ _ (fun J hJ ↦ mem_isPrincipalSubmonoid_iff.mp ?_)
  by_cases hJ0 : J = 0
  · simpa [hJ0] using bot_isPrincipal
  rw [← Subtype.coe_mk J (mem_nonZeroDivisors_of_ne_zero hJ0)]
  refine h (((mem_normalizedFactors_iff (nonZeroDivisors.coe_ne_zero I)).mp hJ).1) ?_
  exact
    (cast_le.mpr <|
          le_of_dvd (absNorm_pos_of_nonZeroDivisors I) <|
            absNorm_dvd_absNorm_of_le <| le_of_dvd <| UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hJ).trans
      hI

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