lift_linear — Mathlib

English

Let R be a commutative ring. If F: C → D is a functor, then lift_R(F) is linear over R; equivalently, for all X,Y and f: X → Y, and r ∈ R, the map satisfies map_smul: (lift_R(F))(r · f) = r · (lift_R(F))(f).

Русский

Пусть R — коммутативное кольцо. Если F: C → D — функтор, то lift_R(F) линейный относительно R; равно тому, что для всех X,Y и f: X → Y и для всех r ∈ R выполняется равенство map_smul: (lift_R(F))(r · f) = r · (lift_R(F))(f).

LaTeX

$$$ \\forall X,Y\\;\\forall f:\\; X \\to Y,\\; \\forall r\\in R,\\; (\\mathrm{Lift}_R(F))(r \\cdot f) = r \\cdot (\\mathrm{Lift}_R(F)(f)).$$$

Lean4

instance lift_linear (F : C ⥤ D) : (lift R F).Linear R where
  map_smul {X Y} f
    r := by
    dsimp
    rw [Finsupp.sum_smul_index] <;> simp [Finsupp.smul_sum, mul_smul]

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