instMonoCommRingCatToTotalQuotientPresheafPresheaf

English

In the TopCat presheaf of rings, the total quotient presheaf map is mono (injective on sections).

Русский

В прешефе TopCat для колец отображение к общей факторной преше сохраняет монотонность (инъективность секций).

LaTeX

$$$F^{\mathrm{presheaf}}\to \text{TotalQuotientPresheaf}$ is mono$$

Lean4

instance (F : X.Sheaf CommRingCat.{w}) : Mono F.presheaf.toTotalQuotientPresheaf :=
  by
  apply (config := { allowSynthFailures := true }) NatTrans.mono_of_mono_app
  intro U
  apply ConcreteCategory.mono_of_injective
  dsimp [toTotalQuotientPresheaf]
    -- Porting note: `M` and `S` need to be specified manually, so used a hack to save some typing

  set m := _
  change Function.Injective (algebraMap _ (Localization m))
  refine IsLocalization.injective (M := m) (S := Localization m) ?_
  rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
  intro s hs t e
  apply section_ext F (unop U)
  intro x hx
  rw [RingHom.map_zero]
  apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2
  rw [← map_mul, e, map_zero]

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