Commit 2025-12-04 09:22 ef5118fd

View on Github →

feat(CategoryTheory): Pullback of equalizer is an equalizer (#30120) We show that the pullback of an equalizer (seen as a subobject) along some morphism h is the subobject that comes from the equalizer of the two original arrows precomposed with h. A TODO was completed in the process. This is a prerequisite of the MTT project, which aims to use the internal language of toposes to reason about e.g. sheaves.

Estimated changes

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

added theorem CategoryTheory.Limits.hasEqualizer_precomp_of_equalizer

added def CategoryTheory.Limits.isLimitPrecompFork

added def CategoryTheory.Limits.liftPrecomp

added def CategoryTheory.Limits.precompFork

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean

modified def CategoryTheory.Limits.PullbackCone.mk

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

added theorem CategoryTheory.Subobject.skeletal

Modified Mathlib/CategoryTheory/Subobject/FactorThru.lean

added def CategoryTheory.Subobject.homOfFactors

added theorem CategoryTheory.Subobject.le_of_factors

Modified Mathlib/CategoryTheory/Subobject/Limits.lean

added theorem CategoryTheory.Limits.pullback_equalizer

added theorem CategoryTheory.Limits.pullback_factors

added theorem CategoryTheory.Limits.pullback_factors_iff