English
The union over i of the supports of the kernels of the composed maps equals the support of ker f.
Русский
Объединение по i поддержек ядер композиции равно поддержке ядра f.
LaTeX
$$\\bigcup_i ((\\mathcal{U}.f_i ≫ f).ker.\\mathrm{support}) = f.ker.\\mathrm{support}$$
Lean4
theorem iUnion_support_ker_openCover_map_comp (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) [Finite 𝒰.I₀] :
⋃ i, ((𝒰.f i ≫ f).ker.support : Set Y) = f.ker.support :=
by
cases isEmpty_or_nonempty 𝒰.I₀
· have : IsEmpty X := Function.isEmpty 𝒰.idx
simp [ker_eq_top_of_isEmpty]
suffices ∀ U : Y.affineOpens, (⋃ i, (𝒰.f i ≫ f).ker.support) ∩ U = (f.ker.support ∩ U : Set Y)
by
ext x
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))
intro U
simp only [Set.iUnion_inter, coe_support_inter, ← f.iInf_ker_openCover_map_comp_apply 𝒰,
Scheme.zeroLocus_iInf_of_nonempty]
