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 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 (x : C) (i : x ⟶ U) => ∃ (l : x ⟶ V), G.map l = CategoryTheory.CategoryStruct.comp (G.map i) f, downward_closed := ⋯ }

Instances For

source

@[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 V : C} (f : U ⟶ V) :

G.imageSieve (G.map f) = ⊤

source

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

Instances For

source

@[simp]

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

(CategoryTheory.Sieve.equalizer f₁ f₂).arrows i = (CategoryTheory.CategoryStruct.comp i f₁ = CategoryTheory.CategoryStruct.comp i f₂)

source

@[simp]

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

CategoryTheory.Sieve.equalizer f f = ⊤

source

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

CategoryTheory.Sieve.equalizer f₁ f₂ = CategoryTheory.Presheaf.equalizerSieve f₁ f₂

source

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 V : C} (f : G.obj U ⟶ G.obj V) :

G.imageSieve f = CategoryTheory.Presheaf.imageSieve (CategoryTheory.yonedaMap G V) f

source

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 (G.obj U)

Instances

source

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 (G.obj U)