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) :
@[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) :
@[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') :
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') :
@[protected, instance]
def
category_theory.linear.preadditive_nat_linear
{C : Type u}
[category_theory.category C]
[category_theory.preadditive 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] :
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)
@[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
@[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) :
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) :
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) :
Composition by a fixed left argument as an R-linear map.
@[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) :
Composition by a fixed right argument as an R-linear map.
@[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) :
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) :
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) :
@[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) :
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' := _}