English
Given a linear relation r on morphisms in a category C, the quotient category Quotient r inherits an R-module structure on each hom-set, compatible with composition, making Quotient r an R-linear category.
Русский
Пусть на морфизмах в категорию C задано линейное отношение r. Тогда у Quotient r на каждом множестве морфизмов задаётся структура модуля над R, совместимая с композициией, что делает Quotient r линейной по R категорией.
LaTeX
$$$\\text{Quotient}(r)$ is an $R$-linear category with $\\mathrm{Hom}_{\\mathrm{Quotient}(r)}(X,Y)$ equipped with an $R$-module structure compatible with composition.$$
Lean4
/-- The scalar multiplications on morphisms in `Quotient R`. -/
def smul (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y) (_ : r f₁ f₂), r (a • f₁) (a • f₂)) (X Y : Quotient r) :
SMul R (X ⟶ Y) where
smul
a :=
Quot.lift (fun g => Quot.mk _ (a • g))
(fun f₁ f₂ h₁₂ => by
dsimp
simp only [compClosure_eq_self] at h₁₂
apply Quot.sound
rw [compClosure_eq_self]
exact hr _ _ _ h₁₂)
