English
A variant relation expressing the image of differentIdeal under coeSubmodule with Integrality and Separable assumptions.
Русский
Вариант соотношения образа differentIdeal через coeSubmodule при предположениях о целостности и сепарабельности.
LaTeX
$$coeSubmodule(FractionRing B)(differentIdeal A B) = ...$$
Lean4
theorem coeSubmodule_differentIdeal_fractionRing [Algebra.IsIntegral A B]
[Algebra.IsSeparable (FractionRing A) (FractionRing B)] [FiniteDimensional (FractionRing A) (FractionRing B)] :
coeSubmodule (FractionRing B) (differentIdeal A B) = 1 / Submodule.traceDual A (FractionRing A) 1 :=
by
have : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
rw [coeSubmodule, differentIdeal, Submodule.map_comap_eq, inf_eq_right]
have := FractionalIdeal.dual_inv_le (A := A) (K := FractionRing A) (1 : FractionalIdeal B⁰ (FractionRing B))
have : _ ≤ ((1 : FractionalIdeal B⁰ (FractionRing B)) : Submodule B (FractionRing B)) := this
simp only [← one_div, FractionalIdeal.val_eq_coe] at this
rw [FractionalIdeal.coe_div (FractionalIdeal.dual_ne_zero _ _ _), FractionalIdeal.coe_dual] at this
· simpa only [FractionalIdeal.coe_one, Submodule.one_eq_range] using this
· exact one_ne_zero
· exact one_ne_zero
