English
Under meromorphic-in-normal-form assumptions with nowhere-zero divisor, the zero set equals the divisor support.
Русский
При предположениях мероморфности в нормальной форме и нигде не нуль-деленное, множество нулей совпадает с поддержкой дивизора.
LaTeX
$$$MeromorphicNFOn\ f\ U \land \text{nowhere locally constant zero} \Rightarrow U \cap f^{-1}\{0\} = \operatorname{Supp}(MeromorphicOn.divisor\ f\ U)$$$
Lean4
/-- If `f` is meromorphic in normal form on `U` and nowhere locally constant zero,
then its zero set equals the support of the associated divisor.
-/
theorem zero_set_eq_divisor_support (h₁f : MeromorphicNFOn f U) (h₂f : ∀ u : U, meromorphicOrderAt f u ≠ ⊤) :
U ∩ f ⁻¹' {0} = Function.support (MeromorphicOn.divisor f U) :=
by
ext u
constructor <;> intro hu
·
simp_all only [ne_eq, Subtype.forall, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff,
Function.mem_support, h₁f.meromorphicOn, MeromorphicOn.divisor_apply, WithTop.untop₀_eq_zero,
(h₁f hu.1).meromorphicOrderAt_eq_zero_iff, not_true_eq_false, or_self, not_false_eq_true]
· simp only [Function.mem_support, ne_eq] at hu
constructor
· exact (MeromorphicOn.divisor f U).supportWithinDomain hu
· rw [Set.mem_preimage, Set.mem_singleton_iff]
have := h₁f ((MeromorphicOn.divisor f U).supportWithinDomain hu) |>.meromorphicOrderAt_eq_zero_iff.not
simp only [h₁f.meromorphicOn, (MeromorphicOn.divisor f U).supportWithinDomain hu, MeromorphicOn.divisor_apply,
WithTop.untop₀_eq_zero, not_or] at hu
simp_all [hu.1]
