Test `mk_concrete_category` by dagurtomas · Pull Request #38652 · leanprover-community/mathlib4

dagurtomas · 2026-04-28T15:07:59Z

…erate-concrete # Conflicts: # Mathlib/CategoryTheory/Types/Basic.lean

github-actions · 2026-04-28T15:09:20Z

PR summary 2d59066e04

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
1882 files `Mathlib.Algebra.BrauerGroup.Defs` `Mathlib.Algebra.Category.AlgCat.Basic` `Mathlib.Algebra.Category.AlgCat.Limits` `Mathlib.Algebra.Category.AlgCat.Monoidal` `Mathlib.Algebra.Category.AlgCat.Symmetric` `Mathlib.Algebra.Category.BialgCat.Basic` `Mathlib.Algebra.Category.BialgCat.Monoidal` `Mathlib.Algebra.Category.BoolRing` `Mathlib.Algebra.Category.CoalgCat.Basic` `Mathlib.Algebra.Category.CoalgCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgCat.Monoidal` `Mathlib.Algebra.Category.CommAlgCat.Basic` `Mathlib.Algebra.Category.CommAlgCat.FiniteType` `Mathlib.Algebra.Category.CommAlgCat.Monoidal` `Mathlib.Algebra.Category.CommBialgCat` `Mathlib.Algebra.Category.ContinuousCohomology.Basic` `Mathlib.Algebra.Category.FGModuleCat.Abelian` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.Algebra.Category.FGModuleCat.Colimits` `Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.Algebra.Category.Grp.Basic` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.Algebra.Category.Grp.CartesianMonoidal` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.EpiMono` `Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Algebra.Category.Grp.FiniteGrp` `Mathlib.Algebra.Category.Grp.ForgetCorepresentable` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.LeftExactFunctor` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Algebra.Category.Grp.Shrink` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.Grp.Yoneda` `Mathlib.Algebra.Category.Grp.ZModuleEquivalence` `Mathlib.Algebra.Category.Grp.Zero` `Mathlib.Algebra.Category.GrpWithZero` `Mathlib.Algebra.Category.HopfAlgCat.Basic` `Mathlib.Algebra.Category.HopfAlgCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.Algebra.Category.ModuleCat.Basic` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.Descent` `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting` `Mathlib.Algebra.Category.ModuleCat.Ext.Finite` `Mathlib.Algebra.Category.ModuleCat.Ext.HasExt` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.LeftResolution` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Localization` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.Category.ModuleCat.Semi` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Stalk` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.ModuleCat.Ulift` `Mathlib.Algebra.Category.MonCat.Adjunctions` `Mathlib.Algebra.Category.MonCat.Basic` `Mathlib.Algebra.Category.MonCat.Colimits` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Algebra.Category.MonCat.ForgetCorepresentable` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Category.MonCat.Shrink` `Mathlib.Algebra.Category.MonCat.Yoneda` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Category.Ring.Basic` `Mathlib.Algebra.Category.Ring.Colimits` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Category.Ring.EqualizerPushout` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.Algebra.Category.Ring.FinitePresentation` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.Algebra.Category.Ring.LinearAlgebra` `Mathlib.Algebra.Category.Ring.Topology` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Category.Ring.Under.Property` `Mathlib.Algebra.Category.Semigrp.Basic` `Mathlib.Algebra.Homology.Additive` `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.Algebra.Homology.Augment` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.CochainComplexOpposite` `Mathlib.Algebra.Homology.CochainComplexPlus` `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Homology.ComplexShapeSigns` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear` `Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Map` `Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure` `Mathlib.Algebra.Homology.DerivedCategory.Fractions` `Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.DerivedCategory.KInjective` `Mathlib.Algebra.Homology.DerivedCategory.KProjective` `Mathlib.Algebra.Homology.DerivedCategory.Linear` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom` `Mathlib.Algebra.Homology.DerivedCategory.TStructure` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Algebra.Homology.Double` `Mathlib.Algebra.Homology.Embedding.AreComplementary` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Algebra.Homology.Embedding.CochainComplex` `Mathlib.Algebra.Homology.Embedding.Connect` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.ExtendHomotopy` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.Algebra.Homology.Embedding.RestrictionHomology` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Homology.Embedding.TruncGEHomology` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.Algebra.Homology.Embedding.TruncLEHomology` `Mathlib.Algebra.Homology.Embedding.TruncLE` `Mathlib.Algebra.Homology.EulerCharacteristic` `Mathlib.Algebra.Homology.ExactSequenceFour` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Homology.Factorizations.CM5a` `Mathlib.Algebra.Homology.Factorizations.CM5b` `Mathlib.Algebra.Homology.Functor` `Mathlib.Algebra.Homology.GrothendieckAbelian` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory.Acyclic` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.KInjective` `Mathlib.Algebra.Homology.HomotopyCategory.KProjective` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.Algebra.Homology.LeftResolution.Basic` `Mathlib.Algebra.Homology.LeftResolution.Reduced` `Mathlib.Algebra.Homology.LeftResolution.Transport` `Mathlib.Algebra.Homology.Linear` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.ModelCategory.Lifting` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.Algebra.Homology.ShortComplex.Basic` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.ShortComplex.Homology` `Mathlib.Algebra.Homology.ShortComplex.LeftHomology` `Mathlib.Algebra.Homology.ShortComplex.Limits` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology` `Mathlib.Algebra.Homology.ShortComplex.QuasiIso` `Mathlib.Algebra.Homology.ShortComplex.Retract` `Mathlib.Algebra.Homology.ShortComplex.RightHomology` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.Single` `Mathlib.Algebra.Homology.SpectralObject.Basic` `Mathlib.Algebra.Homology.SpectralObject.Cycles` `Mathlib.Algebra.Homology.SpectralObject.Differentials` `Mathlib.Algebra.Homology.SpectralObject.EpiMono` `Mathlib.Algebra.Homology.SpectralObject.FirstPage` `Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence` `Mathlib.Algebra.Homology.SpectralObject.Homology` `Mathlib.Algebra.Homology.SpectralObject.Page` `Mathlib.Algebra.Homology.SpectralObject.SpectralSequence` `Mathlib.Algebra.Homology.SpectralSequence.Basic` `Mathlib.Algebra.Homology.Square` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.Algebra.Lie.Basis` `Mathlib.Algebra.Lie.Weights.IsSimple` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.SpanRankOperations` `Mathlib.Algebra.Module.Torsion.PrimaryComponent` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.AlgClosed.Basic` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.EffectiveEpi` `Mathlib.AlgebraicGeometry.EllipticCurve.LFunction` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Geometrically.Basic` `Mathlib.AlgebraicGeometry.Geometrically.Connected` `Mathlib.AlgebraicGeometry.Geometrically.Integral` `Mathlib.AlgebraicGeometry.Geometrically.Irreducible` `Mathlib.AlgebraicGeometry.Geometrically.Reduced` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Group.Smooth` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.ConstantSheaf` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Fpqc` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.Proetale` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.CechNerve` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.AlgebraicTopology.ModelCategory.Basic` `Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy` `Mathlib.AlgebraicTopology.ModelCategory.Bifibrant` `Mathlib.AlgebraicTopology.ModelCategory.BrownLemma` `Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy` `Mathlib.AlgebraicTopology.ModelCategory.Cylinder` `Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant` `Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant` `Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy` `Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma` `Mathlib.AlgebraicTopology.ModelCategory.Homotopy` `Mathlib.AlgebraicTopology.ModelCategory.Instances` `Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant` `Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick` `Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy` `Mathlib.AlgebraicTopology.ModelCategory.Opposite` `Mathlib.AlgebraicTopology.ModelCategory.Over` `Mathlib.AlgebraicTopology.ModelCategory.PathObject` `Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated` `Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells` `Mathlib.AlgebraicTopology.RelativeCellComplex.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal` `Mathlib.AlgebraicTopology.SimplexCategory.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms` `Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty` `Mathlib.AlgebraicTopology.SimplexCategory.Rev` `Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory` `Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne` `Mathlib.AlgebraicTopology.SimplexCategory.Truncated` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialObject.Homotopy` `Mathlib.AlgebraicTopology.SimplicialObject.II` `Mathlib.AlgebraicTopology.SimplicialObject.Op` `Mathlib.AlgebraicTopology.SimplicialObject.Split` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Boundary` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated` `Mathlib.AlgebraicTopology.SimplicialSet.CompStruct` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.Degenerate` `Mathlib.AlgebraicTopology.SimplicialSet.Dimension` `Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits` `Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd` `Mathlib.AlgebraicTopology.SimplicialSet.Finite` `Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.Homotopy` `Mathlib.AlgebraicTopology.SimplicialSet.HornColimits` `Mathlib.AlgebraicTopology.SimplicialSet.Horn` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex` `Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices` `Mathlib.AlgebraicTopology.SimplicialSet.Nonempty` `Mathlib.AlgebraicTopology.SimplicialSet.Op` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.PiZero` `Mathlib.AlgebraicTopology.SimplicialSet.Presentable` `Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne` `Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi` `Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism` `Mathlib.AlgebraicTopology.SimplicialSet.Simplices` `Mathlib.AlgebraicTopology.SimplicialSet.Skeleton` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp` `Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex` `Mathlib.AlgebraicTopology.SimplicialSet.Subdivision` `Mathlib.AlgebraicTopology.SimplicialSet.TopAdj` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.CategoryTheory.Abelian.Basic` `Mathlib.CategoryTheory.Abelian.CommSq` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject` `Mathlib.CategoryTheory.Abelian.Images` `Mathlib.CategoryTheory.Abelian.Indization` `Mathlib.CategoryTheory.Abelian.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Injective.Dimension` `Mathlib.CategoryTheory.Abelian.Injective.Ext` `Mathlib.CategoryTheory.Abelian.Injective.Extend` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Monomorphisms` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.CategoryTheory.Abelian.Preradical.Basic` `Mathlib.CategoryTheory.Abelian.Preradical.Colon` `Mathlib.CategoryTheory.Abelian.Preradical.Radical` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Dimension` `Mathlib.CategoryTheory.Abelian.Projective.Ext` `Mathlib.CategoryTheory.Abelian.Projective.Extend` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Abelian.SerreClass.Basic` `Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield` `Mathlib.CategoryTheory.Abelian.SerreClass.Localization` `Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty` `Mathlib.CategoryTheory.Abelian.ShortExact` `Mathlib.CategoryTheory.Abelian.Subcategory` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Action.Basic` `Mathlib.CategoryTheory.Action.Concrete` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.CategoryTheory.Action.Limits` `Mathlib.CategoryTheory.Action.Monoidal` `Mathlib.CategoryTheory.Action` `Mathlib.CategoryTheory.Adhesive.Basic` `Mathlib.CategoryTheory.Adhesive.Over` `Mathlib.CategoryTheory.Adhesive.Subobject` `Mathlib.CategoryTheory.Adhesive` `Mathlib.CategoryTheory.Adjunction.Additive` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Adjunction.Basic` `Mathlib.CategoryTheory.Adjunction.Comma` `Mathlib.CategoryTheory.Adjunction.CompositionIso` `Mathlib.CategoryTheory.Adjunction.Evaluation` `Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits` `Mathlib.CategoryTheory.Adjunction.FullyFaithful` `Mathlib.CategoryTheory.Adjunction.Lifting.Left` `Mathlib.CategoryTheory.Adjunction.Lifting.Right` `Mathlib.CategoryTheory.Adjunction.Limits` `Mathlib.CategoryTheory.Adjunction.Mates` `Mathlib.CategoryTheory.Adjunction.Opposites` `Mathlib.CategoryTheory.Adjunction.Parametrized` `Mathlib.CategoryTheory.Adjunction.PartialAdjoint` `Mathlib.CategoryTheory.Adjunction.Quadruple` `Mathlib.CategoryTheory.Adjunction.Reflective` `Mathlib.CategoryTheory.Adjunction.Restrict` `Mathlib.CategoryTheory.Adjunction.Triple` `Mathlib.CategoryTheory.Adjunction.Unique` `Mathlib.CategoryTheory.Adjunction.Whiskering` `Mathlib.CategoryTheory.Bicategory.Adjunction.Adj` `Mathlib.CategoryTheory.Bicategory.Adjunction.Cat` `Mathlib.CategoryTheory.Bicategory.CatEnriched` `Mathlib.CategoryTheory.Bicategory.Coherence` `Mathlib.CategoryTheory.Bicategory.Extension` `Mathlib.CategoryTheory.Bicategory.Free` `Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty` `Mathlib.CategoryTheory.Bicategory.Functor.Cat` `Mathlib.CategoryTheory.Bicategory.Functor.Lax` `Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete` `Mathlib.CategoryTheory.Bicategory.Functor.Oplax` `Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor` `Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor` `Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary` `Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax` `Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax` `Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo` `Mathlib.CategoryTheory.Bicategory.Grothendieck` `Mathlib.CategoryTheory.Bicategory.InducedBicategory` `Mathlib.CategoryTheory.Bicategory.Kan.Adjunction` `Mathlib.CategoryTheory.Bicategory.Kan.HasKan` `Mathlib.CategoryTheory.Bicategory.Kan.IsKan` `Mathlib.CategoryTheory.Bicategory.LocallyGroupoid` `Mathlib.CategoryTheory.Bicategory.Modification.Lax` `Mathlib.CategoryTheory.Bicategory.Modification.Oplax` `Mathlib.CategoryTheory.Bicategory.Modification.Pseudo` `Mathlib.CategoryTheory.Bicategory.Monad.Basic` `Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax` `Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax` `Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo` `Mathlib.CategoryTheory.Bicategory.Product` `Mathlib.CategoryTheory.Bicategory.SingleObj` `Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor` `Mathlib.CategoryTheory.Bicategory.Yoneda` `Mathlib.CategoryTheory.Category.Bipointed` `Mathlib.CategoryTheory.Category.Cat.Adjunction` `Mathlib.CategoryTheory.Category.Cat.AsSmall` `Mathlib.CategoryTheory.Category.Cat.CartesianClosed` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.Category.Cat.Limit` `Mathlib.CategoryTheory.Category.Cat.Op` `Mathlib.CategoryTheory.Category.Cat.Terminal` `Mathlib.CategoryTheory.Category.Cat` `Mathlib.CategoryTheory.Category.Factorisation` `Mathlib.CategoryTheory.Category.GaloisConnection` `Mathlib.CategoryTheory.Category.Pairwise` `Mathlib.CategoryTheory.Category.PartialFun` `Mathlib.CategoryTheory.Category.Pointed` `Mathlib.CategoryTheory.Category.Quiv` `Mathlib.CategoryTheory.Category.ReflQuiv` `Mathlib.CategoryTheory.Category.RelCat` `Mathlib.CategoryTheory.Category.TwoP` `Mathlib.CategoryTheory.Center.Linear` `Mathlib.CategoryTheory.Center.Localization` `Mathlib.CategoryTheory.Center.NegOnePow` `Mathlib.CategoryTheory.Center.Preadditive` `Mathlib.CategoryTheory.CodiscreteCategory` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.CategoryTheory.Comma.CardinalArrow` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Comma.LocallySmall` `Mathlib.CategoryTheory.Comma.Over.Basic` `Mathlib.CategoryTheory.Comma.Over.OverClass` `Mathlib.CategoryTheory.Comma.Over.Pullback` `Mathlib.CategoryTheory.Comma.Over.StrictInitial` `Mathlib.CategoryTheory.Comma.Presheaf.Basic` `Mathlib.CategoryTheory.Comma.Presheaf.Colimit` `Mathlib.CategoryTheory.Comma.StructuredArrow.Basic` `Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap` `Mathlib.CategoryTheory.Comma.StructuredArrow.Final` `Mathlib.CategoryTheory.Comma.StructuredArrow.Functor` `Mathlib.CategoryTheory.Comma.StructuredArrow.Small` `Mathlib.CategoryTheory.ConcreteCategory.Elementwise` `Mathlib.CategoryTheory.ConcreteCategory.EpiMono` `Mathlib.CategoryTheory.ConcreteCategory.Forget` `Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso` `Mathlib.CategoryTheory.ConcreteCategory.Representable` `Mathlib.CategoryTheory.CopyDiscardCategory.Basic` `Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian` `Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic` `Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory` `Mathlib.CategoryTheory.Core` `Mathlib.CategoryTheory.Countable` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.CategoryTheory.DifferentialObject` `Mathlib.CategoryTheory.Discrete.StructuredArrow` `Mathlib.CategoryTheory.Distributive.Cartesian` `Mathlib.CategoryTheory.Distributive.Monoidal` `Mathlib.CategoryTheory.EffectiveEpi.Basic` `Mathlib.CategoryTheory.EffectiveEpi.Comp` `Mathlib.CategoryTheory.EffectiveEpi.Coproduct` `Mathlib.CategoryTheory.EffectiveEpi.Enough` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.CategoryTheory.EffectiveEpi.Preserves` `Mathlib.CategoryTheory.Elements` `Mathlib.CategoryTheory.Endofunctor.Algebra` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.CategoryTheory.Enriched.EnrichedCat` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks` `Mathlib.CategoryTheory.Enriched.Limits.HasConicalTerminal` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.CategoryTheory.Enriched.Ordinary.Basic` `Mathlib.CategoryTheory.Equivalence.Symmetry` `Mathlib.CategoryTheory.EssentiallySmall` `Mathlib.CategoryTheory.Extensive` `Mathlib.CategoryTheory.ExtremalEpi` `Mathlib.CategoryTheory.FiberedCategory.Grothendieck` `Mathlib.CategoryTheory.Filtered.Basic` `Mathlib.CategoryTheory.Filtered.Connected` `Mathlib.CategoryTheory.Filtered.CostructuredArrow` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.CategoryTheory.Filtered.FinallySmall` `Mathlib.CategoryTheory.Filtered.Flat` `Mathlib.CategoryTheory.Filtered.Grothendieck` `Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Filtered.Small` `Mathlib.CategoryTheory.FintypeCat` `Mathlib.CategoryTheory.Functor.Derived.Adjunction` `Mathlib.CategoryTheory.Functor.Derived.LeftDerived` `Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived` `Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived` `Mathlib.CategoryTheory.Functor.Derived.RightDerived` `Mathlib.CategoryTheory.Functor.EpiMono` `Mathlib.CategoryTheory.Functor.Flat` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.CategoryTheory.Functor.Hom` `Mathlib.CategoryTheory.Functor.KanExtension.Adjunction` `Mathlib.CategoryTheory.Functor.KanExtension.Basic` `Mathlib.CategoryTheory.Functor.KanExtension.DenseAt` `Mathlib.CategoryTheory.Functor.KanExtension.Dense` `Mathlib.CategoryTheory.Functor.KanExtension.Pointwise` `Mathlib.CategoryTheory.Functor.KanExtension.Preserves` `Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced` `Mathlib.CategoryTheory.Functor.ReflectsIso.Exact` `Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly` `Mathlib.CategoryTheory.Functor.ReflectsIso.Limits` `Mathlib.CategoryTheory.Functor.RegularEpi` `Mathlib.CategoryTheory.Functor.TypeValuedFlat` `Mathlib.CategoryTheory.Galois.Action` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.CategoryTheory.Galois.Equivalence` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.CategoryTheory.Galois.Full` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.CategoryTheory.Generator.HomologicalComplex` `Mathlib.CategoryTheory.Generator.Indization` `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.CategoryTheory.Generator.StrongGenerator` `Mathlib.CategoryTheory.Generator.Type` `Mathlib.CategoryTheory.GlueData` `Mathlib.CategoryTheory.GradedObject.Associator` `Mathlib.CategoryTheory.GradedObject.Bifunctor` `Mathlib.CategoryTheory.GradedObject.Braiding` `Mathlib.CategoryTheory.GradedObject.Monoidal` `Mathlib.CategoryTheory.GradedObject.Single` `Mathlib.CategoryTheory.GradedObject.Trifunctor` `Mathlib.CategoryTheory.GradedObject.Unitor` `Mathlib.CategoryTheory.GradedObject` `Mathlib.CategoryTheory.Grothendieck` `Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory` `Mathlib.CategoryTheory.Groupoid.Grpd.Basic` `Mathlib.CategoryTheory.GuitartExact.Basic` `Mathlib.CategoryTheory.GuitartExact.KanExtension` `Mathlib.CategoryTheory.GuitartExact.Opposite` `Mathlib.CategoryTheory.GuitartExact.Over` `Mathlib.CategoryTheory.GuitartExact.VerticalComposition` `Mathlib.CategoryTheory.Idempotents.Basic` `Mathlib.CategoryTheory.Idempotents.Biproducts` `Mathlib.CategoryTheory.Idempotents.FunctorCategories` `Mathlib.CategoryTheory.Idempotents.FunctorExtension` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi` `Mathlib.CategoryTheory.Idempotents.Karoubi` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.IsomorphismClasses` `Mathlib.CategoryTheory.Join.Final` `Mathlib.CategoryTheory.Join.Pseudofunctor` `Mathlib.CategoryTheory.LiftingProperties.Adjunction` `Mathlib.CategoryTheory.LiftingProperties.Limits` `Mathlib.CategoryTheory.LiftingProperties.Over` `Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction` `Mathlib.CategoryTheory.Limits.Bicones` `Mathlib.CategoryTheory.Limits.ColimitLimit` `Mathlib.CategoryTheory.Limits.Comma` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered` `Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures` `Mathlib.CategoryTheory.Limits.ConeCategory` `Mathlib.CategoryTheory.Limits.Cones` `Mathlib.CategoryTheory.Limits.Connected` `Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.EpiMono` `Mathlib.CategoryTheory.Limits.Constructions.Equalizers` `Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant` `Mathlib.CategoryTheory.Limits.Constructions.Filtered` `Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts` `Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.CategoryTheory.Limits.Constructions.Over.Connected` `Mathlib.CategoryTheory.Limits.Constructions.Over.Products` `Mathlib.CategoryTheory.Limits.Constructions.Pullbacks` `Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial` `Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal` `Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects` `Mathlib.CategoryTheory.Limits.Creates` `Mathlib.CategoryTheory.Limits.Elements` `Mathlib.CategoryTheory.Limits.EpiMono` `Mathlib.CategoryTheory.Limits.EssentiallySmall` `Mathlib.CategoryTheory.Limits.ExactFunctor` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct` `Mathlib.CategoryTheory.Limits.Filtered` `Mathlib.CategoryTheory.Limits.Final.Connected` `Mathlib.CategoryTheory.Limits.Final.ParallelPair` `Mathlib.CategoryTheory.Limits.Final.Type` `Mathlib.CategoryTheory.Limits.Final` `Mathlib.CategoryTheory.Limits.FinallySmall` `Mathlib.CategoryTheory.Limits.FintypeCat` `Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic` `Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech` `Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy` `Mathlib.CategoryTheory.Limits.FormalCoproducts` `Mathlib.CategoryTheory.Limits.Fubini` `Mathlib.CategoryTheory.Limits.FullSubcategory` `Mathlib.CategoryTheory.Limits.FunctorCategory.Basic` `Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts` `Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono` `Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered` `Mathlib.CategoryTheory.Limits.FunctorCategory.Finite` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Kernels` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks` `Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal` `Mathlib.CategoryTheory.Limits.FunctorToTypes` `Mathlib.CategoryTheory.Limits.HasLimits` `Mathlib.CategoryTheory.Limits.IndYoneda` `Mathlib.CategoryTheory.Limits.Indization.Category` `Mathlib.CategoryTheory.Limits.Indization.Equalizers` `Mathlib.CategoryTheory.Limits.Indization.FilteredColimits` `Mathlib.CategoryTheory.Limits.Indization.IndObject` `Mathlib.CategoryTheory.Limits.Indization.LocallySmall` `Mathlib.CategoryTheory.Limits.Indization.ParallelPair` `Mathlib.CategoryTheory.Limits.Indization.Products` `Mathlib.CategoryTheory.Limits.IsConnected` `Mathlib.CategoryTheory.Limits.IsLimit` `Mathlib.CategoryTheory.Limits.Lattice` `Mathlib.CategoryTheory.Limits.MonoCoprod` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.CategoryTheory.Limits.Opposites` `Mathlib.CategoryTheory.Limits.Over` `Mathlib.CategoryTheory.Limits.Pi` `Mathlib.CategoryTheory.Limits.Preorder` `Mathlib.CategoryTheory.Limits.Presentation` `Mathlib.CategoryTheory.Limits.Preserves.Basic` `Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel` `Mathlib.CategoryTheory.Limits.Preserves.Bifunctor` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites` `Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks` `Mathlib.CategoryTheory.Limits.Preserves.Filtered` `Mathlib.CategoryTheory.Limits.Preserves.Finite` `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory` `Mathlib.CategoryTheory.Limits.Preserves.Grothendieck` `Mathlib.CategoryTheory.Limits.Preserves.Limits` `Mathlib.CategoryTheory.Limits.Preserves.Opposites` `Mathlib.CategoryTheory.Limits.Preserves.Over` `Mathlib.CategoryTheory.Limits.Preserves.Presheaf` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero` `Mathlib.CategoryTheory.Limits.Preserves.SigmaConst` `Mathlib.CategoryTheory.Limits.Preserves.Ulift` `Mathlib.CategoryTheory.Limits.Preserves.Yoneda` `Mathlib.CategoryTheory.Limits.Presheaf` `Mathlib.CategoryTheory.Limits.Set` `Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts` `Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts` `Mathlib.CategoryTheory.Limits.Shapes.Biproducts` `Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts` `Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory` `Mathlib.CategoryTheory.Limits.Shapes.Connected` `Mathlib.CategoryTheory.Limits.Shapes.Countable` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal` `Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct` `Mathlib.CategoryTheory.Limits.Shapes.End` `Mathlib.CategoryTheory.Limits.Shapes.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Equivalence` `Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits` `Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer` `Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts` `Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes` `Mathlib.CategoryTheory.Limits.Shapes.Grothendieck` `Mathlib.CategoryTheory.Limits.Shapes.Images` `Mathlib.CategoryTheory.Limits.Shapes.IsTerminal` `Mathlib.CategoryTheory.Limits.Shapes.KernelPair` `Mathlib.CategoryTheory.Limits.Shapes.Kernels` `Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback` `Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers` `Mathlib.CategoryTheory.Limits.Shapes.Opposites.Filtered` `Mathlib.CategoryTheory.Limits.Shapes.Opposites.Kernels` `Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products` `Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks` `Mathlib.CategoryTheory.Limits.Shapes.PiProd` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape` `Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous` `Mathlib.CategoryTheory.Limits.Shapes.Products` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.CategoryTheory.Limits.Shapes.Reflexive` `Mathlib.CategoryTheory.Limits.Shapes.RegularMono` `Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct` `Mathlib.CategoryTheory.Limits.Shapes.SingleObj` `Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer` `Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer` `Mathlib.CategoryTheory.Limits.Shapes.StrictInitial` `Mathlib.CategoryTheory.Limits.Shapes.Terminal` `Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers` `Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks` `Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms` `Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.CategoryTheory.Limits.Skeleton` `Mathlib.CategoryTheory.Limits.SmallComplete` `Mathlib.CategoryTheory.Limits.Types.Coequalizers` `Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered` `Mathlib.CategoryTheory.Limits.Types.ColimitType` `Mathlib.CategoryTheory.Limits.Types.Colimits` `Mathlib.CategoryTheory.Limits.Types.Coproducts` `Mathlib.CategoryTheory.Limits.Types.Equalizers` `Mathlib.CategoryTheory.Limits.Types.Filtered` `Mathlib.CategoryTheory.Limits.Types.Images` `Mathlib.CategoryTheory.Limits.Types.Limits` `Mathlib.CategoryTheory.Limits.Types.Multicoequalizer` `Mathlib.CategoryTheory.Limits.Types.Multiequalizer` `Mathlib.CategoryTheory.Limits.Types.Products` `Mathlib.CategoryTheory.Limits.Types.Pullbacks` `Mathlib.CategoryTheory.Limits.Types.Pushouts` `Mathlib.CategoryTheory.Limits.Types.Yoneda` `Mathlib.CategoryTheory.Limits.Unit` `Mathlib.CategoryTheory.Limits.VanKampen` `Mathlib.CategoryTheory.Limits.Yoneda` `Mathlib.CategoryTheory.Linear.Basic` `Mathlib.CategoryTheory.Linear.FunctorCategory` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.CategoryTheory.Localization.Adjunction` `Mathlib.CategoryTheory.Localization.Bifunctor` `Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition` `Mathlib.CategoryTheory.Localization.Bousfield` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.CategoryTheory.Localization.CalculusOfFractions` `Mathlib.CategoryTheory.Localization.Composition` `Mathlib.CategoryTheory.Localization.Construction` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived` `Mathlib.CategoryTheory.Localization.Equivalence` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.CategoryTheory.Localization.HasLocalization` `Mathlib.CategoryTheory.Localization.HomEquiv` `Mathlib.CategoryTheory.Localization.Linear` `Mathlib.CategoryTheory.Localization.LocalizerMorphism` `Mathlib.CategoryTheory.Localization.LocallySmall` `Mathlib.CategoryTheory.Localization.Monoidal.Basic` `Mathlib.CategoryTheory.Localization.Monoidal.Braided` `Mathlib.CategoryTheory.Localization.Monoidal.Functor` `Mathlib.CategoryTheory.Localization.Monoidal` `Mathlib.CategoryTheory.Localization.Opposite` `Mathlib.CategoryTheory.Localization.Pi` `Mathlib.CategoryTheory.Localization.Preadditive` `Mathlib.CategoryTheory.Localization.Predicate` `Mathlib.CategoryTheory.Localization.Prod` `Mathlib.CategoryTheory.Localization.Quotient` `Mathlib.CategoryTheory.Localization.Resolution` `Mathlib.CategoryTheory.Localization.SmallHom` `Mathlib.CategoryTheory.Localization.SmallShiftedHom` `Mathlib.CategoryTheory.Localization.StructuredArrow` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.CategoryTheory.Localization.Trifunctor` `Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong` `Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism` `Mathlib.CategoryTheory.LocallyCartesianClosed.Over` `Mathlib.CategoryTheory.LocallyCartesianClosed.Sections` `Mathlib.CategoryTheory.LocallyDirected` `Mathlib.CategoryTheory.MarkovCategory.Basic` `Mathlib.CategoryTheory.MarkovCategory.Positive` `Mathlib.CategoryTheory.Monad.Adjunction` `Mathlib.CategoryTheory.Monad.Algebra` `Mathlib.CategoryTheory.Monad.Coequalizer` `Mathlib.CategoryTheory.Monad.Comonadicity` `Mathlib.CategoryTheory.Monad.Equalizer` `Mathlib.CategoryTheory.Monad.EquivMon` `Mathlib.CategoryTheory.Monad.Kleisli` `Mathlib.CategoryTheory.Monad.Limits` `Mathlib.CategoryTheory.Monad.Monadicity` `Mathlib.CategoryTheory.Monad.Products` `Mathlib.CategoryTheory.Monad.Types` `Mathlib.CategoryTheory.Monoidal.Action.End` `Mathlib.CategoryTheory.Monoidal.Action.Opposites` `Mathlib.CategoryTheory.Monoidal.Arrow` `Mathlib.CategoryTheory.Monoidal.Bimod` `Mathlib.CategoryTheory.Monoidal.Bimon_` `Mathlib.CategoryTheory.Monoidal.Braided.Basic` `Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor` `Mathlib.CategoryTheory.Monoidal.Braided.Opposite` `Mathlib.CategoryTheory.Monoidal.Braided.Reflection` `Mathlib.CategoryTheory.Monoidal.Braided.Transport` `Mathlib.CategoryTheory.Monoidal.Cartesian.Basic` `Mathlib.CategoryTheory.Monoidal.Cartesian.Cat` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Cartesian.GrpLimits` `Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_` `Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_` `Mathlib.CategoryTheory.Monoidal.Cartesian.Over` `Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda` `Mathlib.CategoryTheory.Monoidal.Center` `Mathlib.CategoryTheory.Monoidal.Closed.Basic` `Mathlib.CategoryTheory.Monoidal.Closed.Braided` `Mathlib.CategoryTheory.Monoidal.Closed.Cartesian` `Mathlib.CategoryTheory.Monoidal.Closed.Enrichment` `Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic` `Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete` `Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid` `Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes` `Mathlib.CategoryTheory.Monoidal.Closed.Functor` `Mathlib.CategoryTheory.Monoidal.Closed.Ideal` `Mathlib.CategoryTheory.Monoidal.Closed.Transport` `Mathlib.CategoryTheory.Monoidal.Closed.Types` `Mathlib.CategoryTheory.Monoidal.Closed.Zero` `Mathlib.CategoryTheory.Monoidal.CommComon_` `Mathlib.CategoryTheory.Monoidal.CommGrp_` `Mathlib.CategoryTheory.Monoidal.CommMon_` `Mathlib.CategoryTheory.Monoidal.Comon_` `Mathlib.CategoryTheory.Monoidal.Conv` `Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided` `Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed` `Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor` `Mathlib.CategoryTheory.Monoidal.DayConvolution` `Mathlib.CategoryTheory.Monoidal.Discrete` `Mathlib.CategoryTheory.Monoidal.End` `Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic` `Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension` `Mathlib.CategoryTheory.Monoidal.Free.Basic` `Mathlib.CategoryTheory.Monoidal.Free.Coherence` `Mathlib.CategoryTheory.Monoidal.Functor.Types` `Mathlib.CategoryTheory.Monoidal.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Functor` `Mathlib.CategoryTheory.Monoidal.Grp_` `Mathlib.CategoryTheory.Monoidal.Hopf_` `Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Internal.Limits` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_` `Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_` `Mathlib.CategoryTheory.Monoidal.Limits.Basic` `Mathlib.CategoryTheory.Monoidal.Limits.Cokernels` `Mathlib.CategoryTheory.Monoidal.Limits.Colimits` `Mathlib.CategoryTheory.Monoidal.Limits.HasLimits` `Mathlib.CategoryTheory.Monoidal.Limits.Preserves` `Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.CategoryTheory.Monoidal.Mod_` `Mathlib.CategoryTheory.Monoidal.Mon_` `Mathlib.CategoryTheory.Monoidal.Multifunctor` `Mathlib.CategoryTheory.Monoidal.NaturalTransformation` `Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts` `Mathlib.CategoryTheory.Monoidal.Opposite.Mon_` `Mathlib.CategoryTheory.Monoidal.Opposite` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.CategoryTheory.Monoidal.PushoutProduct` `Mathlib.CategoryTheory.Monoidal.Rigid.Basic` `Mathlib.CategoryTheory.Monoidal.Rigid.Braided` `Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory` `Mathlib.CategoryTheory.Monoidal.Rigid.Functor` `Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence` `Mathlib.CategoryTheory.Monoidal.Ring` `Mathlib.CategoryTheory.Monoidal.Skeleton` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Monoidal.Transport` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.CategoryTheory.Monoidal.Widesubcategory` `Mathlib.CategoryTheory.MorphismProperty.CommaSites` `Mathlib.CategoryTheory.MorphismProperty.Comma` `Mathlib.CategoryTheory.MorphismProperty.Concrete` `Mathlib.CategoryTheory.MorphismProperty.Descent` `Mathlib.CategoryTheory.MorphismProperty.FunctorCategory` `Mathlib.CategoryTheory.MorphismProperty.Ind` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.CategoryTheory.MorphismProperty.Local` `Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.CategoryTheory.MorphismProperty.RetractArgument` `Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition` `Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem` `Mathlib.CategoryTheory.Noetherian` `Mathlib.CategoryTheory.ObjectProperty.ClosureShift` `Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure` `Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure` `Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape` `Mathlib.CategoryTheory.ObjectProperty.ContainsZero` `Mathlib.CategoryTheory.ObjectProperty.EpiMono` `Mathlib.CategoryTheory.ObjectProperty.Extensions` `Mathlib.CategoryTheory.ObjectProperty.FiniteProducts` `Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits` `Mathlib.CategoryTheory.ObjectProperty.Ind` `Mathlib.CategoryTheory.ObjectProperty.Kernels` `Mathlib.CategoryTheory.ObjectProperty.LimitsClosure` `Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape` `Mathlib.CategoryTheory.ObjectProperty.Local` `Mathlib.CategoryTheory.ObjectProperty.Orthogonal` `Mathlib.CategoryTheory.ObjectProperty.Retract` `Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive` `Mathlib.CategoryTheory.ObjectProperty.Shift` `Mathlib.CategoryTheory.ObjectProperty.SiteLocal` `Mathlib.CategoryTheory.ObjectProperty.Small` `Mathlib.CategoryTheory.Pi.Monoidal` `Mathlib.CategoryTheory.Preadditive.AdditiveFunctor` `Mathlib.CategoryTheory.Preadditive.Basic` `Mathlib.CategoryTheory.Preadditive.Biproducts` `Mathlib.CategoryTheory.Preadditive.CommGrp_` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Indization` `Mathlib.CategoryTheory.Preadditive.Injective.Basic` `Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Injective.Preserves` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.CategoryTheory.Preadditive.LiftToFinset` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Preadditive.OfBiproducts` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.CategoryTheory.Preadditive.Projective.Basic` `Mathlib.CategoryTheory.Preadditive.Projective.Internal` `Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties` `Mathlib.CategoryTheory.Preadditive.Projective.Preserves` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Preadditive.Transfer` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Presentable.Adjunction` `Mathlib.CategoryTheory.Presentable.Basic` `Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation` `Mathlib.CategoryTheory.Presentable.ColimitPresentation` `Mathlib.CategoryTheory.Presentable.Dense` `Mathlib.CategoryTheory.Presentable.Directed` `Mathlib.CategoryTheory.Presentable.EssentiallyLarge` `Mathlib.CategoryTheory.Presentable.Finite` `Mathlib.CategoryTheory.Presentable.IsCardinalFiltered` `Mathlib.CategoryTheory.Presentable.Limits` `Mathlib.CategoryTheory.Presentable.LocallyPresentable` `Mathlib.CategoryTheory.Presentable.OrthogonalReflection` `Mathlib.CategoryTheory.Presentable.Presheaf` `Mathlib.CategoryTheory.Presentable.Retracts` `Mathlib.CategoryTheory.Presentable.StrongGenerator` `Mathlib.CategoryTheory.Presentable.Type` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.CategoryTheory.Quotient.LocallySmall` `Mathlib.CategoryTheory.Quotient.Preadditive` `Mathlib.CategoryTheory.RegularCategory.Basic` `Mathlib.CategoryTheory.RepresentedBy` `Mathlib.CategoryTheory.Shift.Adjunction` `Mathlib.CategoryTheory.Shift.Basic` `Mathlib.CategoryTheory.Shift.CommShiftTwo` `Mathlib.CategoryTheory.Shift.CommShift` `Mathlib.CategoryTheory.Shift.InducedShiftSequence` `Mathlib.CategoryTheory.Shift.Induced` `Mathlib.CategoryTheory.Shift.Linear` `Mathlib.CategoryTheory.Shift.Localization` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.CategoryTheory.Shift.Pullback` `Mathlib.CategoryTheory.Shift.Quotient` `Mathlib.CategoryTheory.Shift.ShiftSequence` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.CategoryTheory.Shift.ShiftedHom` `Mathlib.CategoryTheory.Shift.SingleFunctors` `Mathlib.CategoryTheory.Shift.Twist` `Mathlib.CategoryTheory.ShrinkYoneda` `Mathlib.CategoryTheory.Simple` `Mathlib.CategoryTheory.SingleObj` `Mathlib.CategoryTheory.Sites.Abelian` `Mathlib.CategoryTheory.Sites.Adjunction` `Mathlib.CategoryTheory.Sites.Canonical` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.CategoryTheory.Sites.CartesianMonoidal` `Mathlib.CategoryTheory.Sites.Closed` `Mathlib.CategoryTheory.Sites.Coherent.Basic` `Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves` `Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology` `Mathlib.CategoryTheory.Sites.Coherent.Comparison` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular` `Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves` `Mathlib.CategoryTheory.Sites.Coherent.RegularTopology` `Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.CategoryTheory.Sites.CompatiblePlus` `Mathlib.CategoryTheory.Sites.CompatibleSheafification` `Mathlib.CategoryTheory.Sites.ConcreteSheafification` `Mathlib.CategoryTheory.Sites.ConstantSheaf` `Mathlib.CategoryTheory.Sites.Continuous` `Mathlib.CategoryTheory.Sites.CoproductSheafCondition` `Mathlib.CategoryTheory.Sites.CoverLifting` `Mathlib.CategoryTheory.Sites.CoverPreserving` `Mathlib.CategoryTheory.Sites.Coverage` `Mathlib.CategoryTheory.Sites.CoversTop` `Mathlib.CategoryTheory.Sites.DenseSubsite.Basic` `Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology` `Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense` `Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv` `Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra` `Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime` `Mathlib.CategoryTheory.Sites.Descent.DescentData` `Mathlib.CategoryTheory.Sites.Descent.IsPrestack` `Mathlib.CategoryTheory.Sites.Descent.IsStack` `Mathlib.CategoryTheory.Sites.Descent.Precoverage` `Mathlib.CategoryTheory.Sites.EffectiveEpimorphic` `Mathlib.CategoryTheory.Sites.EpiMono` `Mathlib.CategoryTheory.Sites.EqualizerSheafCondition` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.CategoryTheory.Sites.Finite` `Mathlib.CategoryTheory.Sites.GlobalSections` `Mathlib.CategoryTheory.Sites.Grothendieck` `Mathlib.CategoryTheory.Sites.Hypercover.Homotopy` `Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf` `Mathlib.CategoryTheory.Sites.Hypercover.One` `Mathlib.CategoryTheory.Sites.Hypercover.Saturate` `Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes` `Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical` `Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily` `Mathlib.CategoryTheory.Sites.Hypercover.Zero` `Mathlib.CategoryTheory.Sites.IsSheafFor` `Mathlib.CategoryTheory.Sites.JointlySurjective` `Mathlib.CategoryTheory.Sites.LeftExact` `Mathlib.CategoryTheory.Sites.Limits` `Mathlib.CategoryTheory.Sites.LocalProperties` `Mathlib.CategoryTheory.Sites.Localization` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.CategoryTheory.Sites.Monoidal` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.CategoryTheory.Sites.Plus` `Mathlib.CategoryTheory.Sites.Point.Basic` `Mathlib.CategoryTheory.Sites.Point.Category` `Mathlib.CategoryTheory.Sites.Point.Comap` `Mathlib.CategoryTheory.Sites.Point.Conservative` `Mathlib.CategoryTheory.Sites.Point.IsMonoidalW` `Mathlib.CategoryTheory.Sites.Point.Map` `Mathlib.CategoryTheory.Sites.Point.Monoidal` `Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered` `Mathlib.CategoryTheory.Sites.Point.Over` `Mathlib.CategoryTheory.Sites.Point.Presheaf` `Mathlib.CategoryTheory.Sites.Point.Skyscraper` `Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck` `Mathlib.CategoryTheory.Sites.Precoverage` `Mathlib.CategoryTheory.Sites.PreservesLimits` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.CategoryTheory.Sites.PreservesSheafification` `Mathlib.CategoryTheory.Sites.Preserves` `Mathlib.CategoryTheory.Sites.Pretopology` `Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.CategoryTheory.Sites.RegularEpi` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.CategoryTheory.Sites.SheafCohomology.Cech` `Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.CategoryTheory.Sites.SheafOfTypes` `Mathlib.CategoryTheory.Sites.Sheaf` `Mathlib.CategoryTheory.Sites.Sheafification` `Mathlib.CategoryTheory.Sites.Sieves` `Mathlib.CategoryTheory.Sites.Spaces` `Mathlib.CategoryTheory.Sites.SubcanonicalOver` `Mathlib.CategoryTheory.Sites.Subcanonical` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.CategoryTheory.Sites.Types` `Mathlib.CategoryTheory.Sites.Whiskering` `Mathlib.CategoryTheory.Skeletal` `Mathlib.CategoryTheory.SmallObject.Basic` `Mathlib.CategoryTheory.SmallObject.Construction` `Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument` `Mathlib.CategoryTheory.SmallObject.Iteration.Basic` `Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc` `Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone` `Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty` `Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting` `Mathlib.CategoryTheory.SmallObject.TransfiniteIteration` `Mathlib.CategoryTheory.SmallObject.WellOrderInductionData` `Mathlib.CategoryTheory.Subfunctor.Basic` `Mathlib.CategoryTheory.Subfunctor.Equalizer` `Mathlib.CategoryTheory.Subfunctor.Finite` `Mathlib.CategoryTheory.Subfunctor.Image` `Mathlib.CategoryTheory.Subfunctor.OfSection` `Mathlib.CategoryTheory.Subfunctor.Sieves` `Mathlib.CategoryTheory.Subfunctor.Subobject` `Mathlib.CategoryTheory.Subobject.ArtinianObject` `Mathlib.CategoryTheory.Subobject.Basic` `Mathlib.CategoryTheory.Subobject.Classifier.Defs` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.CategoryTheory.Subobject.HasCardinalLT` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.CategoryTheory.Subobject.MonoOver` `Mathlib.CategoryTheory.Subobject.NoetherianObject` `Mathlib.CategoryTheory.Subobject.Presheaf` `Mathlib.CategoryTheory.Subobject.Types` `Mathlib.CategoryTheory.Subobject.WellPowered` `Mathlib.CategoryTheory.Subterminal` `Mathlib.CategoryTheory.Topos.Classifier` `Mathlib.CategoryTheory.Topos.Sheaf` `Mathlib.CategoryTheory.Triangulated.Adjunction` `Mathlib.CategoryTheory.Triangulated.Basic` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.CategoryTheory.Triangulated.Generators` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic` `Mathlib.CategoryTheory.Triangulated.Opposite.Functor` `Mathlib.CategoryTheory.Triangulated.Opposite.OpOp` `Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated` `Mathlib.CategoryTheory.Triangulated.Orthogonal` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Rotate` `Mathlib.CategoryTheory.Triangulated.SpectralObject` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc` `Mathlib.CategoryTheory.Triangulated.TStructure.Heart` `Mathlib.CategoryTheory.Triangulated.TStructure.Induced` `Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject` `Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT` `Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.CategoryTheory.Types.Basic` `Mathlib.CategoryTheory.Types.Epimorphisms` `Mathlib.CategoryTheory.Types.Monomorphisms` `Mathlib.CategoryTheory.Types.Set` `Mathlib.CategoryTheory.UnivLE` `Mathlib.CategoryTheory.WithTerminal.Basic` `Mathlib.CategoryTheory.WithTerminal.Cone` `Mathlib.CategoryTheory.WithTerminal.FinCategory` `Mathlib.CategoryTheory.WithTerminal.Lemmas` `Mathlib.CategoryTheory.Yoneda` `Mathlib.Combinatorics.Configuration` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.Combinatorics.Quiver.ReflQuiver` `Mathlib.Combinatorics.SimpleGraph.Ends.Defs` `Mathlib.Combinatorics.SimpleGraph.Ends.Properties` `Mathlib.Combinatorics.SimpleGraph.Finsubgraph` `Mathlib.Combinatorics.SimpleGraph.Hall` `Mathlib.Condensed.AB` `Mathlib.Condensed.Basic` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.EffectiveEpi` `Mathlib.Condensed.Epi` `Mathlib.Condensed.Equivalence` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Light.AB` `Mathlib.Condensed.Light.Basic` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Light.EffectiveEpi` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Instances` `Mathlib.Condensed.Light.InternallyProjective` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.Monoidal` `Mathlib.Condensed.Light.Sequence` `Mathlib.Condensed.Light.Small` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Limits` `Mathlib.Condensed.Module` `Mathlib.Condensed.Solid` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Condensed.TopComparison` `Mathlib.Control.Fold` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.RatFunc.Valuation` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.Geometry.RingedSpace.PresheafedSpace` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.GroupTheory.FreeGroup.NielsenSchreier` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.BaseExists` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Inertia` `Mathlib.NumberTheory.RamificationInertia.Ramification` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.Order.Category.BddDistLat` `Mathlib.Order.Category.BddLat` `Mathlib.Order.Category.BddOrd` `Mathlib.Order.Category.BoolAlg` `Mathlib.Order.Category.CompleteLat` `Mathlib.Order.Category.DistLat` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Category.FinPartOrd` `Mathlib.Order.Category.Frm` `Mathlib.Order.Category.HeytAlg` `Mathlib.Order.Category.Lat` `Mathlib.Order.Category.LinOrd` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Order.Category.OmegaCompletePartialOrder` `Mathlib.Order.Category.PartOrdEmb` `Mathlib.Order.Category.PartOrd` `Mathlib.Order.Category.Preord` `Mathlib.Order.Category.Semilat` `Mathlib.Order.CompleteLattice.MulticoequalizerDiagram` `Mathlib.Order.Interval.Set.Final` `Mathlib.Order.NonemptyFiniteChains` `Mathlib.Probability.Kernel.Category.SFinKer` `Mathlib.Probability.Kernel.Category.Stoch` `Mathlib.RepresentationTheory.Action` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.Coinduced` `Mathlib.RepresentationTheory.Coinvariants` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.FinGroupCharZero` `Mathlib.RepresentationTheory.FiniteIndex` `Mathlib.RepresentationTheory.Homological.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro` `Mathlib.RepresentationTheory.Homological.GroupHomology.Basic` `Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro` `Mathlib.RepresentationTheory.Homological.Resolution` `Mathlib.RepresentationTheory.Induced` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Rep.Basic` `Mathlib.RepresentationTheory.Rep.Iso` `Mathlib.RepresentationTheory.Rep.Res` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.Algebraic.StronglyTranscendental` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.Instances` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Locus` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.Finiteness.Descent` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.RingTheory.Flat.FaithfullyFlat.Descent` `Mathlib.RingTheory.Flat.Rank` `Mathlib.RingTheory.Flat.Tensor` `Mathlib.RingTheory.Flat.TorsionFree` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.Ideal.AssociatedPrime.Localization` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Ideal.Pure` `Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.Regular` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.RingTheory.LocalProperties.InjectiveDimension` `Mathlib.RingTheory.LocalProperties.Injective` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.LocalProperties.ProjectiveDimension` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.RingTheory.LocalProperties.Semilocal` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.AtPrime.Extension` `Mathlib.RingTheory.Morita.Basic` `Mathlib.RingTheory.Morita.Matrix` `Mathlib.RingTheory.OrderOfVanishing.Noetherian` `Mathlib.RingTheory.PicardGroup` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.Regular.Category` `Mathlib.RingTheory.Regular.Depth` `Mathlib.RingTheory.Regular.ProjectiveDimension` `Mathlib.RingTheory.RegularLocalRing.Defs` `Mathlib.RingTheory.RingHom.Bijective` `Mathlib.RingTheory.RingHom.EssFiniteType` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.FaithfullyFlat` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.RingTheory.RingHom.OpenImmersion` `Mathlib.RingTheory.RingHom.QuasiFinite` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RingHomProperties` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Field` `Mathlib.RingTheory.Smooth.Flat` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.NoetherianDescent` `Mathlib.RingTheory.Smooth.Quotient` `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Support` `Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight` `Mathlib.RingTheory.TotallySplit` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Dedekind` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.CategoryTheory.BicategoryCoherence` `Mathlib.Tactic.CategoryTheory.Coherence` `Mathlib.Tactic.CategoryTheory.ToApp` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.CompHaus.Frm` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Topology.Category.CompHausLike.Basic` `Mathlib.Topology.Category.CompHausLike.Cartesian` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi` `Mathlib.Topology.Category.CompHausLike.Limits` `Mathlib.Topology.Category.CompHausLike.SigmaComparison` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Topology.Category.Compactum` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Category.FinTopCat` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.Cartesian` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Injective` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Topology.Category.Locale` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.Category.Profinite.Nobeling.Basic` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Category.Profinite.Nobeling.Span` `Mathlib.Topology.Category.Profinite.Nobeling.Successor` `Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.Category.Sequential` `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.Topology.Category.TopCat.Adjunctions` `Mathlib.Topology.Category.TopCat.Basic` `Mathlib.Topology.Category.TopCat.EffectiveEpi` `Mathlib.Topology.Category.TopCat.EpiMono` `Mathlib.Topology.Category.TopCat.GrothendieckTopology` `Mathlib.Topology.Category.TopCat.Limits.Basic` `Mathlib.Topology.Category.TopCat.Limits.Cofiltered` `Mathlib.Topology.Category.TopCat.Limits.Konig` `Mathlib.Topology.Category.TopCat.Limits.Products` `Mathlib.Topology.Category.TopCat.Limits.Pullbacks` `Mathlib.Topology.Category.TopCat.Monoidal` `Mathlib.Topology.Category.TopCat.OpenNhds` `Mathlib.Topology.Category.TopCat.Opens` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Category.TopCat.ULift` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.Category.UniformSpace` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Gluing` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.TopCat.Basic` `Mathlib.Topology.Homotopy.TopCat.ToSSet` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.Sheaves.Abelian` `Mathlib.Topology.Sheaves.AddCommGrpCat` `Mathlib.Topology.Sheaves.Alexandrov` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.Sheaves.Flasque` `Mathlib.Topology.Sheaves.Forget` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Topology.Sheaves.Limits` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Topology.Sheaves.Over` `Mathlib.Topology.Sheaves.PUnit` `Mathlib.Topology.Sheaves.Points` `Mathlib.Topology.Sheaves.PresheafOfFunctions` `Mathlib.Topology.Sheaves.Presheaf` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.Topology.Sheaves.Sheaf` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Topology.Sheaves.Stalks` `Mathlib.Topology.Specialization` `Mathlib.Topology.Subpath`	1
`Mathlib.Tactic.CategoryTheory.MkConcreteCategory` (new file)	289

Declarations diff

+ Fun
+ Fun.comp
+ Fun.id
+ TestCat
+ instance (X Y : TestCat.{u}) : FunLike (Fun X Y) X.α Y.α
+ ofHom_mk
- CategoryTheory.types
- homEquiv
- hom_bijective
- hom_comp
- hom_id
- hom_injective
- hom_surjective
- instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·)
- instance : ConcreteCategory.{u} (Type u) Fun
- moduleCategory
- ofHom_comp
- ofHom_eq
- ofHom_id
- types_comp
- types_comp_apply
- types_congr_hom
- types_id
- types_id_apply
-- Hom
-- Hom.Simps.hom
-- Hom.hom
-- hom_ofHom
-- ofHom
-- ofHom_apply
-- ofHom_hom

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.34, 0.01)

Current number	Change	Type
756	-2	backward.privateInPublic
393	-1	backward.privateInPublic.warn

Current commit d9c7e42804
Reference commit 2d59066e04

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

github-actions · 2026-04-28T15:09:25Z

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title does not contain a colon

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

feat (feature)
fix (bug fix)
doc (documentation)
style (formatting, missing semicolons, ...)
refactor
test (when adding missing tests)
chore (maintain)
perf (performance improvement, optimization, ...)
ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

Data/Nat/Basic
Algebra/Group/Defs
Topology/Constructions

<subject> has the following constraints:

do not capitalize the first letter
no dot(.) at the end
use imperative, present tense: "change" not "changed" nor "changes"

mathlib-merge-conflicts · 2026-04-30T00:10:00Z

This pull request has conflicts, please merge master and resolve them.

dagurtomas · 2026-05-01T17:49:33Z

Closed in favour of #38671

dagurtomas added 7 commits April 27, 2026 13:55

feat: add concrete category boilerplate command

afb2e8d

.

b000f35

mk_all

df320f0

autogenerate TypeCat

1d34ac7

chore: use notation for TypeCat.ofHom

779a2aa

Merge remote-tracking branch 'origin/typecat-ofhom-upto' into autogen…

e981c35

…erate-concrete # Conflicts: # Mathlib/CategoryTheory/Types/Basic.lean

wip

d9c7e42

dagurtomas added the WIP Work in progress label Apr 28, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 30, 2026

dagurtomas closed this May 1, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Test `mk_concrete_category`#38652

Test `mk_concrete_category`#38652
dagurtomas wants to merge 7 commits intoleanprover-community:masterfrom
dagurtomas:autogenerate-concrete

dagurtomas commented Apr 28, 2026

Uh oh!

github-actions Bot commented Apr 28, 2026

Declarations diff

Uh oh!

github-actions Bot commented Apr 28, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Apr 30, 2026

Uh oh!

dagurtomas commented May 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

dagurtomas commented Apr 28, 2026

Uh oh!

github-actions Bot commented Apr 28, 2026

PR summary 2d59066e04

Import changes for modified files

Declarations diff

Uh oh!

github-actions Bot commented Apr 28, 2026

🚨 PR Title Needs Formatting

Uh oh!

mathlib-merge-conflicts Bot commented Apr 30, 2026

Uh oh!

dagurtomas commented May 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant