Dependency changes

+ Rep.standardComplex
+ Tor
+ apply_bijective
+ augmentationSubmodule
+ augmentationSubmodule_eq_bot_of_isTrivial
+ barComplex
+ barResolution
+ barResolution.extIso
+ coe_linearization_obj
+ coe_linearization_obj_ρ
+ coinvariants
+ coinvariantsAdjunction
+ coinvariantsFinsuppLEquiv
+ coinvariantsFunctor
+ coinvariantsLift_comp_mkQ
+ coinvariantsLift_mk
+ coinvariantsMap
+ coinvariantsMap_comp
+ coinvariantsMap_comp_mkQ
+ coinvariantsMap_id
+ coinvariantsMap_mk
+ coinvariantsMkQ
+ coinvariantsTensor
+ coinvariantsTensorBarResolution
+ coinvariantsTensorFreeLEquiv
+ coinvariantsTensorFreeToFinsupp
+ coinvariantsTensorFreeToFinsupp_mk_tmul_single
+ coinvariantsToFinsupp
+ coinvariantsToFinsupp_mk_single
+ coinvariantsTprodLeftRegularLEquiv
+ coinvariants_mk_inv_tmul
+ coinvariants_mk_tmul_inv
+ cycles
+ dOne
+ dOne_apply_mem_oneCycles
+ dOne_comp_dTwo
+ dOne_comp_eq
+ dOne_single
+ dOne_single_inv_mul_ρ_add_single
+ dOne_single_inv_self_ρ_sub_self_inv
+ dOne_single_one_fst
+ dOne_single_one_snd
+ dOne_single_self_inv_ρ_sub_inv_self
+ dOne_single_ρ_add_single_inv_mul
+ dTwo
+ dTwo_apply_mem_twoCycles
+ dTwo_comp_eq
+ dTwo_single
+ dTwo_single_one_fst
+ dTwo_single_one_snd
+ dTwo_single_one_thd
+ dZero
+ dZero_comp_dOne
+ dZero_comp_eq
+ dZero_eq_zero_of_isTrivial
+ dZero_single
+ dZero_single_inv
+ dZero_single_one
+ d_comp_diagonalSuccIsoFree_inv_eq
+ d_def
+ diagonalOneIsoLeftRegular
+ diagonalSuccIsoFree
+ diagonalSuccIsoFree_hom_hom_single
+ diagonalSuccIsoFree_inv_hom_single
+ diagonalSuccIsoFree_inv_hom_single_single
+ diagonalSuccIsoTensorDiagonal
+ diagonalSuccIsoTensorTrivial_hom_hom
+ diagonalSuccIsoTensorTrivial_hom_hom_single
+ diagonalSuccIsoTensorTrivial_inv_hom
+ diagonalSuccIsoTensorTrivial_inv_hom_single_left
+ diagonalSuccIsoTensorTrivial_inv_hom_single_right
+ diagonalSuccIsoTensorTrivial_inv_hom_single_single
+ diagonal_succ_projective
+ finsuppLEquivFreeAsModule
+ finsuppProdLEquiv_single
+ finsuppProdLEquiv_symm_single_single
+ finsuppTensorLeft
+ finsuppTensorRight
+ finsuppToCoinvariants
+ finsuppToCoinvariantsTensorFree
+ finsuppToCoinvariantsTensorFree_single
+ finsuppToCoinvariants_single_mk
+ finsupp_single
+ freeAsModuleBasis
+ freeLift
+ freeLiftLEquiv
+ freeLift_hom_single_single
+ free_asModule_free
+ free_ext
+ free_projective
+ free_single_single
+ groupHomology
+ groupHomologyIsoTor
+ groupHomologyπ
+ iCycles
+ inhomogeneousChains
+ inhomogeneousChains.d_comp_d
+ inhomogeneousChains.d_def
+ inhomogeneousChainsIso
+ inhomogeneousCochains.d_comp_d
+ instance (A : Rep k G) : ((coinvariantsTensor k G).obj A).Additive := by
+ instance (X : ModuleCat k) : ((trivialFunctor G).obj X).ρ.IsTrivial
+ instance (k G : Type*) [CommRing k] [Monoid G] (α : Type*) :
+ instance : (coinvariantsFunctor k G).Additive
+ instance : (coinvariantsFunctor k G).PreservesZeroMorphisms
+ instance : (invariantsFunctor k G).Additive
+ instance : (invariantsFunctor k G).PreservesZeroMorphisms
+ instance : FiberFunctor (Action.forget FintypeCat G)
+ instance : FiberFunctor (forget₂ (Action FintypeCat G) FintypeCat)
+ instance : GaloisCategory (Action FintypeCat G)
+ instance : IsTrivial (trivial k G V)
+ instance : Limits.PreservesColimits (coinvariantsFunctor k G)
+ instance : Limits.PreservesLimits (invariantsFunctor k G)
+ instance : PreGaloisCategory (Action FintypeCat G)
+ instance : PreservesFiniteLimits (forget (Action FintypeCat G)) := by
+ instance [LeftRigidCategory V] : LeftRigidCategory (SingleObj H ⥤ V) := by
+ instance [RightRigidCategory V] : RightRigidCategory (SingleObj H ⥤ V) := by
+ instance [RigidCategory V] : RigidCategory (SingleObj H ⥤ V) := by
+ instance {G : Type u} [Monoid G] (X : Action FintypeCat G) : MulAction G X.V
+ instance {X Y : Action FintypeCat G} (f : X ⟶ Y) :
+ inv_self_apply
+ invariantsAdjunction
+ invariantsFunctor
+ isTrivial_apply
+ isTrivial_def
+ isZero_Tor_succ_of_projective
+ isZero_groupCohomology_succ_of_subsingleton
+ isZero_groupHomology_succ_of_subsingleton
+ isoStandardComplex
+ leftRegularHomEquiv_symm_hom_single
+ leftRegularHom_hom_single
+ leftRegularTensorTrivialIsoFree
+ leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single
+ leftRegularTensorTrivialIsoFree_inv_hom_single_single
+ leftRegular_projective
+ mem_augmentationSubmodule_of_eq
+ mem_oneCycles_iff
+ mem_oneCycles_of_mem_oneBoundaries
+ mem_twoCycles_iff
+ mem_twoCycles_of_mem_twoBoundaries
+ mkQ_comp_dZero
+ ofCoinvariantsTprodLeftRegular
+ ofCoinvariantsTprodLeftRegular_mk_tmul_single
+ ofMulActionSubsingletonIsoTrivial
+ oneBoundaries
+ oneBoundariesToOneCycles
+ oneBoundariesToOneCycles_apply
+ oneBoundaries_le_oneCycles
+ oneChainsLequiv
+ oneChainsToAugmentationSubmodule
+ oneCycles
+ oneCyclesLequivOfIsTrivial
+ oneCycles_eq_top_of_isTrivial
+ partialProd_contractNth
+ range_dZero_eq_augmentationSubmodule
+ self_inv_apply
+ single_inv_ρ_self_add_single_mem_oneBoundaries
+ single_mem_oneCycles_iff
+ single_mem_oneCycles_of_mem_invariants
+ single_mem_twoCycles_iff
+ single_mem_twoCycles_iff_inv
+ single_one_fst_sub_single_one_fst_mem_twoBoundaries
+ single_one_fst_sub_single_one_snd_mem_twoBoundaries
+ single_one_mem_oneBoundaries
+ single_one_snd_sub_single_one_fst_mem_twoBoundaries
+ single_one_snd_sub_single_one_snd_mem_twoBoundaries
+ single_ρ_self_add_single_inv_mem_oneBoundaries
+ standardResolution
+ standardResolution.extIso
+ tensorObj_def
+ tensorUnit_def
+ tensor_ρ
+ threeChainsLequiv
+ toCycles
+ trivialFunctor
+ trivial_apply
+ trivial_projective_of_subsingleton
+ twoBoundaries
+ twoBoundariesToTwoCycles
+ twoBoundariesToTwoCycles_apply
+ twoBoundaries_le_twoCycles
+ twoChainsLequiv
+ twoCycles
+ zeroChainsLequiv
++ coinvariantsLift
++ d_single
++ diagonalSuccIsoTensorTrivial
++ finsupp
++ free
+++- d
+++-- diagonal
+++-- leftRegular
+-+- trivial
- actionDiagonalSucc
- actionDiagonalSucc_hom_apply
- actionDiagonalSucc_inv_apply
- apply_eq_self
- diagonalHomEquiv
- diagonalHomEquiv_apply
- diagonalHomEquiv_symm_apply
- diagonalHomEquiv_symm_partialProd_succ
- diagonalSucc_hom_single
- diagonalSucc_inv_single_left
- diagonalSucc_inv_single_right
- diagonalSucc_inv_single_single
- groupCohomology.extIso
- groupCohomology.projectiveResolution
- groupCohomology.resolution
- instance : FiberFunctor (Action.forget FintypeCat (MonCat.of G))
- instance : FiberFunctor (forget₂ (Action FintypeCat (MonCat.of G)) FintypeCat)
- instance : GaloisCategory (Action FintypeCat (MonCat.of G))
- instance : IsTrivial (trivial k (G := G) (V := V))
- instance : PreGaloisCategory (Action FintypeCat (MonCat.of G))
- instance : PreservesFiniteLimits (forget (Action FintypeCat (MonCat.of G))) := by
- instance [LeftRigidCategory V] : LeftRigidCategory (SingleObj (H : MonCat.{u}) ⥤ V) := by
- instance [RightRigidCategory V] : RightRigidCategory (SingleObj (H : MonCat.{u}) ⥤ V) := by
- instance [RigidCategory V] : RigidCategory (SingleObj (H : MonCat.{u}) ⥤ V) := by
- instance {G : MonCat.{u}} (X : Action FintypeCat G) : MulAction G X.V := Action.instMulAction X
- instance {G : Type u} [Group G] (X : Action FintypeCat (MonCat.of G)) : MulAction G X.V
- instance {X Y : Action FintypeCat (MonCat.of G)} (f : X ⟶ Y) :
- leftRegularHomEquiv_symm_single
- leftRegularHom_apply
- linearYonedaObjResolution
- linearYonedaObjResolution_d_apply
- linearization_of
- ofMulActionBasis
- ofMulActionBasisAux
- ofMulAction_free
- of_ρ_apply
-++ d_eq
-- diagonalSucc
--+ trivial_def

## 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.

Current commit d51a367bab
Reference commit 1c5e1606e6

You can run this locally as

./scripts/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).