differentIdeal_ne_bot — Mathlib

English

Equality of coeIdeal with a specific dual-inverse construction under integral/separable hypotheses.

Русский

Равенство coeIdeal и конкретной конструкции двойственности-инверсии при условиях целостности и сепарабельности.

LaTeX

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

Lean4

theorem differentIdeal_ne_bot [Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] :
    differentIdeal A B ≠ ⊥ := by
  let K := FractionRing A
  let L := FractionRing B
  have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L := IsIntegralClosure.isLocalization _ K _ _
  have : FiniteDimensional K L := .of_isLocalization A B A⁰
  rw [ne_eq, ← FractionalIdeal.coeIdeal_inj (K := L), coeIdeal_differentIdeal (K := K)]
  simp

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