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} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G) [(CategoryTheory.forget A).ReflectsIsomorphisms] [J.HasSheafCompose (CategoryTheory.forget A)] : CategoryTheory.Sheaf.IsLocallyInjective f ∧ CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.IsIso f

class CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] : Prop

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 : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y), J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f

theorem CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) : J.W f ↔ CategoryTheory.Presheaf.IsLocallyInjective J f ∧ CategoryTheory.Presheaf.IsLocallySurjective J f

theorem CategoryTheory.GrothendieckTopology.W_of_isLocallyBijective {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} (f : X ⟶ Y) [CategoryTheory.Presheaf.IsLocallyInjective J f] [CategoryTheory.Presheaf.IsLocallySurjective J f] : J.W f

theorem CategoryTheory.GrothendieckTopology.W.isLocallyInjective {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} {f : X ⟶ Y} (hf : J.W f) : CategoryTheory.Presheaf.IsLocallyInjective J f

theorem CategoryTheory.GrothendieckTopology.W.isLocallySurjective {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} {f : X ⟶ Y} (hf : J.W f) : CategoryTheory.Presheaf.IsLocallySurjective J f

instance CategoryTheory.GrothendieckTopology.instIsLocallyInjectiveToSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] [CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)

Equations

• ⋯ = ⋯

instance CategoryTheory.GrothendieckTopology.instIsLocallySurjectiveToSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [J.WEqualsLocallyBijective A] [CategoryTheory.HasWeakSheafify J A] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)

Equations

• ⋯ = ⋯

theorem CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.HasWeakSheafify J A] [(CategoryTheory.forget A).ReflectsIsomorphisms] [J.HasSheafCompose (CategoryTheory.forget A)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)] [∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)] : J.WEqualsLocallyBijective A

instance CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.HasWeakSheafify J D] [J.HasSheafCompose (CategoryTheory.forget D)] [J.PreservesSheafification (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : J.WEqualsLocallyBijective D

Equations

• ⋯ = ⋯

instance CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveType {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : J.WEqualsLocallyBijective (Type (max u v))

Equations

• ⋯ = ⋯

theorem CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (φ : P ⟶ Q) : CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallyInjective J φ

theorem CategoryTheory.Presheaf.isLocallySurjective_presheafToSheaf_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.ConcreteCategory A] [CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (φ : P ⟶ Q) : CategoryTheory.Sheaf.IsLocallySurjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔ CategoryTheory.Presheaf.IsLocallySurjective J φ