Commit 2023-03-02 07:55 04511758

View on Github →

feat: port CategoryTheory.Limits.Shapes.Terminal (#2459)

Estimated changes

Modified Mathlib.lean

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

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

added theorem CategoryTheory.Limits.InitialMonoClass.of_initial

added theorem CategoryTheory.Limits.InitialMonoClass.of_isInitial

added theorem CategoryTheory.Limits.InitialMonoClass.of_isTerminal

added theorem CategoryTheory.Limits.InitialMonoClass.of_terminal

added theorem CategoryTheory.Limits.IsInitial.epi_to

added theorem CategoryTheory.Limits.IsInitial.hasInitial

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.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.IsTerminal.comp_from

added def CategoryTheory.Limits.IsTerminal.from

added theorem CategoryTheory.Limits.IsTerminal.from_self

added theorem CategoryTheory.Limits.IsTerminal.hasTerminal

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.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.colimitConstInitial

added def CategoryTheory.Limits.colimitOfDiagramInitial

added def CategoryTheory.Limits.colimitOfDiagramTerminal

added def CategoryTheory.Limits.colimitOfInitial

added def CategoryTheory.Limits.colimitOfTerminal

added def CategoryTheory.Limits.coneOfDiagramInitial

added def CategoryTheory.Limits.coneOfDiagramTerminal

added theorem CategoryTheory.Limits.hasInitialChangeDiagram

added theorem CategoryTheory.Limits.hasInitialChangeUniverse

added theorem CategoryTheory.Limits.hasInitial_of_hasTerminal_op

added theorem CategoryTheory.Limits.hasInitial_of_unique

added theorem CategoryTheory.Limits.hasTerminalChangeDiagram

added theorem CategoryTheory.Limits.hasTerminalChangeUniverse

added theorem CategoryTheory.Limits.hasTerminal_of_hasInitial_op

added theorem CategoryTheory.Limits.hasTerminal_of_unique

added theorem CategoryTheory.Limits.initial.to_comp

added def CategoryTheory.Limits.initialComparison

added def CategoryTheory.Limits.initialIsInitial

added def CategoryTheory.Limits.initialIsoIsInitial

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 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.limitConstTerminal

added theorem CategoryTheory.Limits.limitConstTerminal_inv_π

added def CategoryTheory.Limits.limitOfDiagramInitial

added def CategoryTheory.Limits.limitOfDiagramTerminal

added def CategoryTheory.Limits.limitOfInitial

added def CategoryTheory.Limits.limitOfTerminal

added theorem CategoryTheory.Limits.terminal.comp_from

added def CategoryTheory.Limits.terminalComparison

added def CategoryTheory.Limits.terminalIsTerminal

added def CategoryTheory.Limits.terminalIsoIsTerminal

added def CategoryTheory.Limits.terminalOpOfInitial

added def CategoryTheory.Limits.terminalUnopOfInitial

added theorem CategoryTheory.Limits.ι_colimitConstInitial_hom