Commit 2024-04-12 14:33 65b7affc

View on Github →

chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985) These notions on functors are now Functor.Full, Functor.Faithful, Functor.EssSurj, Functor.IsEquivalence, Functor.ReflectsIsomorphisms. Deprecated aliases are introduced for the previous names.

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Basic.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean

Modified Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/GroupCat/Basic.lean

Modified Mathlib/Algebra/Category/GroupCat/Limits.lean

Modified Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Modified Mathlib/Algebra/Category/Ring/Limits.lean

Modified Mathlib/Algebra/Category/SemigroupCat/Basic.lean

Modified Mathlib/Algebra/Homology/HomologicalBicomplex.lean

Modified Mathlib/Algebra/Homology/HomologicalComplex.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/Algebra/Homology/QuasiIso.lean

modified theorem HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology

modified theorem HomologicalComplex.quasiIso_map_iff_of_preservesHomology

Modified Mathlib/Algebra/Homology/ShortComplex/Exact.lean

Modified Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean

Modified Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/CategoryTheory/Abelian/Exact.lean

Modified Mathlib/CategoryTheory/Abelian/Transfer.lean

Modified Mathlib/CategoryTheory/Adhesive.lean

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

modified theorem CategoryTheory.L_faithful_of_unit_isIso

modified theorem CategoryTheory.R_faithful_of_counit_isIso

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

modified theorem CategoryTheory.Adjunction.hasColimit_comp_equivalence

modified theorem CategoryTheory.Adjunction.hasColimit_of_comp_equivalence

modified theorem CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence

modified theorem CategoryTheory.Adjunction.hasLimit_comp_equivalence

modified theorem CategoryTheory.Adjunction.hasLimit_of_comp_equivalence

modified theorem CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence

modified theorem CategoryTheory.Adjunction.has_colimits_of_equivalence

modified theorem CategoryTheory.Adjunction.has_limits_of_equivalence

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Modified Mathlib/CategoryTheory/Bicategory/SingleObj.lean

Modified Mathlib/CategoryTheory/CatCommSq.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Category/PartialFun.lean

Modified Mathlib/CategoryTheory/Closed/Functor.lean

modified theorem CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

modified theorem CategoryTheory.MonoidalClosed.ofEquiv_curry_def

modified theorem CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def

Modified Mathlib/CategoryTheory/Comma/Basic.lean

Modified Mathlib/CategoryTheory/Comma/Over.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow.lean

modified def CategoryTheory.CostructuredArrow.mkIdTerminal

modified def CategoryTheory.StructuredArrow.mkIdInitial

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

modified theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean

modified theorem CategoryTheory.reflectsIsomorphisms_forget₂

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/Endofunctor/Algebra.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

deleted theorem CategoryTheory.Equivalence.essSurj_of_equivalence

deleted theorem CategoryTheory.Equivalence.functor_map_inj_iff

deleted theorem CategoryTheory.Equivalence.inverse_map_inj_iff

added theorem CategoryTheory.Functor.IsEquivalence.Equivalence.essSurj_of_equivalence

added theorem CategoryTheory.Functor.IsEquivalence.Equivalence.functor_map_inj_iff

added theorem CategoryTheory.Functor.IsEquivalence.Equivalence.inverse_map_inj_iff

added def CategoryTheory.Functor.IsEquivalence.Iso.compInvIso

added def CategoryTheory.Functor.IsEquivalence.Iso.compInverseIso

added def CategoryTheory.Functor.IsEquivalence.Iso.invCompIso

added def CategoryTheory.Functor.IsEquivalence.Iso.inverseCompIso

added def CategoryTheory.Functor.IsEquivalence.Iso.isoCompInv

added def CategoryTheory.Functor.IsEquivalence.Iso.isoCompInverse

added def CategoryTheory.Functor.IsEquivalence.Iso.isoInvComp

added def CategoryTheory.Functor.IsEquivalence.Iso.isoInverseComp

added def CategoryTheory.Functor.IsEquivalence.cancelCompLeft

added def CategoryTheory.Functor.IsEquivalence.cancelCompRight

added def CategoryTheory.Functor.IsEquivalence.equivOfIso

added theorem CategoryTheory.Functor.IsEquivalence.fun_inv_map

added theorem CategoryTheory.Functor.IsEquivalence.inv_fun_map

added def CategoryTheory.Functor.IsEquivalence.ofIso

added theorem CategoryTheory.Functor.IsEquivalence.ofIso_refl

added theorem CategoryTheory.Functor.IsEquivalence.ofIso_trans

deleted def CategoryTheory.IsEquivalence.cancelCompLeft

deleted def CategoryTheory.IsEquivalence.cancelCompRight

deleted def CategoryTheory.IsEquivalence.equivOfIso

deleted theorem CategoryTheory.IsEquivalence.fun_inv_map

deleted theorem CategoryTheory.IsEquivalence.inv_fun_map

deleted def CategoryTheory.IsEquivalence.ofIso

deleted theorem CategoryTheory.IsEquivalence.ofIso_refl

deleted theorem CategoryTheory.IsEquivalence.ofIso_trans

deleted def CategoryTheory.Iso.compInvIso

deleted def CategoryTheory.Iso.compInverseIso

deleted def CategoryTheory.Iso.invCompIso

deleted def CategoryTheory.Iso.inverseCompIso

deleted def CategoryTheory.Iso.isoCompInv

deleted def CategoryTheory.Iso.isoCompInverse

deleted def CategoryTheory.Iso.isoInvComp

deleted def CategoryTheory.Iso.isoInverseComp

Modified Mathlib/CategoryTheory/EssentialImage.lean

added theorem CategoryTheory.Functor.essSurj_of_iso

modified theorem CategoryTheory.Functor.essSurj_of_surj

modified def CategoryTheory.Functor.objObjPreimageIso

modified def CategoryTheory.Functor.objPreimage

deleted theorem CategoryTheory.Iso.map_essSurj

Modified Mathlib/CategoryTheory/EssentiallySmall.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Filtered/Final.lean

modified theorem CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful

modified theorem CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful

modified theorem CategoryTheory.IsCofiltered.of_exists_of_isCofiltered_of_fullyFaithful

modified theorem CategoryTheory.IsFiltered.of_exists_of_isFiltered_of_fullyFaithful

modified theorem CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful

Modified Mathlib/CategoryTheory/Filtered/Small.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

deleted theorem CategoryTheory.Faithful.div_comp

deleted theorem CategoryTheory.Faithful.div_faithful

deleted theorem CategoryTheory.Faithful.of_comp

deleted theorem CategoryTheory.Faithful.of_comp_eq

deleted theorem CategoryTheory.Faithful.of_comp_iso

deleted theorem CategoryTheory.Faithful.of_iso

deleted def CategoryTheory.Full.ofCompFaithful

deleted def CategoryTheory.Full.ofCompFaithfulIso

deleted def CategoryTheory.Full.ofIso

added theorem CategoryTheory.Functor.Faithful.div_comp

added theorem CategoryTheory.Functor.Faithful.div_faithful

added theorem CategoryTheory.Functor.Faithful.of_comp

added theorem CategoryTheory.Functor.Faithful.of_comp_eq

added theorem CategoryTheory.Functor.Faithful.of_comp_iso

added theorem CategoryTheory.Functor.Faithful.of_iso

added def CategoryTheory.Functor.Full.ofCompFaithful

added def CategoryTheory.Functor.Full.ofCompFaithfulIso

added def CategoryTheory.Functor.Full.ofIso

added def CategoryTheory.Functor.fullyFaithfulCancelRight

added theorem CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app

added theorem CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app

added theorem CategoryTheory.Functor.preimage_comp

added theorem CategoryTheory.Functor.preimage_id

added theorem CategoryTheory.Functor.preimage_map

modified def CategoryTheory.equivOfFullyFaithful

deleted def CategoryTheory.fullyFaithfulCancelRight

deleted theorem CategoryTheory.fullyFaithfulCancelRight_hom_app

deleted theorem CategoryTheory.fullyFaithfulCancelRight_inv_app

modified def CategoryTheory.isoEquivOfFullyFaithful

deleted theorem CategoryTheory.preimage_comp

deleted theorem CategoryTheory.preimage_id

deleted theorem CategoryTheory.preimage_map

Modified Mathlib/CategoryTheory/Functor/ReflectsIso.lean

Modified Mathlib/CategoryTheory/Galois/Basic.lean

Modified Mathlib/CategoryTheory/Generator.lean

modified theorem CategoryTheory.isCoseparator_iff_faithful_yoneda_obj

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

Modified Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

modified def CategoryTheory.Idempotents.toKaroubiIsEquivalence

Modified Mathlib/CategoryTheory/IsConnected.lean

modified theorem CategoryTheory.zag_of_zag_obj

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

modified def CategoryTheory.createsColimitOfFullyFaithfulOfIso'

modified def CategoryTheory.createsColimitOfFullyFaithfulOfIso

modified def CategoryTheory.createsColimitOfFullyFaithfulOfLift'

modified def CategoryTheory.createsColimitOfFullyFaithfulOfLift

modified def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves

modified def CategoryTheory.createsColimitOfReflectsIso'

modified def CategoryTheory.createsColimitOfReflectsIso

modified def CategoryTheory.createsLimitOfFullyFaithfulOfIso'

modified def CategoryTheory.createsLimitOfFullyFaithfulOfIso

modified def CategoryTheory.createsLimitOfFullyFaithfulOfLift'

modified def CategoryTheory.createsLimitOfFullyFaithfulOfLift

modified def CategoryTheory.createsLimitOfFullyFaithfulOfPreserves

modified def CategoryTheory.createsLimitOfReflectsIso'

modified def CategoryTheory.createsLimitOfReflectsIso

Modified Mathlib/CategoryTheory/Limits/ExactFunctor.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

modified def CategoryTheory.Limits.IsColimit.ofFaithful

modified def CategoryTheory.Limits.IsLimit.ofFaithful

Modified Mathlib/CategoryTheory/Limits/KanExtension.lean

modified theorem CategoryTheory.Lan.coreflective

modified theorem CategoryTheory.Ran.reflective

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

modified def CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms

modified def CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms

modified def CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms

modified def CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms

modified def CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms

modified def CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean

modified theorem CategoryTheory.IsPullback.of_map_of_faithful

modified theorem CategoryTheory.IsPushout.of_map_of_faithful

Modified Mathlib/CategoryTheory/Limits/Shapes/Equivalence.lean

modified theorem CategoryTheory.hasInitial_of_equivalence

modified theorem CategoryTheory.hasTerminal_of_equivalence

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

modified def CategoryTheory.Limits.compNatIso

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/Linear/Yoneda.lean

Modified Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Localization/Equivalence.lean

Modified Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean

modified theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'

modified theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence

modified theorem CategoryTheory.LocalizerMorphism.nonempty_isEquivalence_iff

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

modified theorem CategoryTheory.Localization.essSurj

Modified Mathlib/CategoryTheory/Localization/Resolution.lean

modified theorem CategoryTheory.LocalizerMorphism.essSurj_of_hasRightResolutions

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

modified def CategoryTheory.Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Linear.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

modified def CategoryTheory.monoidalCounit

modified def CategoryTheory.monoidalUnit

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

modified def CategoryTheory.exactPairingOfFaithful

modified def CategoryTheory.exactPairingOfFullyFaithful

modified def CategoryTheory.hasLeftDualOfEquivalence

modified def CategoryTheory.hasRightDualOfEquivalence

modified def CategoryTheory.leftRigidCategoryOfEquivalence

modified def CategoryTheory.rightRigidCategoryOfEquivalence

modified def CategoryTheory.rigidCategoryOfEquivalence

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean

modified def CategoryTheory.Monoidal.fromInduced

Modified Mathlib/CategoryTheory/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Pi/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

Modified Mathlib/CategoryTheory/Preadditive/Generator.lean

Modified Mathlib/CategoryTheory/Preadditive/Injective.lean

modified theorem CategoryTheory.Adjunction.injective_of_map_injective

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

Modified Mathlib/CategoryTheory/Preadditive/Projective.lean

modified theorem CategoryTheory.Adjunction.projective_of_map_projective

Modified Mathlib/CategoryTheory/Preadditive/Yoneda/Basic.lean

Modified Mathlib/CategoryTheory/Products/Associator.lean

Modified Mathlib/CategoryTheory/Products/Basic.lean

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/Shift/Induced.lean

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/CategoryTheory/Sigma/Basic.lean

Modified Mathlib/CategoryTheory/SingleObj.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ReflectsPrecoherent.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ReflectsPreregular.lean

Modified Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

modified theorem CategoryTheory.compatiblePreservingOfDownwardsClosed

Modified Mathlib/CategoryTheory/Sites/InducedTopology.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

Modified Mathlib/CategoryTheory/Sites/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Pullback.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

modified def CategoryTheory.Sieve.essSurjFullFunctorGaloisInsertion

modified def CategoryTheory.Sieve.fullyFaithfulFunctorGaloisCoinsertion

Modified Mathlib/CategoryTheory/Skeletal.lean

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/CategoryTheory/Subterminal.lean

Modified Mathlib/CategoryTheory/Sums/Associator.lean

Modified Mathlib/CategoryTheory/Sums/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Rotate.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/CategoryTheory/UnivLE.lean

modified theorem UnivLE.ofEssSurj.{u,

Modified Mathlib/CategoryTheory/Whiskering.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Condensed/Explicit.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean

Modified Mathlib/Order/Category/FinBoolAlg.lean

Modified Mathlib/Order/Category/Frm.lean

Modified Mathlib/Order/Category/Preord.lean

Modified Mathlib/RepresentationTheory/Action/Basic.lean

Modified Mathlib/RepresentationTheory/Action/Monoidal.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

Modified Mathlib/Topology/Category/CompHaus/Projective.lean

Modified Mathlib/Topology/Category/Compactum.lean

modified theorem compactumToCompHaus.essSurj

modified theorem compactumToCompHaus.faithful

modified def compactumToCompHaus.full

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

Modified Mathlib/Topology/Category/Locale.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Projective.lean

Modified Mathlib/Topology/Category/Stonean/Basic.lean

Modified Mathlib/Topology/Category/TopCat/Opens.lean

Modified Mathlib/Topology/Category/TopCommRingCat.lean

Modified Mathlib/Topology/Order/Category/AlexDisc.lean

Modified Mathlib/Topology/Sheaves/Abelian.lean

Modified Mathlib/Topology/Sheaves/Forget.lean

Modified Mathlib/Topology/Sheaves/Functors.lean

Modified Mathlib/Topology/Sheaves/Sheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean