Commit 2026-03-24 21:13 3c0b81d6

View on Github →

chore(RepresentationTheory): Refactor Rep (#36127) In this PR I've added three more files in a folder "Rep" to replace the old RepresentationTheory.Rep as it's quite a long file. Rep.Basic: Defines Rep in terms of bundled Representations instead of using Action. Rep.Iso: Proves the category equivalence between Rep k G and ModuleCat k k[G]. Rep.Res: Introduces restriction on a representation induced by a group homomorphism, this is upstreamed from ClassFieldTheory project to avoid the use of Action.

Estimated changes

added theorem Finsupp.mapDomain_sub
modified theorem Rep.coind'_ext
deleted theorem Rep.toCoinvariantsMkQ_hom
modified theorem groupCohomology.congr
modified theorem groupCohomology.map₁_one
modified theorem groupHomology.congr
modified theorem groupHomology.map₁_one
modified def groupHomology.H0π
modified def groupHomology.d₁₀
modified theorem Rep.standardComplex.d_eq
modified theorem Rep.standardComplex.d_of
deleted theorem Rep.Action_ρ_eq_ρ
deleted def Rep.applyAsHom
deleted theorem Rep.applyAsHom_comm
deleted theorem Rep.coe_linearization_obj
deleted theorem Rep.coe_of
deleted theorem Rep.coe_res_obj_ρ
deleted def Rep.counitIso
deleted theorem Rep.epi_iff_surjective
deleted def Rep.freeLift
deleted def Rep.freeLiftLEquiv
deleted theorem Rep.free_ext
deleted def Rep.homEquiv
deleted theorem Rep.homEquiv_def
deleted theorem Rep.hom_comm_apply
deleted theorem Rep.ihom_coev_app_hom
deleted theorem Rep.ihom_ev_app_hom
deleted theorem Rep.ihom_obj_ρ_apply
deleted theorem Rep.ihom_obj_ρ_def
deleted def Rep.leftRegularHom
deleted def Rep.linearization
deleted theorem Rep.linearization_map_hom
deleted theorem Rep.linearization_obj_ρ
deleted theorem Rep.linearization_single
deleted theorem Rep.linearization_δ_hom
deleted theorem Rep.linearization_ε_hom
deleted theorem Rep.linearization_μ_hom
deleted def Rep.mkQ
deleted theorem Rep.mono_iff_injective
deleted def Rep.norm
deleted def Rep.normNatTrans
deleted theorem Rep.norm_comm
deleted def Rep.ofAlgebraAut
deleted theorem Rep.ofHom_ρ
deleted theorem Rep.of_ρ
deleted theorem Rep.res_obj_ρ
deleted def Rep.subtype
deleted theorem Rep.tensor_ρ
deleted def Rep.toAdditive
deleted def Rep.trivialFunctor
deleted theorem Rep.trivial_def
deleted def Rep.unitIso
deleted def Rep.unitIsoAddEquiv
deleted theorem Rep.unit_iso_comm
deleted def Rep.ρ
deleted theorem Rep.ρ_hom
added def Rep.ActionToRep
added structure Rep.Hom
added def Rep.RepToAction
added theorem Rep.RepToAction_obj
added theorem Rep.add_comp
added theorem Rep.add_hom
added def Rep.applyAsHom
added theorem Rep.applyAsHom_apply
added theorem Rep.applyAsHom_comm
added theorem Rep.comp_add
added theorem Rep.comp_apply
added theorem Rep.comp_smul
added theorem Rep.epi_iff_surjective
added theorem Rep.finsupp_V
added theorem Rep.forget_map
added theorem Rep.forget_obj
added theorem Rep.free_ext
added def Rep.homEquiv
added theorem Rep.homEquiv_def
added theorem Rep.hom_bijective
added theorem Rep.hom_braiding
added theorem Rep.hom_comm_apply
added theorem Rep.hom_comp
added theorem Rep.hom_ext
added theorem Rep.hom_hom_associator
added theorem Rep.hom_hom_leftUnitor
added theorem Rep.hom_id
added theorem Rep.hom_injective
added theorem Rep.hom_inv_apply
added theorem Rep.hom_inv_associator
added theorem Rep.hom_inv_leftUnitor
added theorem Rep.hom_ofHom
added theorem Rep.hom_surjective
added theorem Rep.hom_tensorHom
added theorem Rep.hom_whiskerLeft
added theorem Rep.hom_whiskerRight
added theorem Rep.id_apply
added theorem Rep.ihom_coev_app_hom
added theorem Rep.ihom_ev_app_hom
added theorem Rep.ihom_obj_ρ_apply
added theorem Rep.ihom_obj_ρ_def
added theorem Rep.inv_hom_apply
added def Rep.mkIso
added theorem Rep.mkIso_hom_hom
added def Rep.mkQ
added theorem Rep.mono_iff_injective
added theorem Rep.neg_hom
added def Rep.norm
added def Rep.normNatTrans
added theorem Rep.norm_apply
added theorem Rep.norm_comm
added theorem Rep.nsmul_hom
added def Rep.ofAlgebraAut
added theorem Rep.ofHom_add
added theorem Rep.ofHom_apply
added theorem Rep.ofHom_comp
added theorem Rep.ofHom_hom
added theorem Rep.ofHom_id
added theorem Rep.ofHom_neg
added theorem Rep.ofHom_nsmul
added theorem Rep.ofHom_smul
added theorem Rep.ofHom_sub
added theorem Rep.ofHom_sum
added theorem Rep.ofHom_zero
added theorem Rep.ofHom_zsmul
added theorem Rep.of_V
added theorem Rep.of_tensor
added theorem Rep.of_ρ
added def Rep.repIsoAction
added theorem Rep.smul_comp
added theorem Rep.smul_hom
added theorem Rep.sub_hom
added def Rep.subtype
added theorem Rep.sum_hom
added theorem Rep.tensorUnit_V
added theorem Rep.tensorUnit_ρ
added theorem Rep.tensor_V
added theorem Rep.tensor_ρ
added def Rep.toAdditive
added theorem Rep.trivial_V
added theorem Rep.trivial_ρ
added theorem Rep.trivial_ρ_apply
added theorem Rep.zero_hom
added theorem Rep.zsmul_hom
added theorem Rep.δ_def
added theorem Rep.δ_hom
added theorem Rep.ε_def
added theorem Rep.ε_hom
added theorem Rep.η_def
added theorem Rep.η_hom
added theorem Rep.μ_def
added theorem Rep.μ_hom
added theorem Rep.ρ_mul
added structure Rep
added def Rep.counitIso
added def Rep.unitIso
added theorem Rep.unit_iso_comm
added theorem Rep.coe_res_obj_ρ'
added theorem Rep.full_res
added theorem Rep.res_obj_V
added theorem Rep.res_obj_ρ