English
In a short exact sequence 0 → M → N → P → 0, Supp(N) = Supp(M) ∪ Supp(P).
Русский
В краткой точной последовательности 0 → M → N → P → 0 опора N равна объединению опор M и P.
LaTeX
$$Supp_R(N) = Supp_R(M) ∪ Supp_R(P)$$
Lean4
/-- Given an exact sequence `0 → M → N → P → 0` of `R`-modules, `Supp N = Supp M ∪ Supp P`. -/
@[stacks 00L3 "(4)"]
theorem support_of_exact (h : Function.Exact f g) (hf : Function.Injective f) (hg : Function.Surjective g) :
Module.support R N = Module.support R M ∪ Module.support R P :=
by
refine
subset_antisymm ?_
(Set.union_subset (Module.support_subset_of_injective f hf) (Module.support_subset_of_surjective g hg))
intro x
contrapose
simp only [Set.mem_union, not_or, and_imp, notMem_support_iff']
intro H₁ H₂ m
obtain ⟨r, hr, e₁⟩ := H₂ (g m)
rw [← map_smul, h] at e₁
obtain ⟨m', hm'⟩ := e₁
obtain ⟨s, hs, e₁⟩ := H₁ m'
exact ⟨_, x.asIdeal.primeCompl.mul_mem hs hr, by rw [mul_smul, ← hm', ← map_smul, e₁, map_zero]⟩
