[Merged by Bors] - feat(CategoryTheory): left and right lifting properties#19135
Closed
[Merged by Bors] - feat(CategoryTheory): left and right lifting properties#19135
Conversation
PR summary 2ee843a3b2Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.LiftingProperties.Basic | 305 | 312 | +7 (+2.30%) |
Import changes for all files
| Files | Import difference |
|---|---|
983 filesMathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.LeftHomology Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.CategoryTheory.Abelian.Generator Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.CategoryTheory.Limits.Constructions.Filtered Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.CategoryTheory.Monad.Algebra Mathlib.CategoryTheory.Sites.Pullback Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Homology.ShortComplex.RightHomology Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.CategoryTheory.Limits.Shapes.KernelPair Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.CategoryTheory.Shift.Predicate Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Sites.Sieves Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Homology.Opposite Mathlib.CategoryTheory.Sites.SheafHom Mathlib.Algebra.Category.Grp.Subobject Mathlib.CategoryTheory.Action.Continuous Mathlib.Algebra.Category.Grp.AB Mathlib.CategoryTheory.Subobject.Types Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Analysis.Convex.Birkhoff Mathlib.CategoryTheory.Limits.Cones Mathlib.Algebra.Category.Ring.Instances Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.CategoryTheory.Limits.Shapes.Kernels Mathlib.CategoryTheory.Limits.TypesFiltered Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.CategoryTheory.Abelian.Ext Mathlib.Algebra.Category.ModuleCat.AB Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Topology.Sheaves.Sheaf Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.RingTheory.Flat.Basic Mathlib.Algebra.Homology.Additive Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.Condensed.TopComparison Mathlib.CategoryTheory.Localization.Bifunctor Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.CategoryTheory.Functor.KanExtension.Pointwise Mathlib.CategoryTheory.Localization.FiniteProducts Mathlib.CategoryTheory.Limits.Preserves.Yoneda Mathlib.Condensed.Discrete.Basic Mathlib.CategoryTheory.Subobject.Limits Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.CategoryTheory.Adjunction.Comma Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.CategoryTheory.Monoidal.Linear Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.CategoryTheory.Subobject.Basic Mathlib.CategoryTheory.Limits.Constructions.Pullbacks Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.RingTheory.Regular.RegularSequence Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.Combinatorics.Hall.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.MorphismProperty.Representable Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Monad.Monadicity Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.SingleObj Mathlib.CategoryTheory.ConcreteCategory.EpiMono Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Algebra.Category.Semigrp.Basic Mathlib.Algebra.Homology.ShortComplex.PreservesHomology Mathlib.Condensed.Light.Explicit Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Limits.IsLimit Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc Mathlib.Topology.Category.LightProfinite.Extend Mathlib.CategoryTheory.GlueData Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.RingTheory.RingHom.FiniteType Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.GradedObject.Monoidal Mathlib.CategoryTheory.Enriched.Basic Mathlib.CategoryTheory.Limits.Preserves.Opposites Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows Mathlib.CategoryTheory.Dialectica.Basic Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Filtered.Final Mathlib.Topology.Sheaves.CommRingCat Mathlib.Algebra.Homology.ShortComplex.Basic Mathlib.CategoryTheory.Limits.FunctorToTypes Mathlib.CategoryTheory.Sites.Preserves Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Algebra.Category.Grp.Abelian Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.CategoryTheory.Action.Limits Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.CategoryTheory.Sites.EpiMono Mathlib.AlgebraicTopology.CechNerve Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Abelian.Opposite Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.CategoryTheory.Subobject.WellPowered Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers Mathlib.CategoryTheory.Preadditive.Generator Mathlib.Condensed.Explicit Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.RingTheory.Localization.Finiteness Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Condensed.Discrete.Characterization Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Comma.StructuredArrow.Basic Mathlib.Algebra.Category.Grp.Kernels Mathlib.CategoryTheory.Limits.Elements Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.CategoryTheory.Closed.Ideal Mathlib.Topology.Sheaves.Forget Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.CategoryTheory.Shift.Adjunction Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Condensed.Light.CartesianClosed Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.CategoryTheory.Preadditive.Projective Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.CategoryTheory.Sites.Continuous Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.CategoryTheory.Comma.Presheaf.Basic Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone Mathlib.CategoryTheory.Localization.Pi Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.CategoryTheory.Adjunction.PartialAdjoint Mathlib.RepresentationTheory.Rep Mathlib.CategoryTheory.Monad.Equalizer Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Monoidal.Center Mathlib.RingTheory.RingHom.Flat Mathlib.CategoryTheory.Filtered.Basic Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.Algebra.Homology.BifunctorFlip Mathlib.CategoryTheory.Limits.Shapes.Images Mathlib.Algebra.Homology.TotalComplexShift Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.CategoryTheory.Limits.Shapes.Terminal Mathlib.CategoryTheory.Limits.Preserves.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Products Mathlib.CategoryTheory.Localization.Opposite Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.CategoryTheory.Limits.Presheaf Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.AlgebraicGeometry.Sites.Small Mathlib.MeasureTheory.Category.MeasCat Mathlib.AlgebraicGeometry.Spec Mathlib.Order.Category.OmegaCompletePartialOrder Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory Mathlib.NumberTheory.Cyclotomic.Three Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.Unramified.Field Mathlib.CategoryTheory.Closed.Functor Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.CategoryTheory.Shift.Quotient Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts Mathlib.AlgebraicGeometry.ResidueField Mathlib.CategoryTheory.Limits.Shapes.RegularMono Mathlib.CategoryTheory.Monoidal.Hopf_ Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.CategoryTheory.Limits.Preserves.Limits Mathlib.RingTheory.Flat.Localization Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Homology.Square Mathlib.CategoryTheory.GradedObject.Associator Mathlib.CategoryTheory.Action Mathlib.CategoryTheory.Limits.Shapes.End Mathlib.CategoryTheory.Category.Pairwise Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Enriched.FunctorCategory Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers Mathlib.Algebra.Category.ModuleCat.Products Mathlib.AlgebraicGeometry.Over Mathlib.CategoryTheory.Monoidal.Braided.Reflection Mathlib.CategoryTheory.Bicategory.Kan.IsKan Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Category.Profinite.AsLimit Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.Pretopology Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor Mathlib.CategoryTheory.Comma.StructuredArrow.Small Mathlib.CategoryTheory.Monad.EquivMon Mathlib.AlgebraicGeometry.Pullbacks Mathlib.CategoryTheory.Monoidal.Types.Basic Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Abelian Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.MonCat.Limits Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.CategoryTheory.EffectiveEpi.Enough Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Limits.Constructions.EpiMono Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero Mathlib.CategoryTheory.Monad.Types Mathlib.CategoryTheory.Preadditive.OfBiproducts Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.CategoryTheory.Limits.ColimitLimit Mathlib.CategoryTheory.Sites.Localization Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.CategoryTheory.Limits.Yoneda Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Condensed.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks Mathlib.CategoryTheory.Enriched.Opposite Mathlib.CategoryTheory.Sites.Closed Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Limits.Creates Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts Mathlib.CategoryTheory.Monoidal.Bimon_ Mathlib.CategoryTheory.Subterminal Mathlib.Condensed.Discrete.LocallyConstant Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Filtered.Small Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.CategoryTheory.Limits.Preserves.Presheaf Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.Algebra.Homology.ShortComplex.Homology Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.CategoryTheory.Monad.Comonadicity Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.CategoryTheory.Functor.EpiMono Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.CategoryTheory.Monad.Basic Mathlib.Combinatorics.Configuration Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone Mathlib.AlgebraicGeometry.Properties Mathlib.CategoryTheory.ChosenFiniteProducts.Cat Mathlib.RingTheory.Etale.Field Mathlib.CategoryTheory.SmallObject.Construction Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.CategoryTheory.Endofunctor.Algebra Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.CategoryTheory.Localization.Prod Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.CategoryTheory.Action.Basic Mathlib.RepresentationTheory.Invariants Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.CategoryTheory.Adjunction.Triple Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.Flat.CategoryTheory Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.Condensed.Solid Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.CategoryTheory.Monoidal.Types.Coyoneda Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.Condensed.Discrete.Module Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.CompHaus.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.CategoryTheory.Limits.Shapes.Diagonal Mathlib.AlgebraicTopology.SingularSet Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Sites.EffectiveEpimorphic Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Homology.ImageToKernel Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.AlgebraicGeometry.RationalMap Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Category.CompHaus.Projective Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.Topology.Gluing Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.CategoryTheory.Preadditive.Mat Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.FieldTheory.Galois.Profinite Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.FieldTheory.LinearDisjoint Mathlib.AlgebraicGeometry.Cover.Over Mathlib.CategoryTheory.DifferentialObject Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Monoidal.Mod_ Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.EffectiveEpi.Comp Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ Mathlib.NumberTheory.MulChar.Duality Mathlib.Condensed.Light.Epi Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.GuitartExact.Basic Mathlib.CategoryTheory.Abelian.Injective Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.Algebra.Category.GrpWithZero Mathlib.Topology.Category.Profinite.Projective Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.RepresentationTheory.Character Mathlib.CategoryTheory.Limits.Shapes.Equalizers Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.CategoryTheory.Filtered.Grothendieck Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.CategoryTheory.Galois.Decomposition Mathlib.NumberTheory.FLT.Three Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Topology.Category.Profinite.Basic Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.Abelian.Projective Mathlib.CategoryTheory.Sites.Limits Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.CategoryTheory.Subobject.MonoOver Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.CategoryTheory.Grothendieck Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Geometry.RingedSpace.Basic Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Topology.CWComplex Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.CategoryTheory.Localization.Adjunction Mathlib.Topology.Category.CompHaus.Limits Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Linear.Basic Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.Algebra.Category.Grp.Preadditive Mathlib.RingTheory.RingHom.Integral Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.AlgebraicGeometry.AffineSpace Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.Condensed.TopCatAdjunction Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Limits.Opposites Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.CategoryTheory.Adjunction.Evaluation Mathlib.CategoryTheory.Monoidal.Mon_ Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Category.Ring.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.CategoryTheory.Preadditive.Basic Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.CategoryTheory.Limits.ConeCategory Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Topology.Category.TopCat.Opens Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory Mathlib.CategoryTheory.CofilteredSystem Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.Algebra.Homology.Refinements Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.Algebra.Category.MonCat.Colimits Mathlib.Algebra.Module.PID Mathlib.CategoryTheory.Closed.FunctorCategory.Complete Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence Mathlib.CategoryTheory.Limits.IsConnected Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.CategoryTheory.Limits.Comma Mathlib.Topology.Category.CompactlyGenerated Mathlib.CategoryTheory.Sites.Spaces Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts Mathlib.CategoryTheory.Shift.Induced Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Sites.Sheafification Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Monoidal.Limits Mathlib.CategoryTheory.Sites.Coverage Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.CategoryTheory.Limits.Final.ParallelPair Mathlib.CategoryTheory.Limits.Filtered Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Topology.Sheaves.Limits Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.Algebra.Homology.ShortComplex.QuasiIso Mathlib.CategoryTheory.Limits.Shapes.Countable Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Limits.Shapes.Equivalence Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Monoidal.Internal.Limits Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Homology.Localization Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.RingTheory.Localization.Free Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.CategoryTheory.Simple Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.NumberTheory.Cyclotomic.PID Mathlib.CategoryTheory.Preadditive.Injective Mathlib.CategoryTheory.Monad.Limits Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.CategoryTheory.Monoidal.Rigid.Braided Mathlib.CategoryTheory.Monoidal.Comon_ Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.CategoryTheory.Limits.Fubini Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.GradedObject.Trifunctor Mathlib.CategoryTheory.Adjunction.Limits Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.AlgebraicGeometry.AffineScheme Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.CategoryTheory.Abelian.Images Mathlib.CategoryTheory.Limits.Shapes.Reflexive Mathlib.CategoryTheory.Limits.ExactFunctor Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.GuitartExact.VerticalComposition Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.Algebra.Category.Grp.Images Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Condensed.Light.AB Mathlib.Algebra.Homology.SingleHomology Mathlib.AlgebraicTopology.SimplexCategory Mathlib.CategoryTheory.GradedObject Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Subobject.Comma Mathlib.CategoryTheory.Closed.Types Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.CategoryTheory.Limits.Shapes.Types Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Comma.OverClass Mathlib.CategoryTheory.Shift.SingleFunctors Mathlib.Algebra.Category.Ring.Limits Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Limits.Shapes.PiProd Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Shift.Localization Mathlib.Topology.Category.Compactum Mathlib.CategoryTheory.Shift.CommShift Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Adjunction.Over Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Limits.Preserves.Filtered Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts Mathlib.Geometry.RingedSpace.Stalks Mathlib.CategoryTheory.GradedObject.Single Mathlib.Condensed.Light.Limits Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Algebra.Homology.TotalComplex Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.CategoryTheory.Adjunction.Lifting.Left Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits Mathlib.Condensed.Discrete.Colimit Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Filtered.Connected Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Topology.Category.Profinite.Extend Mathlib.RingTheory.RingHom.Locally Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.RepresentationTheory.FDRep Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.Condensed.CartesianClosed Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.CategoryTheory.Limits.IndYoneda Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.RingTheory.Trace.Quotient Mathlib.Topology.Category.Stonean.Basic Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Comma.StructuredArrow.Functor Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Algebra.Homology.DifferentialObject Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.CategoryTheory.Limits.Constructions.Equalizers Mathlib.CategoryTheory.GradedObject.Braiding Mathlib.Topology.Category.LightProfinite.Basic Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.EffectiveEpi.Coproduct Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.RingTheory.LocalProperties.Reduced Mathlib.CategoryTheory.GradedObject.Bifunctor Mathlib.CategoryTheory.GradedObject.Unitor Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.Algebra.Category.CoalgebraCat.Monoidal Mathlib.Algebra.Homology.LocalCohomology Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.CategoryTheory.Abelian.Exact Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.CategoryTheory.Comma.Final Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.CategoryTheory.Monoidal.CommMon_ Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.AlgebraicGeometry.Scheme Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Algebra.Homology.QuasiIso Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Condensed.Light.Basic Mathlib.AlgebraicGeometry.Gluing Mathlib.Topology.Sheaves.Functors Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Subobject.Lattice Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RingTheory.RingHomProperties Mathlib.AlgebraicGeometry.Cover.Open Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Algebra.Category.Ring.Constructions Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.Topology.Category.Locale Mathlib.CategoryTheory.Localization.SmallHom Mathlib.Algebra.Category.Grp.Limits Mathlib.CategoryTheory.Limits.EssentiallySmall Mathlib.CategoryTheory.Comma.Over Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.CategoryTheory.Monoidal.Types.Symmetric Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Algebra.Homology.Linear Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.RingTheory.LinearDisjoint Mathlib.CategoryTheory.Category.Factorisation Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.Functor Mathlib.RingTheory.LocalRing.Module Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.CategoryTheory.ConcreteCategory.Elementwise Mathlib.CategoryTheory.Limits.VanKampen Mathlib.Topology.Sheaves.Skyscraper Mathlib.CategoryTheory.Elements Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Sites.SheafOfTypes Mathlib.CategoryTheory.Abelian.GrothendieckCategory Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts Mathlib.CategoryTheory.Generator Mathlib.CategoryTheory.Limits.Over Mathlib.Algebra.Category.Grp.Biproducts Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.CategoryTheory.Functor.ReflectsIso Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.ExactSequence Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Adjunction.Lifting.Right Mathlib.CategoryTheory.Limits.Shapes.IsTerminal Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.CategoryTheory.Functor.FunctorHom Mathlib.Order.Category.Frm Mathlib.RingTheory.LocalProperties.Basic Mathlib.NumberTheory.NumberField.House Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic Mathlib.Algebra.Category.Grp.Colimits Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.CategoryTheory.Limits.Shapes.StrongEpi Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.Condensed.Epi Mathlib.CategoryTheory.Limits.Shapes.StrictInitial Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting Mathlib.CategoryTheory.Localization.Predicate Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.Algebra.Homology.Homotopy Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects Mathlib.CategoryTheory.MorphismProperty.OverAdjunction Mathlib.RingTheory.Flat.Equalizer Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.CategoryTheory.Extensive Mathlib.Algebra.Homology.CommSq Mathlib.CategoryTheory.Monad.Products Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.CategoryTheory.ChosenFiniteProducts Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial Mathlib.CategoryTheory.Enriched.HomCongr Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.Topology.Sheaves.PUnit Mathlib.Algebra.Category.ModuleCat.Free Mathlib.CategoryTheory.Monad.Coequalizer Mathlib.AlgebraicTopology.MooreComplex Mathlib.Condensed.Light.Functors Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.Topology.Sheaves.Presheaf Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.Limits.HasLimits Mathlib.CategoryTheory.Closed.Enrichment Mathlib.CategoryTheory.Limits.Shapes.Biproducts Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.Algebra.Category.MonCat.ForgetCorepresentable Mathlib.CategoryTheory.Functor.KanExtension.Basic Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic Mathlib.CategoryTheory.Closed.Zero Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory Mathlib.CategoryTheory.SmallObject.Iteration.Basic Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.CategoryTheory.Closed.FunctorToTypes Mathlib.Algebra.Homology.Bifunctor Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.CategoryTheory.Limits.Lattice Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Augment Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.RingTheory.Flat.Stability Mathlib.CategoryTheory.Limits.FintypeCat Mathlib.CategoryTheory.Sites.Adjunction Mathlib.Condensed.Functors Mathlib.Algebra.Category.ModuleCat.Images Mathlib.CategoryTheory.Limits.Pi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.Limits.EpiMono Mathlib.Topology.Category.TopCat.Yoneda Mathlib.CategoryTheory.Limits.Preserves.Ulift Mathlib.CategoryTheory.Monoidal.Bimod Mathlib.Topology.Category.TopCommRingCat Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Bicategory.Extension Mathlib.Condensed.Equivalence Mathlib.CategoryTheory.Sites.IsSheafFor Mathlib.CategoryTheory.EffectiveEpi.Basic Mathlib.CategoryTheory.Closed.Cartesian Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Topology.Category.Profinite.Product Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.Topology.Category.Profinite.Limits Mathlib.CategoryTheory.Galois.EssSurj Mathlib.Topology.Category.UniformSpace Mathlib.CategoryTheory.Linear.Yoneda Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.Algebra.Homology.HomologySequence Mathlib.CategoryTheory.Comma.Presheaf.Colimit Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.CategoryTheory.Shift.Basic Mathlib.CategoryTheory.Category.Grpd Mathlib.CategoryTheory.LiftingProperties.Adjunction Mathlib.CategoryTheory.Limits.Preserves.Finite Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.RingTheory.RingHom.Surjective Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.Limits.Unit Mathlib.RingTheory.DedekindDomain.PID Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.BoolRing Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.CategoryTheory.Action.Concrete Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.CategoryTheory.Localization.Resolution Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Homology.HomotopyCategory Mathlib.CategoryTheory.Limits.Shapes.Products Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Homology.ShortComplex.Limits Mathlib.Topology.Sheaves.Sheafify Mathlib.RingTheory.Unramified.Finite Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.CategoryTheory.MorphismProperty.Limits Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.CategoryTheory.Localization.Equivalence Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct Mathlib.CategoryTheory.Functor.Flat Mathlib.CategoryTheory.Monoidal.Conv Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.Algebra.Homology.BifunctorShift Mathlib.CategoryTheory.EffectiveEpi.RegularEpi Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.CategoryTheory.Limits.FunctorCategory.Finite Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.CategoryTheory.Sites.Grothendieck Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Topology.Sheaves.Stalks Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Limits.Final Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Enriched.Ordinary Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.ConcreteCategory Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Monad.Kleisli Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.CategoryTheory.WithTerminal Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.CategoryTheory.Limits.Types Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.Category.Stonean.Limits Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.CategoryTheory.Limits.Sifted Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.CategoryTheory.Limits.MonoCoprod Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.CategoryTheory.Limits.FunctorCategory.Basic Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit Mathlib.CategoryTheory.Sites.CoverLifting |
1 |
Mathlib.CategoryTheory.LiftingProperties.Basic |
7 |
Mathlib.CategoryTheory.LiftingProperties.Limits (new file) |
576 |
Mathlib.CategoryTheory.MorphismProperty.LiftingProperty (new file) |
591 |
Declarations diff
+ IsPullback.hasLiftingProperty
+ IsPushout.hasLiftingProperty
+ IsStableUnderCobaseChange.isomorphisms
+ IsStableUnderColimitsOfShape
+ IsStableUnderColimitsOfShape.colim_map
+ IsStableUnderCoproductsOfShape
+ IsStableUnderCoproductsOfShape.mk
+ IsStableUnderFiniteCoproducts
+ RetractArrow.leftLiftingProperty
+ RetractArrow.rightLiftingProperty
+ instance [HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty p g] :
+ instance [HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty p t] :
+ instance [HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty f p] :
+ instance [HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty s p] :
+ instance {J : Type*} {A B : J → C} [HasCoproduct A] [HasCoproduct B]
+ instance {J : Type*} {A B : J → C} [HasProduct A] [HasProduct B]
+ isStableUnderCoproductsOfShape_of_isStableUnderFiniteCoproducts
+ llp
+ llp_IsStableUnderCoproductsOfShape
+ llp_isMultiplicative
+ llp_isStableUnderCobaseChange
+ llp_isStableUnderRetracts
+ rlp
+ rlp_IsStableUnderProductsOfShape
+ rlp_isMultiplicative
+ rlp_isStableUnderBaseChange
+ rlp_isStableUnderRetracts
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 17, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
joelriou
reviewed
Nov 18, 2024
Contributor
|
It could be advisable to split this PR into two:
|
Collaborator
Author
I think that's a good call. I'll split the PR. |
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
joelriou
reviewed
Dec 21, 2024
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Dec 22, 2024
Defines left/right lifting property wrt a `MorphismProperty` and shows basic closure properties (retracts, pullback/pushout, composition etc.). Co-authored-by: Jack McKoen <104791831+mckoen@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Defines left/right lifting property wrt a
MorphismPropertyand shows basic closure properties (retracts, pullback/pushout, composition etc.).