English
Under a linear equivalence l: M ≃ₗ[R] M', the associated primes are preserved.
Русский
При линейном эквиваленте l: M ≃ₗ[R] M' сохраняются ассоциированные простые.
LaTeX
$$$$\forall l:\, M \simeq M',\ \IsAssociatedPrime I M \iff \IsAssociatedPrime I M'. $$$$
Lean4
/-- If `0 → M → M' → M''` is an exact sequence, then the set of associated primes of `M'` is
contained in the union of those of `M` and `M''`. -/
@[stacks 02M3 "second part"]
theorem subset_union_of_exact (hf : Function.Injective f) (hfg : Function.Exact f g) :
associatedPrimes R M' ⊆ associatedPrimes R M ∪ associatedPrimes R M'' :=
by
rintro p ⟨_, x, hx⟩
by_cases h : ∃ a ∈ p.primeCompl, ∃ y : M, f y = a • x
· obtain ⟨a, ha, y, h⟩ := h
left
refine ⟨‹_›, y, le_antisymm (fun b hb ↦ ?_) (fun b hb ↦ ?_)⟩
· rw [hx] at hb
rw [LinearMap.mem_ker, LinearMap.toSpanSingleton_apply] at hb ⊢
apply_fun _ using hf
rw [map_smul, map_zero, h, smul_comm, hb, smul_zero]
· rw [LinearMap.mem_ker, LinearMap.toSpanSingleton_apply] at hb
apply_fun f at hb
rw [map_smul, map_zero, h, ← mul_smul, ← LinearMap.toSpanSingleton_apply, ← LinearMap.mem_ker, ← hx] at hb
contrapose! hb
exact p.primeCompl.mul_mem hb ha
· push_neg at h
right
refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b hb ↦ ?_)⟩
· rw [hx] at hb
rw [LinearMap.mem_ker, LinearMap.toSpanSingleton_apply] at hb ⊢
rw [← map_smul, hb, map_zero]
· rw [LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, ← map_smul, ← LinearMap.mem_ker,
hfg.linearMap_ker_eq] at hb
obtain ⟨y, hy⟩ := hb
by_contra! H
exact h b H y hy
