linear_iff — Mathlib

English

A functor F: C → D is linear over R if it respects scalar multiplication of morphisms: F.map(r·f) = r·F.map(f) for all r ∈ R.

Русский

Функтор F: C → D линейный по отношению к R, если сохраняет масштабирование морфизмов: F.map(r·f) = r·F.map(f).

LaTeX

$$$\\text{linear_iff}(F) : \\mathrm{Functor.Linear}\\;R\\;F \\iff \\forall X\\, r\\in R,\\ F.map(r\\cdot 1_X) = r\\cdot 1_{F X}$$$

Lean4

theorem linear_iff (F : C ⥤ D) : Functor.Linear R F ↔ ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X) :=
  by
  constructor
  · intro h X r
    rw [h.map_smul, F.map_id]
  · refine fun h => ⟨fun {X Y} f r => ?_⟩
    have : r • f = (r • 𝟙 X) ≫ f := by simp
    rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]

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