Commit 2023-06-21 09:25 64f96b7c

View on Github →

feat: port RepresentationTheory.Rep (#5041)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

Modified Mathlib/RepresentationTheory/Action.lean

Created Mathlib/RepresentationTheory/Rep.lean

added theorem Rep.Action_ρ_eq_ρ

added theorem Rep.MonoidalCategory.braiding_hom_apply

added theorem Rep.MonoidalCategory.braiding_inv_apply

added def Rep.MonoidalClosed.linearHomEquiv

added def Rep.MonoidalClosed.linearHomEquivComm

added theorem Rep.MonoidalClosed.linearHomEquivComm_hom

added theorem Rep.MonoidalClosed.linearHomEquivComm_symm_hom

added theorem Rep.MonoidalClosed.linearHomEquiv_hom

added theorem Rep.MonoidalClosed.linearHomEquiv_symm_hom

added theorem Rep.coe_of

added def Rep.counitIso

added def Rep.counitIsoAddEquiv

added def Rep.equivalenceModuleMonoidAlgebra

added def Rep.homEquiv

added theorem Rep.homEquiv_apply_hom

added theorem Rep.homEquiv_def

added theorem Rep.homEquiv_symm_apply_hom

added theorem Rep.hom_comm_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.leftRegularHomEquiv_symm_single

added theorem Rep.leftRegularHom_apply

added theorem Rep.linearization_map_hom

added theorem Rep.linearization_map_hom_single

added theorem Rep.linearization_obj_ρ

added theorem Rep.linearization_of

added theorem Rep.linearization_single

added theorem Rep.linearization_ε_hom

added theorem Rep.linearization_ε_inv_hom_apply

added theorem Rep.linearization_μ_hom

added theorem Rep.linearization_μ_inv_hom

added def Rep.of

added def Rep.ofModuleMonoidAlgebra

added theorem Rep.ofModuleMonoidAlgebra_obj_coe

added theorem Rep.ofModuleMonoidAlgebra_obj_ρ

added theorem Rep.of_ρ

added theorem Rep.of_ρ_apply

added def Rep.toModuleMonoidAlgebra

added def Rep.toModuleMonoidAlgebraMap

added theorem Rep.to_Module_monoidAlgebra_map_aux

added def Rep.trivial

added theorem Rep.trivial_def

added def Rep.unitIso

added def Rep.unitIsoAddEquiv

added theorem Rep.unit_iso_comm

added def Rep.ρ

added theorem Rep.ρ_inv_self_apply

added theorem Rep.ρ_self_inv_apply

added def Representation.repOfTprodIso

added theorem Representation.repOfTprodIso_apply

added theorem Representation.repOfTprodIso_inv_apply