Commit 2022-07-24 23:44 5ed2c728

View on Github →

feat(representation_theory/Rep): Rep k G ≌ Module (monoid_algebra k G) (#13713)

Estimated changes

Modified src/algebra/algebra/restrict_scalars.lean

modified def restrict_scalars.add_equiv

modified theorem restrict_scalars.add_equiv_map_smul

added theorem restrict_scalars.add_equiv_symm_map_algebra_map_smul

added theorem restrict_scalars.add_equiv_symm_map_smul_smul

added theorem restrict_scalars.lsmul_apply_apply

Modified src/algebra/module/linear_map.lean

Modified src/representation_theory/Rep.lean

added theorem Rep.coe_of

added def Rep.counit_iso

added def Rep.counit_iso_add_equiv

added def Rep.equivalence_Module_monoid_algebra

added def Rep.of_Module_monoid_algebra

added theorem Rep.of_Module_monoid_algebra_obj_coe

added theorem Rep.of_Module_monoid_algebra_obj_ρ

added theorem Rep.of_ρ

added def Rep.to_Module_monoid_algebra

added def Rep.to_Module_monoid_algebra_map

added theorem Rep.to_Module_monoid_algebra_map_aux

added def Rep.unit_iso

added def Rep.unit_iso_add_equiv

added theorem Rep.unit_iso_comm

added def Rep.ρ

Modified src/representation_theory/basic.lean

modified theorem representation.as_algebra_hom_def

modified theorem representation.as_algebra_hom_of

modified theorem representation.as_algebra_hom_single

added theorem representation.as_algebra_hom_single_one

added def representation.as_module

added def representation.as_module_equiv

added theorem representation.as_module_equiv_map_smul

added theorem representation.as_module_equiv_symm_map_rho

added theorem representation.as_module_equiv_symm_map_smul

added def representation.of_module'

added def representation.of_module

added theorem representation.of_module_as_algebra_hom_apply_apply

added theorem representation.of_module_as_module_act

added theorem representation.smul_of_module_as_module

Modified src/representation_theory/invariants.lean