feat(CategoryTheory): Additive and Linear when Hom types are only monoids#28826
Open
alreadydone wants to merge 1 commit intoleanprover-community:masterfrom
Open
feat(CategoryTheory): Additive and Linear when Hom types are only monoids#28826alreadydone wants to merge 1 commit intoleanprover-community:masterfrom
alreadydone wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary 3b097993a0
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Preadditive.Biproducts | 715 | 714 | -1 (-0.14%) |
| Mathlib.CategoryTheory.Preadditive.AdditiveFunctor | 719 | 718 | -1 (-0.14%) |
Import changes for all files
| Files | Import difference |
|---|---|
98 filesMathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.ChosenFiniteProducts Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.Square Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.MooreComplex 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.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.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Generator.Indization 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.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Rotate |
-1 |
367 filesMathlib.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.AlgebraCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal 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.ContinuousCohomology.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.Grp.ZModuleEquivalence 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.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono 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.Limits 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.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.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.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor 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.PullbackContinuous 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.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift 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.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.Embedding.ExtendHomology 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.HomologySequenceLemmas Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor 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.Linear Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.PID Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.ValuativeCriterion 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.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Condensed.AB Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Explicit Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.FieldTheory.LinearDisjoint Mathlib.FieldTheory.PurelyInseparable.Tower Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.Discriminant.Different Mathlib.NumberTheory.RamificationInertia.Unramified Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.Coinduced Mathlib.RepresentationTheory.Coinvariants Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.FiniteIndex Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic 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.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 Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Grassmannian Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.PicardGroup Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.Regular.Depth Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.Etale Mathlib.RingTheory.RingHom.FaithfullyFlat Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Smooth Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Sheaves.MayerVietoris |
1 |
197 filesMathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Topology Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.IdealSheaf Mathlib.AlgebraicGeometry.Limits 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.FiniteType Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Topology Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Equivalence Mathlib.Condensed.Functors Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.NumberTheory.ClassNumber.Finite Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.Basic 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 Mathlib.NumberTheory.NumberField.DedekindZeta Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.NumberTheory.NumberField.Embeddings 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.Ideal Mathlib.NumberTheory.NumberField.InfinitePlace.Basic Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex Mathlib.NumberTheory.NumberField.Norm Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.Instances Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Ideal.Int Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.Invariant.Basic Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.Invariant Mathlib.RingTheory.KrullDimension.Module Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.OpenImmersion Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Support Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Sheaves.CommRingCat |
2 |
Mathlib.CategoryTheory.Preadditive.Semi (new file) |
618 |
Mathlib.Algebra.Category.MonCat.Presemiadditive (new file) |
626 |
Mathlib.Algebra.Category.ModuleCat.Semi (new file) |
780 |
Declarations diff
+ Hom
+ Hom.Simps.hom
+ Hom.hom
+ Hom.hom₂
+ Hom.hom₂_ofHom₂
+ Hom.instModule
+ Iso.conj_eq_conj
+ Iso.homCongr_eq_arrowCongr
+ LinearEquiv.toModuleIso
+ LinearMap.comp_id_moduleCat
+ LinearMap.id_moduleCat_comp
+ Presemiadditive
+ SemimoduleCat
+ coe_of
+ comp_apply
+ comp_left_eq_zero
+ comp_nsmul
+ comp_right_eq_zero
+ comp_sum
+ endSemiringEquiv
+ forget_map
+ forget_obj
+ forget₂_map
+ forget₂_map_homMk
+ forget₂_obj
+ forget₂_obj_moduleCat_of
+ fullSubcategory
+ hasForgetToAddCommMonoid
+ homEquiv
+ homLinearEquiv
+ homMk
+ hom_add_apply
+ hom_bijective
+ hom_comp
+ hom_ext
+ hom_id
+ hom_injective
+ hom_inv_apply
+ hom_ofHom
+ hom_smul
+ hom_sum
+ hom_surjective
+ hom_zsmul
+ id_apply
+ inducedCategory
+ instPresemiadditive_injective
+ instance (P Q : AddCommMonCat) : AddCommMonoid (P ⟶ Q)
+ instance (X : C) : AddCommMonoid (End X) := inferInstanceAs (AddCommMonoid (X ⟶ X))
+ instance : (forget (SemimoduleCat.{v} R)).ReflectsIsomorphisms
+ instance : (forget₂ (SemimoduleCat.{v} R) AddCommMonCat).Additive
+ instance : (forget₂ (SemimoduleCat.{v} R) AddCommMonCat.{v}).ReflectsIsomorphisms
+ instance : AddCommMonoid (M ⟶ N)
+ instance : AddCommMonoid (mkOfSMul' φ) := by
+ instance : CoeSort (SemimoduleCat.{v} R) (Type v)
+ instance : ConcreteCategory (SemimoduleCat.{v} R) (· →ₗ[R] ·)
+ instance : Functor.Additive (AdditiveFunctor.forget C D)
+ instance : HasZeroMorphisms (SemimoduleCat.{v} R)
+ instance : HasZeroObject (SemimoduleCat.{v} R)
+ instance : Inhabited (SemimoduleCat R)
+ instance : Linear S (SemimoduleCat.{v} S) := SemimoduleCat.Algebra.instLinear
+ instance : Module R (mkOfSMul' φ)
+ instance : Presemiadditive (C ⥤ D)
+ instance : Presemiadditive (C ⥤+ D)
+ instance : Presemiadditive (SemimoduleCat.{v} R)
+ instance : Presemiadditive AddCommMonCat
+ instance : SMul R (mkOfSMul' φ) := ⟨fun r (x : A) => (show A ⟶ A from φ r) x⟩
+ instance : SMul S (M ⟶ N)
+ instance [Preadditive C] : Presemiadditive C
+ instance [Preadditive D] : Preadditive (C ⥤+ D) := .inducedCategory _
+ inv_hom_apply
+ isZero_iff_subsingleton
+ isZero_of_iff_subsingleton
+ isZero_of_subsingleton
+ leftComp
+ linearEquivIsoModuleIso
+ mkOfSMul
+ mkOfSMul'
+ mkOfSMul'_smul
+ mkOfSMul_smul
+ moduleCategory
+ nsmul_comp
+ of
+ ofHom
+ ofHom_apply
+ ofHom_comp
+ ofHom_hom
+ ofHom_id
+ ofHom₂
+ ofHom₂_hom₂
+ ofSelfIso
+ of_coe
+ rightComp
+ smul
+ smulNatTrans
+ smul_naturality
+ subsingleton_of_isZero
+ subsingleton_presemiadditive_of_hasBinaryBiproducts
+ sum_comp
+ sum_comp'
+ toLinearEquiv
++ homAddEquiv
++ hom_add
++ hom_nsmul
++ hom_zero
++ instance : Add (M ⟶ N)
++ instance : Zero (M ⟶ N)
+++ instance : SMul ℕ (M ⟶ N)
+-+ compHom
- instance : Functor.Additive (AdditiveFunctor.forget C D) where map_add := rfl
- instance : Preadditive (C ⥤+ D)
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) = (1.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 791 | -1 | erw |
Current commit eb89360f52
Reference commit 3b097993a0
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).
079f8ed to
eb89360
Compare
Contributor
|
Should |
Collaborator
|
This pull request has conflicts, please merge |
Contributor
Author
If you start from a module that is a group then the group structure coming from the ring will not be defeq to the original one. I don't know how much trouble this will cause but I'd rather not deal with it for now. |
SemimoduleCat
Closed
1 task
BeibeiX0
pushed a commit
to BeibeiX0/mathlib4
that referenced
this pull request
Nov 7, 2025
…anprover-community#31023) + Introduce SemimoduleCat, the category of semimodules (mathlib's Module) over a Semiring. The new file ModuleCat/Semi.lean is copied from ModuleCat/Basic.lean. The additive/linear instances would require leanprover-community#28826.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
introduce Presemiadditive categories, which generalizes Preadditive categories: the Hom sets are commutative monoids rather than groups, and
comp_zeroandzero_compis no longer automatic. The new file Preadditive/Semi.lean is adapted from Preadditive/Basic.lean, though many contents can't be generalized.generalize Functor.Additive and Functor.Linear to take Presemiadditive categories instead. The former needs a
map_zerofield since it's not automatic for Presemiadditive categories.introduce SemimoduleCat, the category of semimodules (mathlib's Module) over a Semiring. The new file ModuleCat/Semi.lean is copied from ModuleCat/Basic.lean.
TODOs: additive/linear equivalence between SemimoduleCat and ModuleCat and use it to transfer results; monoidal structure on SemimoduleCat; change
CommRing.Picto use SemimoduleCat.