English
If I is nonzero and J is irreducible, then the supremum of J^n and I equals J^n for every n, determined by the multiplicity of J in I.
Русский
Если I не нулевой и J неразложим, то верхняя грань между J^n и I равна J^n для каждого n, определяемая по кратности J в I.
LaTeX
$$J^n ⊔ I = J^n$$
Lean4
theorem _root_.FractionalIdeal.sup_mul_inf (I J : FractionalIdeal A⁰ K) : (I ⊓ J) * (I ⊔ J) = I * J :=
by
apply
mul_left_injective₀ (b := spanSingleton A⁰ (algebraMap A K (I.den.1 * I.den.1 * J.den.1 * J.den.1)))
(by simp [spanSingleton_eq_zero_iff])
have := Ideal.sup_mul_inf (Ideal.span { J.den.1 } * I.num) (Ideal.span { I.den.1 } * J.num)
simp only [← coeIdeal_inj (K := K), coeIdeal_mul, coeIdeal_sup, coeIdeal_inf, ← den_mul_self_eq_num',
coeIdeal_span_singleton] at this
rw [mul_left_comm, ← mul_add, ← mul_add, ← mul_inf₀ (FractionalIdeal.zero_le _), ←
mul_inf₀ (FractionalIdeal.zero_le _)] at this
simp only [FractionalIdeal.sup_eq_add, _root_.map_mul, ← spanSingleton_mul_spanSingleton]
convert this using 1 <;> ring
