leanprover-community
refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure
This PR refactors the definition of morphisms in full subcategories (and induced categories), by making them a 1-field structure. This prevents certain defeq abuse, and improves automation. (The only issue is that this adds an extra layer: f sometimes becomes f.hom, etc.)
(It would make sense to redefine CommGrp/Grp/CommMon as full subcategories of Mon, rather than defining CommGrp by applying InducedCategory twice, which adds one unnecessary layer of .hom, but no attempt was made to change this in this PR.)
PR summary 5bd1b3ba0c
Import changes exceeding 2%
| % | File |
|---|---|
| +3.71% | Mathlib.CategoryTheory.Linear.Basic |
| +3.24% | Mathlib.CategoryTheory.Preadditive.Basic |
Import changes for modified files
Dependency changes
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Linear.Basic | 485 | 503 | +18 (+3.71%) |
| Mathlib.CategoryTheory.Preadditive.Basic | 463 | 478 | +15 (+3.24%) |
| Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty | 514 | 524 | +10 (+1.95%) |
| Mathlib.CategoryTheory.Monoidal.Subcategory | 590 | 594 | +4 (+0.68%) |
| Mathlib.Algebra.Category.ModuleCat.Tannaka | 736 | 740 | +4 (+0.54%) |
| Mathlib.CategoryTheory.Galois.Examples | 858 | 861 | +3 (+0.35%) |
| Mathlib.CategoryTheory.Preadditive.AdditiveFunctor | 512 | 513 | +1 (+0.20%) |
| Mathlib.CategoryTheory.Sites.Sheaf | 545 | 546 | +1 (+0.18%) |
| Mathlib.CategoryTheory.Subobject.FactorThru | 555 | 556 | +1 (+0.18%) |
| Mathlib.CategoryTheory.Galois.EssSurj | 1129 | 1131 | +2 (+0.18%) |
| Mathlib.CategoryTheory.Galois.Equivalence | 1132 | 1134 | +2 (+0.18%) |
| Mathlib.CategoryTheory.Subobject.Lattice | 566 | 567 | +1 (+0.18%) |
| Mathlib.CategoryTheory.Sites.CartesianClosed | 608 | 609 | +1 (+0.16%) |
| Mathlib.CategoryTheory.Simple | 625 | 626 | +1 (+0.16%) |
| Mathlib.CategoryTheory.Sites.SheafHom | 635 | 636 | +1 (+0.16%) |
| Mathlib.Topology.Category.CompHausLike.EffectiveEpi | 759 | 760 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves | 765 | 766 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Presentable.Dense | 797 | 798 | +1 (+0.13%) |
| Mathlib.CategoryTheory.Presentable.StrongGenerator | 802 | 803 | +1 (+0.12%) |
| Mathlib.CategoryTheory.Presentable.OrthogonalReflection | 854 | 855 | +1 (+0.12%) |
| Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover | 859 | 860 | +1 (+0.12%) |
| Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections | 861 | 862 | +1 (+0.12%) |
| Mathlib.Topology.Sheaves.Sheafify | 869 | 870 | +1 (+0.12%) |
| Mathlib.Geometry.RingedSpace.SheafedSpace | 876 | 877 | +1 (+0.11%) |
| Mathlib.Topology.Sheaves.Alexandrov | 880 | 881 | +1 (+0.11%) |
Import changes for all files
| Files | Import difference |
|---|---|
154 filesMathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.Square Mathlib.AlgebraicTopology.MooreComplex Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Center.NegOnePow Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.ExtremalEpi Mathlib.CategoryTheory.Functor.KanExtension.Dense Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Generator.StrongGenerator Mathlib.CategoryTheory.Generator.Type 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.Monoidal.Preadditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Presentable.Adjunction Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation Mathlib.CategoryTheory.Presentable.Dense Mathlib.CategoryTheory.Presentable.EssentiallyLarge Mathlib.CategoryTheory.Presentable.LocallyPresentable Mathlib.CategoryTheory.Presentable.OrthogonalReflection Mathlib.CategoryTheory.Presentable.Presheaf Mathlib.CategoryTheory.Presentable.StrongGenerator Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal 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.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.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.Hypercover.Homotopy Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf Mathlib.CategoryTheory.Sites.Hypercover.One Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.MorphismProperty Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit 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 |
1 |
6 filesMathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Full |
2 |
106 filesMathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.CochainComplexOpposite Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass 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.TStructure Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.CochainComplex 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.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.Factorizations.CM5b Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomotopyCategory.Acyclic Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.KInjective Mathlib.Algebra.Homology.HomotopyCategory.KProjective 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.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.TotalComplexShift 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.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.Injective.Extend Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Extend Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.HomologicalFunctor 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.Subcategory |
3 |
36 filesMathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Shift.CommShiftTwo Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Triangulated.Basic Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.CategoryTheory.Triangulated.SpectralObject Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.RingTheory.Morita.Matrix |
4 |
Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty |
10 |
6 filesMathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Preadditive Mathlib.CategoryTheory.Center.Preadditive Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.FunctorCategory |
15 |
3 filesMathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory |
18 |
Declarations diff
+ AdditiveFunctor.ofExact_map_hom
+ AdditiveFunctor.ofLeftExact_map_hom
+ AdditiveFunctor.ofRightExact_map_hom
+ FullSubcategory.comp_hom
+ FullSubcategory.id_hom
+ FunctorsInverting.comp_hom
+ FunctorsInverting.id_hom
+ Hom
+ Hom.tr_comp'
+ InducedCategory.endEquiv
+ InducedCategory.eqToHom_hom
+ LeftExactFunctor.ofExact_map_hom
+ ObjectProperty.eqToHom_hom
+ RightExactFunctor.ofExact_map_hom
+ SheafedSpace.isOpenImmersion_iff_hom
+ Skeleton.comp_hom
+ _root_.CategoryTheory.InducedCategory.homAddEquiv
+ _root_.CategoryTheory.InducedCategory.homLinearEquiv
+ additiveFunctor
+ additiveFunctor_iff
+ associator_hom_hom_hom
+ associator_inv_hom_hom
+ braiding_hom_hom_hom
+ braiding_inv_hom_hom
+ comp_hom_base
+ comp_hom_c_app
+ comp_hom_c_app'
+ comp_hom_hom
+ comp_toHom
+ congr_hom_app
+ exactFunctor
+ exactFunctor_iff
+ exactFunctor_le_additiveFunctor
+ exactFunctor_le_leftExactFunctor
+ exactFunctor_le_rightExactFunctor
+ extension_comp_hom
+ fst_hom_hom
+ fullyFaithfulForgetToPresheafedSpace
+ fullyFaithfulForgetToPresheafedSpace_preimage_hom
+ hasCoeToSort
+ homEquiv
+ homMk'
+ homMk''
+ homMk_apply
+ homMk_eq_comp_iff
+ homMk_eq_id_iff
+ hom_apply
+ hom_hom_action_ρ
+ hom_hom_div
+ hom_hom_inv
+ hom_hom_zpow
+ id_hom_base
+ id_hom_c
+ id_hom_c_app
+ id_hom_hom
+ id_toHom
+ ihom_map_hom
+ instance (F : AdditiveFunctor C D) : F.obj.Additive := F.property
+ instance (V W : FGModuleCat.{v} K) : Module.Finite K (V.obj ⟶ W.obj)
+ instance (priority := 100) of_isIso [IsIso g] : LocallyRingedSpace.IsOpenImmersion g := by
+ instance : (forget₂CommMon C).Faithful := (fullyFaithfulForget₂CommMon _).faithful
+ instance : (forget₂CommMon C).Full := (fullyFaithfulForget₂CommMon _).full
+ instance : Category FiniteGrp
+ instance : Category LightDiagram
+ instance : Category LightDiagram'
+ instance : Category.{v} (InducedCategory D F)
+ instance : CreatesLimit (cospan f g) (compHausLikeToTop P)
+ instance : GrpObj H where inv := Grp.homMk' { hom := ι[H.X] }
+ instance : LightDiagram'.toLightFunctor.{u}.Faithful
+ instance : forgetToSheafedSpace.ReflectsIsomorphisms
+ instance : incl.Full where map_surjective f := ⟨f.hom, rfl⟩
+ instance [HasLimits C] {X Y : SheafedSpace C} (f g : X ⟶ Y) :
+ instance {A B : MonoOver X} (f : A ⟶ B) [IsIso f] : IsIso f.hom.left
+ instance {G H : CommGrp C} {f : G ⟶ H} [IsIso f] : IsIso f.hom.hom
+ instance {G H : Grp C} {f : G ⟶ H} [IsIso f] : IsIso f.hom.hom
+ instance {M N : CommMon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom.hom
+ instance {X : C} : Bot (MonoOver X) where bot := mk (initial.to X)
+ instance {X : C} : Top (MonoOver X) where top := mk (𝟙 _)
+ instance {X Y : LocallyRingedSpace} (f : X ⟶ Y) [LocallyRingedSpace.IsOpenImmersion f] :
+ isIso_hom_left_iff_subobjectMk_eq
+ isIso_iff_isIso_hom_left
+ isIso_toPshHom
+ isLocalHomStalkMap'
+ isoHom_inv_id_hom
+ isoInv_hom_id_hom
+ isoOfComponents_hom_hom_hom_app
+ isoOfComponents_inv_hom_hom_app
+ iso_inv_hom_left_comp
+ leftExactFunctor
+ leftExactFunctor_iff
+ leftExactFunctor_le_additiveFunctor
+ leftUnitor_hom_hom_hom
+ leftUnitor_inv_hom_hom
+ mk
+ mkArrowIso
+ mkIso_hom_hom_hom_hom
+ mkIso_inv_hom_hom_hom
+ mk_arrow
+ mk_coe
+ ofHom_hom_hom
+ rightExactFunctor
+ rightExactFunctor_iff
+ rightExactFunctor_le_additiveFunctor
+ rightUnitor_hom_hom_hom
+ rightUnitor_inv_hom_hom
+ snd_hom_hom
+ spanFunctorIsoIndexFunctor
+ toSheafedSpaceHom_hom_base
+ toSheafedSpaceHom_hom_c
+ whiskerLeft_hom_hom
+ whiskerRight_hom_hom
++ hom_hom_ofHom
++ mkIso_hom_hom
++ mkIso_inv_hom
+++ hom_hom_comp
+++ hom_hom_id
++++++ homMk
+++--- hom_comp
+++--- hom_id
++- comp_hom
++-- hom_ofHom
+-+ ext
+-+ isoMk
+-+++-++---+ id_hom
+-+- fullSubcategory
+-- comp'
+--+ to_iso
+---+ id'
- Grp.homMk
- Grp.homMk_hom'
- Grp_.homMk
- Grp_.homMk_hom'
- Hom.Simps.toShHom
- InducedCategory.category
- InducedCategory.hasCoeToSort
- InducedCategory.isoMk
- fullyFaithfulForget₂CommMon_
- instance (X : C) : Category (MonoOver X)
- instance (n : ℕ) : (inclusion n : Truncated n ⥤ _).Faithful := ObjectProperty.faithful_ι _
- instance (n : ℕ) : (inclusion n : Truncated n ⥤ _).Full := ObjectProperty.full_ι _
- instance (priority := 100) of_isIso [IsIso g] : LocallyRingedSpace.IsOpenImmersion g
- instance : (AdditiveFunctor.forget C D).Faithful
- instance : (AdditiveFunctor.forget C D).Full
- instance : (AdditiveFunctor.ofExact C D).Faithful := ObjectProperty.faithful_ιOfLE _
- instance : (AdditiveFunctor.ofExact C D).Full := ObjectProperty.full_ιOfLE _
- instance : (AdditiveFunctor.ofLeftExact C D).Faithful := ObjectProperty.faithful_ιOfLE _
- instance : (AdditiveFunctor.ofLeftExact C D).Full := ObjectProperty.full_ιOfLE _
- instance : (AdditiveFunctor.ofRightExact C D).Faithful := ObjectProperty.faithful_ιOfLE _
- instance : (AdditiveFunctor.ofRightExact C D).Full := ObjectProperty.full_ιOfLE _
- instance : (ExactFunctor.forget C D).Faithful
- instance : (ExactFunctor.forget C D).Full
- instance : (LeftExactFunctor.forget C D).Faithful
- instance : (LeftExactFunctor.forget C D).Full
- instance : (LeftExactFunctor.ofExact C D).Faithful
- instance : (LeftExactFunctor.ofExact C D).Full
- instance : (RightExactFunctor.forget C D).Faithful
- instance : (RightExactFunctor.forget C D).Full
- instance : (RightExactFunctor.ofExact C D).Faithful
- instance : (RightExactFunctor.ofExact C D).Full
- instance : (forget X).Faithful
- instance : (forget X).Full
- instance : (forget₂CommMon C).Faithful := InducedCategory.faithful _
- instance : (forget₂CommMon C).Full := InducedCategory.full _
- instance : Category (AdditiveFunctor C D)
- instance : Category (ContAction V G)
- instance : Category (ExactFunctor C D)
- instance : Category (LeftExactFunctor C D)
- instance : Category (RightExactFunctor C D)
- instance : Category FiniteGrp := InducedCategory.category FiniteGrp.toGrp
- instance : Category LightDiagram := InducedCategory.category toProfinite
- instance : Category LightDiagram' := InducedCategory.category LightDiagram'.toProfinite
- instance : CreatesLimit (cospan f g) (compHausLikeToTop P) := by
- instance : GrpObj H where inv := .mk ι[H.X]
- instance : HasForget (ContAction V G)
- instance : HasForget₂ (ContAction V G) (Action V G)
- instance : LightDiagram'.toLightFunctor.{u}.Faithful := ⟨id⟩
- instance : Preadditive (C ⥤+ D)
- instance : forgetToSheafedSpace.ReflectsIsomorphisms where reflects {_ _} f i
- instance : incl.Full where map_surjective f := ⟨f, rfl⟩
- instance [HasLimits C] {X Y : SheafedSpace C} (f g : X ⟶ Y) : Epi (coequalizer.π f g).base := by
- instance {A B : MonoOver X} (f : A ⟶ B) [IsIso f] : IsIso f.left
- instance {FV : V → V → Type*} {CV : V → Type*} [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)]
- instance {G H : Grp C} {f : G ⟶ H} [IsIso f] : IsIso f.hom
- instance {M N : CommMon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom
- instance {X : C} : Bot (MonoOver X) where bot := mk' (initial.to X)
- instance {X : C} : Top (MonoOver X) where top := mk' (𝟙 _)
- openNhdsCategory
-+-+ forget₂Mon_map_hom
-+-+-+-+-+-++-+++-+-+ hom_ext
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details about this script.
Decrease in tech debt: (relative, absolute) = (18.00, 0.03)
| Current number | Change | Type |
|---|---|---|
| 646 | -18 | erw |
Current commit 396459d4b8 Reference commit 5bd1b3ba0c
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
Okay, so this is really useful. I suffered a lot in a recent project because of the way morphisms in full subcategories are encoded in mathlib, so did my master's student, and @erdOne told me at Big Proof last month that he also had trouble with that. Is there anything I can do to help this move along?
Why is the import increase needed?
As the morphisms in full subcategories are no longer defeq to the morphisms in the original category, we need to import Mathlib.Algebra.Equiv.TransferInstance (which I had to split into two parts) in order to transport an abelian group structure via a bijection.
This pull request has conflicts, please merge master and resolve them.
This pull request has conflicts, please merge master and resolve them.
This pull request has conflicts, please merge master and resolve them.
This pull request has conflicts, please merge master and resolve them.
Benchmark results for 271fb1763b1aab1972f30f5abcf6785500c82c4c against 1f81f0f07632d72dbbb3f32e4ec907ed24a995e4 are in! @jcommelin @kbuzzard @robin-carlier
Major changes (1)
- 🟥
build/module/Mathlib.Algebra.Category.FGModuleCat.Abelian//instructions: +14.4G (+24.3%)
Minor changes (4)
- 🟥
build/module/Mathlib.CategoryTheory.Limits.ExactFunctor//instructions: +8.2G (+40.1%) from estimate, +6.4G (+28.7%) from previous value - 🟥
build/module/Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_//instructions: +5.6G (+13.7%) from estimate, +4.8G (+11.5%) from previous value - ✅
build/module/Mathlib.CategoryTheory.Monoidal.Grp_//instructions: -7.0G (-8.1%) from estimate, +221.3M (+0.3%) from previous value - ✅
build/module/Mathlib.CategoryTheory.Preadditive.Basic//instructions: -8.3G (-25.5%) from estimate, -7.7G (-24.0%) from previous value
This pull request has conflicts, please merge master and resolve them.
🚀 Pull request has been placed on the maintainer queue by dagurtomas.
This is clearly an improvement, we can fix things later if needed.
bors d+
:v: joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.
![mathlib-bors[bot] avatar](https://avatars.githubusercontent.com/in/421226?v=4 "Published by a pub.dev verified publisher"){kind=small}
Pull request successfully merged into master.
Build succeeded: