Commit 2024-02-10 10:41 b6a4cc4c

View on Github →

refactor(RepresentationTheory/GroupCohomology): tidy up 8599 and add more low degree cocycle API (#8785)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added theorem AlgEquiv.smul_units_def

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem Algebra.smul_units_def

Modified Mathlib/RepresentationTheory/Basic.lean

modified theorem Representation.ofMulDistribMulAction_apply_apply

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

deleted theorem Hilbert90.aux_ne_zero

added theorem groupCohomology.Hilbert90.aux_ne_zero

added theorem groupCohomology.isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units

deleted theorem hilbert90

Modified Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

added def groupCohomology.IsMulOneCoboundary

added def groupCohomology.IsMulOneCocycle

added def groupCohomology.IsMulTwoCoboundary

added def groupCohomology.IsMulTwoCocycle

added def groupCohomology.IsOneCoboundary

added def groupCohomology.IsOneCocycle

added def groupCohomology.IsTwoCoboundary

added def groupCohomology.IsTwoCocycle

added theorem groupCohomology.isMulOneCoboundary_of_oneCoboundaries

added theorem groupCohomology.isMulOneCocycle_of_oneCocycles

added theorem groupCohomology.isMulTwoCoboundary_of_twoCoboundaries

added theorem groupCohomology.isMulTwoCocycle_of_twoCocycles

added theorem groupCohomology.isOneCoboundary_of_oneCoboundaries

added theorem groupCohomology.isOneCocycle_of_oneCocycles

added theorem groupCohomology.isTwoCoboundary_of_twoCoboundaries

added theorem groupCohomology.isTwoCocycle_of_twoCocycles

added theorem groupCohomology.map_inv_of_isMulOneCocycle

added theorem groupCohomology.map_inv_of_isOneCocycle

added theorem groupCohomology.map_one_fst_of_isMulTwoCocycle

added theorem groupCohomology.map_one_fst_of_isTwoCocycle

added theorem groupCohomology.map_one_of_isMulOneCocycle

added theorem groupCohomology.map_one_of_isOneCocycle

added theorem groupCohomology.map_one_snd_of_isMulTwoCocycle

added theorem groupCohomology.map_one_snd_of_isTwoCocycle

deleted theorem groupCohomology.mem_oneCoboundaries_of_dZero_apply

deleted theorem groupCohomology.mem_oneCoboundaries_of_mem_range

modified theorem groupCohomology.mem_range_of_mem_oneCoboundaries

modified theorem groupCohomology.mem_range_of_mem_twoCoboundaries

deleted theorem groupCohomology.mem_twoCoboundaries_of_dOne_apply

deleted theorem groupCohomology.mem_twoCoboundaries_of_mem_range

added def groupCohomology.oneCoboundariesOfEq

added theorem groupCohomology.oneCoboundariesOfEq_apply

added def groupCohomology.oneCoboundariesOfIsMulOneCoboundary

added def groupCohomology.oneCoboundariesOfIsOneCoboundary

added def groupCohomology.oneCoboundariesOfMemRange

added theorem groupCohomology.oneCoboundaries_of_mem_range_apply

added def groupCohomology.oneCocyclesOfIsMulOneCocycle

added def groupCohomology.oneCocyclesOfIsOneCocycle

added theorem groupCohomology.smul_map_inv_div_map_inv_of_isMulTwoCocycle

added theorem groupCohomology.smul_map_inv_sub_map_inv_of_isTwoCocycle

added def groupCohomology.twoCoboundariesOfEq

added theorem groupCohomology.twoCoboundariesOfEq_apply

added def groupCohomology.twoCoboundariesOfIsMulTwoCoboundary

added def groupCohomology.twoCoboundariesOfIsTwoCoboundary

added def groupCohomology.twoCoboundariesOfMemRange

added theorem groupCohomology.twoCoboundariesOfMemRange_apply

added def groupCohomology.twoCocyclesOfIsMulTwoCocycle

added def groupCohomology.twoCocyclesOfIsTwoCocycle

Modified Mathlib/RepresentationTheory/Rep.lean

modified theorem Rep.ofMulDistribMulAction_ρ_apply_apply