Commit 2024-10-25 14:58 aea6f296

View on Github →

chore: split Limits/Shapes/Terminal.lean to reduce imports (#18229) The parts that require HasLimit stay in Terminal.lean, and the parts that only require IsLimit go to IsTerminal.lean. Found using the new lake exe unused.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Adjunction/Comma.lean

Modified Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean

Modified Mathlib/CategoryTheory/Comma/Over.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/Endofunctor/Algebra.lean

Created Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

added theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial

added theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal

added theorem CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal

added theorem CategoryTheory.Limits.IsInitial.epi_to

added def CategoryTheory.Limits.IsInitial.equivOfIso

added theorem CategoryTheory.Limits.IsInitial.hom_ext

added theorem CategoryTheory.Limits.IsInitial.isSplitEpi_to

added theorem CategoryTheory.Limits.IsInitial.mono_from

added def CategoryTheory.Limits.IsInitial.ofIso

added def CategoryTheory.Limits.IsInitial.ofUnique

added def CategoryTheory.Limits.IsInitial.ofUniqueHom

added def CategoryTheory.Limits.IsInitial.to

added theorem CategoryTheory.Limits.IsInitial.to_comp

added theorem CategoryTheory.Limits.IsInitial.to_self

added def CategoryTheory.Limits.IsInitial.uniqueUpToIso

added theorem CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial

added theorem CategoryTheory.Limits.IsTerminal.comp_from

added def CategoryTheory.Limits.IsTerminal.equivOfIso

added def CategoryTheory.Limits.IsTerminal.from

added theorem CategoryTheory.Limits.IsTerminal.from_self

added theorem CategoryTheory.Limits.IsTerminal.hom_ext

added theorem CategoryTheory.Limits.IsTerminal.isSplitMono_from

added theorem CategoryTheory.Limits.IsTerminal.mono_from

added def CategoryTheory.Limits.IsTerminal.ofIso

added def CategoryTheory.Limits.IsTerminal.ofUnique

added def CategoryTheory.Limits.IsTerminal.ofUniqueHom

added def CategoryTheory.Limits.IsTerminal.uniqueUpToIso

added def CategoryTheory.Limits.asEmptyCocone

added def CategoryTheory.Limits.asEmptyCone

added def CategoryTheory.Limits.coconeOfDiagramInitial

added def CategoryTheory.Limits.coconeOfDiagramTerminal

added def CategoryTheory.Limits.colimitOfDiagramInitial

added def CategoryTheory.Limits.colimitOfDiagramTerminal

added def CategoryTheory.Limits.coneOfDiagramInitial

added def CategoryTheory.Limits.coneOfDiagramTerminal

added def CategoryTheory.Limits.initialOpOfTerminal

added def CategoryTheory.Limits.initialUnopOfTerminal

added def CategoryTheory.Limits.isColimitChangeEmptyCocone

added def CategoryTheory.Limits.isColimitEmptyCoconeEquiv

added def CategoryTheory.Limits.isInitialBot

added def CategoryTheory.Limits.isInitialEquivUnique

added theorem CategoryTheory.Limits.isIso_of_isInitial

added theorem CategoryTheory.Limits.isIso_of_isTerminal

added def CategoryTheory.Limits.isLimitChangeEmptyCone

added def CategoryTheory.Limits.isLimitEmptyConeEquiv

added def CategoryTheory.Limits.isTerminalEquivUnique

added def CategoryTheory.Limits.isTerminalTop

added def CategoryTheory.Limits.limitOfDiagramInitial

added def CategoryTheory.Limits.limitOfDiagramTerminal

added def CategoryTheory.Limits.terminalOpOfInitial

added def CategoryTheory.Limits.terminalUnopOfInitial

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

deleted theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial

deleted theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal

deleted theorem CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal

deleted theorem CategoryTheory.Limits.IsInitial.epi_to

deleted def CategoryTheory.Limits.IsInitial.equivOfIso

deleted theorem CategoryTheory.Limits.IsInitial.hom_ext

deleted theorem CategoryTheory.Limits.IsInitial.isSplitEpi_to

deleted theorem CategoryTheory.Limits.IsInitial.mono_from

deleted def CategoryTheory.Limits.IsInitial.ofIso

deleted def CategoryTheory.Limits.IsInitial.ofUnique

deleted def CategoryTheory.Limits.IsInitial.ofUniqueHom

deleted def CategoryTheory.Limits.IsInitial.to

deleted theorem CategoryTheory.Limits.IsInitial.to_comp

deleted theorem CategoryTheory.Limits.IsInitial.to_self

deleted def CategoryTheory.Limits.IsInitial.uniqueUpToIso

deleted theorem CategoryTheory.Limits.IsLimit.isIso_π_app_of_isInitial

deleted theorem CategoryTheory.Limits.IsTerminal.comp_from

deleted def CategoryTheory.Limits.IsTerminal.equivOfIso

deleted def CategoryTheory.Limits.IsTerminal.from

deleted theorem CategoryTheory.Limits.IsTerminal.from_self

deleted theorem CategoryTheory.Limits.IsTerminal.hom_ext

deleted theorem CategoryTheory.Limits.IsTerminal.isSplitMono_from

deleted theorem CategoryTheory.Limits.IsTerminal.mono_from

deleted def CategoryTheory.Limits.IsTerminal.ofIso

deleted def CategoryTheory.Limits.IsTerminal.ofUnique

deleted def CategoryTheory.Limits.IsTerminal.ofUniqueHom

deleted def CategoryTheory.Limits.IsTerminal.uniqueUpToIso

deleted def CategoryTheory.Limits.asEmptyCocone

deleted def CategoryTheory.Limits.asEmptyCone

deleted def CategoryTheory.Limits.coconeOfDiagramInitial

deleted def CategoryTheory.Limits.coconeOfDiagramTerminal

deleted def CategoryTheory.Limits.colimitOfDiagramInitial

deleted def CategoryTheory.Limits.colimitOfDiagramTerminal

deleted def CategoryTheory.Limits.coneOfDiagramInitial

deleted def CategoryTheory.Limits.coneOfDiagramTerminal

deleted def CategoryTheory.Limits.initialOpOfTerminal

deleted def CategoryTheory.Limits.initialUnopOfTerminal

deleted def CategoryTheory.Limits.isColimitChangeEmptyCocone

deleted def CategoryTheory.Limits.isColimitEmptyCoconeEquiv

deleted def CategoryTheory.Limits.isInitialBot

deleted def CategoryTheory.Limits.isInitialEquivUnique

deleted theorem CategoryTheory.Limits.isIso_of_isInitial

deleted theorem CategoryTheory.Limits.isIso_of_isTerminal

deleted def CategoryTheory.Limits.isLimitChangeEmptyCone

deleted def CategoryTheory.Limits.isLimitEmptyConeEquiv

deleted def CategoryTheory.Limits.isTerminalEquivUnique

deleted def CategoryTheory.Limits.isTerminalTop

deleted def CategoryTheory.Limits.limitOfDiagramInitial

deleted def CategoryTheory.Limits.limitOfDiagramTerminal

deleted def CategoryTheory.Limits.terminalOpOfInitial

deleted def CategoryTheory.Limits.terminalUnopOfInitial

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean