chore: scope notations from category theory. (#5685)

Make sure in particular one can import Mathlib.Tactic for teaching without getting category theory notations in scope. Note that only two files needed an extra open.
leanprover-community · Jul 3, 2023 · 5c108f1 · 5c108f1
1 parent db9fb24
commit 5c108f1
Show file tree

Hide file tree

Showing 8 changed files with 19 additions and 19 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)