differentialIdeal_le_iff — Mathlib

English

Under suitable hypotheses, the coeIdeal of the different ideal equals a dual-inverse construction.

Русский

При подходящих гипотезах коэффициентное отображение различного идеала совпадает с конструкцией двойственности-обратного.

LaTeX

$$coeIdeal(differentIdeal(A,B)) = (dual(A,K,1))^{-1}$$

Lean4

theorem differentialIdeal_le_iff {I : Ideal B} (hI : I ≠ ⊥) :
    differentIdeal A B ≤ I ↔
      (((I⁻¹ : FractionalIdeal B⁰ L) : Submodule B L).restrictScalars A).map ((Algebra.trace K L).restrictScalars A) ≤
        1 :=
  (FractionalIdeal.coeIdeal_le_coeIdeal _).symm.trans
    (differentialIdeal_le_fractionalIdeal_iff (I := (I : FractionalIdeal B⁰ L)) (by simpa))

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