Skip to content

Commit

Permalink
chore(CategoryTheory): move file about abelian sheaf categories to co…
Browse files Browse the repository at this point in the history
…rrect location (#12216)
  • Loading branch information
dagurtomas committed Apr 18, 2024
1 parent dc34930 commit 706b883
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 4 deletions.
2 changes: 1 addition & 1 deletion Mathlib.lean
Expand Up @@ -1461,6 +1461,7 @@ import Mathlib.CategoryTheory.Shift.ShiftSequence
import Mathlib.CategoryTheory.Sigma.Basic
import Mathlib.CategoryTheory.Simple
import Mathlib.CategoryTheory.SingleObj
import Mathlib.CategoryTheory.Sites.Abelian
import Mathlib.CategoryTheory.Sites.Adjunction
import Mathlib.CategoryTheory.Sites.Canonical
import Mathlib.CategoryTheory.Sites.Closed
Expand Down Expand Up @@ -4065,7 +4066,6 @@ import Mathlib.Topology.Sets.Closeds
import Mathlib.Topology.Sets.Compacts
import Mathlib.Topology.Sets.Opens
import Mathlib.Topology.Sets.Order
import Mathlib.Topology.Sheaves.Abelian
import Mathlib.Topology.Sheaves.Forget
import Mathlib.Topology.Sheaves.Functors
import Mathlib.Topology.Sheaves.Init
Expand Down
Expand Up @@ -18,8 +18,6 @@ sheafification is possible in `C`, `Sheaf J D` is abelian as well (`sheafIsAbeli
Hence, `presheafToSheaf` is an additive functor (`presheafToSheaf_additive`).
TODO: This file should be moved to `CategoryTheory/Sites`.
-/


Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Condensed/Abelian.lean
Expand Up @@ -3,9 +3,9 @@ Copyright (c) 2023 Adam Topaz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz
-/
import Mathlib.Topology.Sheaves.Abelian
import Mathlib.Algebra.Category.GroupCat.Abelian
import Mathlib.Algebra.Category.GroupCat.FilteredColimits
import Mathlib.CategoryTheory.Sites.Abelian
import Mathlib.Condensed.Basic

/-!
Expand Down

0 comments on commit 706b883

Please sign in to comment.