diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean index ca39de7d7282f..edb277c726718 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean @@ -22,6 +22,7 @@ homotopy equivalence. With this, the fundamental group of `X` based at `x` is ju group of `x`. -/ +open CategoryTheory universe u v diff --git a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean index 151dc7d3893e6..1f775f3b88841 100644 --- a/Mathlib/AlgebraicTopology/TopologicalSimplex.lean +++ b/Mathlib/AlgebraicTopology/TopologicalSimplex.lean @@ -25,7 +25,7 @@ noncomputable section namespace SimplexCategory -open Simplicial NNReal BigOperators Classical +open Simplicial NNReal BigOperators Classical CategoryTheory attribute [local instance] CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.funLike diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean index 63ca2aa258e9f..3fe7ab3f58467 100644 --- a/Mathlib/CategoryTheory/Category/Basic.lean +++ b/Mathlib/CategoryTheory/Category/Basic.lean @@ -20,7 +20,7 @@ Defines a category, as a type class parametrised by the type of objects. ## Notations -Introduces notations +Introduces notations in the `CategoryTheory` scope * `X ⟶ Y` for the morphism spaces (type as `\hom`), * `𝟙 X` for the identity morphism on `X` (type as `\b1`), * `f ≫ g` for composition in the 'arrows' convention (type as `\gg`). @@ -105,10 +105,10 @@ class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + initialize_simps_projections CategoryStruct (-toQuiver_Hom) /-- Notation for the identity morphism in a category. -/ -notation "𝟙" => CategoryStruct.id -- type as \b1 +scoped notation "𝟙" => CategoryStruct.id -- type as \b1 /-- Notation for composition of morphisms in a category. -/ -infixr:80 " ≫ " => CategoryStruct.comp -- type as \gg +scoped infixr:80 " ≫ " => CategoryStruct.comp -- type as \gg /-- A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and @@ -199,13 +199,13 @@ theorem whisker_eq (f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h Notation for whiskering an equation by a morphism (on the right). If `f g : X ⟶ Y` and `w : f = g` and `h : Y ⟶ Z`, then `w =≫ h : f ≫ h = g ≫ h`. -/ -infixr:80 " =≫ " => eq_whisker +scoped infixr:80 " =≫ " => eq_whisker /-- Notation for whiskering an equation by a morphism (on the left). If `g h : Y ⟶ Z` and `w : g = h` and `h : X ⟶ Y`, then `f ≫= w : f ≫ g = f ≫ h`. -/ -infixr:80 " ≫= " => whisker_eq +scoped infixr:80 " ≫= " => whisker_eq theorem eq_of_comp_left_eq {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) : f = g := by diff --git a/Mathlib/CategoryTheory/Category/Preorder.lean b/Mathlib/CategoryTheory/Category/Preorder.lean index 9181d62e38059..e3109d68e2e83 100644 --- a/Mathlib/CategoryTheory/Category/Preorder.lean +++ b/Mathlib/CategoryTheory/Category/Preorder.lean @@ -130,6 +130,8 @@ end CategoryTheory section +open CategoryTheory + variable {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] /-- A monotone function between preorders induces a functor between the associated categories. diff --git a/Mathlib/CategoryTheory/Functor/Basic.lean b/Mathlib/CategoryTheory/Functor/Basic.lean index 1932f22853be0..70d7323b5ada0 100644 --- a/Mathlib/CategoryTheory/Functor/Basic.lean +++ b/Mathlib/CategoryTheory/Functor/Basic.lean @@ -16,9 +16,10 @@ import Mathlib.CategoryTheory.Category.Basic Defines a functor between categories, extending a `Prefunctor` between quivers. -Introduces notation `C ⥤ D` for the type of all functors from `C` to `D`. -(Unfortunately the `⇒` arrow (`\functor`) is taken by core, -but in mathlib4 we should switch to this.) +Introduces, in the `CategoryTheory` scope, notations `C ⥤ D` for the type of all functors +from `C` to `D`, `𝟭` for the identity functor and `⋙` for functor composition. + +TODO: Switch to using the `⇒` arrow. -/ @@ -58,7 +59,7 @@ end /-- Notation for a functor between categories. -/ -- A functor is basically a function, so give ⥤ a similar precedence to → (25). -- For example, `C × D ⥤ E` should parse as `(C × D) ⥤ E` not `C × (D ⥤ E)`. -infixr:26 " ⥤ " => Functor -- type as \func +scoped [CategoryTheory] infixr:26 " ⥤ " => Functor -- type as \func attribute [simp] Functor.map_id Functor.map_comp @@ -87,7 +88,7 @@ protected def id : C ⥤ C where #align category_theory.functor.id CategoryTheory.Functor.id /-- Notation for the identity functor on a category. -/ -notation "𝟭" => Functor.id -- Type this as `\sb1` +scoped [CategoryTheory] notation "𝟭" => Functor.id -- Type this as `\sb1` instance : Inhabited (C ⥤ C) := ⟨Functor.id C⟩ @@ -120,7 +121,7 @@ def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where #align category_theory.functor.comp_obj CategoryTheory.Functor.comp_obj /-- Notation for composition of functors. -/ -infixr:80 " ⋙ " => comp +scoped [CategoryTheory] infixr:80 " ⋙ " => Functor.comp @[simp] theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) : diff --git a/Mathlib/Combinatorics/Hall/Basic.lean b/Mathlib/Combinatorics/Hall/Basic.lean index 82a98b4b063cf..ad0e8fc3d83ce 100644 --- a/Mathlib/Combinatorics/Hall/Basic.lean +++ b/Mathlib/Combinatorics/Hall/Basic.lean @@ -56,7 +56,7 @@ Hall's Marriage Theorem, indexed families -/ -open Finset +open Finset CategoryTheory universe u v diff --git a/Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean index 994102d1cdc47..3c933d6caaf6b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean @@ -36,7 +36,7 @@ finite subgraphs `G'' ≤ G'`, the inverse system `finsubgraphHomFunctor` restri -/ -open Set +open Set CategoryTheory universe u v diff --git a/Mathlib/Topology/Sheaves/Sheafify.lean b/Mathlib/Topology/Sheaves/Sheafify.lean index cda49b1b1e2ea..c03863e37ab66 100644 --- a/Mathlib/Topology/Sheaves/Sheafify.lean +++ b/Mathlib/Topology/Sheaves/Sheafify.lean @@ -37,11 +37,7 @@ universe v noncomputable section -open TopCat - -open Opposite - -open TopologicalSpace +open TopCat Opposite TopologicalSpace CategoryTheory variable {X : TopCat.{v}} (F : Presheaf (Type v) X)