PreservesLocallyBijective

📁 Source: Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean

Statistics

Metric	Count
Definitions	0
Theorems isLocallyInjective_of_whisker, isLocallyInjective_whisker, isLocallyInjective_whisker_iff, isLocallySurjective_of_whisker, isLocallySurjective_whisker, isLocallySurjective_whisker_iff	6
Total	6

CategoryTheory.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallyInjective_of_whisker 📖	mathematical	CategoryTheory.CoverPreserving	IsLocallyInjective	—	CategoryTheory.GrothendieckTopology.transitive CategoryTheory.Functor.is_cover_of_isCoverDense CategoryTheory.Sieve.pullback_comp CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Sieve.functorPullback_pushforward_le CategoryTheory.Sieve.functorPushforward_monotone CategoryTheory.Functor.map_comp CategoryTheory.comp_apply CategoryTheory.CoverPreserving.cover_preserve equalizerSieve_mem CategoryTheory.NatTrans.naturality_apply
isLocallyInjective_whisker 📖	mathematical	—	IsLocallyInjective CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Functor.cover_lift equalizerSieve_mem
isLocallyInjective_whisker_iff 📖	mathematical	CategoryTheory.CoverPreserving	IsLocallyInjective CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Functor.whiskerLeft	—	isLocallyInjective_of_whisker isLocallyInjective_whisker
isLocallySurjective_of_whisker 📖	mathematical	CategoryTheory.CoverPreserving	IsLocallySurjective	—	CategoryTheory.GrothendieckTopology.transitive CategoryTheory.Functor.is_cover_of_isCoverDense CategoryTheory.Sieve.pullback_comp CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.CoverPreserving.cover_preserve imageSieve_mem CategoryTheory.GrothendieckTopology.superset_covering CategoryTheory.Sieve.functorPullback_pushforward_le CategoryTheory.Sieve.functorPushforward_monotone CategoryTheory.Functor.map_comp CategoryTheory.comp_apply
isLocallySurjective_whisker 📖	mathematical	—	IsLocallySurjective CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Functor.whiskerLeft	—	CategoryTheory.Functor.cover_lift imageSieve_mem
isLocallySurjective_whisker_iff 📖	mathematical	CategoryTheory.CoverPreserving	IsLocallySurjective CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Functor.whiskerLeft	—	isLocallySurjective_of_whisker isLocallySurjective_whisker

---

← Back to Index