Locally fully faithful functors into sites

Main results

• CategoryTheory.Functor.IsLocallyFull: 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.
• CategoryTheory.Functor.IsLocallyFaithful: 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.

References

• [Car20]: Olivia Caramello, Denseness conditions, morphisms and equivalences of toposes

def CategoryTheory.Functor.imageSieve {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 : G.obj U ⟶ G.obj V) : CategoryTheory.Sieve U

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

• G.imageSieve f = { arrows := fun (Y : C) (i : Y ⟶ U) => ∃ (l : Y ⟶ V), G.map l = CategoryTheory.CategoryStruct.comp (G.map i) f, downward_closed := ⋯ }

@[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) : (CategoryTheory.Sieve.equalizer f₁ f₂).arrows i = (CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂)

def CategoryTheory.Sieve.equalizer {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U : C} {V : C} (f₁ : U ⟶ V) (f₂ : U ⟶ V) : CategoryTheory.Sieve U

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

Equations

• CategoryTheory.Sieve.equalizer f₁ f₂ = { arrows := fun (Y : C) (i : Y ⟶ U) => CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.equalizer_self {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U : C} {V : C} (f : U ⟶ V) : CategoryTheory.Sieve.equalizer f f = ⊤

theorem CategoryTheory.Sieve.equalizer_eq_equalizerSieve {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {U : C} {V : C} (f₁ : U ⟶ V) (f₂ : U ⟶ V) : CategoryTheory.Sieve.equalizer f₁ f₂ = CategoryTheory.Presheaf.equalizerSieve f₁ f₂

theorem CategoryTheory.Functor.imageSieve_eq_imageSieve {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vC, uD} D] (G : CategoryTheory.Functor C D) {U : C} {V : C} (f : G.obj U ⟶ G.obj V) : G.imageSieve f = CategoryTheory.Presheaf.imageSieve (CategoryTheory.yonedaMap G V) f

class CategoryTheory.Functor.IsLocallyFull {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) : Prop

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.

• functorPushforward_imageSieve_mem : ∀ {U V : C} (f : G.obj U ⟶ G.obj V), CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K.sieves (G.obj U)

theorem CategoryTheory.Functor.IsLocallyFull.functorPushforward_imageSieve_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} [self : G.IsLocallyFull K] {U : C} {V : C} (f : G.obj U ⟶ G.obj V) : CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K.sieves (G.obj U)

class CategoryTheory.Functor.IsLocallyFaithful {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) : Prop

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.

• functorPushforward_equalizer_mem : ∀ {U V : C} (f₁ f₂ : U ⟶ V), G.map f₁ = G.map f₂ → CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K.sieves (G.obj U)

theorem CategoryTheory.Functor.IsLocallyFaithful.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} [self : G.IsLocallyFaithful K] {U : C} {V : C} (f₁ : U ⟶ V) (f₂ : U ⟶ V) : G.map f₁ = G.map f₂ → CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K.sieves (G.obj U)

theorem CategoryTheory.Functor.functorPushforward_imageSieve_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.IsLocallyFull K] {U : C} {V : C} (f : G.obj U ⟶ G.obj V) : CategoryTheory.Sieve.functorPushforward G (G.imageSieve f) ∈ K.sieves (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₂) : CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.equalizer f₁ f₂) ∈ K.sieves (G.obj U)

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]

instance CategoryTheory.Functor.IsLocallyFull.of_full {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.Full] : G.IsLocallyFull K

Equations

• ⋯ = ⋯

@[instance 900]

instance CategoryTheory.Functor.IsLocallyFaithful.of_faithful {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.Faithful] : G.IsLocallyFaithful K

Equations

• ⋯ = ⋯