feat(algebra/category/FinVect): has finite limits (#13793)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/FinVect.lean

@@ -11,8 +11,8 @@ import algebra.category.Module.monoidal
 /-!
 # The category of finite dimensional vector spaces
 
-This introduces `FinVect K`, the category of finite dimensional vector spaces on a field `K`.
-It is implemented as a full subcategory on a subtype of  `Module K`.
+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`.
 We first create the instance as a category, then as a monoidal category and then as a rigid monoidal
 category.
 
@@ -31,12 +31,12 @@ universes u
 variables (K : Type u) [field K]
 
 /-- Define `FinVect` as the subtype of `Module.{u} K` of finite dimensional vector spaces. -/
-@[derive [category, λ α, has_coe_to_sort α (Sort*)]]
+@[derive [large_category, λ α, has_coe_to_sort α (Sort*), concrete_category]]
 def FinVect := { V : Module.{u} K // finite_dimensional K V }
 
 namespace FinVect
 
-instance finite_dimensional (V : FinVect K): finite_dimensional K V := V.prop
+instance finite_dimensional (V : FinVect K) : finite_dimensional K V := V.prop
 
 instance : inhabited (FinVect K) := ⟨⟨Module.of K K, finite_dimensional.finite_dimensional_self K⟩⟩
 
@@ -45,6 +45,16 @@ instance : has_coe (FinVect.{u} K) (Module.{u} K) := { coe := λ V, V.1, }
 protected lemma coe_comp {U V W : FinVect K} (f : U ⟶ V) (g : V ⟶ W) :
   ((f ≫ g) : U → W) = (g : V → W) ∘ (f : U → V) := rfl
 
+/-- Lift an unbundled vector space to `FinVect K`. -/
+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 : 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, }
+
 instance monoidal_category : monoidal_category (FinVect K) :=
 monoidal_category.full_monoidal_subcategory
   (λ V, finite_dimensional K V)

src/algebra/category/FinVect/limits.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.category.FinVect
+import algebra.category.Module.limits
+import algebra.category.Module.products
+import algebra.category.Module.epi_mono
+import category_theory.limits.creates
+import category_theory.limits.shapes.finite_limits
+import category_theory.limits.constructions.limits_of_products_and_equalizers
+
+/-!
+# `forget₂ (FinVect K) (Module K)` creates all finite limits.
+
+And hence `FinVect K` has all finite limits.
+-/
+
+noncomputable theory
+universes v u
+
+open category_theory
+open category_theory.limits
+
+namespace FinVect
+
+variables {J : Type v} [small_category J] [fin_category J]
+variables {k : Type v} [field k]
+
+instance {J : Type v} [fintype J] (Z : J → Module.{v} k) [∀ j, finite_dimensional k (Z j)] :
+  finite_dimensional k (∏ λ j, Z j : Module.{v} k) :=
+begin
+  haveI : finite_dimensional k (Module.of k (Π j, Z j)), { dsimp, apply_instance, },
+  exact finite_dimensional.of_injective
+    (Module.pi_iso_pi _).hom
+    ((Module.mono_iff_injective _).1 (by apply_instance)),
+end
+
+/-- Finite limits of finite finite dimensional vectors spaces are finite dimensional,
+because we can realise them as subobjects of a finite product. -/
+instance (F : J ⥤ FinVect k) :
+  finite_dimensional k (limit (F ⋙ forget₂ (FinVect k) (Module.{v} k)) : Module.{v} k) :=
+begin
+  haveI : ∀ j, finite_dimensional k ((F ⋙ forget₂ (FinVect k) (Module.{v} k)).obj j),
+  { intro j, change finite_dimensional k (F.obj j), apply_instance, },
+  exact finite_dimensional.of_injective
+    (limit_subobject_product (F ⋙ forget₂ (FinVect k) (Module.{v} k)))
+    ((Module.mono_iff_injective _).1 (by apply_instance)),
+end
+
+/-- The forgetful functor from `FinVect k` to `Module k` creates all finite limits. -/
+def forget₂_creates_limit (F : J ⥤ FinVect k) :
+  creates_limit F (forget₂ (FinVect k) (Module.{v} k)) :=
+creates_limit_of_fully_faithful_of_iso
+  ⟨(limit (F ⋙ forget₂ (FinVect k) (Module.{v} k)) : Module.{v} k), by apply_instance⟩
+  (iso.refl _)
+
+instance : creates_limits_of_shape J (forget₂ (FinVect k) (Module.{v} k)) :=
+{ creates_limit := λ F, forget₂_creates_limit F, }
+
+instance : has_finite_limits (FinVect k) :=
+{ out := λ J _ _, by exactI
+  has_limits_of_shape_of_has_limits_of_shape_creates_limits_of_shape
+    (forget₂ (FinVect k) (Module.{v} k)), }
+
+instance : preserves_finite_limits (forget₂ (FinVect k) (Module.{v} k)) :=
+{ preserves_finite_limits := λ J _ _, by exactI infer_instance, }
+
+end FinVect

src/algebra/category/Module/products.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import algebra.category.Module.epi_mono
+import linear_algebra.pi
+
+/-!
+# The concrete products in the category of modules are products in the categorical sense.
+-/
+
+open category_theory
+open category_theory.limits
+
+universes u v
+
+namespace Module
+variables {R : Type u} [ring R]
+
+variables {ι : Type v} (Z : ι → Module.{v} R)
+
+/-- The product cone induced by the concrete product. -/
+def product_cone : fan Z :=
+fan.mk (Module.of R (Π i : ι, Z i)) (λ i, (linear_map.proj i : (Π i : ι, Z i) →ₗ[R] Z i))
+
+/-- The concrete product cone is limiting. -/
+def product_cone_is_limit : is_limit (product_cone Z) :=
+{ lift := λ s, (linear_map.pi s.π.app : s.X →ₗ[R] (Π i : ι, Z i)),
+  fac' := by tidy,
+  uniq' := λ s m w, by { ext x i, exact linear_map.congr_fun (w i) x, }, }
+
+-- While we could use this to construct a `has_products (Module R)` instance,
+-- we already have `has_limits (Module R)` in `algebra.category.Module.limits`.
+
+variables [has_products (Module.{v} R)]
+
+/--
+The categorical product of a family of objects in `Module`
+agrees with the usual module-theoretical product.
+-/
+noncomputable def pi_iso_pi :
+  ∏ Z ≅ Module.of R (Π i, Z i) :=
+limit.iso_limit_cone ⟨_, product_cone_is_limit Z⟩
+
+-- We now show this isomorphism commutes with the inclusion of the kernel into the source.
+
+@[simp, elementwise] lemma pi_iso_pi_inv_kernel_ι (i : ι) :
+  (pi_iso_pi Z).inv ≫ pi.π Z i = (linear_map.proj i : (Π i : ι, Z i) →ₗ[R] Z i) :=
+limit.iso_limit_cone_inv_π _ _
+
+@[simp, elementwise] lemma pi_iso_pi_hom_ker_subtype (i : ι) :
+  (pi_iso_pi Z).hom ≫ (linear_map.proj i : (Π i : ι, Z i) →ₗ[R] Z i) = pi.π Z i :=
+is_limit.cone_point_unique_up_to_iso_inv_comp _ (limit.is_limit _) _
+
+end Module

src/category_theory/concrete_category/basic.lean

@@ -177,6 +177,15 @@ instance induced_category.has_forget₂ {C : Type v} {D : Type v'} [category D]
 { forget₂ := induced_functor f,
   forget_comp := rfl }
 
+instance full_subcategory.concrete_category {C : Type v} [category C] [concrete_category C]
+  (Z : C → Prop) : concrete_category {X : C // Z X} :=
+{ forget := full_subcategory_inclusion Z ⋙ forget C }
+
+instance full_subcategory.has_forget₂ {C : Type v} [category C] [concrete_category C]
+  (Z : C → Prop) : has_forget₂ {X : C // Z X} C :=
+{ forget₂ := full_subcategory_inclusion Z,
+  forget_comp := rfl }
+
 /--
 In order to construct a “partially forgetting” functor, we do not need to verify functor laws;
 it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`.

src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean

@@ -82,15 +82,15 @@ end has_limit_of_has_products_of_has_equalizers
 open has_limit_of_has_products_of_has_equalizers
 
 /--
-Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of
-`F` exists.
+Given the existence of the appropriate (possibly finite) products and equalizers,
+we can construct a limit cone for `F`.
 (This assumes the existence of all equalizers, which is technically stronger than needed.)
 -/
-lemma has_limit_of_equalizer_and_product (F : J ⥤ C)
+noncomputable
+def limit_cone_of_equalizer_and_product (F : J ⥤ C)
   [has_limit (discrete.functor F.obj)]
   [has_limit (discrete.functor (λ f : (Σ p : J × J, p.1 ⟶ p.2), F.obj f.1.2))]
-  [has_equalizers C] : has_limit F :=
-has_limit.mk
+  [has_equalizers C] : limit_cone F :=
 { cone := _,
   is_limit :=
     build_is_limit
@@ -102,6 +102,27 @@ has_limit.mk
       (limit.is_limit _)
       (limit.is_limit _) }
 
+/--
+Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of
+`F` exists.
+(This assumes the existence of all equalizers, which is technically stronger than needed.)
+-/
+lemma has_limit_of_equalizer_and_product (F : J ⥤ C)
+  [has_limit (discrete.functor F.obj)]
+  [has_limit (discrete.functor (λ f : (Σ p : J × J, p.1 ⟶ p.2), F.obj f.1.2))]
+  [has_equalizers C] : has_limit F :=
+has_limit.mk (limit_cone_of_equalizer_and_product F)
+
+/-- A limit can be realised as a subobject of a product. -/
+noncomputable
+def limit_subobject_product [has_limits C] (F : J ⥤ C) :
+  limit F ⟶ ∏ (λ j, F.obj j) :=
+(limit.iso_limit_cone (limit_cone_of_equalizer_and_product F)).hom ≫ equalizer.ι _ _
+
+instance limit_subobject_product_mono [has_limits C] (F : J ⥤ C) :
+  mono (limit_subobject_product F) :=
+mono_comp _ _
+
 /--
 Any category with products and equalizers has all limits.
 
@@ -244,14 +265,14 @@ open has_colimit_of_has_coproducts_of_has_coequalizers
 
 /--
 Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
-we know a colimit of `F` exists.
+we can construct a colimit cocone for `F`.
 (This assumes the existence of all coequalizers, which is technically stronger than needed.)
 -/
-lemma has_colimit_of_coequalizer_and_coproduct (F : J ⥤ C)
+noncomputable
+def colimit_cocone_of_coequalizer_and_coproduct (F : J ⥤ C)
   [has_colimit (discrete.functor F.obj)]
   [has_colimit (discrete.functor (λ f : (Σ p : J × J, p.1 ⟶ p.2), F.obj f.1.1))]
-  [has_coequalizers C] : has_colimit F :=
-has_colimit.mk
+  [has_coequalizers C] : colimit_cocone F :=
 { cocone := _,
   is_colimit :=
     build_is_colimit
@@ -263,6 +284,28 @@ has_colimit.mk
       (colimit.is_colimit _)
       (colimit.is_colimit _) }
 
+
+/--
+Given the existence of the appropriate (possibly finite) coproducts and coequalizers,
+we know a colimit of `F` exists.
+(This assumes the existence of all coequalizers, which is technically stronger than needed.)
+-/
+lemma has_colimit_of_coequalizer_and_coproduct (F : J ⥤ C)
+  [has_colimit (discrete.functor F.obj)]
+  [has_colimit (discrete.functor (λ f : (Σ p : J × J, p.1 ⟶ p.2), F.obj f.1.1))]
+  [has_coequalizers C] : has_colimit F :=
+has_colimit.mk (colimit_cocone_of_coequalizer_and_coproduct F)
+
+/-- A colimit can be realised as a quotient of a coproduct. -/
+noncomputable
+def colimit_quotient_coproduct [has_colimits C] (F : J ⥤ C) :
+  ∐ (λ j, F.obj j) ⟶ colimit F :=
+coequalizer.π _ _ ≫ (colimit.iso_colimit_cocone (colimit_cocone_of_coequalizer_and_coproduct F)).inv
+
+instance colimit_quotient_coproduct_epi [has_colimits C] (F : J ⥤ C) :
+  epi (colimit_quotient_coproduct F) :=
+epi_comp _ _
+
 /--
 Any category with coproducts and coequalizers has all colimits.
 

src/linear_algebra/finite_dimensional.lean

@@ -108,6 +108,14 @@ variables (K V)
 instance finite_dimensional_pi {ι} [fintype ι] : finite_dimensional K (ι → K) :=
 iff_fg.1 is_noetherian_pi
 
+instance finite_dimensional_pi' {ι} [fintype ι] (M : ι → Type*)
+  [∀ i, add_comm_group (M i)] [∀ i, module K (M i)] [I : ∀ i, finite_dimensional K (M i)] :
+  finite_dimensional K (Π i, M i) :=
+begin
+  haveI : ∀ i : ι, is_noetherian K (M i) := λ i, iff_fg.2 (I i),
+  exact iff_fg.1 is_noetherian_pi
+end
+
 /-- A finite dimensional vector space over a finite field is finite -/
 noncomputable def fintype_of_fintype [fintype K] [finite_dimensional K V] : fintype V :=
 module.fintype_of_fintype (@finset_basis K V _ _ _ (iff_fg.2 infer_instance))