localizationPresheaf — Mathlib

English

There is an isomorphism between the principalOpen presheaf and the right Kan extension along principals.

Русский

Существует изоморфизм между пресешефом principalOpen и правым кан-расширением вдоль princip als.

LaTeX

$$$\\operatorname{principalOpen} \\cong \\mathrm{principalsKanExtension}(F)$$$

Lean4

/-- The localization of a presheaf of `CommRing`s with respect to a `SubmonoidPresheaf`. -/
protected noncomputable def localizationPresheaf : X.Presheaf CommRingCat
    where
  obj U := CommRingCat.of <| Localization (G.obj U)
  map {_ _} i := CommRingCat.ofHom <| IsLocalization.map _ (F.map i).hom (G.map i)
  map_id
    U := by
    simp_rw [F.map_id]
    ext x
    exact IsLocalization.map_id x
  map_comp {U V W} i
    j := by
    delta CommRingCat.ofHom CommRingCat.of Bundled.of
    simp_rw [F.map_comp]
    ext : 1
    dsimp
    rw [IsLocalization.map_comp_map]

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