Structures · Category theory
CategoryTheory.Functor.EssSurj
A functor F : C ⥤ D is essentially surjective if every object of D is in the essential
image of F. In other words, for every Y : D, there is some X : C with F.obj X ≅ Y.
- Defined in
- Mathlib.CategoryTheory.EssentialImage
- Shape
- One type argument · adds mem_essImage
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances26
- CategoryTheory.Over
- ModuleCat
- HomologicalComplex
- CategoryTheory.Quotient
- CategoryTheory.Skeleton
- CategoryTheory.Comma
- HomotopyCategory
- CategoryTheory.Under
- CategoryTheory.InducedCategory
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- CategoryTheory.Arrow
- CategoryTheory.Bundled.α
- CategoryTheory.Comonad.Coalgebra
- CategoryTheory.Monad.Algebra
- CategoryTheory.Mat_
- Compactum
- LightDiagram'
- CochainComplex
- CochainComplex.Plus
- SimplexCategory
- HomotopyCategory.Plus
- FintypeCat.Skeleton
- CategoryTheory.Decomposed
- Opposite
- Sum
How is a type an instance?
Loading the hierarchy index…
Assumed by76
- CategoryTheory.Functor.objObjPreimageIso
- CategoryTheory.Functor.objPreimage
- CategoryTheory.Functor.EssSurj.mem_essImage
- CategoryTheory.Functor.essImage_comp_of_essSurj
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_isLocalizedEquivalence
- CategoryTheory.TwoSquare.GuitartExact.of_hComp
- CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff
- CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft
- CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj
- CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj
- CategoryTheory.TwoSquare.GuitartExact.of_vComp
- CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_iso_of_essSurj_of_full
- CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_pathObjects
- CategoryTheory.Functor.hasFiniteProducts_of_additive_of_essSurj
- CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished
- CategoryTheory.Functor.essImage_comp_apply_of_essSurj
- CategoryTheory.LocalizerMorphism.hasRightResolutions_iff_iso_of_essSurj_of_full
- CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport
- CategoryTheory.Functor.essSurj_of_comp_fully_faithful
- CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence
- CategoryTheory.Functor.isTriangulated_of_precomp
- CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two
- CategoryTheory.TwoSquare.GuitartExact.of_vComp'
- CategoryTheory.Functor.distTriang_iff
- CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy
- CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj_of_full
- CategoryTheory.Functor.isLocalization_of_essSurj_of_full_of_exists_cylinders
- CategoryTheory.LocalizerMorphism.hasLeftResolutions_of_iso_of_essSurj_of_full
- CategoryTheory.Functor.essSurj_of_iso
- CategoryTheory.TwoSquare.GuitartExact.of_hComp'
- CategoryTheory.Functor.linear_of_full_essSurj_comp
- CategoryTheory.MorphismProperty.map_top_eq_top_of_essSurj_of_full
- CategoryTheory.Functor.faithful_of_comp_essSurj
- CategoryTheory.Functor.instEssSurjOppositeOp
- CategoryTheory.LocalizerMorphism.hasRightResolutions_arrow_of_essSurj_of_full
- CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_rightHomotopy
- CategoryTheory.Functor.essSurj_mapArrow
- CategoryTheory.TwoSquare.GuitartExact.hComp'_iff_of_essSurj
- CategoryTheory.GrothendieckTopology.PreservesSheafification.transport
- CategoryTheory.CostructuredArrow.instEssSurjOverToOver
- CategoryTheory.GrothendieckTopology.W.transport_isMonoidal
- CategoryTheory.Under.instEssSurjObjPostOfFull
- CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_essSurj
- CategoryTheory.Functor.instEssSurjSkeletonMapSkeleton
- CategoryTheory.Comma.instEssSurjCompPreLeft
- CategoryTheory.Functor.isTriangulated_of_precomp_iso
- CategoryTheory.Functor.instEssSurjQuotientHomRelLift
- CategoryTheory.Functor.LeftExtension.isPointwiseLeftKanExtensionOfCompTwoSquare
- CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_isLocalizedEquivalence
- CategoryTheory.Functor.mapSkeleton_surjective
Ancestors0
No ancestors.