feat: fix namespaces

sinhp · Nov 17, 2024 · 9256c08 · 9256c08
1 parent 69744a3
commit 9256c08
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 43 deletions.
diff --git a/GroupoidModel/Groupoids/GroupoidNaturalModel.lean b/GroupoidModel/Groupoids/GroupoidNaturalModel.lean
@@ -9,8 +9,7 @@ Here we construct the natural model for groupoids.
 
 universe u v u₁ v₁ u₂ v₂
 
-namespace CategoryTheory
-
+open CategoryTheory
 noncomputable section
 
 -- Here I am using sGrpd to be a small category version of Grpd. There is likely a better way to do this.

diff --git a/GroupoidModel/Groupoids/GroupoidalGrothendieck.lean b/GroupoidModel/Groupoids/GroupoidalGrothendieck.lean
@@ -8,7 +8,6 @@ Here we define the Grothendieck construction for groupoids
 universe u v u₁ v₁ u₂ v₂
 
 namespace CategoryTheory
-
 noncomputable section
 
 @[simps!]
@@ -109,3 +108,7 @@ def functorial {C D : Grpd.{v₁,u₁}} (F : C ⟶ D) (G : D ⥤ Grpd.{v₂,u₂
 end GroupoidalGrothendieck
 
 end
+end
+
+end CategoryTheory
+
diff --git a/GroupoidModel/Groupoids/PointedCat.lean b/GroupoidModel/Groupoids/PointedCat.lean
@@ -238,3 +238,5 @@ lemma comp_point {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) :
 end PGrpd
 
 end PointedCategories
+
+end CategoryTheory
diff --git a/GroupoidModel/Groupoids/PullBackProofs.lean b/GroupoidModel/Groupoids/PullBackProofs.lean
@@ -658,3 +658,7 @@ def PshGrpdPB {Γ : Grpd.{u,u}}(A : Γ ⥤ Grpd.{u,u}) : @IsPullback (Grpd.{u,u}
   (PshGrpd.map ((Down_uni (GroupoidalGrothendieck A)) ⋙ (GroupoidalGrothendieck.forget) ⋙ (Up_uni Γ)))
   (PshGrpd.map (PGrpd.forgetPoint))
   (PshGrpd.map ((Down_uni Γ) ⋙ A)) := Functor.map_isPullback PshGrpd (PBasPB A)
+
+end
+
+end CategoryTheory
diff --git a/blueprint/src/chapter/groupoid_model.tex b/blueprint/src/chapter/groupoid_model.tex
@@ -42,6 +42,7 @@ \subsection{Classifying display maps}
 
 \begin{defn}[The display map classifier]
   \label{tp_defn}
+  \lean{CategoryTheory.GroupoidNM} \leanok %%This should probably just be GroupoidNM or GroupoidNM.Base
   We would like to define a natural transformation in
   $\Pshgrpd$
   \[ \tp \co \Term \to \Type \]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -110,46 +110,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "groupoid_model",
  "lakeDir": ".lake"}
Original file line number	Diff line number	Diff line change
Expand Up		@@ -238,3 +238,5 @@ lemma comp_point {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) :
		end PGrpd

		end PointedCategories

		end CategoryTheory