Structures · Category theory
CategoryTheory.Functor.IsDenseSubsite
The functor G : C ⥤ D exhibits (C, J) as a dense subsite of (D, K)
if G is cover-dense, locally fully-faithful,
and S is a cover of C if and only if the image of S in D is a cover.
- Shape
- 3 explicit arguments · adds isCoverDense', isLocallyFull', isLocallyFaithful', functorPushforward_mem_iff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- CategoryTheory.Over
- TopologicalSpace.Opens
- AlgebraicGeometry.Scheme.AffineEtale
- AlgebraicGeometry.Scheme.AffineZariskiSite
How is a type an instance?
Loading the hierarchy index…
Assumed by120
- CategoryTheory.Equivalence.sheafCongr.inverse
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage
- CategoryTheory.Equivalence.sheafCongr.functor
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction
- CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem
- CategoryTheory.Functor.IsDenseSubsite.sheafifyOfIsEquivalence
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv
- CategoryTheory.Functor.IsDenseSubsite.isCoverDense
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map
- CategoryTheory.Equivalence.sheafCongr
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π
- CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover
- CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom
- CategoryTheory.Functor.IsDenseSubsite.functorPushforward_mem_iff
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_fac
- CategoryTheory.Functor.functorPushforward_mem_iff
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp_map
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π
- CategoryTheory.Functor.IsDenseSubsite.isLocallyFull
- CategoryTheory.Equivalence.sheafCongr.unitIso
- CategoryTheory.Functor.IsDenseSubsite.coverPreserving
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map
- CategoryTheory.Equivalence.sheafCongr.counitIso
- CategoryTheory.Sheaf.isConstant_iff_of_equivalence
- CategoryTheory.Functor.IsDenseSubsite.equalizer_mem
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction
- CategoryTheory.Functor.IsDenseSubsite.sheafifyAdjunctionOfIsEquivalence
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map
- CategoryTheory.Functor.IsDenseSubsite.sheafEquiv
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_restriction
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_presheafObjObjIso_hom
- CategoryTheory.Functor.IsDenseSubsite.isCoverDense'
- CategoryTheory.Functor.IsDenseSubsite.map_eq_of_eq
- CategoryTheory.Functor.OneHypercoverDenseData.isEquivalence
- CategoryTheory.Equivalence.transportSheafificationAdjunction
- CategoryTheory.Equivalence.hasSheafify
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.sheafIso
- CategoryTheory.equivCommuteConstant'
- CategoryTheory.Functor.IsDenseSubsite.sheafifyHomEquivOfIsEquivalence_naturality_left
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage.congr_simp
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_mapPreimage
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv_π_assoc
Ancestors0
No ancestors.