From cd7a8a184d7c5635e30083eabc4baf5589c30b7a Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Tue, 12 Jan 2021 08:26:45 +0000 Subject: [PATCH] chore(category_theory/limits): move constructions folder (#5681) As mentioned here: https://github.com/leanprover-community/mathlib/pull/5516#issuecomment-753450199 The linter is giving new errors, so I might as well fix them in this PR. --- src/category_theory/abelian/basic.lean | 2 +- .../constructions/binary_products.lean | 4 +- .../constructions/equalizers.lean | 0 .../limits_of_products_and_equalizers.lean | 0 .../constructions/over/connected.lean | 7 +++- .../constructions/over/default.lean | 14 +++++-- .../constructions/over/products.lean | 39 +++++++++++++------ .../{shapes => }/constructions/pullbacks.lean | 4 +- .../omega_complete_partial_order.lean | 2 +- 9 files changed, 49 insertions(+), 23 deletions(-) rename src/category_theory/limits/{shapes => }/constructions/binary_products.lean (100%) rename src/category_theory/limits/{shapes => }/constructions/equalizers.lean (100%) rename src/category_theory/limits/{shapes => }/constructions/limits_of_products_and_equalizers.lean (100%) rename src/category_theory/limits/{shapes => }/constructions/over/connected.lean (92%) rename src/category_theory/limits/{shapes => }/constructions/over/default.lean (78%) rename src/category_theory/limits/{shapes => }/constructions/over/products.lean (81%) rename src/category_theory/limits/{shapes => }/constructions/pullbacks.lean (100%) diff --git a/src/category_theory/abelian/basic.lean b/src/category_theory/abelian/basic.lean index 5e77f61b78f5e..dbb2f1e6beccb 100644 --- a/src/category_theory/abelian/basic.lean +++ b/src/category_theory/abelian/basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Markus Himmel -/ -import category_theory.limits.shapes.constructions.pullbacks +import category_theory.limits.constructions.pullbacks import category_theory.limits.shapes.biproducts import category_theory.limits.shapes.images import category_theory.abelian.non_preadditive diff --git a/src/category_theory/limits/shapes/constructions/binary_products.lean b/src/category_theory/limits/constructions/binary_products.lean similarity index 100% rename from src/category_theory/limits/shapes/constructions/binary_products.lean rename to src/category_theory/limits/constructions/binary_products.lean index db9d17bacbde0..ec481c4814597 100644 --- a/src/category_theory/limits/shapes/constructions/binary_products.lean +++ b/src/category_theory/limits/constructions/binary_products.lean @@ -7,8 +7,6 @@ import category_theory.limits.shapes.terminal import category_theory.limits.shapes.pullbacks import category_theory.limits.shapes.binary_products -universes v u - /-! # Constructing binary product from pullbacks and terminal object. @@ -17,6 +15,8 @@ If a category has pullbacks and a terminal object, then it has binary products. TODO: provide the dual result. -/ +universes v u + open category_theory category_theory.category category_theory.limits /-- Any category with pullbacks and terminal object has binary products. -/ diff --git a/src/category_theory/limits/shapes/constructions/equalizers.lean b/src/category_theory/limits/constructions/equalizers.lean similarity index 100% rename from src/category_theory/limits/shapes/constructions/equalizers.lean rename to src/category_theory/limits/constructions/equalizers.lean diff --git a/src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean b/src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean similarity index 100% rename from src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean rename to src/category_theory/limits/constructions/limits_of_products_and_equalizers.lean diff --git a/src/category_theory/limits/shapes/constructions/over/connected.lean b/src/category_theory/limits/constructions/over/connected.lean similarity index 92% rename from src/category_theory/limits/shapes/constructions/over/connected.lean rename to src/category_theory/limits/constructions/over/connected.lean index f4fdbb9edf374..4a9b1f6b2a657 100644 --- a/src/category_theory/limits/shapes/constructions/over/connected.lean +++ b/src/category_theory/limits/constructions/over/connected.lean @@ -8,8 +8,10 @@ import category_theory.limits.connected import category_theory.limits.creates /-! -# `forget : over B ⥤ C` creates connected limits. +# Connected limits in the over category +Shows that the forgetful functor `over B ⥤ C` creates connected limits, in particular `over B` has +any connected limit which `C` has. -/ universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation @@ -54,7 +56,8 @@ lemma raised_cone_lowers_to_original [is_connected J] {B : C} {F : J ⥤ over B} by tidy /-- (Impl) Show that the raised cone is a limit. -/ -def raised_cone_is_limit [is_connected J] {B : C} {F : J ⥤ over B} {c : cone (F ⋙ forget B)} (t : is_limit c) : +def raised_cone_is_limit [is_connected J] {B : C} {F : J ⥤ over B} + {c : cone (F ⋙ forget B)} (t : is_limit c) : is_limit (raise_cone c) := { lift := λ s, over.hom_mk (t.lift ((forget B).map_cone s)) (by { dsimp, simp }), uniq' := λ s m K, by { ext1, apply t.hom_ext, intro j, simp [← K j] } } diff --git a/src/category_theory/limits/shapes/constructions/over/default.lean b/src/category_theory/limits/constructions/over/default.lean similarity index 78% rename from src/category_theory/limits/shapes/constructions/over/default.lean rename to src/category_theory/limits/constructions/over/default.lean index aaf423724db3b..d40b6d39f3fec 100644 --- a/src/category_theory/limits/shapes/constructions/over/default.lean +++ b/src/category_theory/limits/constructions/over/default.lean @@ -3,11 +3,17 @@ Copyright (c) 2018 Johan Commelin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Reid Barton, Bhavik Mehta -/ -import category_theory.limits.shapes.constructions.over.products -import category_theory.limits.shapes.constructions.over.connected -import category_theory.limits.shapes.constructions.limits_of_products_and_equalizers -import category_theory.limits.shapes.constructions.equalizers +import category_theory.limits.constructions.over.products +import category_theory.limits.constructions.over.connected +import category_theory.limits.constructions.limits_of_products_and_equalizers +import category_theory.limits.constructions.equalizers +/-! +# Limits in the over category + +Declare instances for limits in the over category: If `C` has finite wide pullbacks, `over B` has +finite limits, and if `C` has arbitrary wide pullbacks then `over B` has limits. +-/ universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation open category_theory category_theory.limits diff --git a/src/category_theory/limits/shapes/constructions/over/products.lean b/src/category_theory/limits/constructions/over/products.lean similarity index 81% rename from src/category_theory/limits/shapes/constructions/over/products.lean rename to src/category_theory/limits/constructions/over/products.lean index eb7e52b036498..e4a1f3cb0764b 100644 --- a/src/category_theory/limits/shapes/constructions/over/products.lean +++ b/src/category_theory/limits/constructions/over/products.lean @@ -8,11 +8,18 @@ import category_theory.limits.shapes.pullbacks import category_theory.limits.shapes.wide_pullbacks import category_theory.limits.shapes.finite_products +/-! +# Products in the over category + +Shows that products in the over category can be derived from wide pullbacks in the base category. +The main result is `over_product_of_wide_pullback`, which says that if `C` has `J`-indexed wide +pullbacks, then `over B` has `J`-indexed products. +-/ universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation open category_theory category_theory.limits -variables {J : Type v} [small_category J] +variables {J : Type v} variables {C : Type u} [category.{v} C] variable {X : C} @@ -20,9 +27,14 @@ namespace category_theory.over namespace construct_products -/-- (Impl) Given a product shape in `C/B`, construct the corresponding wide pullback diagram in `C`. -/ +/-- +(Implementation) +Given a product diagram in `C/B`, construct the corresponding wide pullback diagram +in `C`. +-/ @[reducible] -def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) : wide_pullback_shape J ⥤ C := +def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) : + wide_pullback_shape J ⥤ C := wide_pullback_shape.wide_cospan B (λ j, (F.obj j).left) (λ j, (F.obj j).hom) /-- (Impl) A preliminary definition to avoid timeouts. -/ @@ -63,7 +75,9 @@ def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) : cone (wide_pullback_diagram_of_diagram_over B F) ⥤ cone F := { obj := λ c, { X := over.mk (c.π.app none), - π := { app := λ j, over.hom_mk (c.π.app (some j)) (by apply c.w (wide_pullback_shape.hom.term j)) } }, + π := + { app := λ j, over.hom_mk (c.π.app (some j)) + (by apply c.w (wide_pullback_shape.hom.term j)) } }, map := λ c₁ c₂ f, { hom := over.hom_mk f.hom } } @@ -71,22 +85,25 @@ local attribute [tidy] tactic.case_bash /-- (Impl) A preliminary definition to avoid timeouts. -/ @[simp] -def cones_equiv_unit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) : +def cones_equiv_unit_iso (B : C) (F : discrete J ⥤ over B) : 𝟭 (cone (wide_pullback_diagram_of_diagram_over B F)) ≅ cones_equiv_functor B F ⋙ cones_equiv_inverse B F := nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy) /-- (Impl) A preliminary definition to avoid timeouts. -/ @[simp] -def cones_equiv_counit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) : +def cones_equiv_counit_iso (B : C) (F : discrete J ⥤ over B) : cones_equiv_inverse B F ⋙ cones_equiv_functor B F ≅ 𝟭 (cone F) := nat_iso.of_components (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy) --- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and `cones.ext`? -/-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`. -/ +-- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and +-- `cones.ext`? +/-- +(Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`. +-/ @[simps] -def cones_equiv (B : C) {J : Type v} (F : discrete J ⥤ over B) : +def cones_equiv (B : C) (F : discrete J ⥤ over B) : cone (wide_pullback_diagram_of_diagram_over B F) ≌ cone F := { functor := cones_equiv_functor B F, inverse := cones_equiv_inverse B F, @@ -94,7 +111,7 @@ def cones_equiv (B : C) {J : Type v} (F : discrete J ⥤ over B) : counit_iso := cones_equiv_counit_iso B F, } /-- Use the above equivalence to prove we have a limit. -/ -lemma has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : discrete J ⥤ over B) +lemma has_over_limit_discrete_of_wide_pullback_limit {B : C} (F : discrete J ⥤ over B) [has_limit (wide_pullback_diagram_of_diagram_over B F)] : has_limit F := has_limit.mk @@ -103,7 +120,7 @@ has_limit.mk (cones_equiv B F).functor (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) } /-- Given a wide pullback in `C`, construct a product in `C/B`. -/ -lemma over_product_of_wide_pullback {J : Type v} [has_limits_of_shape (wide_pullback_shape J) C] {B : C} : +lemma over_product_of_wide_pullback [has_limits_of_shape (wide_pullback_shape J) C] {B : C} : has_limits_of_shape (discrete J) (over B) := { has_limit := λ F, has_over_limit_discrete_of_wide_pullback_limit F } diff --git a/src/category_theory/limits/shapes/constructions/pullbacks.lean b/src/category_theory/limits/constructions/pullbacks.lean similarity index 100% rename from src/category_theory/limits/shapes/constructions/pullbacks.lean rename to src/category_theory/limits/constructions/pullbacks.lean index 5604d42183041..ab1562ce95345 100644 --- a/src/category_theory/limits/shapes/constructions/pullbacks.lean +++ b/src/category_theory/limits/constructions/pullbacks.lean @@ -7,8 +7,6 @@ import category_theory.limits.shapes.binary_products import category_theory.limits.shapes.equalizers import category_theory.limits.shapes.pullbacks -universes v u - /-! # Constructing pullbacks from binary products and equalizers @@ -16,6 +14,8 @@ If a category as binary products and equalizers, then it has pullbacks. Also, if a category has binary coproducts and coequalizers, then it has pushouts -/ +universes v u + open category_theory namespace category_theory.limits diff --git a/src/order/category/omega_complete_partial_order.lean b/src/order/category/omega_complete_partial_order.lean index 28b43a09519cc..570f8ac395084 100644 --- a/src/order/category/omega_complete_partial_order.lean +++ b/src/order/category/omega_complete_partial_order.lean @@ -8,7 +8,7 @@ import order.omega_complete_partial_order import order.category.Preorder import category_theory.limits.shapes.products import category_theory.limits.shapes.equalizers -import category_theory.limits.shapes.constructions.limits_of_products_and_equalizers +import category_theory.limits.constructions.limits_of_products_and_equalizers /-! # Category of types with a omega complete partial order