Documentation

Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Locally fully faithful functors into sites #

Main results #

References #

For a functor G : C ⥤ D, and a morphism f : G.obj U ⟶ G.obj V, Functor.imageSieve G f is the sieve of U consisting of those arrows whose composition with f has a lift in G.

This is the image sieve of f under yonedaMap G V and hence the name. See Functor.imageSieve_eq_imageSieve.

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Functor.imageSieve_map {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (G : CategoryTheory.Functor C D) {U : C} {V : C} (f : U V) :
    G.imageSieve (G.map f) =
    @[simp]
    theorem CategoryTheory.Sieve.equalizer_apply {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U : C} {V : C} (f₁ : U V) (f₂ : U V) (Y : C) (i : Y U) :
    def CategoryTheory.Sieve.equalizer {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U : C} {V : C} (f₁ : U V) (f₂ : U V) :

    For two arrows f₁ f₂ : U ⟶ V, the arrows i such that i ≫ f₁ = i ≫ f₂ forms a sieve.

    Equations
    Instances For

      A functor G : C ⥤ D is locally full wrt a topology on D if for every f : G.obj U ⟶ G.obj V, the set of G.map fᵢ : G.obj Wᵢ ⟶ G.obj U such that G.map fᵢ ≫ f is in the image of G is a coverage of the topology on D.

      Instances
        theorem CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_mem {C : Type uC} :
        ∀ {inst : CategoryTheory.Category.{vC, uC} C} {D : Type uD} {inst_1 : CategoryTheory.Category.{vD, uD} D} {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsLocallyFull K] {U V : C} (f : G.obj U G.obj V), CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) K (G.obj U)

        A functor G : C ⥤ D is locally faithful wrt a topology on D if for every f₁ f₂ : U ⟶ V whose image in D are equal, the set of G.map gᵢ : G.obj Wᵢ ⟶ G.obj U such that gᵢ ≫ f₁ = gᵢ ≫ f₂ is a coverage of the topology on D.

        Instances
          theorem CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem {C : Type uC} :
          ∀ {inst : CategoryTheory.Category.{vC, uC} C} {D : Type uD} {inst_1 : CategoryTheory.Category.{vD, uD} D} {G : CategoryTheory.Functor C D} {K : CategoryTheory.GrothendieckTopology D} [self : G.IsLocallyFaithful K] {U V : C} (f₁ f₂ : U V), G.map f₁ = G.map f₂CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) K (G.obj U)
          theorem CategoryTheory.Functor.functorPushforward_equalizer_mem {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (G : CategoryTheory.Functor C D) (K : CategoryTheory.GrothendieckTopology D) [G.IsLocallyFaithful K] {U : C} {V : C} (f₁ : U V) (f₂ : U V) (e : G.map f₁ = G.map f₂) :
          theorem CategoryTheory.Functor.IsLocallyFull.ext {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsLocallyFull K] (ℱ : CategoryTheory.SheafOfTypes K) {X : C} {Y : C} (i : G.obj X G.obj Y) {s : .val.obj (Opposite.op (G.obj X))} {t : .val.obj (Opposite.op (G.obj X))} (h : ∀ ⦃Z : C⦄ (j : Z X) (f : Z Y), G.map f = CategoryTheory.CategoryStruct.comp (G.map j) i.val.map (G.map j).op s = .val.map (G.map j).op t) :
          s = t
          theorem CategoryTheory.Functor.IsLocallyFaithful.ext {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.IsLocallyFaithful K] (ℱ : CategoryTheory.SheafOfTypes K) {X : C} {Y : C} (i₁ : X Y) (i₂ : X Y) (e : G.map i₁ = G.map i₂) {s : .val.obj (Opposite.op (G.obj X))} {t : .val.obj (Opposite.op (G.obj X))} (h : ∀ ⦃Z : C⦄ (j : Z X), CategoryTheory.CategoryStruct.comp j i₁ = CategoryTheory.CategoryStruct.comp j i₂.val.map (G.map j).op s = .val.map (G.map j).op t) :
          s = t
          @[instance 900]
          Equations
          • =
          @[instance 900]
          Equations
          • =