Structures · Category theory
CategoryTheory.Functor.IsLocallyFaithful
A functor G : C ⥤ D is locally faithful w.r.t. a topology on D if for every f₁ f₂ : U ⟶ V
whose images 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.
- Shape
- 2 explicit arguments · adds functorPushforward_equalizer_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- CategoryTheory.Functor.mem_inducedTopology_iff_of_isCoverDense
- CategoryTheory.Functor.functorPushforward_equalizer_mem
- CategoryTheory.Functor.coverPreserving_restrictedTopology
- CategoryTheory.Functor.mem_restrictedTopology_iff
- CategoryTheory.Functor.IsCoverDense.compatiblePreserving
- CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense
- CategoryTheory.Functor.IsLocallyFaithful.functorPushforward_equalizer_mem
- CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense
- CategoryTheory.Functor.instIsDenseSubsiteRestrictedTopologyOfIsCoverDense
- CategoryTheory.Functor.inducedTopology_coverPreserving
- CategoryTheory.Functor.isDenseSubsite_of_isOneHypercoverDense
- CategoryTheory.Functor.IsCoverDense.isContinuous
- CategoryTheory.Functor.mem_inducedTopology_sieves_iff
Ancestors0
No ancestors.