Theorems · Inductive type · category theory

CategoryTheory.Linear

(R : Type w) →
  [Semiring R] →
    (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Preadditive C] → Type (max (max u v) w)

A category is called R-linear if P ⟶ Q is an R-module such that composition is R-linear in both variables.

Defined in

Mathlib.CategoryTheory.Linear.Basic

Cited by

131 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SemiringCategoryTheory.CategoryCategoryTheory.Preadditive