mathlib3 documentation

category_theory.linear.basic

Linear categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An R-linear category is a category in which X ⟶ Y is an R-module in such a way that composition of morphisms is R-linear in both variables.

Note that sometimes in the literature a "linear category" is further required to be abelian.

Implementation #

Corresponding to the fact that we need to have an add_comm_group X structure in place to talk about a module R X structure, we need preadditive C as a prerequisite typeclass for linear R C. This makes for longer signatures than would be ideal.

Future work #

It would be nice to have a usable framework of enriched categories in which this just became a category enriched in Module R.

@[class]

structure category_theory.linear (R : Type w) [semiring R] (C : Type u) [category_theory.category C] [category_theory.preadditive C] :

Type (max u v w)

hom_module : (Π (X Y : C), module R (X ⟶ Y)) . "apply_instance"
smul_comp' : (∀ (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g) . "obviously"
comp_smul' : (∀ (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g) . "obviously"

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

Instances of this typeclass

Instances of other typeclasses for category_theory.linear

category_theory.linear.has_sizeof_inst

@[simp]

theorem category_theory.linear.smul_comp {R : Type w} [semiring R] {C : Type u} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R C] (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z) :

(r • f) ≫ g = r • f ≫ g

@[simp]

theorem category_theory.linear.comp_smul {R : Type w} [semiring R] {C : Type u} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R C] (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z) :

f ≫ (r • g) = r • f ≫ g

@[simp]

theorem category_theory.linear.smul_comp_assoc {R : Type w} [semiring R] {C : Type u} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R C] (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z) {X' : C} (f' : Z ⟶ X') :

(r • f) ≫ g ≫ f' = (r • f ≫ g) ≫ f'

theorem category_theory.linear.comp_smul_assoc {R : Type w} [semiring R] {C : Type u} [category_theory.category C] [category_theory.preadditive C] [self : category_theory.linear R C] (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z) {X' : C} (f' : Z ⟶ X') :

f ≫ (r • g) ≫ f' = (r • f ≫ g) ≫ f'

@[protected, instance]

def category_theory.linear.preadditive_nat_linear {C : Type u} [category_theory.category C] [category_theory.preadditive C] :

category_theory.linear ℕ C

Equations

category_theory.linear.preadditive_nat_linear = {hom_module := λ (X Y : C), add_comm_monoid.nat_module, smul_comp' := _, comp_smul' := _}

@[protected, instance]

def category_theory.linear.preadditive_int_linear {C : Type u} [category_theory.category C] [category_theory.preadditive C] :

category_theory.linear ℤ C

Equations

category_theory.linear.preadditive_int_linear = {hom_module := λ (X Y : C), add_comm_group.int_module (X ⟶ Y), smul_comp' := _, comp_smul' := _}

@[protected, instance]

def category_theory.linear.category_theory.End.module {C : Type u} [category_theory.category C] [category_theory.preadditive C] {R : Type w} [semiring R] [category_theory.linear R C] (X : C) :

module R (category_theory.End X)

Equations

category_theory.linear.category_theory.End.module X = id (category_theory.linear.hom_module X X)

@[protected, instance]

def category_theory.linear.category_theory.End.algebra {C : Type u} [category_theory.category C] [category_theory.preadditive C] {R : Type w} [comm_semiring R] [category_theory.linear R C] (X : C) :

algebra R (category_theory.End X)

Equations

category_theory.linear.category_theory.End.algebra X = algebra.of_module _ _

@[protected, instance]

def category_theory.linear.induced_category {C : Type u} [category_theory.category C] [category_theory.preadditive C] {R : Type w} [semiring R] [category_theory.linear R C] {D : Type u'} (F : D → C) :

category_theory.linear R (category_theory.induced_category C F)

Equations

category_theory.linear.induced_category F = {hom_module := λ (X Y : category_theory.induced_category C F), category_theory.linear.hom_module (F X) (F Y), smul_comp' := _, comp_smul' := _}

@[protected, instance]

def category_theory.linear.full_subcategory {C : Type u} [category_theory.category C] [category_theory.preadditive C] {R : Type w} [semiring R] [category_theory.linear R C] (Z : C → Prop) :

category_theory.linear R (category_theory.full_subcategory Z)

Equations

category_theory.linear.full_subcategory Z = {hom_module := λ (X Y : category_theory.full_subcategory Z), category_theory.linear.hom_module X.obj Y.obj, smul_comp' := _, comp_smul' := _}

def category_theory.linear.left_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {X Y : C} (Z : C) (f : X ⟶ Y) :

(Y ⟶ Z) →ₗ[R] X ⟶ Z

Composition by a fixed left argument as an R-linear map.

Equations

category_theory.linear.left_comp R Z f = {to_fun := λ (g : Y ⟶ Z), f ≫ g, map_add' := _, map_smul' := _}

@[simp]

theorem category_theory.linear.left_comp_apply {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {X Y : C} (Z : C) (f : X ⟶ Y) (g : Y ⟶ Z) :

⇑(category_theory.linear.left_comp R Z f) g = f ≫ g

@[simp]

theorem category_theory.linear.right_comp_apply {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] (X : C) {Y Z : C} (g : Y ⟶ Z) (f : X ⟶ Y) :

⇑(category_theory.linear.right_comp R X g) f = f ≫ g

def category_theory.linear.right_comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] (X : C) {Y Z : C} (g : Y ⟶ Z) :

(X ⟶ Y) →ₗ[R] X ⟶ Z

Composition by a fixed right argument as an R-linear map.

Equations

category_theory.linear.right_comp R X g = {to_fun := λ (f : X ⟶ Y), f ≫ g, map_add' := _, map_smul' := _}

@[protected, instance]

def category_theory.linear.has_smul.smul.category_theory.epi {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {X Y : C} (f : X ⟶ Y) [category_theory.epi f] (r : R) [invertible r] :

category_theory.epi (r • f)

@[protected, instance]

def category_theory.linear.has_smul.smul.category_theory.mono {C : Type u} [category_theory.category C] [category_theory.preadditive C] (R : Type w) [semiring R] [category_theory.linear R C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] (r : R) [invertible r] :

category_theory.mono (r • f)

def category_theory.linear.hom_congr (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) :

(X ⟶ W) ≃ₗ[k] Y ⟶ Z

Given isomorphic objects X ≅ Y, W ≅ Z in a k-linear category, we have a k-linear isomorphism between Hom(X, W) and Hom(Y, Z).

Equations

category_theory.linear.hom_congr k f₁ f₂ = {to_fun := ((category_theory.linear.right_comp k Y f₂.hom).comp (category_theory.linear.left_comp k W f₁.symm.hom)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑((category_theory.linear.left_comp k W f₁.hom).comp (category_theory.linear.right_comp k Y f₂.symm.hom)), left_inv := _, right_inv := _}

theorem category_theory.linear.hom_congr_apply (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : X ⟶ W) :

⇑(category_theory.linear.hom_congr k f₁ f₂) f = (f₁.inv ≫ f) ≫ f₂.hom

theorem category_theory.linear.hom_congr_symm_apply (k : Type u_1) {C : Type u_2} [category_theory.category C] [semiring k] [category_theory.preadditive C] [category_theory.linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) :

⇑((category_theory.linear.hom_congr k f₁ f₂).symm) f = f₁.hom ≫ f ≫ f₂.inv

@[simp]

theorem category_theory.linear.comp_apply {C : Type u} [category_theory.category C] [category_theory.preadditive C] {S : Type w} [comm_semiring S] [category_theory.linear S C] (X Y Z : C) (f : X ⟶ Y) :

⇑(category_theory.linear.comp X Y Z) f = category_theory.linear.left_comp S Z f

def category_theory.linear.comp {C : Type u} [category_theory.category C] [category_theory.preadditive C] {S : Type w} [comm_semiring S] [category_theory.linear S C] (X Y Z : C) :

(X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z

Composition as a bilinear map.

Equations

category_theory.linear.comp X Y Z = {to_fun := λ (f : X ⟶ Y), category_theory.linear.left_comp S Z f, map_add' := _, map_smul' := _}