Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-16 19:53
c47b5709
View on Github →
chore(CategoryTheory): fix whitespace (
#32928
)
Estimated changes
Modified
Mathlib/CategoryTheory/Abelian/Injective/Basic.lean
Modified
Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
Modified
Mathlib/CategoryTheory/Abelian/LeftDerived.lean
Modified
Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
Modified
Mathlib/CategoryTheory/Adjunction/Additive.lean
Modified
Mathlib/CategoryTheory/Adjunction/Evaluation.lean
Modified
Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean
Modified
Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean
modified
def
CategoryTheory.LiftRightAdjoint.otherMap
Modified
Mathlib/CategoryTheory/Adjunction/Reflective.lean
Modified
Mathlib/CategoryTheory/Adjunction/Triple.lean
modified
theorem
CategoryTheory.Adjunction.Triple.op_rightToLeft
Modified
Mathlib/CategoryTheory/Bicategory/Adjunction/Mate.lean
Modified
Mathlib/CategoryTheory/Bicategory/CatEnriched.lean
Modified
Mathlib/CategoryTheory/Bicategory/EqToHom.lean
Modified
Mathlib/CategoryTheory/Bicategory/Extension.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/Lax.lean
Modified
Mathlib/CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean
Modified
Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean
Modified
Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean
modified
def
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.hom
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean
Modified
Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Pseudo.lean
Modified
Mathlib/CategoryTheory/Bicategory/Strict/Pseudofunctor.lean
Modified
Mathlib/CategoryTheory/CodiscreteCategory.lean
modified
def
CategoryTheory.Codiscrete.functorToCat
Modified
Mathlib/CategoryTheory/Comma/CardinalArrow.lean
Modified
Mathlib/CategoryTheory/Comma/Final.lean
Modified
Mathlib/CategoryTheory/Comma/Over/Pullback.lean
Modified
Mathlib/CategoryTheory/Core.lean
Modified
Mathlib/CategoryTheory/EffectiveEpi/Preserves.lean
Modified
Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean
modified
theorem
CategoryTheory.BasedFunctor.comp_id
Modified
Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
Modified
Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
Modified
Mathlib/CategoryTheory/Filtered/Small.lean
Modified
Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean
Modified
Mathlib/CategoryTheory/Functor/FunctorHom.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
Modified
Mathlib/CategoryTheory/Generator/Basic.lean
Modified
Mathlib/CategoryTheory/GradedObject/Braiding.lean
Modified
Mathlib/CategoryTheory/GradedObject/Monoidal.lean
Modified
Mathlib/CategoryTheory/Grothendieck.lean
modified
def
CategoryTheory.Grothendieck.functor
Modified
Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean
modified
def
CategoryTheory.FreeGroupoid.mapComp
Modified
Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean
Modified
Mathlib/CategoryTheory/IsConnected.lean
Modified
Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
Modified
Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/Fubini.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/Presheaf.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/End.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
Modified
Mathlib/CategoryTheory/Limits/Sifted.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean
Modified
Mathlib/CategoryTheory/Limits/VanKampen.lean
Modified
Mathlib/CategoryTheory/Linear/Yoneda.lean
Modified
Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
Modified
Mathlib/CategoryTheory/Localization/Construction.lean
Modified
Mathlib/CategoryTheory/Localization/DerivabilityStructure/PointwiseRightDerived.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Basic.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Braided.lean
Modified
Mathlib/CategoryTheory/Localization/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monad/Algebra.lean
Modified
Mathlib/CategoryTheory/Monad/Equalizer.lean
modified
def
CategoryTheory.Comonad.CofreeEqualizer.topMap
Modified
Mathlib/CategoryTheory/Monad/Limits.lean
modified
def
CategoryTheory.Comonad.ForgetCreatesColimits'.γ
Modified
Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Cat.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
modified
def
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnit
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/Closed.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution/DayFunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean
Modified
Mathlib/CategoryTheory/Monoidal/ExternalProduct/KanExtension.lean
Modified
Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
modified
theorem
CategoryTheory.GrpObj.tensorObj.Functor.obj.ι_def
Modified
Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Multifunctor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Opposite.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Composition.lean
Modified
Mathlib/CategoryTheory/MorphismProperty/Representable.lean
Modified
Mathlib/CategoryTheory/Preadditive/LeftExact.lean
Modified
Mathlib/CategoryTheory/Presentable/EssentiallyLarge.lean
Modified
Mathlib/CategoryTheory/Quotient.lean
Modified
Mathlib/CategoryTheory/Shift/Twist.lean
Modified
Mathlib/CategoryTheory/Sites/Adjunction.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/CoherentTopology.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/RegularTopology.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
Modified
Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/CoverLifting.lean
Modified
Mathlib/CategoryTheory/Sites/Coverage.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean
Modified
Mathlib/CategoryTheory/Sites/EpiMono.lean
Modified
Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
modified
def
CategoryTheory.Equalizer.Presieve.Arrows.SecondObj
Modified
Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
Modified
Mathlib/CategoryTheory/Sites/PreservesSheafification.lean
Modified
Mathlib/CategoryTheory/Sites/Sheafification.lean
Modified
Mathlib/CategoryTheory/Sites/Sieves.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
Modified
Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
Modified
Mathlib/CategoryTheory/Subobject/Lattice.lean
Modified
Mathlib/CategoryTheory/Topos/Classifier.lean
Modified
Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
Modified
Mathlib/CategoryTheory/Triangulated/Rotate.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
Modified
Mathlib/CategoryTheory/Triangulated/Triangulated.lean