Commit 2024-04-27 09:23 ce289a0e

View on Github →

chore(CategoryTheory): make Functor.Full a Prop (#12449) Before this PR, Functor.Full contained the data of the preimage of maps by a full functor F. This PR makes Functor.Full a proposition. This is to prevent any diamond to appear. The lemma Functor.image_preimage is also renamed Functor.map_preimage.

Estimated changes

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

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

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

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

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

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

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

added theorem CategoryTheory.L_full_of_unit_isIso

added theorem CategoryTheory.R_full_of_counit_isIso

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

modified def CategoryTheory.Adjunction.leftAdjointUniq

modified def CategoryTheory.Adjunction.natIsoOfLeftAdjointNatIso

modified def CategoryTheory.Adjunction.natIsoOfRightAdjointNatIso

modified def CategoryTheory.Adjunction.rightAdjointUniq

Modified Mathlib/CategoryTheory/Adjunction/Restrict.lean

deleted def CategoryTheory.Adjunction.restrictFullyFaithful

Modified Mathlib/CategoryTheory/Category/Cat.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Modified Mathlib/CategoryTheory/Closed/Ideal.lean

Modified Mathlib/CategoryTheory/Comma/Basic.lean

Modified Mathlib/CategoryTheory/Comma/Over.lean

deleted def CategoryTheory.Over.mkIdTerminal

deleted def CategoryTheory.Under.mkIdInitial

Modified Mathlib/CategoryTheory/Comma/StructuredArrow.lean

deleted def CategoryTheory.CostructuredArrow.mkIdTerminal

deleted def CategoryTheory.StructuredArrow.mkIdInitial

Modified Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/CategoryTheory/Endomorphism.lean

deleted def CategoryTheory.Functor.autMulEquivOfFullyFaithful

deleted def CategoryTheory.Functor.mulEquivOfFullyFaithful

Modified Mathlib/CategoryTheory/EpiMono.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/EssentialImage.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/FullSubcategory.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

deleted def CategoryTheory.Functor.splitEpiEquiv

deleted def CategoryTheory.Functor.splitMonoEquiv

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

deleted def CategoryTheory.Functor.Full.ofCompFaithful

deleted def CategoryTheory.Functor.Full.ofCompFaithfulIso

deleted def CategoryTheory.Functor.Full.ofIso

added theorem CategoryTheory.Functor.Full.of_comp_faithful

added theorem CategoryTheory.Functor.Full.of_comp_faithful_iso

added theorem CategoryTheory.Functor.Full.of_iso

deleted def CategoryTheory.Functor.fullyFaithfulCancelRight

deleted theorem CategoryTheory.Functor.image_preimage

added theorem CategoryTheory.Functor.map_preimage

deleted def CategoryTheory.Functor.preimage

deleted def CategoryTheory.Functor.preimageIso

deleted def CategoryTheory.NatIso.equivOfCompFullyFaithful

deleted def CategoryTheory.NatTrans.equivOfCompFullyFaithful

deleted def CategoryTheory.equivOfFullyFaithful

deleted def CategoryTheory.isoEquivOfFullyFaithful

deleted def CategoryTheory.natIsoOfCompFullyFaithful

deleted def CategoryTheory.natTransOfCompFullyFaithful

Modified Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

Modified Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Modified Mathlib/CategoryTheory/IsConnected.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/Creates.lean

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

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

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

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

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Linear/Yoneda.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

added theorem CategoryTheory.Localization.faithful_whiskeringLeft

added theorem CategoryTheory.Localization.full_whiskeringLeft

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/Opposites.lean

Modified Mathlib/CategoryTheory/Preadditive/Mat.lean

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

Modified Mathlib/CategoryTheory/Quotient.lean

Modified Mathlib/CategoryTheory/Shift/Induced.lean

Modified Mathlib/CategoryTheory/Shift/InducedShiftSequence.lean

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/CategoryTheory/Shift/Quotient.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/Coherent/SheafComparison.lean

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

added def CategoryTheory.Sheaf.homEquiv

Modified Mathlib/CategoryTheory/Sites/SheafHom.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

Modified Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.Coyoneda.map_preimage

added def CategoryTheory.Coyoneda.preimage

added def CategoryTheory.Coyoneda.preimageIso

added def CategoryTheory.Coyoneda.preimageNatIso

added def CategoryTheory.Coyoneda.preimageNatTrans

modified def CategoryTheory.Yoneda.ext

added theorem CategoryTheory.Yoneda.map_preimage

added def CategoryTheory.Yoneda.preimage

added def CategoryTheory.Yoneda.preimageIso

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

modified def AlgebraicGeometry.LocallyRingedSpace.restrictTopIso

Modified Mathlib/Geometry/RingedSpace/SheafedSpace.lean

added def AlgebraicGeometry.SheafedSpace.isoMk

Modified Mathlib/Order/Category/FinBoolAlg.lean

Modified Mathlib/Order/Category/Preord.lean

Modified Mathlib/RepresentationTheory/Action/Limits.lean

deleted def Action.preservesColimitOfPreserves

deleted def Action.preservesColimitsOfShapeOfPreserves

deleted def Action.preservesColimitsOfSizeOfPreserves

deleted def Action.preservesLimitOfPreserves

deleted def Action.preservesLimitsOfShapeOfPreserves

deleted def Action.preservesLimitsOfSizeOfPreserves

Modified Mathlib/Topology/Category/Compactum.lean

deleted theorem compactumToCompHaus.essSurj

deleted theorem compactumToCompHaus.faithful

deleted def compactumToCompHaus.full

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

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

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

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

Modified Mathlib/Topology/Category/UniformSpace.lean

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

Modified Mathlib/Topology/Sheaves/Sheaf.lean