English
The join of two ideals I ⊔ J equals the product of the common normalized factors: (normalizedFactors I ∩ normalizedFactors J).prod.
Русский
Объединение двух идеалов равно произведению общих нормализованных факторов.
LaTeX
$$I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod$$
Lean4
theorem sup_eq_prod_inf_factors [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod :=
by
have H :
normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod = normalizedFactors I ∩ normalizedFactors J :=
by
apply normalizedFactors_prod_of_prime
intro p hp
rw [mem_inter] at hp
exact prime_of_normalized_factor p hp.left
have :=
Multiset.prod_ne_zero_of_prime (normalizedFactors I ∩ normalizedFactors J) fun _ h =>
prime_of_normalized_factor _ (Multiset.mem_inter.1 h).1
apply le_antisymm
· rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
constructor
· rw [dvd_iff_normalizedFactors_le_normalizedFactors this hI, H]
exact inf_le_left
· rw [dvd_iff_normalizedFactors_le_normalizedFactors this hJ, H]
exact inf_le_right
· rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors, normalizedFactors_prod_of_prime, le_iff_count]
· intro a
rw [Multiset.count_inter]
exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)
· intro p hp
rw [mem_inter] at hp
exact prime_of_normalized_factor p hp.left
· exact ne_bot_of_le_ne_bot hI le_sup_left
· exact this
