Structures · Category theory
CategoryTheory.Functor.Faithful
A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.
- Shape
- One type argument · adds map_injective
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
- Rep
- CategoryTheory.Quotient
- CommGrpCat
- GrpCat
- AddGrpCat
- SheafOfModules
- CategoryTheory.Ind
- CategoryTheory.Skeleton
- CategoryTheory.Comma
- HomotopyCategory
- AlgebraicGeometry.SheafedSpace
- AlgebraicGeometry.LocallyRingedSpace
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.InducedCategory
- AlgebraicGeometry.Scheme.Modules
- CategoryTheory.CostructuredArrow
- ContinuousGeneratedByCat
- CategoryTheory.GradedObject
- CategoryTheory.StructuredArrow
- ProfiniteGrp
- CategoryTheory.Limits.Cocone
- CategoryTheory.Limits.Cone
- CategoryTheory.Bundled.α
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
- CategoryTheory.MorphismProperty.Comma
- TopCat.Sheaf
- MonCat
- CategoryTheory.Comonad.Coalgebra
- CompHausLike
- CategoryTheory.Monad.Algebra
- CommAlgCat
- CategoryTheory.Monad
- CategoryTheory.Pretriangulated.Triangle
- CategoryTheory.Comon
- CategoryTheory.Comonad
- CategoryTheory.Idempotents.Karoubi
- CategoryTheory.Mat_
- CategoryTheory.WideSubcategory
- Sequential
- Preord
- Compactum
- CompactlyGenerated
- AlgebraicGeometry.Scheme.AffineEtale
- AlexDisc
- ProfiniteAddGrp
- CategoryTheory.Endofunctor.Coalgebra
- CategoryTheory.DifferentialObject
- CategoryTheory.Endofunctor.Algebra
- LightDiagram
- CategoryTheory.Functor.Elements
- AlgebraicGeometry.Scheme.ProEt
- CategoryTheory.CommGrp
- CategoryTheory.CommMon
- AlgebraicGeometry.Scheme.Etale
- LightDiagram'
- FGModuleCat
- CategoryTheory.CommRingObjCat
- CategoryTheory.Subterminals
- CategoryTheory.Core
- AlgebraicGeometry.AffineScheme
- HasFibers.Fib
- CategoryTheory.Limits.Bicone
- CategoryTheory.Limits.BinaryBicone
- CategoryTheory.InducedWideCategory
- CategoryTheory.RingObjCat
- CategoryTheory.Subobject
- CategoryTheory.Functor.Fiber
- CategoryTheory.Cat
- LightProfinite
- FintypeCat
- HomotopicalAlgebra.BifibrantObject.HoCat
- SimplexCategory
- CategoryTheory.MorphismProperty.Over
- FDRep
- CompHaus
- HomotopyCategory.Plus
- AlgebraicGeometry.Scheme.AffineZariskiSite
- CategoryTheory.MonoOver
- FinBoolAlg
- CategoryTheory.MorphismProperty.CostructuredArrow
- SSet.Truncated
- CategoryTheory.MorphismProperty.Under
- SemiSimplexCategory
- CategoryTheory.Grpd
- FintypeCat.Skeleton
How is a type an instance?
Loading the hierarchy index…
Assumed by472
- CategoryTheory.Functor.map_injective
- CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
- CategoryTheory.Adjunction.Triple.rightToLeft
- CategoryTheory.Adjunction.Triple.leftToRight
- CategoryTheory.Functor.preimageIso
- CategoryTheory.Abelian.LeftResolution.chainComplex
- CategoryTheory.Functor.relativelyRepresentable.lift₃
- CategoryTheory.isIso_of_fully_faithful
- CategoryTheory.Abelian.LeftResolution.chainComplexMap
- CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso
- CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso
- CategoryTheory.Abelian.LeftResolution.chainComplexXIso
- CategoryTheory.Functor.Faithful.of_comp
- CategoryTheory.HasShift.induced
- CategoryTheory.Functor.CommShift.OfComp.iso
- CategoryTheory.Functor.ShiftSequence.induced
- CategoryTheory.locallySmall_of_faithful
- 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.Functor.relativelyRepresentable.lift'_fst
- CategoryTheory.Functor.essImage.liftFunctor
- CategoryTheory.Adjunction.Triple.map_rightToLeft_app
- CategoryTheory.Functor.final_of_comp_full_faithful
- 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.Functor.Faithful.map_injective
- CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion
- CategoryTheory.Adjunction.hasCardinalFilteredGenerator
- CategoryTheory.Triangulated.AbelianSubcategory.mor₁_πQ
- CategoryTheory.HasShift.Induced.add
- CategoryTheory.Functor.map_eq_zero_iff
- CategoryTheory.Functor.reflects_precoherent
- CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphisms
- CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful
- CategoryTheory.ShortComplex.exact_map_iff_of_faithful
- CategoryTheory.Functor.reflects_exact_of_faithful
- CategoryTheory.Functor.relativelyRepresentable.hom_ext'
- CategoryTheory.Functor.ShiftSequence.induced_shiftMap
- CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ
- CategoryTheory.Adjunction.isLocalization
- CategoryTheory.ObjectProperty.isLocal_adj_unit_app
- CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
- CategoryTheory.Functor.ShiftSequence.induced_shiftIso_hom_app_obj
- CategoryTheory.Functor.relativelyRepresentable.lift_snd
Ancestors0
No ancestors.