English
There is a linear structure on Quotient r making functorial liftings additive and compatible with the quotient functor.
Русский
Существует линейная структура на Quotient r, делающая переходы через косвенные отображения аддитивными и совместимыми с квотиентом.
LaTeX
$$$\\text{linear}(hr) :\\; \\text{Linear } R (\\mathrm{Quotient}(r))$$$
Lean4
/-- Assuming `Quotient r` has already been endowed with a preadditive category structure
such that `functor r : C ⥤ Quotient r` is additive, and that `C` has a `R`-linear category
structure compatible with `r`, this is the induced `R`-linear category structure on
`Quotient r`. -/
def linear (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y) (_ : r f₁ f₂), r (a • f₁) (a • f₂)) [Preadditive (Quotient r)]
[(functor r).Additive] : Linear R (Quotient r) :=
by
letI := Linear.module r hr
exact
{ smul_comp := by
rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ a f g
obtain ⟨f, rfl⟩ := (functor r).map_surjective f
obtain ⟨g, rfl⟩ := (functor r).map_surjective g
rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp, Linear.smul_eq, Linear.smul_comp]
comp_smul := by
rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ f a g
obtain ⟨f, rfl⟩ := (functor r).map_surjective f
obtain ⟨g, rfl⟩ := (functor r).map_surjective g
rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp, Linear.smul_eq, Linear.comp_smul] }
