iInf_ker_openCover_map_comp_apply

English

For a quasi-compact morphism f: X ⟶ Y and an open cover 𝒰 of X, the infimum of the kernels over the cover equals the kernel of f on a fixed affine open U.

Русский

Для квазикопактного морфизма f: X ⟶ Y и открытого покрытия 𝒰 L, на каждом аффинном $U$ инфимум ядер равен ядру f на U.

LaTeX

$$\\bigwedge_i ((\\mathcal{U}.f_i \\;≫\\; f).ker.ideal U) = f.ker.ideal U$$

Lean4

theorem iInf_ker_openCover_map_comp_apply (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) (U : Y.affineOpens) :
    ⨅ i, (𝒰.f i ≫ f).ker.ideal U = f.ker.ideal U :=
  by
  refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f U)
  intro s hs
  simp only [Hom.ker_apply, RingHom.mem_ker]
  apply X.IsSheaf.section_ext
  rintro x hxU
  obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
  simp only [homOfLE_leOfHom, map_zero, exists_and_left]
  refine ⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩, Set.image_preimage_subset (𝒰.f i).base (f ⁻¹ᵁ U), ?_⟩
  apply ((𝒰.f i).appIso _).commRingCatIsoToRingEquiv.injective
  rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom, Scheme.Hom.appIso_hom']
  simp only [homOfLE_leOfHom, Scheme.Hom.app_eq_appLE, ← RingHom.comp_apply, ← CommRingCat.hom_comp,
    Scheme.Hom.appLE_map, Scheme.appLE_comp_appLE]
  simpa [Scheme.Hom.appLE] using ideal_ker_le _ _ (Ideal.mem_iInf.mp hs i)

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