Theorems · Definition · category theory
CategoryTheory.ObjectProperty.map
{C : Type u} →
{D : Type u'} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.Category.{v', u'} D] →
CategoryTheory.ObjectProperty C → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty DThe essential image of a property of objects by a functor.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Isoproof · cited by 3,963
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
Cited by15
Results whose statement or proof uses this declaration.
- CategoryTheory.Adjunction.hasCardinalFilteredGeneratorproof · cited by 3
- CategoryTheory.Adjunction.isCardinalFilteredGeneratorstatement and proof · cited by 1
- CategoryTheory.IsCardinalFilteredGenerator.of_isDensestatement and proof · cited by 1
- CategoryTheory.IsCardinalFilteredGenerator.of_isDense_ιproof · cited by 1
- CategoryTheory.ObjectProperty.prop_map_objstatement · cited by 1
- CategoryTheory.ObjectProperty.EssentiallySmall.of_functorstatement and proof · cited by 1
- CategoryTheory.ObjectProperty.strictMap_le_mapstatement · cited by 1
- CategoryTheory.ObjectProperty.ι_map_topstatement and proof · cited by 1
- CategoryTheory.ObjectProperty.map_monotonestatement and proof · cited by 1
- CategoryTheory.ObjectProperty.map_topstatement and proof · cited by 0
- CategoryTheory.MorphismProperty.ofObjectProperty_map_lestatement and proof · cited by 0
- CategoryTheory.ObjectProperty.prop_map_iffstatement · cited by 0