Definitions of group actions
This file defines a heirarchy of group action type-classes:
has_scalar α β
mul_action α β
distrib_mul_action α β
The hierarchy is extended further by semimodule
, defined elsewhere.
Also provided are type-classes regarding the interaction of different group actions,
smul_comm_class M N α
is_scalar_tower M N α
Notation
a • b
is used as notation for smul a b
.
Implementation details
This file should avoid depending on other parts of group_theory
, to avoid import cycles.
More sophisticated lemmas belong in group_theory.group_action
.
- smul : α → γ → γ
Typeclass for types with a scalar multiplication operation, denoted •
(\bu
)
Instances
- algebra.to_has_scalar
- mul_action.to_has_scalar
- opposite.has_scalar
- set.has_scalar_set
- set.has_scalar
- pi.has_scalar
- pi.has_scalar'
- matrix.has_scalar
- prod.has_scalar
- sub_mul_action.has_scalar
- submodule.has_scalar
- finsupp.has_scalar
- linear_map.has_scalar
- submodule.quotient.has_scalar
- tensor_product.has_scalar'
- tensor_product.has_scalar
- order_dual.has_scalar
- monoid_algebra.has_scalar
- add_monoid_algebra.has_scalar
- free_algebra.has_scalar
- dfinsupp.has_scalar
- mv_polynomial.has_scalar
- submodule.has_scalar'
- multilinear_map.has_scalar
- alternating_map.has_scalar
- triv_sq_zero_ext.has_scalar
- ulift.has_scalar
- ulift.has_scalar'
- continuous_linear_map.has_scalar
- continuous_has_scalar
- continuous_map_has_scalar
- continuous_has_scalar'
- continuous_map_has_scalar'
- bounded_continuous_function.has_scalar
- bounded_continuous_function.has_scalar'
- continuous_linear_map.has_scalar_extend_scalars
- continuous_multilinear_map.has_scalar
- measure_theory.outer_measure.has_scalar
- measure_theory.measure.has_scalar
- measure_theory.simple_func.has_scalar
- filter.germ.has_scalar
- filter.germ.has_scalar'
- measure_theory.ae_eq_fun.has_scalar
- measure_theory.l1.has_scalar
- holor.has_scalar
- smooth_map_has_scalar
- smooth_map_has_scalar'
- quadratic_form.has_scalar
- pi_tensor_product.has_scalar'
- pi_tensor_product.has_scalar
- nat.arithmetic_function.has_scalar
- to_has_scalar : has_scalar α β
- one_smul : ∀ (b : β), 1 • b = b
- mul_smul : ∀ (x y : α) (b : β), (x * y) • b = x • y • b
Typeclass for multiplicative actions by monoids. This generalizes group actions.
Instances
- distrib_mul_action.to_mul_action
- opposite.mul_action
- set.mul_action_set
- pi.mul_action
- pi.mul_action'
- mul_action.quotient
- mul_action.mul_left_cosets_comp_subtype_val
- sub_mul_action.mul_action
- order_dual.mul_action
- triv_sq_zero_ext.mul_action
- ulift.mul_action
- ulift.mul_action'
- filter.germ.mul_action
- filter.germ.mul_action'
- sylow.rotate_vectors_prod_eq_one.mul_action
A typeclass mixin saying that two actions on the same space commute.
Commutativity of actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.
An instance of is_scalar_tower M N α
states that the multiplicative
action of M
on α
is determined by the multiplicative actions of M
on N
and N
on α
.
Instances
- is_scalar_tower.subsemiring
- is_scalar_tower.subring
- mul_action.is_scalar_tower.left
- add_comm_monoid.nat_is_scalar_tower
- add_comm_group.int_is_scalar_tower
- pi.is_scalar_tower
- pi.is_scalar_tower'
- pi.is_scalar_tower''
- restrict_scalars.is_scalar_tower
- submodule.restricted_module_is_scalar_tower
- linear_map.is_scalar_tower_extend_scalars
- is_scalar_tower.subalgebra
- is_scalar_tower.subalgebra'
- is_scalar_tower.right
- is_scalar_tower.comap
- is_scalar_tower.of_ring_hom
- is_scalar_tower.rat
- ulift.is_scalar_tower
- ulift.is_scalar_tower'
- ulift.is_scalar_tower''
- is_scalar_tower.polynomial
- module.real_complex_tower
- continuous_multilinear_map.is_scalar_tower
- mv_power_series.is_scalar_tower
- power_series.is_scalar_tower
- polynomial.splitting_field_aux.scalar_tower
- polynomial.splitting_field_aux.scalar_tower'
- intermediate_field.is_scalar_tower
- intermediate_field.lift2_tower
- intermediate_field.is_scalar_tower_over_bot
- algebraic_closure.step.scalar_tower
- intermediate_field.fixed_field.is_scalar_tower
- derivation.is_scalar_tower
Pullback a multiplicative action along an injective map respecting •
.
Equations
- function.injective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}
Pushforward a multiplicative action along a surjective map respecting •
.
Equations
- function.surjective.mul_action f hf smul = {to_has_scalar := {smul := has_scalar.smul _inst_3}, one_smul := _, mul_smul := _}
The regular action of a monoid on itself by left multiplication.
Equations
- mul_action.regular α = {to_has_scalar := {smul := λ (a₁ a₂ : α), a₁ * a₂}, one_smul := _, mul_smul := _}
Embedding induced by action.
An action of α
on β
and a monoid homomorphism γ → α
induce an action of γ
on β
.
Equations
- mul_action.comp_hom β g = {to_has_scalar := {smul := λ (x : γ) (b : β), ⇑g x • b}, one_smul := _, mul_smul := _}
- to_mul_action : mul_action α β
- smul_add : ∀ (r : α) (x y : β), r • (x + y) = r • x + r • y
- smul_zero : ∀ (r : α), r • 0 = 0
Typeclass for multiplicative actions on additive structures. This generalizes group modules.
Instances
- semimodule.to_distrib_mul_action
- mul_semiring_action.to_distrib_mul_action
- opposite.distrib_mul_action
- pi.distrib_mul_action
- pi.distrib_mul_action'
- linear_map.distrib_mul_action
- order_dual.distrib_mul_action
- monoid_algebra.distrib_mul_action
- multilinear_map.distrib_mul_action
- alternating_map.distrib_mul_action
- triv_sq_zero_ext.distrib_mul_action
- ulift.distrib_mul_action
- ulift.distrib_mul_action'
- filter.germ.distrib_mul_action
- filter.germ.distrib_mul_action'
Pullback a distributive multiplicative action along an injective additive monoid homomorphism.
Equations
- function.injective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism.
Equations
- function.surjective.distrib_mul_action f hf smul = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Scalar multiplication by r
as an add_monoid_hom
.
Equations
- const_smul_hom β r = {to_fun := has_scalar.smul r, map_zero' := _, map_add' := _}