differentialIdeal_le_fractionalIdeal_iff

English

Relates coeSubmodule to the trace dual in the presence of integral closure and Dedekind-domain hypotheses.

Русский

Связь между coeSubmodule и trace-dual при целостном замыкании и условиях Дедекинд-доменов.

LaTeX

$$coeSubmodule( FractionRing B ) (differentIdeal A B ) = 1 / Submodule.traceDual A (FractionRing A) 1$$

Lean4

theorem differentialIdeal_le_fractionalIdeal_iff {I : FractionalIdeal B⁰ L} (hI : I ≠ 0) :
    differentIdeal A B ≤ I ↔
      (((I⁻¹ :) : Submodule B L).restrictScalars A).map ((Algebra.trace K L).restrictScalars A) ≤ 1 :=
  by
  rw [coeIdeal_differentIdeal A K L B, FractionalIdeal.inv_le_comm (by simp) hI, ← FractionalIdeal.coe_le_coe,
    FractionalIdeal.coe_dual_one]
  refine le_traceDual_iff_map_le_one.trans ?_
  simp

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