Basic

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Basic.lean

Statistics

Metric	Count
Definitions `Is`, `inverseImage`, `map`, `ofObj`, `pair`, `singleton`, `strictMap`	7
Theorems `prop`, `is_iff`, `is_of_prop`, `le_def`, `map_monotone`, `ofObj_apply`, `ofObj_iff`, `ofObj_le_iff`, `ofObj_subtypeVal`, `pair_iff`, `prop_inverseImage_iff`, `prop_map_iff`, `prop_map_obj`, `prop_of_is`, `singleton_iff`, `singleton_le_iff`, `strictMap_iff`, `strictMap_le_map`, `strictMap_monotone`, `strictMap_obj`, `strictMap_ofObj`, `strictMap_singleton`	22
Total	29

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`Is` 📖	CompData	2 math math: `is_iff`, `is_of_prop`
`inverseImage` 📖	CompOp	23 math math: `CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall`, `inverseImage_trW_isInverted`, `instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift`, `instIsClosedUnderSubobjectsInverseImageOfPreservesMonomorphisms`, `CategoryTheory.CostructuredArrow.isSeparating_inverseImage_proj`, `instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits`, `instIsSerreClassInverseImageOfPreservesFiniteLimitsOfPreservesFiniteColimits`, `CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall`, `CategoryTheory.CostructuredArrow.isSeparating_proj_preimage`, `isClosedUnderLimitsOfShape_inverseImage_iff`, `instIsClosedUnderQuotientsInverseImageOfPreservesEpimorphisms`, `instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject`, `IsClosedUnderLimitsOfShape.inverseImage`, `IsClosedUnderColimitsOfShape.inverseImage`, `inverseImage_trW_iff`, `isClosedUnderColimitsOfShape_inverseImage_iff`, `CategoryTheory.StructuredArrow.isCoseparating_proj_preimage`, `instIsTriangulatedInverseImage`, `prop_inverseImage_iff`, `CategoryTheory.StructuredArrow.isCoseparating_inverseImage_proj`, `CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall`, `instIsClosedUnderIsomorphismsInverseImage`, `CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall`
`map` 📖	CompOp	14 math math: `isoClosure_strictMap`, `prop_map_iff`, `prop_map_obj`, `instEssentiallySmallMap`, `CategoryTheory.Functor.essImage_ι_comp`, `map_isoClosure`, `strictMap_le_map`, `instIsClosedUnderIsomorphismsMap`, `ι_map_top`, `map_monotone`, `instIsTriangulatedMapOfIsTriangulatedOfFull`, `CategoryTheory.IsCardinalFilteredGenerator.of_isDense`, `CategoryTheory.Adjunction.isCardinalFilteredGenerator`, `instContainsZeroMapOfPreservesZeroMorphisms`
`ofObj` 📖	CompData	17 math math: `unop_ofObj`, `ofObj_iff`, `hasCardinalLT_subtype_ofObj`, `CategoryTheory.isSeparator_sigma`, `ofObj_apply`, `ofObj_le_iff`, `op_ofObj`, `CategoryTheory.isSeparator_iff_of_isColimit_cofan`, `instSmallOfObjOfSmall`, `CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.single_P`, `CategoryTheory.isCoseparator_pi`, `CategoryTheory.Presheaf.isStrongGenerator`, `ofObj_subtypeVal`, `CategoryTheory.Ind.isSeparating_range_yoneda`, `CategoryTheory.isCoseparator_iff_of_isLimit_fan`, `strictMap_ofObj`, `CategoryTheory.Functor.isStrongGenerator_of_isDense`
`pair` 📖	CompOp	4 math math: `CategoryTheory.isSeparator_coprod`, `CategoryTheory.isCoseparator_prod`, `instSmallPair`, `pair_iff`
`singleton` 📖	CompOp	5 math math: `strictMap_singleton`, `op_singleton`, `singleton_iff`, `singleton_le_iff`, `unop_singleton`
`strictMap` 📖	CompData	12 math math: `isoClosure_strictMap`, `strictMap_obj`, `CategoryTheory.IsSeparating.of_equivalence`, `strictMap_singleton`, `CategoryTheory.IsCoseparating.of_equivalence`, `strictMap_le_map`, `strictMap_iff`, `IsSeparating.of_equivalence`, `strictMap_monotone`, `IsCoseparating.of_equivalence`, `strictMap_ofObj`, `instSmallStrictMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_iff` 📖	mathematical	—	`Is`	—	—
`is_of_prop` 📖	mathematical	—	`Is`	—	`is_iff`
`le_def` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `Pi.hasLe` `Prop.le`	—	—
`map_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`map`	—	—
`ofObj_apply` 📖	mathematical	—	`ofObj`	—	—
`ofObj_iff` 📖	mathematical	—	`ofObj`	—	—
`ofObj_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `Pi.hasLe` `Prop.le` `ofObj`	—	—
`ofObj_subtypeVal` 📖	mathematical	—	`ofObj`	—	`ofObj_apply`
`pair_iff` 📖	mathematical	—	`pair`	—	—
`prop_inverseImage_iff` 📖	mathematical	—	`inverseImage` `CategoryTheory.Functor.obj`	—	—
`prop_map_iff` 📖	mathematical	—	`map` `CategoryTheory.Iso` `CategoryTheory.Functor.obj`	—	—
`prop_map_obj` 📖	mathematical	—	`map` `CategoryTheory.Functor.obj`	—	—
`prop_of_is` 📖	—	—	—	—	`is_iff`
`singleton_iff` 📖	mathematical	—	`singleton`	—	—
`singleton_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `Pi.hasLe` `Prop.le` `singleton`	—	—
`strictMap_iff` 📖	mathematical	—	`strictMap` `CategoryTheory.Functor.obj`	—	—
`strictMap_le_map` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `strictMap` `map`	—	—
`strictMap_monotone` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`strictMap`	—	—
`strictMap_obj` 📖	mathematical	—	`strictMap` `CategoryTheory.Functor.obj`	—	—
`strictMap_ofObj` 📖	mathematical	—	`strictMap` `ofObj` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—
`strictMap_singleton` 📖	mathematical	—	`strictMap` `singleton` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj`	—	—

CategoryTheory.ObjectProperty.Is

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prop` 📖	—	—	—	—	—

---

← Back to Index