Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-10 03:46 7138d354

View on Github →

feat(category_theory/action): currying (#7085) A functor from an action category can be 'curried' to an ordinary group homomorphism. Also defines transitive group actions.

Estimated changes

Modified src/category_theory/action.lean

added def category_theory.action_category.End_mul_equiv_subgroup

added theorem category_theory.action_category.back_coe

added theorem category_theory.action_category.coe_back

added def category_theory.action_category.curry

added theorem category_theory.action_category.hom_of_pair.val

added def category_theory.action_category.hom_of_pair

modified def category_theory.action_category.stabilizer_iso_End

added def category_theory.action_category.uncurry

Modified src/category_theory/single_obj.lean

added theorem category_theory.single_obj.comp_as_mul

added theorem category_theory.single_obj.id_as_one

added theorem category_theory.single_obj.inv_as_inv

Modified src/group_theory/group_action/basic.lean

added theorem exists_smul_eq

added theorem mul_action.stabilizer_quotient

Modified src/group_theory/group_action/group.lean

added def arrow_action

added def mul_aut_arrow