range_subset_ker_support — Mathlib

English

For any morphism f: X ⟶ Y, the range of the base map is contained in the kernel support.

Русский

Для любого морфизма f: X ⟶ Y образ базовой карты содержится в поддержке ядра.

LaTeX

$$range(f.base) \\subseteq f.ker.support$$

Lean4

theorem range_subset_ker_support (f : X.Hom Y) : Set.range f.base ⊆ f.ker.support :=
  by
  rintro _ ⟨x, rfl⟩
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ
  refine ((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1
  simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
  intro s hs hxs
  have : x ∈ f ⁻¹ᵁ Y.basicOpen s := hxs
  rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs), Scheme.basicOpen_zero] at this

Похожие утверждения