feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add IsOneCycle predicate and friends#21757
feat(RepresentationTheory/Homological/GroupHomology/LowDegree): add IsOneCycle predicate and friends#21757101damnations wants to merge 165 commits intomasterfrom
IsOneCycle predicate and friends#21757Conversation
PR summary 292d9ea726
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RepresentationTheory.GroupCohomology.Basic | 1607 | 0 | -1607 (-100.00%) |
| Mathlib.RepresentationTheory.GroupCohomology.Resolution | 1606 | 0 | -1606 (-100.00%) |
| Mathlib.CategoryTheory.Action.Monoidal | 1010 | 1030 | +20 (+1.98%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 |
-1807 |
Mathlib.RepresentationTheory.GroupCohomology.LowDegree |
-1802 |
Mathlib.RepresentationTheory.GroupCohomology.Basic |
-1607 |
Mathlib.RepresentationTheory.GroupCohomology.Resolution |
-1606 |
3 filesMathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.Invariants |
2 |
Mathlib.RepresentationTheory.Rep |
7 |
Mathlib.CategoryTheory.Action.Monoidal |
20 |
Mathlib.RepresentationTheory.Coinvariants (new file) |
1523 |
Mathlib.RepresentationTheory.Homological.Resolution (new file) |
1604 |
Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic (new file) |
1605 |
Mathlib.RepresentationTheory.Homological.GroupHomology.Basic (new file) |
1606 |
Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (new file) |
1783 |
Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree |
1801 |
Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90 |
1806 |
Declarations diff
+ IsOneBoundary
+ IsOneCycle
+ IsTwoBoundary
+ IsTwoCycle
+ IsZeroBoundary
+ Rep.standardComplex
+ Tor
+ apply_bijective
+ augmentationSubmodule
+ augmentationSubmoduleOfIsZeroBoundary
+ 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
+ isOneBoundary_iff
+ isOneBoundary_of_mem_oneBoundaries
+ isOneCycle_of_mem_oneCycles
+ isTrivial_apply
+ isTrivial_def
+ isTwoBoundary_iff
+ isTwoBoundary_of_mem_twoBoundaries
+ isTwoCycle_of_mem_twoCycles
+ isZeroBoundary_iff
+ isZeroBoundary_of_mem_augmentationSubmodule
+ 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
+ oneBoundariesOfIsOneBoundary
+ oneBoundariesToOneCycles
+ oneBoundariesToOneCycles_apply
+ oneBoundaries_le_oneCycles
+ oneChainsLequiv
+ oneChainsToAugmentationSubmodule
+ oneCycles
+ oneCyclesLequivOfIsTrivial
+ oneCyclesOfIsOneCycle
+ oneCycles_eq_top_of_isTrivial
+ partialProd_contractNth
+ range_dZero_eq_augmentationSubmodule
+ self_inv_apply
+ single_inv_ρ_self_add_single_mem_oneBoundaries
+ single_isOneCycle_iff
+ single_isOneCycle_of_mem_fixedPoints
+ single_isTwoCycle_iff
+ single_isTwoCycle_iff_inv
+ 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
+ twoBoundariesOfIsTwoBoundary
+ twoBoundariesToTwoCycles
+ twoBoundariesToTwoCycles_apply
+ twoBoundaries_le_twoCycles
+ twoChainsLequiv
+ twoCycles
+ twoCyclesOfIsTwoCycle
+ 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
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) = (19.46, 0.02)
| Current number | Change | Type |
|---|---|---|
| 3594 | -18 | porting notes |
| 1321 | -20 | erw |
Current commit 292d9ea726
Reference commit 1c5e1606e6
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).
…lib4 into actionmoncat
…mathlib4 into coinvariantsstuffhalf
…-community/mathlib4 into coinvariantsstuff
…mathlib4 into diagonalsuccisohalf
…ommunity/mathlib4 into diagonalsucciso
|
This PR has been migrated to a fork-based workflow: #25884 |
Given an additive abelian group
Awith an appropriate scalar action ofG, we provide supportfor turning a finsupp
f : G →₀ Asatisfying the 1-cycle identity into an element of theoneCyclesof the representation onAcorresponding to the scalar action. We also do this for0-boundaries, 1-boundaries, 2-cycles and 2-boundaries. We follow the structure of
RepresentationTheory.Homological.GroupCohomology.LowDegree.Action.rhoaMonoidHominstead of a morphism inMonCat#21652Finsupp#21732Rep.diagonal k G (n + 1) ≅ Rep.free k G (Fin n → G)#21736