diff --git a/src/algebra/category/FinVect.lean b/src/algebra/category/FinVect.lean index f3b2583d36e51..f1b1f919611ab 100644 --- a/src/algebra/category/FinVect.lean +++ b/src/algebra/category/FinVect.lean @@ -13,9 +13,17 @@ import algebra.category.Module.monoidal # The category of finite dimensional vector spaces This introduces `FinVect K`, the category of finite dimensional vector spaces over a field `K`. -It is implemented as a full subcategory on a subtype of `Module K`, which inherits monoidal and -symmetric structure as `finite_dimensional K` is a monoidal predicate. -We also provide a right rigid monoidal category instance. +It is implemented as a full subcategory on a subtype of `Module K`. + +We first create the instance as a `K`-linear category, +then as a `K`-linear monoidal category and then as a right-rigid monoidal category. + +## Future work + +* Show that `FinVect K` is a symmetric monoidal category (it is already monoidal). +* Show that `FinVect K` is abelian. +* Show that `FinVect K` is rigid (it is already right rigid). + -/ noncomputable theory @@ -36,8 +44,9 @@ instance closed_predicate_finite_dimensional : { prop_ihom' := λ X Y hX hY, by exactI @linear_map.finite_dimensional K _ X _ _ hX Y _ _ hY } /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/ -@[derive [large_category, concrete_category, monoidal_category, symmetric_category, -monoidal_closed]] +@[derive [large_category, concrete_category, preadditive, linear K, + monoidal_category, symmetric_category, monoidal_preadditive, monoidal_linear K, + monoidal_closed]] def FinVect := full_subcategory (λ (V : Module.{u} K), finite_dimensional K V) namespace FinVect @@ -50,12 +59,28 @@ instance : inhabited (FinVect K) := ⟨⟨Module.of K K, finite_dimensional.fini def of (V : Type u) [add_comm_group V] [module K V] [finite_dimensional K V] : FinVect K := ⟨Module.of K V, by { change finite_dimensional K V, apply_instance }⟩ +instance (V W : FinVect K) : finite_dimensional K (V ⟶ W) := +(by apply_instance : finite_dimensional K (V.obj →ₗ[K] W.obj)) + instance : has_forget₂ (FinVect.{u} K) (Module.{u} K) := by { dsimp [FinVect], apply_instance, } instance : full (forget₂ (FinVect K) (Module.{u} K)) := { preimage := λ X Y f, f, } +/-- The forgetful functor `FinVect K ⥤ Module K` as a monoidal functor. -/ +def forget₂_monoidal : monoidal_functor (FinVect K) (Module.{u} K) := +monoidal_category.full_monoidal_subcategory_inclusion _ + +instance forget₂_monoidal_faithful : faithful (forget₂_monoidal K).to_functor := +by { dsimp [forget₂_monoidal], apply_instance, } + +instance forget₂_monoidal_additive : (forget₂_monoidal K).to_functor.additive := +by { dsimp [forget₂_monoidal], apply_instance, } + +instance forget₂_monoidal_linear : (forget₂_monoidal K).to_functor.linear K := +by { dsimp [forget₂_monoidal], apply_instance, } + variables (V W : FinVect K) @[simp] lemma ihom_obj : (ihom V).obj W = FinVect.of K (V.obj →ₗ[K] W.obj) := rfl diff --git a/src/category_theory/linear/default.lean b/src/category_theory/linear/default.lean index 8cbffda48e876..9b76f7fce0ad9 100644 --- a/src/category_theory/linear/default.lean +++ b/src/category_theory/linear/default.lean @@ -88,13 +88,18 @@ section induced_category universes u' variables {C} {D : Type u'} (F : D → C) -instance induced_category.category : linear.{w v} R (induced_category C F) := +instance induced_category : linear.{w v} R (induced_category C F) := { hom_module := λ X Y, @linear.hom_module R _ C _ _ _ (F X) (F Y), smul_comp' := λ P Q R f f' g, smul_comp' _ _ _ _ _ _, comp_smul' := λ P Q R f g g', comp_smul' _ _ _ _ _ _, } end induced_category +instance full_subcategory (Z : C → Prop) : linear.{w v} R (full_subcategory Z) := +{ hom_module := λ X Y, @linear.hom_module R _ C _ _ _ X.obj Y.obj, + smul_comp' := λ P Q R f f' g, smul_comp' _ _ _ _ _ _, + comp_smul' := λ P Q R f g g', comp_smul' _ _ _ _ _ _, } + variables (R) /-- Composition by a fixed left argument as an `R`-linear map. -/ diff --git a/src/category_theory/linear/linear_functor.lean b/src/category_theory/linear/linear_functor.lean index d532a7e4136ef..d9d46eb91ef07 100644 --- a/src/category_theory/linear/linear_functor.lean +++ b/src/category_theory/linear/linear_functor.lean @@ -71,6 +71,10 @@ instance induced_functor_linear : functor.linear R (induced_functor F) := {} end induced_category +instance full_subcategory_inclusion_linear + {C : Type*} [category C] [preadditive C] [category_theory.linear R C] (Z : C → Prop) : + (full_subcategory_inclusion Z).linear R := {} + section variables {R} {C D : Type*} [category C] [category D] diff --git a/src/category_theory/monoidal/linear.lean b/src/category_theory/monoidal/linear.lean index 30269ad6723b5..75d95bead92ff 100644 --- a/src/category_theory/monoidal/linear.lean +++ b/src/category_theory/monoidal/linear.lean @@ -35,11 +35,32 @@ restate_axiom monoidal_linear.tensor_smul' restate_axiom monoidal_linear.smul_tensor' attribute [simp] monoidal_linear.tensor_smul monoidal_linear.smul_tensor -variables [monoidal_linear R C] +variables {C} [monoidal_linear R C] instance tensor_left_linear (X : C) : (tensor_left X).linear R := {} instance tensor_right_linear (X : C) : (tensor_right X).linear R := {} instance tensoring_left_linear (X : C) : ((tensoring_left C).obj X).linear R := {} instance tensoring_right_linear (X : C) : ((tensoring_right C).obj X).linear R := {} +/-- A faithful linear monoidal functor to a linear monoidal category +ensures that the domain is linear monoidal. -/ +def monoidal_linear_of_faithful + {D : Type*} [category D] [preadditive D] [linear R D] + [monoidal_category D] [monoidal_preadditive D] + (F : monoidal_functor D C) [faithful F.to_functor] + [F.to_functor.additive] [F.to_functor.linear R] : + monoidal_linear R D := +{ tensor_smul' := begin + intros, + apply F.to_functor.map_injective, + simp only [F.to_functor.map_smul r (f ⊗ g), F.to_functor.map_smul r g, F.map_tensor, + monoidal_linear.tensor_smul, linear.smul_comp, linear.comp_smul], + end, + smul_tensor' := begin + intros, + apply F.to_functor.map_injective, + simp only [F.to_functor.map_smul r (f ⊗ g), F.to_functor.map_smul r f, F.map_tensor, + monoidal_linear.smul_tensor, linear.smul_comp, linear.comp_smul], + end, } + end category_theory diff --git a/src/category_theory/monoidal/preadditive.lean b/src/category_theory/monoidal/preadditive.lean index 67852e38c4cb3..10c0e82a49605 100644 --- a/src/category_theory/monoidal/preadditive.lean +++ b/src/category_theory/monoidal/preadditive.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison -/ import category_theory.preadditive.additive_functor -import category_theory.monoidal.category +import category_theory.monoidal.functor /-! # Preadditive monoidal categories @@ -41,7 +41,7 @@ restate_axiom monoidal_preadditive.tensor_add' restate_axiom monoidal_preadditive.add_tensor' attribute [simp] monoidal_preadditive.tensor_zero monoidal_preadditive.zero_tensor -variables [monoidal_preadditive C] +variables {C} [monoidal_preadditive C] local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor @@ -50,6 +50,26 @@ instance tensor_right_additive (X : C) : (tensor_right X).additive := {} instance tensoring_left_additive (X : C) : ((tensoring_left C).obj X).additive := {} instance tensoring_right_additive (X : C) : ((tensoring_right C).obj X).additive := {} +/-- A faithful additive monoidal functor to a monoidal preadditive category +ensures that the domain is monoidal preadditive. -/ +def monoidal_preadditive_of_faithful {D : Type*} [category D] [preadditive D] [monoidal_category D] + (F : monoidal_functor D C) [faithful F.to_functor] [F.to_functor.additive] : + monoidal_preadditive D := +{ tensor_zero' := by { intros, apply F.to_functor.map_injective, simp [F.map_tensor], }, + zero_tensor' := by { intros, apply F.to_functor.map_injective, simp [F.map_tensor], }, + tensor_add' := begin + intros, + apply F.to_functor.map_injective, + simp only [F.map_tensor, F.to_functor.map_add, preadditive.comp_add, preadditive.add_comp, + monoidal_preadditive.tensor_add], + end, + add_tensor' := begin + intros, + apply F.to_functor.map_injective, + simp only [F.map_tensor, F.to_functor.map_add, preadditive.comp_add, preadditive.add_comp, + monoidal_preadditive.add_tensor], + end, } + open_locale big_operators lemma tensor_sum {P Q R S : C} {J : Type*} (s : finset J) (f : P ⟶ Q) (g : J → (R ⟶ S)) : diff --git a/src/category_theory/monoidal/subcategory.lean b/src/category_theory/monoidal/subcategory.lean index 5bf28be48ca43..cf5eb1b503d5e 100644 --- a/src/category_theory/monoidal/subcategory.lean +++ b/src/category_theory/monoidal/subcategory.lean @@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Antoine Labelle -/ import category_theory.monoidal.braided +import category_theory.monoidal.linear import category_theory.concrete_category.basic +import category_theory.preadditive.additive_functor +import category_theory.linear.linear_functor import category_theory.closed.monoidal /-! @@ -82,6 +85,28 @@ instance full_monoidal_subcategory.full : instance full_monoidal_subcategory.faithful : faithful (full_monoidal_subcategory_inclusion P).to_functor := full_subcategory.faithful P +section + +variables [preadditive C] + +instance full_monoidal_subcategory_inclusion_additive : + (full_monoidal_subcategory_inclusion P).to_functor.additive := +functor.full_subcategory_inclusion_additive _ + +instance [monoidal_preadditive C] : monoidal_preadditive (full_subcategory P) := +monoidal_preadditive_of_faithful (full_monoidal_subcategory_inclusion P) + +variables (R : Type*) [ring R] [linear R C] + +instance full_monoidal_subcategory_inclusion_linear : + (full_monoidal_subcategory_inclusion P).to_functor.linear R := +functor.full_subcategory_inclusion_linear R _ + +instance [monoidal_preadditive C] [monoidal_linear R C] : monoidal_linear R (full_subcategory P) := +monoidal_linear_of_faithful R (full_monoidal_subcategory_inclusion P) + +end + variables {P} {P' : C → Prop} [monoidal_predicate P'] /-- An implication of predicates `P → P'` induces a monoidal functor between full monoidal diff --git a/src/category_theory/preadditive/additive_functor.lean b/src/category_theory/preadditive/additive_functor.lean index 05903b8bb0c89..7b8080af28d67 100644 --- a/src/category_theory/preadditive/additive_functor.lean +++ b/src/category_theory/preadditive/additive_functor.lean @@ -98,6 +98,10 @@ instance induced_functor_additive : functor.additive (induced_functor F) := {} end induced_category +instance full_subcategory_inclusion_additive + {C : Type*} [category C] [preadditive C] (Z : C → Prop) : + (full_subcategory_inclusion Z).additive := {} + section -- To talk about preservation of biproducts we need to specify universes explicitly. @@ -154,7 +158,7 @@ full_subcategory (λ (F : C ⥤ D), F.additive) infixr ` ⥤+ `:26 := AdditiveFunctor instance : preadditive (C ⥤+ D) := -preadditive.induced_category.category _ +preadditive.induced_category _ /-- An additive functor is in particular a functor. -/ @[derive full, derive faithful] diff --git a/src/category_theory/preadditive/default.lean b/src/category_theory/preadditive/default.lean index 878e29a2ddcc6..e2925475cc225 100644 --- a/src/category_theory/preadditive/default.lean +++ b/src/category_theory/preadditive/default.lean @@ -83,13 +83,18 @@ section induced_category universes u' variables {C} {D : Type u'} (F : D → C) -instance induced_category.category : preadditive.{v} (induced_category C F) := +instance induced_category : preadditive.{v} (induced_category C F) := { hom_group := λ P Q, @preadditive.hom_group C _ _ (F P) (F Q), add_comp' := λ P Q R f f' g, add_comp' _ _ _ _ _ _, comp_add' := λ P Q R f g g', comp_add' _ _ _ _ _ _, } end induced_category +instance full_subcategory (Z : C → Prop) : preadditive.{v} (full_subcategory Z) := +{ hom_group := λ P Q, @preadditive.hom_group C _ _ P.obj Q.obj, + add_comp' := λ P Q R f f' g, add_comp' _ _ _ _ _ _, + comp_add' := λ P Q R f g g', comp_add' _ _ _ _ _ _, } + instance (X : C) : add_comm_group (End X) := by { dsimp [End], apply_instance, } instance (X : C) : ring (End X) := diff --git a/src/representation_theory/Action.lean b/src/representation_theory/Action.lean index feacd272fbe35..a57e2f892e22b 100644 --- a/src/representation_theory/Action.lean +++ b/src/representation_theory/Action.lean @@ -267,9 +267,15 @@ section has_zero_morphisms variables [has_zero_morphisms V] instance : has_zero_morphisms (Action V G) := -{ has_zero := λ X Y, ⟨⟨0, by tidy⟩⟩, } +{ has_zero := λ X Y, ⟨⟨0, by { intro g, simp }⟩⟩, + comp_zero' := λ P Q f R, by { ext1, simp }, + zero_comp' := λ P Q R f, by { ext1, simp }, } -instance : functor.preserves_zero_morphisms (functor_category_equivalence V G).functor := {} +instance forget_preserves_zero_morphisms : functor.preserves_zero_morphisms (forget V G) := {} +instance forget₂_preserves_zero_morphisms [concrete_category V] : + functor.preserves_zero_morphisms (forget₂ (Action V G) V) := {} +instance functor_category_equivalence_preserves_zero_morphisms : + functor.preserves_zero_morphisms (functor_category_equivalence V G).functor := {} end has_zero_morphisms @@ -289,8 +295,12 @@ instance : preadditive (Action V G) := add_comp' := by { intros, ext, exact preadditive.add_comp _ _ _ _ _ _, }, comp_add' := by { intros, ext, exact preadditive.comp_add _ _ _ _ _ _, }, } -instance : functor.additive (functor_category_equivalence V G).functor := {} -instance forget_additive : functor.additive (forget V G) := {} +instance forget_additive : + functor.additive (forget V G) := {} +instance forget₂_additive [concrete_category V] : + functor.additive (forget₂ (Action V G) V) := {} +instance functor_category_equivalence_additive : + functor.additive (functor_category_equivalence V G).functor := {} @[simp] lemma zero_hom {X Y : Action V G} : (0 : X ⟶ Y).hom = 0 := rfl @[simp] lemma neg_hom {X Y : Action V G} (f : X ⟶ Y) : (-f).hom = -f.hom := rfl @@ -315,7 +325,12 @@ instance : linear R (Action V G) := smul_comp' := by { intros, ext, exact linear.smul_comp _ _ _ _ _ _, }, comp_smul' := by { intros, ext, exact linear.comp_smul _ _ _ _ _ _, }, } -instance : functor.linear R (functor_category_equivalence V G).functor := {} +instance forget_linear : + functor.linear R (forget V G) := {} +instance forget₂_linear [concrete_category V] : + functor.linear R (forget₂ (Action V G) V) := {} +instance functor_category_equivalence_linear : + functor.linear R (functor_category_equivalence V G).functor := {} @[simp] lemma smul_hom {X Y : Action V G} (r : R) (f : X ⟶ Y) : (r • f).hom = r • f.hom := rfl @@ -412,10 +427,10 @@ instance [symmetric_category V] : symmetric_category (Action V G) := symmetric_category_of_faithful (forget_braided V G) section -local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor - variables [preadditive V] [monoidal_preadditive V] +local attribute [simp] monoidal_preadditive.tensor_add monoidal_preadditive.add_tensor + instance : monoidal_preadditive (Action V G) := {} variables {R : Type*} [semiring R] [linear R V] [monoidal_linear R V] diff --git a/src/representation_theory/fdRep.lean b/src/representation_theory/fdRep.lean index 054983741e6a1..856242b9cd4f5 100644 --- a/src/representation_theory/fdRep.lean +++ b/src/representation_theory/fdRep.lean @@ -17,13 +17,15 @@ Also `V.ρ` gives the homomorphism `G →* (V →ₗ[k] V)`. Conversely, given a homomorphism `ρ : G →* (V →ₗ[k] V)`, you can construct the bundled representation as `Rep.of ρ`. -We verify that `fdRep k G` is a rigid monoidal category. +We verify that `fdRep k G` is a `k`-linear monoidal category, and right rigid when `G` is a group. ## TODO +* `fdRep k G ≌ full_subcategory (finite_dimensional k)` +* Upgrade the right rigid structure to a rigid structure (this just needs to be done for `FinVect`). * `fdRep k G` has all finite (co)limits. * `fdRep k G` is abelian. * `fdRep k G ≌ FinVect (monoid_algebra k G)` (this will require generalising `FinVect` first). -* Upgrade the right rigid structure to a rigid structure. + -/ universes u @@ -32,7 +34,7 @@ open category_theory open category_theory.limits /-- The category of finite dimensional `k`-linear representations of a monoid `G`. -/ -@[derive [large_category, concrete_category/-, has_limits, has_colimits-/]] +@[derive [large_category, concrete_category, preadditive]] abbreviation fdRep (k G : Type u) [field k] [monoid G] := Action (FinVect.{u} k) (Mon.of G) @@ -40,6 +42,8 @@ namespace fdRep variables {k G : Type u} [field k] [monoid G] +instance : linear k (fdRep k G) := by apply_instance + instance : has_coe_to_sort (fdRep k G) (Type u) := concrete_category.has_coe_to_sort _ instance (V : fdRep k G) : add_comm_group V := @@ -51,6 +55,11 @@ by { change module k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_inst instance (V : fdRep k G) : finite_dimensional k V := by { change finite_dimensional k ((forget₂ (fdRep k G) (FinVect k)).obj V).obj, apply_instance, } +/-- All hom spaces are finite dimensional. -/ +instance (V W : fdRep k G) : finite_dimensional k (V ⟶ W) := +finite_dimensional.of_injective + ((forget₂ (fdRep k G) (FinVect k)).map_linear_map k) (functor.map_injective _) + /-- The monoid homomorphism corresponding to the action of `G` onto `V : fdRep k G`. -/ def ρ (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ @@ -66,9 +75,6 @@ begin exact (i.hom.comm g).symm, end --- This works well with the new design for representations: -example (V : fdRep k G) : G →* (V →ₗ[k] V) := V.ρ - /-- Lift an unbundled representation to `fdRep`. -/ @[simps ρ] def of {V : Type u} [add_comm_group V] [module k V] [finite_dimensional k V] @@ -80,6 +86,8 @@ instance : has_forget₂ (fdRep k G) (Rep k G) := -- Verify that the monoidal structure is available. example : monoidal_category (fdRep k G) := by apply_instance +example : monoidal_preadditive (fdRep k G) := by apply_instance +example : monoidal_linear k (fdRep k G) := by apply_instance end fdRep