Localization
In this file, given a Grothendieck topology J on a category C and X : C, we construct
a Grothendieck topology J.over X on the category Over X. In order to do this,
we first construct a bijection Sieve.overEquiv Y : Sieve Y ≃ Sieve Y.left
for all Y : Over X. Then, as it is stated in SGA 4 III 5.2.1, a sieve of Y : Over X
is covering for J.over X if and only if the corresponding sieve of Y.left
is covering for J. As a result, the forgetful functor
Over.forget X : Over X ⥤ X is both cover-preserving and cover-lifting.
def
CategoryTheory.Sieve.overEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
(Y : CategoryTheory.Over X)
:
CategoryTheory.Sieve Y ≃ CategoryTheory.Sieve Y.left
The equivalence Sieve Y ≃ Sieve Y.left for all Y : Over X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Sieve.overEquiv_top
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
(Y : CategoryTheory.Over X)
:
@[simp]
theorem
CategoryTheory.Sieve.overEquiv_symm_top
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
(Y : CategoryTheory.Over X)
:
(CategoryTheory.Sieve.overEquiv Y).symm ⊤ = ⊤
theorem
CategoryTheory.Sieve.overEquiv_pullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y₁ : CategoryTheory.Over X}
{Y₂ : CategoryTheory.Over X}
(f : Y₁ ⟶ Y₂)
(S : CategoryTheory.Sieve Y₂)
:
(CategoryTheory.Sieve.overEquiv Y₁) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f.left ((CategoryTheory.Sieve.overEquiv Y₂) S)
@[simp]
theorem
CategoryTheory.Sieve.overEquiv_symm_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : CategoryTheory.Over X}
(S : CategoryTheory.Sieve Y.left)
{Z : CategoryTheory.Over X}
(f : Z ⟶ Y)
:
((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f ↔ S.arrows f.left
theorem
CategoryTheory.Sieve.overEquiv_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : CategoryTheory.Over X}
(S : CategoryTheory.Sieve Y)
{Z : C}
(f : Z ⟶ Y.left)
:
((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)
@[simp]
theorem
CategoryTheory.Sieve.functorPushforward_over_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(Z : CategoryTheory.Over X)
(S : CategoryTheory.Sieve Z.left)
:
CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map f) ((CategoryTheory.Sieve.overEquiv Z).symm S) = (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.map f).obj Z)).symm S
def
CategoryTheory.GrothendieckTopology.over
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(X : C)
:
The Grothendieck topology on the category Over X for any X : C that is
induced by a Grothendieck topology on C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.GrothendieckTopology.mem_over_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
{Y : CategoryTheory.Over X}
(S : CategoryTheory.Sieve Y)
:
S ∈ (J.over X).sieves Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J.sieves Y.left
theorem
CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
(Y : CategoryTheory.Over X)
(S : CategoryTheory.Sieve Y.left)
(hS : S ∈ J.sieves Y.left)
:
(CategoryTheory.Sieve.overEquiv Y).symm S ∈ (J.over X).sieves Y
theorem
CategoryTheory.GrothendieckTopology.over_forget_coverPreserving
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(X : C)
:
CategoryTheory.CoverPreserving (J.over X) J (CategoryTheory.Over.forget X)
instance
CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(X : C)
:
(CategoryTheory.Over.forget X).IsCocontinuous (J.over X) J
Equations
- ⋯ = ⋯
instance
CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(X : C)
:
(CategoryTheory.Over.forget X).IsContinuous (J.over X) J
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.GrothendieckTopology.overPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(A : Type u')
[CategoryTheory.Category.{v', u'} A]
(X : C)
:
CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf (J.over X) A)
The pullback functor Sheaf J A ⥤ Sheaf (J.over X) A
Equations
- J.overPullback A X = (CategoryTheory.Over.forget X).sheafPushforwardContinuous A (J.over X) J
Instances For
theorem
CategoryTheory.GrothendieckTopology.over_map_coverPreserving
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.CoverPreserving (J.over X) (J.over Y) (CategoryTheory.Over.map f)
theorem
CategoryTheory.GrothendieckTopology.over_map_compatiblePreserving
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.CompatiblePreserving (J.over Y) (CategoryTheory.Over.map f)
instance
CategoryTheory.GrothendieckTopology.instIsContinuousOverMapOver
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.Over.map f).IsContinuous (J.over X) (J.over Y)
Equations
- ⋯ = ⋯
@[reducible, inline]
abbrev
CategoryTheory.GrothendieckTopology.overMapPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(J : CategoryTheory.GrothendieckTopology C)
(A : Type u')
[CategoryTheory.Category.{v', u'} A]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)
The pullback functor Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A induced
by a morphism f : X ⟶ Y.
Equations
- J.overMapPullback A f = (CategoryTheory.Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)