Documentation

Mathlib.CategoryTheory.Sites.LocallySurjective

Locally surjective morphisms #

Main definitions #

Main results #

source
๐Ÿ”ธ coverage
def CategoryTheory.Presheaf.imageSieve {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : C} (s : ToType (G.obj (Opposite.op U))) :
Sieve U

Given f : F โŸถ G, a morphism between presieves, and s : G.obj (op U), this is the sieve of U consisting of the i : V โŸถ U such that s restricted along i is in the image of f.

Equations
    Instances For
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.Presheaf.imageSieve_apply {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : C} (s : ToType (G.obj (Opposite.op U))) (V : C) (i : V โŸถ U) :
      (imageSieve f s).arrows i = โˆƒ (t : ToType (F.obj (Opposite.op V))), (ConcreteCategory.hom (f.app (Opposite.op V))) t = (ConcreteCategory.hom (G.map i.op)) s
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : C} (s : ToType (G.obj (Opposite.op U))) :
      imageSieve f s = (Subfunctor.range (Functor.whiskerRight f (forget A))).sieveOfSection s
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.Presheaf.imageSieve_whisker_forget {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : C} (s : ToType (G.obj (Opposite.op U))) :
      imageSieve (Functor.whiskerRight f (forget A)) s = imageSieve f s
      source
      ๐Ÿ“ coverage
      theorem CategoryTheory.Presheaf.imageSieve_app {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : C} (s : ToType (F.obj (Opposite.op U))) :
      imageSieve f ((ConcreteCategory.hom (f.app (Opposite.op U))) s) = โŠค
      source
      ๐Ÿ”ธ coverage
      noncomputable def CategoryTheory.Presheaf.localPreimage {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : Cแต’แต–} (s : ToType (G.obj U)) {V : C} (g : V โŸถ Opposite.unop U) (hg : (imageSieve f s).arrows g) :
      ToType (F.obj (Opposite.op V))

      If a morphism g : V โŸถ U.unop belongs to the sieve imageSieve f s g, then this is choice of a preimage of G.map g.op s in F.obj (op V), see app_localPreimage.

      Equations
        Instances For
          source
          ๐Ÿ“ coverage
          @[simp]
          theorem CategoryTheory.Presheaf.app_localPreimage {C : Type u} [Category.{v, u} 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 : Functor Cแต’แต– A} (f : F โŸถ G) {U : Cแต’แต–} (s : ToType (G.obj U)) {V : C} (g : V โŸถ Opposite.unop U) (hg : (imageSieve f s).arrows g) :
          (ConcreteCategory.hom (f.app (Opposite.op V))) (localPreimage f s g hg) = (ConcreteCategory.hom (G.map g.op)) s
          source
          ๐Ÿ”ถ coverage
          class CategoryTheory.Presheaf.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] {F G : Functor Cแต’แต– A} (f : F โŸถ G) :
          Prop

          A morphism of presheaves f : F โŸถ G is locally surjective with respect to a Grothendieck topology if every section of G is locally in the image of f.

          Instances
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.imageSieve_mem {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 : Functor Cแต’แต– A} (f : F โŸถ G) [IsLocallySurjective J f] {U : Cแต’แต–} (s : ToType (G.obj U)) :
            imageSieve f s โˆˆ J (Opposite.unop U)
            source
            ๐Ÿ“ coverage
            instance CategoryTheory.Presheaf.instIsLocallySurjectiveHomWhiskerRightOppositeForget {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 : Functor Cแต’แต– A} (f : F โŸถ G) [IsLocallySurjective J f] :
            IsLocallySurjective J (Functor.whiskerRight f (forget A))
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top {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 : Functor Cแต’แต– A} (f : F โŸถ G) :
            IsLocallySurjective J f โ†” Subfunctor.sheafify J (Subfunctor.range (Functor.whiskerRight f (forget A))) = โŠค
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F G : Functor Cแต’แต– (Type w)} (f : F โŸถ G) :
            IsLocallySurjective J f โ†” Subfunctor.sheafify J (Subfunctor.range f) = โŠค
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_iff_whisker_forget {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 : Functor Cแต’แต– A} (f : F โŸถ G) :
            IsLocallySurjective J f โ†” IsLocallySurjective J (Functor.whiskerRight f (forget A))
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_surjective {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 : Functor Cแต’แต– A} (f : F โŸถ G) (H : โˆ€ (U : Cแต’แต–), Function.Surjective โ‡‘(ConcreteCategory.hom (f.app U))) :
            IsLocallySurjective J f
            source
            ๐Ÿ“ coverage
            instance CategoryTheory.Presheaf.isLocallySurjective_of_iso {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 : Functor Cแต’แต– A} (f : F โŸถ G) [IsIso f] :
            IsLocallySurjective J f
            source
            ๐Ÿ“ coverage
            instance CategoryTheory.Presheaf.isLocallySurjective_comp {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โ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallySurjective J fโ‚] [IsLocallySurjective J fโ‚‚] :
            IsLocallySurjective J (CategoryStruct.comp fโ‚ fโ‚‚)
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallySurjective J (CategoryStruct.comp fโ‚ fโ‚‚)] :
            IsLocallySurjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac {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โ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} {fโ‚ : Fโ‚ โŸถ Fโ‚‚} {fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ} {fโ‚ƒ : Fโ‚ โŸถ Fโ‚ƒ} (fac : CategoryStruct.comp fโ‚ fโ‚‚ = fโ‚ƒ) [IsLocallySurjective J fโ‚ƒ] :
            IsLocallySurjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_iff_of_fac {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โ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} {fโ‚ : Fโ‚ โŸถ Fโ‚‚} {fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ} {fโ‚ƒ : Fโ‚ โŸถ Fโ‚ƒ} (fac : CategoryStruct.comp fโ‚ fโ‚‚ = fโ‚ƒ) [IsLocallySurjective J fโ‚] :
            IsLocallySurjective J fโ‚ƒ โ†” IsLocallySurjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.comp_isLocallySurjective_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallySurjective J fโ‚] :
            IsLocallySurjective J (CategoryStruct.comp fโ‚ fโ‚‚) โ†” IsLocallySurjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_le {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] {K : GrothendieckTopology C} (hJK : J โ‰ค K) {F G : Functor Cแต’แต– A} (f : F โŸถ G) (h : IsLocallySurjective J f) :
            IsLocallySurjective K f
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallyInjective J (CategoryStruct.comp fโ‚ fโ‚‚)] [IsLocallySurjective J fโ‚] :
            IsLocallyInjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective_fac {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โ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} {fโ‚ : Fโ‚ โŸถ Fโ‚‚} {fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ} (fโ‚ƒ : Fโ‚ โŸถ Fโ‚ƒ) (fac : CategoryStruct.comp fโ‚ fโ‚‚ = fโ‚ƒ) [IsLocallyInjective J fโ‚ƒ] [IsLocallySurjective J fโ‚] :
            IsLocallyInjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallySurjective J (CategoryStruct.comp fโ‚ fโ‚‚)] [IsLocallyInjective J fโ‚‚] :
            IsLocallySurjective J fโ‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac {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โ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} {fโ‚ : Fโ‚ โŸถ Fโ‚‚} {fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ} (fโ‚ƒ : Fโ‚ โŸถ Fโ‚ƒ) (fac : CategoryStruct.comp fโ‚ fโ‚‚ = fโ‚ƒ) [IsLocallySurjective J fโ‚ƒ] [IsLocallyInjective J fโ‚‚] :
            IsLocallySurjective J fโ‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.comp_isLocallyInjective_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallyInjective J fโ‚] [IsLocallySurjective J fโ‚] :
            IsLocallyInjective J (CategoryStruct.comp fโ‚ fโ‚‚) โ†” IsLocallyInjective J fโ‚‚
            source
            ๐Ÿ“ coverage
            theorem CategoryTheory.Presheaf.isLocallySurjective_comp_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] {Fโ‚ Fโ‚‚ Fโ‚ƒ : Functor Cแต’แต– A} (fโ‚ : Fโ‚ โŸถ Fโ‚‚) (fโ‚‚ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallyInjective J fโ‚‚] [IsLocallySurjective J fโ‚‚] :
            IsLocallySurjective J (CategoryStruct.comp fโ‚ fโ‚‚) โ†” IsLocallySurjective J fโ‚
            source
            ๐Ÿ“ coverage
            instance CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {Fโ‚ Fโ‚‚ : Functor Cแต’แต– (Type w)} (f : Fโ‚ โŸถ Fโ‚‚) :
            IsLocallySurjective J (Subfunctor.toRangeSheafify J f)
            source
            ๐Ÿ”ธ coverage
            noncomputable def CategoryTheory.Presheaf.sheafificationIsoImagePresheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (F : Functor Cแต’แต– (Type (max u v))) :
            J.sheafify F โ‰… (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).toFunctor

            The image of F in J.sheafify F is isomorphic to the sheafification.

            Equations
              Instances For
                source
                ๐Ÿ“ coverage
                instance CategoryTheory.Presheaf.isLocallySurjective_toPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (P : Functor Cแต’แต– (Type (max u v))) :
                IsLocallySurjective J (J.toPlus P)
                source
                ๐Ÿ“ coverage
                instance CategoryTheory.Presheaf.isLocallySurjective_toSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (P : Functor Cแต’แต– (Type (max u v))) :
                IsLocallySurjective J (J.toSheafify P)
                source
                ๐Ÿ“ coverage
                instance CategoryTheory.Presheaf.isLocallySurjective_toSheafify' {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_2} [Category.{v_1, u_2} D] {FD : D โ†’ D โ†’ Type u_3} {CD : D โ†’ Type (max u v)} [(X Y : D) โ†’ FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] (P : Functor Cแต’แต– D) [HasWeakSheafify J D] [J.HasSheafCompose (forget D)] [J.PreservesSheafification (forget D)] :
                IsLocallySurjective J (toSheafify J P)
                source
                ๐Ÿ”น coverage
                @[reducible, inline]
                abbrev CategoryTheory.Sheaf.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] {Fโ‚ Fโ‚‚ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) :
                Prop

                If ฯ† : Fโ‚ โŸถ Fโ‚‚ is a morphism of sheaves, this is an abbreviation for Presheaf.IsLocallySurjective J ฯ†.val.

                Equations
                  Instances For
                    source
                    ๐Ÿ“ coverage
                    theorem CategoryTheory.Sheaf.isLocallySurjective_sheafToPresheaf_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] {Fโ‚ Fโ‚‚ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) :
                    Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map ฯ†) โ†” IsLocallySurjective ฯ†
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.isLocallySurjective_comp {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โ‚ Fโ‚‚ Fโ‚ƒ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) (ฯˆ : Fโ‚‚ โŸถ Fโ‚ƒ) [IsLocallySurjective ฯ†] [IsLocallySurjective ฯˆ] :
                    IsLocallySurjective (CategoryStruct.comp ฯ† ฯˆ)
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.isLocallySurjective_of_iso {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โ‚ Fโ‚‚ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) [IsIso ฯ†] :
                    IsLocallySurjective ฯ†
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.instIsLocallySurjectiveHomToImage {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type w)} (f : F โŸถ G) :
                    IsLocallySurjective (toImage f)
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.instIsLocallySurjectiveHomMapTypeSheafComposeForget {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โ‚ Fโ‚‚ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) [J.HasSheafCompose (forget A)] [IsLocallySurjective ฯ†] :
                    IsLocallySurjective ((sheafCompose J (forget A)).map ฯ†)
                    source
                    ๐Ÿ“ coverage
                    theorem CategoryTheory.Sheaf.isLocallySurjective_iff_isIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type w)} (f : F โŸถ G) :
                    IsLocallySurjective f โ†” IsIso (imageฮน f)
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.epi_of_isLocallySurjective' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {Fโ‚ Fโ‚‚ : Sheaf J (Type w)} (ฯ† : Fโ‚ โŸถ Fโ‚‚) [IsLocallySurjective ฯ†] :
                    Epi ฯ†
                    source
                    ๐Ÿ“ coverage
                    instance CategoryTheory.Sheaf.epi_of_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] {Fโ‚ Fโ‚‚ : Sheaf J A} (ฯ† : Fโ‚ โŸถ Fโ‚‚) [J.HasSheafCompose (forget A)] [IsLocallySurjective ฯ†] :
                    Epi ฯ†
                    source
                    ๐Ÿ“ coverage
                    theorem CategoryTheory.Sheaf.isLocallySurjective_iff_epi {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : Sheaf J (Type w)} (ฯ† : F โŸถ G) [HasSheafify J (Type w)] :
                    IsLocallySurjective ฯ† โ†” Epi ฯ†
                    source
                    ๐Ÿ”ธ coverage
                    noncomputable def CategoryTheory.Presieve.FamilyOfElements.localPreimage {C : Type u} [Category.{v, u} C] {R R' : Functor Cแต’แต– (Type w)} (ฯ† : R โŸถ R') {X : Cแต’แต–} (r' : R'.obj X) :
                    FamilyOfElements R (Presheaf.imageSieve ฯ† r').arrows

                    Given a morphism ฯ† : R โŸถ R' of presheaves of types and r' : R'.obj X, this is the family of elements of R defined over the sieve Presheaf.imageSieve ฯ† r' which sends a map in this sieve to an arbitrary choice of a preimage of the restriction of r'.

                    Equations
                      Instances For
                        source
                        ๐Ÿ“ coverage
                        theorem CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_map_localPreimage {C : Type u} [Category.{v, u} C] {R R' : Functor Cแต’แต– (Type w)} (ฯ† : R โŸถ R') {X : Cแต’แต–} (r' : R'.obj X) :
                        ((localPreimage ฯ† r').map ฯ†).IsAmalgamation r'