English
If a is in the normalized factors of b (in a normalization monoid), then the span of a is in the normalized factors of the span of b.
Русский
Если a принадлежит нормализованным факторорам b, тогда идеал span{a} принадлежит нормализованным факторорам span{b}.
LaTeX
$$span{a} ∈ normalizedFactors(span{b}) given a ∈ normalizedFactors(b)$$
Lean4
theorem singleton_span_mem_normalizedFactors_of_mem_normalizedFactors [NormalizationMonoid R] {a b : R}
(ha : a ∈ normalizedFactors b) : Ideal.span ({ a } : Set R) ∈ normalizedFactors (Ideal.span ({ b } : Set R)) :=
by
by_cases hb : b = 0
· rw [Ideal.span_singleton_eq_bot.mpr hb, bot_eq_zero, normalizedFactors_zero]
rw [hb, normalizedFactors_zero] at ha
exact absurd ha (Multiset.notMem_zero a)
· suffices Prime (Ideal.span ({ a } : Set R))
by
obtain ⟨c, hc, hc'⟩ :=
exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
(dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
rwa [associated_iff_eq.mp hc']
· by_contra h
exact hb (span_singleton_eq_bot.mp h)
rw [prime_iff_isPrime]
· exact (span_singleton_prime (prime_of_normalized_factor a ha).ne_zero).mpr (prime_of_normalized_factor a ha)
· by_contra h
exact (prime_of_normalized_factor a ha).ne_zero (span_singleton_eq_bot.mp h)
