Locally bijective morphisms of presheaves #
Let C a be category equipped with a Grothendieck topology J.
Let A be a concrete category.
In this file, we introduce a type-class J.WEqualsLocallyBijective A which says
that the class J.W (of morphisms of presheaves which become isomorphisms
after sheafification) is the class of morphisms that are both locally injective
and locally surjective (i.e. locally bijective). We prove that this holds iff
for any presheaf P : Cᵒᵖ ⥤ A, the sheafification map toSheafify J P is locally bijective.
We show that this holds under certain universe assumptions.
theorem
CategoryTheory.Sheaf.isLocallyBijective_iff_isIso
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
{F G : Sheaf J A}
(f : F ⟶ G)
[(forget A).ReflectsIsomorphisms]
[J.HasSheafCompose (forget A)]
:
class
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(A : Type u')
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
:
Given a category C equipped with a Grothendieck topology J and a concrete category A,
this property holds if a morphism in Cᵒᵖ ⥤ A satisfies J.W (i.e. becomes an iso after
sheafification) iff it is both locally injective and locally surjective.
- iff {X Y : Functor Cᵒᵖ A} (f : X ⟶ Y) : J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
Instances
theorem
CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
{X Y : Functor Cᵒᵖ A}
(f : X ⟶ Y)
:
theorem
CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
{X Y : Functor Cᵒᵖ A}
(f : X ⟶ Y)
[Presheaf.IsLocallyInjective J f]
[Presheaf.IsLocallySurjective J f]
:
J.W f
theorem
CategoryTheory.GrothendieckTopology.W.isLocallyInjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
{X Y : Functor Cᵒᵖ A}
{f : X ⟶ Y}
(hf : J.W f)
:
theorem
CategoryTheory.GrothendieckTopology.W.isLocallySurjective
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
{X Y : Functor Cᵒᵖ A}
{f : X ⟶ Y}
(hf : J.W f)
:
instance
CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
[HasWeakSheafify J A]
(P : Functor Cᵒᵖ A)
:
instance
CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify
{C : Type u}
[Category.{v, u} C]
{J : GrothendieckTopology C}
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[J.WEqualsLocallyBijective A]
[HasWeakSheafify J A]
(P : Functor Cᵒᵖ A)
:
theorem
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk'
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
(A : Type u')
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[HasWeakSheafify J A]
[(forget A).ReflectsIsomorphisms]
[J.HasSheafCompose (forget A)]
[∀ (P : Functor Cᵒᵖ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)]
[∀ (P : Functor Cᵒᵖ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)]
:
instance
CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{D : Type w}
[Category.{w', w} D]
{FD : D → D → Type u_2}
{CD : D → Type (max u v)}
[(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
[ConcreteCategory D FD]
[HasWeakSheafify J D]
[J.HasSheafCompose (forget D)]
[J.PreservesSheafification (forget D)]
[(forget D).ReflectsIsomorphisms]
:
instance
CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHomObjForget
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
:
J.WEqualsLocallyBijective (Type (max u v))
theorem
CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[HasWeakSheafify J A]
[J.WEqualsLocallyBijective A]
{P Q : Functor Cᵒᵖ A}
(φ : P ⟶ Q)
:
theorem
CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff
{C : Type u}
[Category.{v, u} C]
(J : GrothendieckTopology C)
{A : Type u'}
[Category.{v', u'} A]
{FA : A → A → Type u_1}
{CA : A → Type w'}
[(X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
[ConcreteCategory A FA]
[HasWeakSheafify J A]
[J.WEqualsLocallyBijective A]
{P Q : Functor Cᵒᵖ A}
(φ : P ⟶ Q)
: