Commit 2025-07-03 00:27 7e9586b1

View on Github →

refactor: denote low degree group cohomology API indices with subscripts (#26546) This PR replaces names like groupCohomology.oneCocycles with groupCohomology.cocycles₁, to bring this API in line with the group homology naming scheme suggested by @jcommelin in #25873.

Estimated changes

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean

added theorem groupCohomology.cochainsMap_f_0_comp_cochainsIso₀

deleted theorem groupCohomology.cochainsMap_f_0_comp_zeroCochainsIso

added theorem groupCohomology.cochainsMap_f_1_comp_cochainsIso₁

deleted theorem groupCohomology.cochainsMap_f_1_comp_oneCochainsIso

added theorem groupCohomology.cochainsMap_f_2_comp_cochainsIso₂

deleted theorem groupCohomology.cochainsMap_f_2_comp_twoCochainsIso

added theorem groupCohomology.cochainsMap_f_3_comp_cochainsIso₃

deleted theorem groupCohomology.cochainsMap_f_3_comp_threeCochainsIso

added theorem groupCohomology.cocyclesMap_cocyclesIso₀_hom_f

added theorem groupCohomology.cocyclesMap_comp_isoCocycles₁_hom

added theorem groupCohomology.cocyclesMap_comp_isoCocycles₂_hom

deleted theorem groupCohomology.cocyclesMap_comp_isoOneCocycles_hom

deleted theorem groupCohomology.cocyclesMap_comp_isoTwoCocycles_hom

deleted theorem groupCohomology.cocyclesMap_zeroIsoCocycles_hom_f

added theorem groupCohomology.coe_mapCocycles₁

added theorem groupCohomology.coe_mapCocycles₂

deleted theorem groupCohomology.coe_mapOneCocycles

deleted theorem groupCohomology.coe_mapTwoCocycles

added theorem groupCohomology.mapCocycles₁_comp_i

added theorem groupCohomology.mapCocycles₁_one

added theorem groupCohomology.mapCocycles₂_comp_i

deleted theorem groupCohomology.mapOneCocycles_comp_i

deleted theorem groupCohomology.mapOneCocycles_one

deleted theorem groupCohomology.mapTwoCocycles_comp_i

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/Hilbert90.lean

added theorem groupCohomology.isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units

deleted theorem groupCohomology.isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean

added theorem groupCohomology.mem_cocycles₁_of_comp_eq_d₀₁

added theorem groupCohomology.mem_cocycles₂_of_comp_eq_d₁₂

deleted theorem groupCohomology.mem_oneCocycles_of_comp_eq_dZero

deleted theorem groupCohomology.mem_twoCocycles_of_comp_eq_dOne

Modified Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

modified theorem groupCohomology.H1_induction_on

modified def groupCohomology.H1π

modified theorem groupCohomology.H1π_eq_iff

modified theorem groupCohomology.H1π_eq_zero_iff

modified theorem groupCohomology.H2_induction_on

modified def groupCohomology.H2π

modified theorem groupCohomology.H2π_eq_iff

modified theorem groupCohomology.H2π_eq_zero_iff

added def groupCohomology.IsCoboundary₁

added def groupCohomology.IsCoboundary₂

added def groupCohomology.IsCocycle₁

added def groupCohomology.IsCocycle₂

added def groupCohomology.IsMulCoboundary₁

added def groupCohomology.IsMulCoboundary₂

added def groupCohomology.IsMulCocycle₁

added def groupCohomology.IsMulCocycle₂

deleted def groupCohomology.IsMulOneCoboundary

deleted def groupCohomology.IsMulOneCocycle

deleted def groupCohomology.IsMulTwoCoboundary

deleted def groupCohomology.IsMulTwoCocycle

deleted def groupCohomology.IsOneCoboundary

deleted def groupCohomology.IsOneCocycle

deleted def groupCohomology.IsTwoCoboundary

deleted def groupCohomology.IsTwoCocycle

added def groupCohomology.coboundariesOfIsCoboundary₁

added def groupCohomology.coboundariesOfIsCoboundary₂

added def groupCohomology.coboundariesOfIsMulCoboundary₁

added def groupCohomology.coboundariesOfIsMulCoboundary₂

added theorem groupCohomology.coboundariesToCocycles₁_apply

added theorem groupCohomology.coboundariesToCocycles₂_apply

added theorem groupCohomology.coboundaries₁.coe_mk

added theorem groupCohomology.coboundaries₁.val_eq_coe

added def groupCohomology.coboundaries₁

added theorem groupCohomology.coboundaries₁_eq_bot_of_isTrivial

added theorem groupCohomology.coboundaries₁_ext

added theorem groupCohomology.coboundaries₁_le_cocycles₁

added theorem groupCohomology.coboundaries₂.coe_mk

added theorem groupCohomology.coboundaries₂.val_eq_coe

added def groupCohomology.coboundaries₂

added theorem groupCohomology.coboundaries₂_ext

added theorem groupCohomology.coboundaries₂_le_cocycles₂

added def groupCohomology.cochainsIso₀

added def groupCohomology.cochainsIso₁

added def groupCohomology.cochainsIso₂

added def groupCohomology.cochainsIso₃

added def groupCohomology.cocyclesIso₀

added theorem groupCohomology.cocyclesIso₀_hom_comp_f

added theorem groupCohomology.cocyclesIso₀_inv_comp_iCocycles

deleted theorem groupCohomology.cocyclesMk_0_eq

deleted theorem groupCohomology.cocyclesMk_1_eq

deleted theorem groupCohomology.cocyclesMk_2_eq

added theorem groupCohomology.cocyclesMk₀_eq

added theorem groupCohomology.cocyclesMk₁_eq

added theorem groupCohomology.cocyclesMk₂_eq

added def groupCohomology.cocyclesOfIsCocycle₁

added def groupCohomology.cocyclesOfIsCocycle₂

added def groupCohomology.cocyclesOfIsMulCocycle₁

added def groupCohomology.cocyclesOfIsMulCocycle₂

added theorem groupCohomology.cocycles₁.coe_mk

added theorem groupCohomology.cocycles₁.d₁₂_apply

added theorem groupCohomology.cocycles₁.val_eq_coe

added def groupCohomology.cocycles₁

added def groupCohomology.cocycles₁IsoOfIsTrivial

added theorem groupCohomology.cocycles₁_ext

added theorem groupCohomology.cocycles₁_map_inv

added theorem groupCohomology.cocycles₁_map_mul_of_isTrivial

added theorem groupCohomology.cocycles₁_map_one

added theorem groupCohomology.cocycles₂.coe_mk

added theorem groupCohomology.cocycles₂.d₂₃_apply

added theorem groupCohomology.cocycles₂.val_eq_coe

added def groupCohomology.cocycles₂

added theorem groupCohomology.cocycles₂_ext

added theorem groupCohomology.cocycles₂_map_one_fst

added theorem groupCohomology.cocycles₂_map_one_snd

added theorem groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv

deleted theorem groupCohomology.comp_dOne_eq

deleted theorem groupCohomology.comp_dTwo_eq

deleted theorem groupCohomology.comp_dZero_eq

added theorem groupCohomology.comp_d₀₁_eq

added theorem groupCohomology.comp_d₁₂_eq

added theorem groupCohomology.comp_d₂₃_eq

added def groupCohomology.dArrowIso₀₁

deleted def groupCohomology.dOne

deleted theorem groupCohomology.dOne_apply_mem_twoCocycles

deleted theorem groupCohomology.dOne_comp_dTwo

deleted def groupCohomology.dTwo

deleted def groupCohomology.dZero

deleted def groupCohomology.dZeroArrowIso

deleted theorem groupCohomology.dZero_apply_mem_oneCocycles

deleted theorem groupCohomology.dZero_comp_dOne

deleted theorem groupCohomology.dZero_eq_zero

deleted theorem groupCohomology.dZero_ker_eq_invariants

added def groupCohomology.d₀₁

added theorem groupCohomology.d₀₁_apply_mem_cocycles₁

added theorem groupCohomology.d₀₁_comp_d₁₂

added theorem groupCohomology.d₀₁_eq_zero

added theorem groupCohomology.d₀₁_ker_eq_invariants

added def groupCohomology.d₁₂

added theorem groupCohomology.d₁₂_apply_mem_cocycles₂

added theorem groupCohomology.d₁₂_comp_d₂₃

added def groupCohomology.d₂₃

deleted theorem groupCohomology.eq_dOne_comp_inv

deleted theorem groupCohomology.eq_dTwo_comp_inv

deleted theorem groupCohomology.eq_dZero_comp_inv

added theorem groupCohomology.eq_d₀₁_comp_inv

added theorem groupCohomology.eq_d₁₂_comp_inv

added theorem groupCohomology.eq_d₂₃_comp_inv

added theorem groupCohomology.isCoboundary₁_of_mem_coboundaries₁

added theorem groupCohomology.isCoboundary₂_of_mem_coboundaries₂

added theorem groupCohomology.isCocycle₁_of_mem_cocycles₁

added theorem groupCohomology.isCocycle₂_of_mem_cocycles₂

added theorem groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁

added theorem groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂

added theorem groupCohomology.isMulCocycle₁_of_mem_cocycles₁

added theorem groupCohomology.isMulCocycle₂_of_mem_cocycles₂

deleted theorem groupCohomology.isMulOneCoboundary_of_mem_oneCoboundaries

deleted theorem groupCohomology.isMulOneCocycle_of_mem_oneCocycles

deleted theorem groupCohomology.isMulTwoCoboundary_of_mem_twoCoboundaries

deleted theorem groupCohomology.isMulTwoCocycle_of_mem_twoCocycles

deleted theorem groupCohomology.isOneCoboundary_of_mem_oneCoboundaries

deleted theorem groupCohomology.isOneCocycle_of_mem_oneCocycles

deleted theorem groupCohomology.isTwoCoboundary_of_mem_twoCoboundaries

deleted theorem groupCohomology.isTwoCocycle_of_mem_twoCocycles

added def groupCohomology.isoCocycles₁

added theorem groupCohomology.isoCocycles₁_hom_comp_i

added theorem groupCohomology.isoCocycles₁_inv_comp_iCocycles

added def groupCohomology.isoCocycles₂

added theorem groupCohomology.isoCocycles₂_hom_comp_i

added theorem groupCohomology.isoCocycles₂_inv_comp_iCocycles

deleted def groupCohomology.isoOneCocycles

deleted theorem groupCohomology.isoOneCocycles_hom_comp_i

deleted theorem groupCohomology.isoOneCocycles_inv_comp_iCocycles

deleted def groupCohomology.isoTwoCocycles

deleted theorem groupCohomology.isoTwoCocycles_hom_comp_i

deleted theorem groupCohomology.isoTwoCocycles_inv_comp_iCocycles

added theorem groupCohomology.map_inv_of_isCocycle₁

added theorem groupCohomology.map_inv_of_isMulCocycle₁

deleted theorem groupCohomology.map_inv_of_isMulOneCocycle

deleted theorem groupCohomology.map_inv_of_isOneCocycle

added theorem groupCohomology.map_one_fst_of_isCocycle₂

added theorem groupCohomology.map_one_fst_of_isMulCocycle₂

deleted theorem groupCohomology.map_one_fst_of_isMulTwoCocycle

deleted theorem groupCohomology.map_one_fst_of_isTwoCocycle

added theorem groupCohomology.map_one_of_isCocycle₁

added theorem groupCohomology.map_one_of_isMulCocycle₁

deleted theorem groupCohomology.map_one_of_isMulOneCocycle

deleted theorem groupCohomology.map_one_of_isOneCocycle

added theorem groupCohomology.map_one_snd_of_isCocycle₂

added theorem groupCohomology.map_one_snd_of_isMulCocycle₂

deleted theorem groupCohomology.map_one_snd_of_isMulTwoCocycle

deleted theorem groupCohomology.map_one_snd_of_isTwoCocycle

added theorem groupCohomology.mem_cocycles₁_def

added theorem groupCohomology.mem_cocycles₁_iff

added theorem groupCohomology.mem_cocycles₁_of_addMonoidHom

added theorem groupCohomology.mem_cocycles₂_def

added theorem groupCohomology.mem_cocycles₂_iff

deleted theorem groupCohomology.mem_oneCocycles_def

deleted theorem groupCohomology.mem_oneCocycles_iff

deleted theorem groupCohomology.mem_oneCocycles_of_addMonoidHom

deleted theorem groupCohomology.mem_twoCocycles_def

deleted theorem groupCohomology.mem_twoCocycles_iff

deleted theorem groupCohomology.oneCoboundaries.coe_mk

deleted theorem groupCohomology.oneCoboundaries.val_eq_coe

deleted def groupCohomology.oneCoboundaries

deleted def groupCohomology.oneCoboundariesOfIsMulOneCoboundary

deleted def groupCohomology.oneCoboundariesOfIsOneCoboundary

deleted theorem groupCohomology.oneCoboundariesToOneCocycles_apply

deleted theorem groupCohomology.oneCoboundaries_eq_bot_of_isTrivial

deleted theorem groupCohomology.oneCoboundaries_ext

deleted theorem groupCohomology.oneCoboundaries_le_oneCocycles

deleted def groupCohomology.oneCochainsIso

deleted theorem groupCohomology.oneCocycles.coe_mk

deleted theorem groupCohomology.oneCocycles.dOne_apply

deleted theorem groupCohomology.oneCocycles.val_eq_coe

deleted def groupCohomology.oneCocycles

deleted def groupCohomology.oneCocyclesIsoOfIsTrivial

deleted def groupCohomology.oneCocyclesOfIsMulOneCocycle

deleted def groupCohomology.oneCocyclesOfIsOneCocycle

deleted theorem groupCohomology.oneCocycles_ext

deleted theorem groupCohomology.oneCocycles_map_inv

deleted theorem groupCohomology.oneCocycles_map_mul_of_isTrivial

deleted theorem groupCohomology.oneCocycles_map_one

added theorem groupCohomology.smul_map_inv_div_map_inv_of_isMulCocycle₂

deleted theorem groupCohomology.smul_map_inv_div_map_inv_of_isMulTwoCocycle

added theorem groupCohomology.smul_map_inv_sub_map_inv_of_isCocycle₂

deleted theorem groupCohomology.smul_map_inv_sub_map_inv_of_isTwoCocycle

deleted theorem groupCohomology.subtype_comp_dZero

added theorem groupCohomology.subtype_comp_d₀₁

deleted def groupCohomology.threeCochainsIso

added theorem groupCohomology.toCocycles_comp_isoCocycles₁_hom

added theorem groupCohomology.toCocycles_comp_isoCocycles₂_hom

deleted theorem groupCohomology.toCocycles_comp_isoOneCocycles_hom

deleted theorem groupCohomology.toCocycles_comp_isoTwoCocycles_hom

deleted theorem groupCohomology.twoCoboundaries.coe_mk

deleted theorem groupCohomology.twoCoboundaries.val_eq_coe

deleted def groupCohomology.twoCoboundaries

deleted def groupCohomology.twoCoboundariesOfIsMulTwoCoboundary

deleted def groupCohomology.twoCoboundariesOfIsTwoCoboundary

deleted theorem groupCohomology.twoCoboundariesToTwoCocycles_apply

deleted theorem groupCohomology.twoCoboundaries_ext

deleted theorem groupCohomology.twoCoboundaries_le_twoCocycles

deleted def groupCohomology.twoCochainsIso

deleted theorem groupCohomology.twoCocycles.coe_mk

deleted theorem groupCohomology.twoCocycles.dTwo_apply

deleted theorem groupCohomology.twoCocycles.val_eq_coe

deleted def groupCohomology.twoCocycles

deleted def groupCohomology.twoCocyclesOfIsMulTwoCocycle

deleted def groupCohomology.twoCocyclesOfIsTwoCocycle

deleted theorem groupCohomology.twoCocycles_ext

deleted theorem groupCohomology.twoCocycles_map_one_fst

deleted theorem groupCohomology.twoCocycles_map_one_snd

deleted theorem groupCohomology.twoCocycles_ρ_map_inv_sub_map_inv

deleted def groupCohomology.zeroCochainsIso

deleted def groupCohomology.zeroCocyclesIso

deleted theorem groupCohomology.zeroCocyclesIso_hom_comp_f

deleted theorem groupCohomology.zeroCocyclesIso_inv_comp_iCocycles