From 9f525c7425ad6c3b58127bb4f73f7d9599d171dc Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Thu, 20 Aug 2020 21:33:47 +0000 Subject: [PATCH] chore(category_theory/limits/types): cleanup (#3871) Backporting some cleaning up work from `prop_limits`, while it rumbles onwards. Co-authored-by: Scott Morrison --- src/algebra/category/Module/limits.lean | 4 +- src/algebra/category/Mon/limits.lean | 4 +- src/category_theory/limits/limits.lean | 2 + .../limits/preserves/basic.lean | 72 +++++++++- src/category_theory/limits/shapes/types.lean | 2 +- src/category_theory/limits/types.lean | 126 +++++++++++------- 6 files changed, 149 insertions(+), 61 deletions(-) diff --git a/src/algebra/category/Module/limits.lean b/src/algebra/category/Module/limits.lean index d34864c9bf1e6..6771e8baa87fa 100644 --- a/src/algebra/category/Module/limits.lean +++ b/src/algebra/category/Module/limits.lean @@ -63,8 +63,8 @@ end def limit_π_linear_map (F : J ⥤ Module R) (j) : limit (F ⋙ forget (Module R)) →ₗ[R] (F ⋙ forget (Module R)).obj j := { to_fun := limit.π (F ⋙ forget (Module R)) j, - map_smul' := λ x y, by { simp only [types.types_limit_π], refl }, - map_add' := λ x y, by { simp only [types.types_limit_π], refl } } + map_smul' := λ x y, rfl, + map_add' := λ x y, rfl } namespace has_limits -- The next two definitions are used in the construction of `has_limits (Module R)`. diff --git a/src/algebra/category/Mon/limits.lean b/src/algebra/category/Mon/limits.lean index 63a0b6b9ee06d..46a334e560aa8 100644 --- a/src/algebra/category/Mon/limits.lean +++ b/src/algebra/category/Mon/limits.lean @@ -58,8 +58,8 @@ instance limit_monoid (F : J ⥤ Mon) : def limit_π_monoid_hom (F : J ⥤ Mon) (j) : limit (F ⋙ forget Mon) →* (F ⋙ forget Mon).obj j := { to_fun := limit.π (F ⋙ forget Mon) j, - map_one' := by { simp only [types.types_limit_π], refl }, - map_mul' := λ x y, by { simp only [types.types_limit_π], refl } } + map_one' := rfl, + map_mul' := λ x y, rfl } namespace has_limits -- The next two definitions are used in the construction of `has_limits Mon`. diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean index 973506bfaa457..4b2de41b6f2e6 100644 --- a/src/category_theory/limits/limits.lean +++ b/src/category_theory/limits/limits.lean @@ -63,6 +63,7 @@ def mk_cone_morphism {t : cone F} congr_arg cone_morphism.hom this } /-- Limit cones on `F` are unique up to isomorphism. -/ +@[simps] def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t := { hom := Q.lift_cone_morphism s, inv := P.lift_cone_morphism t, @@ -416,6 +417,7 @@ def mk_cocone_morphism {t : cocone F} congr_arg cocone_morphism.hom this } /-- Colimit cocones on `F` are unique up to isomorphism. -/ +@[simps] def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s ≅ t := { hom := P.desc_cocone_morphism t, inv := Q.desc_cocone_morphism s, diff --git a/src/category_theory/limits/preserves/basic.lean b/src/category_theory/limits/preserves/basic.lean index 106ec608f6234..82dc5430cca2f 100644 --- a/src/category_theory/limits/preserves/basic.lean +++ b/src/category_theory/limits/preserves/basic.lean @@ -43,8 +43,16 @@ variables {D : Type u₂} [category.{v} D] variables {J : Type v} [small_category J] {K : J ⥤ C} +/-- +A functor `F` preserves limits of shape `K` (written as `preserves_limit K F`) +if `F` maps any limit cone over `K` to a limit cone. +-/ class preserves_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) := (preserves : Π {c : cone K}, is_limit c → is_limit (F.map_cone c)) +/-- +A functor `F` preserves colimits of shape `K` (written as `preserves_colimit K F`) +if `F` maps any colimit cocone over `K` to a colimit cocone. +-/ class preserves_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) := (preserves : Π {c : cocone K}, is_colimit c → is_colimit (F.map_cocone c)) @@ -162,25 +170,54 @@ def preserves_colimit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K simp, end } -/- -A functor F : C → D reflects limits if whenever the image of a cone -under F is a limit cone in D, the cone was already a limit cone in C. -Note that again we do not assume a priori that D actually has any -limits. +/-- +A functor `F : C ⥤ D` reflects limits for `K : J ⥤ C` if +whenever the image of a cone over `K` under `F` is a limit cone in `D`, +the cone was already a limit cone in `C`. +Note that we do not assume a priori that `D` actually has any limits. -/ - class reflects_limit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) := (reflects : Π {c : cone K}, is_limit (F.map_cone c) → is_limit c) +/-- +A functor `F : C ⥤ D` reflects colimits for `K : J ⥤ C` if +whenever the image of a cocone over `K` under `F` is a colimit cocone in `D`, +the cocone was already a colimit cocone in `C`. +Note that we do not assume a priori that `D` actually has any colimits. +-/ class reflects_colimit (K : J ⥤ C) (F : C ⥤ D) : Type (max u₁ u₂ v) := (reflects : Π {c : cocone K}, is_colimit (F.map_cocone c) → is_colimit c) +/-- +A functor `F : C ⥤ D` reflects limits of shape `J` if +whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`, +the cone was already a limit cone in `C`. +Note that we do not assume a priori that `D` actually has any limits. +-/ class reflects_limits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) := (reflects_limit : Π {K : J ⥤ C}, reflects_limit K F) +/-- +A functor `F : C ⥤ D` reflects colimits of shape `J` if +whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`, +the cocone was already a colimit cocone in `C`. +Note that we do not assume a priori that `D` actually has any colimits. +-/ class reflects_colimits_of_shape (J : Type v) [small_category J] (F : C ⥤ D) : Type (max u₁ u₂ v) := (reflects_colimit : Π {K : J ⥤ C}, reflects_colimit K F) +/-- +A functor `F : C ⥤ D` reflects limits if +whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`, +the cone was already a limit cone in `C`. +Note that we do not assume a priori that `D` actually has any limits. +-/ class reflects_limits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := (reflects_limits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_limits_of_shape J F) +/-- +A functor `F : C ⥤ D` reflects colimits if +whenever the image of a cocone over some `K : J ⥤ C` under `F` is a colimit cocone in `D`, +the cocone was already a colimit cocone in `C`. +Note that we do not assume a priori that `D` actually has any colimits. +-/ class reflects_colimits (F : C ⥤ D) : Type (max u₁ u₂ (v+1)) := (reflects_colimits_of_shape : Π {J : Type v} {𝒥 : small_category J}, by exactI reflects_colimits_of_shape J F) @@ -245,6 +282,29 @@ instance comp_reflects_colimit [reflects_colimit K F] [reflects_colimit (K ⋙ F reflects_colimit K (F ⋙ G) := ⟨λ c h, reflects_colimit.reflects (reflects_colimit.reflects h)⟩ +/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`, +then `F` preserves limits for `K`. -/ +def preserves_limit_of_reflects_of_preserves [preserves_limit K (F ⋙ G)] + [reflects_limit (K ⋙ F) G] : preserves_limit K F := +⟨λ c h, + begin + apply @reflects_limit.reflects _ _ _ _ _ _ _ G, + change limits.is_limit ((F ⋙ G).map_cone c), + exact preserves_limit.preserves h + end⟩ + +/-- If `F ⋙ G` preserves colimits for `K`, and `G` reflects colimits for `K ⋙ F`, +then `F` preserves colimits for `K`. -/ +def preserves_colimit_of_reflects_of_preserves [preserves_colimit K (F ⋙ G)] + [reflects_colimit (K ⋙ F) G] : preserves_colimit K F := +⟨λ c h, + begin + apply @reflects_colimit.reflects _ _ _ _ _ _ _ G, + change limits.is_colimit ((F ⋙ G).map_cocone c), + exact preserves_colimit.preserves h + end⟩ + + end variable (F : C ⥤ D) diff --git a/src/category_theory/limits/shapes/types.lean b/src/category_theory/limits/shapes/types.lean index 1c13013a53cbe..ab58304f3b979 100644 --- a/src/category_theory/limits/shapes/types.lean +++ b/src/category_theory/limits/shapes/types.lean @@ -179,6 +179,6 @@ by ext @[simp] lemma sigma_desc {J : Type u} {f : J → Type u} {W : Type u} {g : Π j, f j ⟶ W} {p : Σ j, f j} : (sigma.desc g) p = g p.1 p.2 := rfl @[simp] lemma sigma_map {J : Type u} {f g : J → Type u} {h : Π j, f j ⟶ g j} : - sigma.map h = λ (k : Σ j, f j), (⟨k.1, h k.1 (k.2)⟩ : Σ j, g j) := rfl + limits.sigma.map h = λ (k : Σ j, f j), (⟨k.1, h k.1 (k.2)⟩ : Σ j, g j) := rfl end category_theory.limits.types diff --git a/src/category_theory/limits/types.lean b/src/category_theory/limits/types.lean index b2490c896a1b6..25f956e8b4019 100644 --- a/src/category_theory/limits/types.lean +++ b/src/category_theory/limits/types.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Reid Barton -/ import category_theory.limits.shapes.images +import tactic.equiv_rw universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation @@ -14,44 +15,77 @@ namespace category_theory.limits.types variables {J : Type u} [small_category J] -/-- (internal implementation) the limit cone of a functor, implemented as flat sections of a pi type -/ -def limit_ (F : J ⥤ Type u) : cone F := +/-- +(internal implementation) the limit cone of a functor, +implemented as flat sections of a pi type +-/ +def limit_cone (F : J ⥤ Type u) : cone F := { X := F.sections, π := { app := λ j u, u.val j } } local attribute [elab_simple] congr_fun /-- (internal implementation) the fact that the proposed limit cone is the limit -/ -def limit_is_limit_ (F : J ⥤ Type u) : is_limit (limit_ F) := +def limit_cone_is_limit (F : J ⥤ Type u) : is_limit (limit_cone F) := { lift := λ s v, ⟨λ j, s.π.app j v, λ j j' f, congr_fun (cone.w s f) _⟩, uniq' := by { intros, ext x j, exact congr_fun (w j) x } } instance : has_limits (Type u) := -{ has_limits_of_shape := λ J 𝒥, - { has_limit := λ F, by exactI { cone := limit_ F, is_limit := limit_is_limit_ F } } } - - --- We don't make any of these `simp` lemmas: --- it's up to the user to decide to stop using the limits API, --- and rely on the particular implementation. -lemma types_limit (F : J ⥤ Type u) : - limits.limit F = {u : Π j, F.obj j // ∀ {j j'} f, F.map f (u j) = u j'} := rfl -lemma types_limit_π (F : J ⥤ Type u) (j : J) (g : limit F) : - limit.π F j g = g.val j := rfl -lemma types_limit_pre - (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : limit F) : - limit.pre F E g = (⟨λ k, g.val (E.obj k), by obviously⟩ : limit (E ⋙ F)) := rfl -lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : limit F) : - (lim.map α : limit F → limit G) g = - (⟨λ j, (α.app j) (g.val j), λ j j' f, - by {rw ←functor_to_types.naturality, dsimp, rw ←(g.prop f)}⟩ : limit G) := rfl - -lemma types_limit_lift (F : J ⥤ Type u) (c : cone F) (x : c.X) : - limit.lift F c x = (⟨λ j, c.π.app j x, λ j j' f, congr_fun (cone.w c f) x⟩ : limit F) := +{ has_limits_of_shape := λ J 𝒥, by exactI + { has_limit := λ F, + { cone := limit_cone F, is_limit := limit_cone_is_limit F } } } + +/-- +The equivalence between the abstract limit of `F` in `Type u` +and the "concrete" definition as the sections of `F`. +-/ +def limit_equiv_sections (F : J ⥤ Type u) : (limit F : Type u) ≃ F.sections := +(is_limit.cone_point_unique_up_to_iso (limit.is_limit F) (limit_cone_is_limit F)).to_equiv + +@[simp] +lemma limit_equiv_sections_apply (F : J ⥤ Type u) (x : limit F) (j : J) : + (((limit_equiv_sections F) x) : Π j, F.obj j) j = limit.π F j x := rfl -/-- (internal implementation) the limit cone of a functor, implemented as a quotient of a sigma type -/ -def colimit_ (F : J ⥤ Type u) : cocone F := -{ X := @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2), +@[simp] +lemma limit_equiv_sections_symm_apply (F : J ⥤ Type u) (x : F.sections) (j : J) : + limit.π F j ((limit_equiv_sections F).symm x) = (x : Π j, F.obj j) j := +begin + equiv_rw (limit_equiv_sections F).symm at x, + simp, +end + +-- PROJECT: prove this for concrete categories where the forgetful functor preserves limits +lemma limit_ext (F : J ⥤ Type u) (x y : limit F) (w : ∀ j, limit.π F j x = limit.π F j y) : + x = y := +begin + apply (limit_equiv_sections F).injective, + ext j, + simp [w j], +end + +-- TODO: are there other limits lemmas that should have `_apply` versions? +-- Can we generate these like with `@[reassoc]`? +-- PROJECT: prove these for any concrete category where the forgetful functor preserves limits? +@[simp] +lemma lift_π_apply (F : J ⥤ Type u) (s : cone F) (j : J) (x : s.X) : + limit.π F j (limit.lift F s x) = s.π.app j x := +congr_fun (limit.lift_π s j) x + +/-- +A quotient type implementing the colimit of a functor `F : J ⥤ Type u`, +as pairs `⟨j, x⟩` where `x : F.obj j`, modulo the equivalence relation generated by +`⟨j, x⟩ ~ ⟨j', x'⟩` whenever there is a morphism `f : j ⟶ j'` so `F.map f x = x'`. +-/ +@[nolint has_inhabited_instance] +def quot (F : J ⥤ Type u) : Type u := +@quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2) + +/-- +(internal implementation) the colimit cocone of a functor, +implemented as a quotient of a sigma type +-/ +def colimit_cocone (F : J ⥤ Type u) : cocone F := +{ X := quot F, ι := { app := λ j x, quot.mk _ ⟨j, x⟩, naturality' := λ j j' f, funext $ λ x, eq.symm (quot.sound ⟨f, rfl⟩) } } @@ -59,34 +93,26 @@ def colimit_ (F : J ⥤ Type u) : cocone F := local attribute [elab_with_expected_type] quot.lift /-- (internal implementation) the fact that the proposed colimit cocone is the colimit -/ -def colimit_is_colimit_ (F : J ⥤ Type u) : is_colimit (colimit_ F) := +def colimit_cocone_is_colimit (F : J ⥤ Type u) : is_colimit (colimit_cocone F) := { desc := λ s, quot.lift (λ (p : Σ j, F.obj j), s.ι.app p.1 p.2) (assume ⟨j, x⟩ ⟨j', x'⟩ ⟨f, hf⟩, by rw hf; exact (congr_fun (cocone.w s f) x).symm) } instance : has_colimits (Type u) := -{ has_colimits_of_shape := λ J 𝒥, - { has_colimit := λ F, by exactI { cocone := colimit_ F, is_colimit := colimit_is_colimit_ F } } } - -lemma types_colimit (F : J ⥤ Type u) : - limits.colimit F = @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2) := rfl -lemma types_colimit_ι (F : J ⥤ Type u) (j : J) : - colimit.ι F j = λ x, quot.mk _ ⟨j, x⟩ := rfl -lemma types_colimit_pre - (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) : - colimit.pre F E = - quot.lift (λ p, quot.mk _ ⟨E.obj p.1, p.2⟩) (λ p p' ⟨f, h⟩, quot.sound ⟨E.map f, h⟩) := rfl -lemma types_colimit_map {F G : J ⥤ Type u} (α : F ⟶ G) : - (colim.map α : colimit F → colimit G) = - quot.lift - (λ p, quot.mk _ ⟨p.1, (α.app p.1) p.2⟩) - (λ p p' ⟨f, h⟩, quot.sound ⟨f, by rw h; exact functor_to_types.naturality _ _ α f _⟩) := rfl - -lemma types_colimit_desc (F : J ⥤ Type u) (c : cocone F) : - colimit.desc F c = - quot.lift - (λ p, c.ι.app p.1 p.2) - (λ p p' ⟨f, h⟩, by rw h; exact (functor_to_types.naturality _ _ c.ι f _).symm) := rfl +{ has_colimits_of_shape := λ J 𝒥, by exactI + { has_colimit := λ F, + { cocone := colimit_cocone F, is_colimit := colimit_cocone_is_colimit F } } } + +/-- +The equivalence between the abstract colimit of `F` in `Type u` +and the "concrete" definition as a quotient. +-/ +def colimit_equiv_quot (F : J ⥤ Type u) : (colimit F : Type u) ≃ quot F := +(is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit F) (colimit_cocone_is_colimit F)).to_equiv +@[simp] +lemma colimit_equiv_quot_symm_apply (F : J ⥤ Type u) (j : J) (x : F.obj j) : + (colimit_equiv_quot F).symm (quot.mk _ ⟨j, x⟩) = colimit.ι F j x := +rfl variables {α β : Type u} (f : α ⟶ β)