localizationRingHom — Mathlib

English

There is a ring hom CatCenter C → CatCenter D given by r ↦ r.localization L W, preserving 0, 1, +, and ×.

Русский

Существует однозначное кольцевое отображение CatCenter C → CatCenter D, задаваемое r ↦ r.localization L W, сохраняющее 0, 1, сложение и умножение.

LaTeX

$$$\text{localizationRingHom}(L,W): CatCenter C \to CatCenter D$, with toFun(r) = r.localization L W, and preserves 0, 1, +, \cdot$$$

Lean4

/-- The morphism of rings `CatCenter C →+* CatCenter D` when `L : C ⥤ D`
is an additive localization functor between preadditive categories. -/
noncomputable def localizationRingHom : CatCenter C →+* CatCenter D
    where
  toFun r := r.localization L W
  map_zero' := localization_zero L W
  map_one' := localization_one L W
  map_add' _ _ := localization_add _ _ _ _
  map_mul' _ _ := localization_mul _ _ _ _

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