Structures · Category theory
CategoryTheory.GrothendieckTopology.HasSheafCompose
Describes the property of a functor to "preserve sheaves".
- Defined in
- Mathlib.CategoryTheory.Sites.Whiskering
- Shape
- 2 explicit arguments · adds isSheaf
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 by70
- CategoryTheory.sheafCompose
- CategoryTheory.Sheaf.isSeparated
- CategoryTheory.sheafifyComposeIso
- CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
- CategoryTheory.sheafComposeNatTrans
- CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf
- CategoryTheory.Sheaf.adjunction
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms
- CategoryTheory.constantCommuteCompose
- CategoryTheory.sheafComposeNatTrans_fac
- CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso
- CategoryTheory.sheafCompose_map
- CategoryTheory.sheafComposeIso_hom_fac
- CategoryTheory.Sheaf.isConstant_iff_forget
- Condensed.epi_iff_locallySurjective_on_compHaus
- CategoryTheory.constantCommuteCompose_hom_app_hom
- Condensed.epi_iff_surjective_on_stonean
- CategoryTheory.Sheaf.isLocallyBijective_iff_isIso
- CategoryTheory.Sheaf.adjunction_unit_app_hom
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff
- CategoryTheory.constantSheafAdj_counit_w
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms
- CategoryTheory.sheafComposeIso_inv_fac
- TopCat.Sheaf.isLocallySurjective_iff_epi
- CategoryTheory.sheafComposeIso_hom_fac_assoc
- CategoryTheory.Sheaf.adjunction_counit_app_hom
- CategoryTheory.Sheaf.isLocallyInjective_iff_injective
- CategoryTheory.sheafCompose_map_hom
- CategoryTheory.Sheaf.isConstant_of_forget
- CategoryTheory.Sheaf.mono_of_isLocallyInjective
- CategoryTheory.Presheaf.IsSheaf.isSeparated
- CategoryTheory.Presheaf.isLocallySurjective_toSheafify'
- CategoryTheory.Sheaf.adjunction_unit_app_val
- CategoryTheory.Sheaf.isLocallyInjective_forget
- CategoryTheory.instIsConstantObjSheafSheafCompose
- CategoryTheory.fullyFaithfulSheafComposeCompSheafToPresheaf
- CategoryTheory.instFullSheafSheafComposeOfFaithful
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W
- CategoryTheory.sheafComposeIso_inv_fac_assoc
- CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf
- CategoryTheory.Sheaf.instEpiAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization
- CategoryTheory.Sheaf.adjunction_counit_app_val
- CategoryTheory.Sheaf.instIsLocallySurjectiveFunMapTypeSheafComposeForget
- CategoryTheory.Sheaf.epi_of_isLocallySurjective
- CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans
- CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.mk'
- CategoryTheory.Equivalence.hasSheafCompose
- CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints
- CategoryTheory.sheafComposeNatTrans_app_uniq
Ancestors0
No ancestors.