functor_linear — Mathlib

English

For L: C → D a localization functor with W, and assuming C and D are suitably R-linear, the induced functor L is R-linear: L maps r · f to r · L(f) for all scalars r ∈ R and morphisms f.

Русский

Для локализационного функторы L: C → D при условии линейности C и D, индукцируемый функтор L является R-линейным: L(r · f) = r · L(f) для любых скаляров r ∈ R и морфизмов f.

LaTeX

$$$L(r\cdot f) = r\cdot L(f)$$$

Lean4

theorem functor_linear :
    letI := linear R L W
    Functor.Linear R L :=
  by
  letI := linear R L W
  constructor
  intro X Y f r
  change L.map (r • f) = ((Linear.toCatCenter R C r).localization L W).app (L.obj X) ≫ L.map f
  simp only [CatCenter.localization_app, ← L.map_comp, Functor.id_obj, Linear.toCatCenter_apply_app, Linear.smul_comp,
    Category.id_comp]

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