Documentation

Mathlib.CategoryTheory.Sites.LocallyBijective

Locally bijective morphisms of presheaves #

Let C be a 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.

source
๐Ÿ“ coverage
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)] :
IsLocallyInjective f โˆง IsLocallySurjective f โ†” IsIso f
source
๐Ÿ”ถ coverage
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] :
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.

Instances
    source
    ๐Ÿ“ coverage
    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) :
    J.W f โ†” Presheaf.IsLocallyInjective J f โˆง Presheaf.IsLocallySurjective J f
    source
    ๐Ÿ“ coverage
    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
    source
    ๐Ÿ“ coverage
    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) :
    Presheaf.IsLocallyInjective J f
    source
    ๐Ÿ“ coverage
    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) :
    Presheaf.IsLocallySurjective J f
    source
    ๐Ÿ“ coverage
    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) :
    Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)
    source
    ๐Ÿ“ coverage
    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) :
    Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)
    source
    ๐Ÿ“ coverage
    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)] :
    J.WEqualsLocallyBijective A
    source
    ๐Ÿ“ coverage
    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] :
    J.WEqualsLocallyBijective D
    source
    ๐Ÿ“ coverage
    instance CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveTypeHom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) :
    J.WEqualsLocallyBijective (Type (max u v))
    source
    ๐Ÿ“ coverage
    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) :
    Sheaf.IsLocallyInjective ((presheafToSheaf J A).map ฯ†) โ†” IsLocallyInjective J ฯ†
    source
    ๐Ÿ“ coverage
    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) :
    Sheaf.IsLocallySurjective ((presheafToSheaf J A).map ฯ†) โ†” IsLocallySurjective J ฯ†