Commit 2024-09-10 12:58 f7eae0a3

View on Github →

refactor(CategoryTheory/Adjunction): switch to unit-counit definition of adjunction (#16317) This makes the lemmas homEquiv_unit and homEquiv_counit definitional equalities. This results in a reduction in erws and makes automation work slightly better.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

modified def CommGrp.forget₂CommMonAdj

modified def Grp.forget₂MonAdj

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

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

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

added theorem PresheafOfModules.sheaififcationAdjunction_homEquiv_apply

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

modified def AlgebraicGeometry.ΓSpec.adjunction

modified def AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

added structure CategoryTheory.Adjunction.CoreHomEquivUnitCounit

modified def CategoryTheory.Adjunction.comp

added theorem CategoryTheory.Adjunction.comp_homEquiv

added theorem CategoryTheory.Adjunction.eq_unit_comp_map_iff

added def CategoryTheory.Adjunction.homEquiv

deleted theorem CategoryTheory.Adjunction.left_triangle_components

added def CategoryTheory.Adjunction.mk'

added theorem CategoryTheory.Adjunction.mk'_homEquiv

added theorem CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv

modified def CategoryTheory.Adjunction.mkOfUnitCounit

deleted theorem CategoryTheory.Adjunction.right_triangle_components

added theorem CategoryTheory.Adjunction.unit_comp_map_eq_iff

modified def CategoryTheory.Equivalence.toAdjunction

Modified Mathlib/CategoryTheory/Adjunction/Comma.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

modified def CategoryTheory.Adjunction.functorialityAdjunction'

modified def CategoryTheory.Adjunction.functorialityAdjunction

Modified Mathlib/CategoryTheory/Adjunction/Mates.lean

Modified Mathlib/CategoryTheory/Adjunction/Opposites.lean

Modified Mathlib/CategoryTheory/Adjunction/Restrict.lean

Modified Mathlib/CategoryTheory/Adjunction/Whiskering.lean

Modified Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

modified def CategoryTheory.Cat.connectedComponentsTypeToCatAdj

modified def CategoryTheory.Cat.typeToCatObjectsAdj

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Closed/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Closed/Ideal.lean

Modified Mathlib/CategoryTheory/Closed/Monoidal.lean

modified theorem CategoryTheory.MonoidalClosed.uncurry_eq

Modified Mathlib/CategoryTheory/Closed/Types.lean

Modified Mathlib/CategoryTheory/Functor/EpiMono.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

modified def CategoryTheory.Limits.colimConstAdj

modified def CategoryTheory.Limits.constLimAdj

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean

Modified Mathlib/CategoryTheory/Monoidal/Subcategory.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

Modified Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

Modified Mathlib/CategoryTheory/Skeletal.lean

modified def CategoryTheory.ThinSkeleton.lowerAdjunction

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/RepresentationTheory/Rep.lean

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

modified def TopCat.adj₁

modified def TopCat.adj₂

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

modified def IsOpenMap.adjunctionNhds

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

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

modified def Locale.adjunctionTopToLocalePT

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

deleted def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk

deleted theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper

deleted theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk