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

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

def CategoryTheory.Functor.imageSieve {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] (G : Functor C D) {U V : C} (f : G.obj U ⟶ G.obj V) : 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 (x : C) (i : x ⟶ U) => ∃ (l : x ⟶ V), G.map l = CategoryTheory.CategoryStruct.comp (G.map i) f, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Functor.imageSieve_map {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] (G : Functor C D) {U V : C} (f : U ⟶ V) : G.imageSieve (G.map f) = ⊤

def CategoryTheory.Sieve.equalizer {C : Type uC} [Category.{vC, uC} C] {U V : C} (f₁ f₂ : U ⟶ V) : 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 (x : C) (i : x ⟶ U) => CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂, downward_closed := ⋯ }

@[simp]

theorem CategoryTheory.Sieve.equalizer_apply {C : Type uC} [Category.{vC, uC} C] {U V : C} (f₁ f₂ : U ⟶ V) (x✝ : C) (i : x✝ ⟶ U) : (equalizer f₁ f₂).arrows i = (CategoryStruct.comp i f₁ = CategoryStruct.comp i f₂)

@[simp]

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

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

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

class CategoryTheory.Functor.IsLocallyFull {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] (G : Functor C D) (K : 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) : Sieve.functorPushforward G (G.imageSieve f) ∈ K (G.obj U)

class CategoryTheory.Functor.IsLocallyFaithful {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] (G : Functor C D) (K : 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₂ → Sieve.functorPushforward G (Sieve.equalizer f₁ f₂) ∈ K (G.obj U)

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

theorem CategoryTheory.Functor.functorPushforward_equalizer_mem {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] (G : Functor C D) (K : GrothendieckTopology D) [G.IsLocallyFaithful K] {U V : C} (f₁ f₂ : U ⟶ V) (e : G.map f₁ = G.map f₂) : Sieve.functorPushforward G (Sieve.equalizer f₁ f₂) ∈ K (G.obj U)

theorem CategoryTheory.Functor.IsLocallyFull.ext {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] {K : GrothendieckTopology D} (G : Functor C D) [G.IsLocallyFull K] (ℱ : Sheaf K (Type u_2)) {X Y : C} (i : G.obj X ⟶ G.obj Y) {s t : ℱ.val.obj (Opposite.op (G.obj X))} (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = 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} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] {K : GrothendieckTopology D} (G : Functor C D) [G.IsLocallyFaithful K] (ℱ : Sheaf K (Type u_2)) {X Y : C} (i₁ i₂ : X ⟶ Y) (e : G.map i₁ = G.map i₂) {s t : ℱ.val.obj (Opposite.op (G.obj X))} (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), CategoryStruct.comp j i₁ = 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} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] {K : GrothendieckTopology D} (G : Functor C D) [G.Full] : G.IsLocallyFull K

@[instance 900]

instance CategoryTheory.Functor.IsLocallyFaithful.of_faithful {C : Type uC} [Category.{vC, uC} C] {D : Type uD} [Category.{vD, uD} D] {K : GrothendieckTopology D} (G : Functor C D) [G.Faithful] : G.IsLocallyFaithful K