Commit 2024-06-13 19:34 c9f95f42

View on Github →

chore: move material on limits out of ConcreteCategory.Basic (#13549) This significantly reduces this imports of ConcreteCategory.Basic (the imports never should have been added; one day we will have CI help for this!). There may actually be some duplication between the material I'm moving and the material in the destination file (which @joelriou added last week), but I'm going to declare deduplicating out of scope for this PR, please.

Estimated changes

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

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

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

Modified Mathlib/AlgebraicTopology/SimplexCategory.lean

Modified Mathlib/CategoryTheory/Adhesive.lean

Modified Mathlib/CategoryTheory/Category/Pointed.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

deleted theorem CategoryTheory.ConcreteCategory.bijective_of_isIso

deleted theorem CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout

deleted theorem CategoryTheory.ConcreteCategory.epi_of_surjective

deleted theorem CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback

deleted theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective

deleted theorem CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback

deleted theorem CategoryTheory.ConcreteCategory.mono_of_injective

deleted theorem CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout

Modified Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean

added theorem CategoryTheory.ConcreteCategory.bijective_of_isIso

added theorem CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout

added theorem CategoryTheory.ConcreteCategory.epi_of_surjective

added theorem CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback

added theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective

added theorem CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback

added theorem CategoryTheory.ConcreteCategory.mono_of_injective

added theorem CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout

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

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrd.lean

Modified Mathlib/Order/Category/PartOrd.lean

Modified Mathlib/Order/Category/Preord.lean

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

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

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

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

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean