Structures · Category theory
CategoryTheory.Functor.Full
A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective.
- Shape
- One type argument · adds map_surjective
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Provided automatically by
Concrete types that are instances100
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- CategoryTheory.Grp
- HomologicalComplex
- Action
- CategoryTheory.Mon
- AlgebraicGeometry.Scheme
- AddCommGrpCat
- CategoryTheory.ObjectProperty.FullSubcategory
- TopCat
- TopologicalSpace.Opens
- CategoryTheory.Quotient
- CommGrpCat
- GrpCat
- AddGrpCat
- SheafOfModules
- CategoryTheory.Paths
- CategoryTheory.Ind
- CategoryTheory.Skeleton
- CategoryTheory.Comma
- CategoryTheory.Cat.FreeRefl
- HomotopyCategory
- CommRingCat
- AlgebraicGeometry.SheafedSpace
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.InducedCategory
- AlgebraicGeometry.Scheme.Modules
- CategoryTheory.CostructuredArrow
- ContinuousGeneratedByCat
- CategoryTheory.StructuredArrow
- CommMonCat
- CategoryTheory.Arrow
- CategoryTheory.Limits.Cocone
- CategoryTheory.Limits.Cone
- CategoryTheory.Bundled.α
- CategoryTheory.AddGrp
- AddCommMonCat
- CategoryTheory.AddMon
- CategoryTheory.MorphismProperty.Comma
- TopCat.Sheaf
- MonCat
- CategoryTheory.Comonad.Coalgebra
- CompHausLike
- CategoryTheory.Monad.Algebra
- CommAlgCat
- RingCat
- CommSemiRingCat
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.Idempotents.Karoubi
- CategoryTheory.Mat_
- AddSemigrp
- Semigrp
- Sequential
- Preord
- Compactum
- CompactlyGenerated
- AlgebraicGeometry.Scheme.AffineEtale
- AlexDisc
- LightDiagram
- AlgebraicGeometry.Scheme.ProEt
- CategoryTheory.CommGrp
- CategoryTheory.CommMon
- AlgebraicGeometry.Scheme.Etale
- LightDiagram'
- FGModuleCat
- CategoryTheory.CommRingObjCat
- CategoryTheory.Subterminals
- AlgebraicGeometry.AffineScheme
- CategoryTheory.Limits.Bicone
- CategoryTheory.Limits.BinaryBicone
- CategoryTheory.Cat
- LightProfinite
- FintypeCat
- HomotopicalAlgebra.BifibrantObject.HoCat
- CochainComplex.Plus
- SimplexCategory
- CategoryTheory.MorphismProperty.Over
- FDRep
- CompHaus
- HomotopyCategory.Plus
- CategoryTheory.MonoOver
- FinBoolAlg
- CategoryTheory.MorphismProperty.CostructuredArrow
- SSet.Truncated
- CategoryTheory.MorphismProperty.Under
- HomotopicalAlgebra.CofibrantObject
- HomotopicalAlgebra.BifibrantObject
- HomotopicalAlgebra.FibrantObject
- AlgebraicGeometry.Scheme.Opens
- CategoryTheory.Grpd
- FintypeCat.Skeleton
- CategoryTheory.IsCofiltered.SmallCofilteredIntermediate
- CategoryTheory.IsFiltered.SmallFilteredIntermediate
- Condensed
- CategoryTheory.Decomposed
- CategoryTheory.SimplicialObject.Truncated
- FGAlgCat
How is a type an instance?
Loading the hierarchy index…
Assumed by496
- CategoryTheory.Functor.map_preimage
- CategoryTheory.Functor.preimage
- CategoryTheory.Functor.relativelyRepresentable.fst'
- CategoryTheory.Functor.map_surjective
- CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
- CategoryTheory.Adjunction.Triple.rightToLeft
- CategoryTheory.Adjunction.Triple.leftToRight
- CategoryTheory.Functor.relativelyRepresentable.pullback₃
- CategoryTheory.Functor.preimageIso
- CategoryTheory.Abelian.LeftResolution.chainComplex
- CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁
- CategoryTheory.Functor.relativelyRepresentable.symmetry
- CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂
- CategoryTheory.Functor.relativelyRepresentable.lift'
- CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃
- CategoryTheory.Triangulated.AbelianSubcategory.ιK
- CategoryTheory.Triangulated.AbelianSubcategory.πQ
- CategoryTheory.Functor.relativelyRepresentable.lift₃
- CategoryTheory.isIso_of_fully_faithful
- CategoryTheory.Abelian.LeftResolution.chainComplexMap
- CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso
- CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso
- CategoryTheory.Functor.relativelyRepresentable.lift
- CategoryTheory.Functor.relativelyRepresentable.pullback₃.π
- CategoryTheory.Abelian.LeftResolution.chainComplexXIso
- CategoryTheory.HasShift.induced
- CategoryTheory.Functor.CommShift.OfComp.iso
- CategoryTheory.Functor.ShiftSequence.induced
- CategoryTheory.SingleFunctors.lift
- CategoryTheory.Functor.relativelyRepresentable.lift'_snd
- CategoryTheory.LocalizerMorphism.functorialRightResolutions.ι
- CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app
- CategoryTheory.Functor.initial_of_comp_full_faithful
- CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK
- CategoryTheory.Functor.relativelyRepresentable.lift'_fst
- CategoryTheory.Functor.essImage.liftFunctor
- CategoryTheory.Adjunction.Triple.map_rightToLeft_app
- CategoryTheory.Functor.final_of_comp_full_faithful
- CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQ
- CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app'
- CategoryTheory.Functor.fullyFaithfulCancelRight
- CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage
- CategoryTheory.Adjunction.Triple.leftToRight_app_obj
- CategoryTheory.Functor.reflects_preregular
- CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion
- CategoryTheory.Adjunction.hasCardinalFilteredGenerator
- CategoryTheory.Functor.Full.map_surjective
- CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ
- CategoryTheory.HasShift.Induced.add
- CategoryTheory.Functor.reflects_precoherent
Ancestors0
No ancestors.