module — Mathlib

English

Define a family of R-modules on hom-sets of Quotient r using the previously defined smul, ensuring linear structure is compatible with composition.

Русский

Определяем семейство модулей над R на множестве морфизмов квотиента Quotient r, используя ранее определённое умножение, чтобы структура была совместима с композициями.

LaTeX

$$$\\text{module}:\\;\\text{Hom}_{\\mathrm{Quotient}(r)}(X,Y)\\text{ is an } R\\text{-module with linear operations as above}$$$

Lean4

/-- Auxiliary definition for `Quotient.linear`. -/
def module (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y) (_ : r f₁ f₂), r (a • f₁) (a • f₂)) [Preadditive (Quotient r)]
    [(functor r).Additive] (X Y : Quotient r) : Module R (X ⟶ Y) :=
  module' r hr X.as Y.as

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