Locally fully faithful functors into sites #
Main results #
CategoryTheory.Functor.IsLocallyFull
: A functorG : C ⥤ D
is locally full wrt a topology onD
if for everyf : G.obj U ⟶ G.obj V
, the set ofG.map fᵢ : G.obj Wᵢ ⟶ G.obj U
such thatG.map fᵢ ≫ f
is in the image ofG
is a coverage of the topology onD
.CategoryTheory.Functor.IsLocallyFaithful
: A functorG : C ⥤ D
is locally faithful wrt a topology onD
if for everyf₁ f₂ : U ⟶ V
whose image inD
are equal, the set ofG.map gᵢ : G.obj Wᵢ ⟶ G.obj U
such thatgᵢ ≫ f₁ = gᵢ ≫ f₂
is a coverage of the topology onD
.
References #
- [Car20]: Olivia Caramello, Denseness conditions, morphisms and equivalences of toposes
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 := ⋯ }
Instances For
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 := ⋯ }
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
.
- 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
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)
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯