LocallyDirected

📁 Source: Mathlib/CategoryTheory/LocallyDirected.lean

Statistics

Metric	Count
Definitions LocallyDirected, IsLocallyDirected	2
Theorems cond, exists_map_eq_of_isLocallyDirected, instIsLocallyDirectedDiscrete, instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit	4
Total	6

AlgebraicGeometry.Scheme.Cover

Definitions

Name	Category	Theorems
LocallyDirected 📖	CompData	—

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLocallyDirectedDiscrete 📖	mathematical	—	Functor.IsLocallyDirected Discrete discreteCategory	—	Discrete.functor_map_id FunctorToTypes.map_id_apply
instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit 📖	mathematical	Mono types Functor.obj Limits.WidePushoutShape Limits.WidePushoutShape.category Functor.map Limits.WidePushoutShape.Hom.init	Functor.IsLocallyDirected	—	FunctorToTypes.map_id_apply mono_iff_injective

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsLocallyDirected 📖	CompData	9 math math: AlgebraicGeometry.Scheme.Cover.instIsLocallyDirectedI₀CompFunctorOfLocallyDirectedForget, CategoryTheory.instIsLocallyDirectedDiscrete, CategoryTheory.instIsLocallyDirectedWidePushoutShapeOfMonoObjNoneSomeMapInit, AlgebraicGeometry.Scheme.IsLocallyDirected.instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.isLocallyDirected, AlgebraicGeometry.instIsLocallyDirectedCompSchemeOverOverTopMorphismPropertyForgetForgetForget, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin, AlgebraicGeometry.Scheme.Hom.instIsLocallyDirectedI₀DirectedCoverCompFunctorNormalizationGlueDataForget, AlgebraicGeometry.Scheme.isLocallyDirected_of_equifibered_of_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_map_eq_of_isLocallyDirected 📖	—	map CategoryTheory.types	—	—	IsLocallyDirected.cond

CategoryTheory.Functor.IsLocallyDirected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cond 📖	—	CategoryTheory.Functor.map CategoryTheory.types	—	—	—

---

← Back to Index