Commit 2023-06-06 18:52 ae871a75

View on Github →

feat: port RepresentationTheory.Action (#4700)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

added theorem MonCat.mul_of

added theorem MonCat.oneHom_apply

added theorem MonCat.one_of

Modified Mathlib/CategoryTheory/Conj.lean

modified theorem CategoryTheory.Iso.conjAut_apply

Modified Mathlib/CategoryTheory/Endomorphism.lean

added theorem CategoryTheory.Aut.ext

Created Mathlib/RepresentationTheory/Action.lean

added def Action.FunctorCategoryEquivalence.counitIso

added def Action.FunctorCategoryEquivalence.functor

added def Action.FunctorCategoryEquivalence.inverse

added def Action.FunctorCategoryEquivalence.unitIso

added def Action.Hom.comp

added def Action.Hom.id

added structure Action.Hom

added theorem Action.Iso.conj_ρ

added def Action.abelianAux

added def Action.actionPunitEquivalence

added theorem Action.add_hom

added theorem Action.associator_hom_hom

added theorem Action.associator_inv_hom

added theorem Action.comp_hom

added def Action.diagonal

added def Action.diagonalOneIsoLeftRegular

added def Action.forget

added def Action.forgetBraided

added def Action.forgetMonoidal

added def Action.functorCategoryEquivalence

added def Action.functorCategoryEquivalenceCompEvaluation

added theorem Action.functorCategoryMonoidalEquivalence.counit_app

added theorem Action.functorCategoryMonoidalEquivalence.functor_map

added theorem Action.functorCategoryMonoidalEquivalence.inv_counit_app_hom

added theorem Action.functorCategoryMonoidalEquivalence.inv_unit_app_app

added theorem Action.functorCategoryMonoidalEquivalence.inverse_map

added theorem Action.functorCategoryMonoidalEquivalence.unit_app_hom

added theorem Action.functorCategoryMonoidalEquivalence.ε_app

added theorem Action.functorCategoryMonoidalEquivalence.μIso_inv_app

added theorem Action.functorCategoryMonoidalEquivalence.μ_app

added def Action.functorCategoryMonoidalEquivalence

added theorem Action.hom_ext

added theorem Action.id_hom

added theorem Action.leftDual_v

added theorem Action.leftDual_ρ

added def Action.leftRegular

added theorem Action.leftUnitor_hom_hom

added theorem Action.leftUnitor_inv_hom

added def Action.mkIso

added theorem Action.neg_hom

added def Action.ofMulAction

added def Action.ofMulActionLimitCone

added theorem Action.ofMulAction_apply

added def Action.res

added def Action.resComp

added def Action.resId

added theorem Action.rightDual_v

added theorem Action.rightDual_ρ

added theorem Action.rightUnitor_hom_hom

added theorem Action.rightUnitor_inv_hom

added theorem Action.smul_hom

added theorem Action.sum_hom

added theorem Action.tensorHom

added def Action.tensorUnitIso

added theorem Action.tensorUnit_rho

added theorem Action.tensorUnit_v

added theorem Action.tensor_rho

added theorem Action.tensor_v

added def Action.trivial

added theorem Action.zero_hom

added def Action.ρAut

added theorem Action.ρ_one

added structure Action

added def CategoryTheory.Functor.mapAction

added def CategoryTheory.MonoidalFunctor.mapAction

added theorem CategoryTheory.MonoidalFunctor.mapAction_ε_inv_hom

added theorem CategoryTheory.MonoidalFunctor.mapAction_μ_inv_hom