Definitions of group actions #
This file defines a hierarchy of group action type-classes on top of the previously defined
notation classes has_smul
and its additive version has_vadd
:
mul_action M α
and its additive versionadd_action G P
are typeclasses used for actions of multiplicative and additive monoids and groups; they extend notation classeshas_smul
andhas_vadd
that are defined inalgebra.group.defs
;distrib_mul_action M A
is a typeclass for an action of a multiplicative monoid on an additive monoid such thata • (b + c) = a • b + a • c
anda • 0 = 0
.
The hierarchy is extended further by module
, defined elsewhere.
Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,
smul_comm_class M N α
and its additive versionvadd_comm_class M N α
;is_scalar_tower M N α
(no additive version).is_central_scalar M α
(no additive version).
Notation #
a • b
is used as notation forhas_smul.smul a b
.a +ᵥ b
is used as notation forhas_vadd.vadd 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
.
Tags #
group action
Faithful actions #
Typeclass for faithful actions.
Instances of this typeclass
- add_units.has_faithful_vadd
- add_left_cancel_monoid.to_has_faithful_opposite_scalar
- prod.has_faithful_vadd_left
- prod.has_faithful_vadd_right
- add_right_cancel_monoid.to_has_faithful_vadd
- pi.has_faithful_vadd
- option.has_faithful_vadd
- sigma.has_faithful_vadd
- sum.has_faithful_vadd_left
- sum.has_faithful_vadd_right
Typeclass for faithful actions.
Instances of this typeclass
- function.End.apply_has_faithful_smul
- add_monoid.End.apply_has_faithful_smul
- units.has_faithful_smul
- left_cancel_monoid.to_has_faithful_opposite_scalar
- cancel_monoid_with_zero.to_has_faithful_opposite_scalar
- prod.has_faithful_smul_left
- prod.has_faithful_smul_right
- mul_aut.apply_has_faithful_smul
- add_aut.apply_has_faithful_smul
- right_cancel_monoid.to_has_faithful_smul
- equiv.perm.apply_has_faithful_smul
- cancel_monoid_with_zero.to_has_faithful_smul
- ring_hom.apply_has_faithful_smul
- submonoid.has_faithful_smul
- subgroup.has_faithful_smul
- subsemiring.has_faithful_smul
- subring.has_faithful_smul
- pi.has_faithful_smul
- linear_map.apply_has_faithful_smul
- linear_equiv.apply_has_faithful_smul
- finsupp.has_faithful_smul
- alg_equiv.apply_has_faithful_smul
- monoid_algebra.has_faithful_smul
- add_monoid_algebra.has_faithful_smul
- polynomial.has_faithful_smul
- subalgebra.has_faithful_smul
- mv_polynomial.has_faithful_smul
- continuous_linear_map.apply_has_faithful_smul
- option.has_faithful_smul
- sigma.has_faithful_smul
- sum.has_faithful_smul_left
- sum.has_faithful_smul_right
See also monoid.to_mul_action
and mul_zero_class.to_smul_with_zero
.
Equations
- has_mul.to_has_smul α = {smul := has_mul.mul _inst_1}
See also add_monoid.to_add_action
Equations
- has_add.to_has_vadd α = {vadd := has_add.add _inst_1}
- to_has_vadd : has_vadd G P
- zero_vadd : ∀ (p : P), 0 +ᵥ p = p
- add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Type class for additive monoid actions.
Instances of this typeclass
- add_torsor.to_add_action
- add_monoid.to_add_action
- add_action.function_End
- additive.add_action
- add_units.add_action
- add_opposite.add_action
- add_monoid.to_opposite_add_action
- prod.add_action
- add_submonoid.add_action
- add_subgroup.add_action
- pi.add_action
- pi.add_action'
- ulift.add_action
- ulift.add_action'
- add_action.orbit.add_action
- add_action.quotient
- add_action.add_left_cosets_comp_subtype_val
- uniform_space.completion.add_action
- add_subgroup.left_transversals.add_action
- function.embedding.add_action
- sigma.add_action
- sum.add_action
Instances of other typeclasses for add_action
- add_action.has_sizeof_inst
- to_has_smul : has_smul α β
- 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 of this typeclass
- distrib_mul_action.to_mul_action
- mul_distrib_mul_action.to_mul_action
- mul_action_with_zero.to_mul_action
- monoid.to_mul_action
- function.End.apply_mul_action
- multiplicative.mul_action
- units.mul_action
- units.mul_action'
- mul_opposite.mul_action
- monoid.to_opposite_mul_action
- prod.mul_action
- equiv.perm.apply_mul_action
- submonoid.mul_action
- subgroup.mul_action
- subsemiring.mul_action
- subring.mul_action
- pi.mul_action
- pi.mul_action'
- ulift.mul_action
- ulift.mul_action'
- mul_action.orbit.mul_action
- sub_mul_action.mul_action'
- sub_mul_action.mul_action
- punit.mul_action
- submodule.quotient.mul_action'
- submodule.quotient.mul_action
- subalgebra.mul_action
- localization.mul_action
- self_adjoint.mul_action
- matrix.mul_action
- category_theory.End.mul_action_right
- category_theory.End.mul_action_left
- mul_action.quotient
- mul_action.mul_left_cosets_comp_subtype_val
- unitization.mul_action
- conj_act.mul_action₀
- graded_monoid.grade_zero.mul_action
- triv_sq_zero_ext.mul_action
- order_dual.mul_action
- nnreal.mul_action
- ennreal.mul_action
- uniform_space.completion.mul_action
- complex.mul_action
- continuous_linear_map.mul_action
- affine_map.mul_action
- ray_vector.mul_action
- module.ray.mul_action
- continuous_map.mul_action
- continuous_multilinear_map.mul_action
- measure_theory.outer_measure.mul_action
- measure_theory.measure.mul_action
- bounded_continuous_function.mul_action
- filter.germ.mul_action
- filter.germ.mul_action'
- measure_theory.ae_eq_fun.mul_action
- continuous_affine_map.mul_action
- weak_dual.mul_action
- upper_half_plane.mul_action
- upper_half_plane.SL_action
- seminorm.mul_action
- mul_action_closed_ball_ball
- mul_action_closed_ball_closed_ball
- mul_action_sphere_ball
- mul_action_sphere_closed_ball
- mul_action_sphere_sphere
- nnrat.mul_action
- polynomial.gal.gal_action_aux
- polynomial.gal.gal_action
- subgroup.left_transversals.mul_action
- free_product.word.summand_action
- free_product.word.mul_action
- function.embedding.mul_action
- option.mul_action
- sigma.mul_action
- sum.mul_action
- sylow.mul_action_left
- sylow.pointwise_mul_action
- sylow.mul_action
- subgroup.quotient_diff.mul_action
- locally_constant.mul_action
Instances of other typeclasses for mul_action
- mul_action.has_sizeof_inst
(Pre)transitive action #
M
acts pretransitively on α
if for any x y
there is g
such that g • x = y
(or g +ᵥ x = y
for an additive action). A transitive action should furthermore have α
nonempty.
In this section we define typeclasses mul_action.is_pretransitive
and
add_action.is_pretransitive
and provide mul_action.exists_smul_eq
/add_action.exists_vadd_eq
,
mul_action.surjective_smul
/add_action.surjective_vadd
as public interface to access this
property. We do not provide typeclasses *_action.is_transitive
; users should assume
[mul_action.is_pretransitive M α] [nonempty α]
instead.
M
acts pretransitively on α
if for any x y
there is g
such that g +ᵥ x = y
.
A transitive action should furthermore have α
nonempty.
M
acts pretransitively on α
if for any x y
there is g
such that g • x = y
.
A transitive action should furthermore have α
nonempty.
The regular action of a group on itself is transitive.
The regular action of a group on itself is transitive.
Scalar tower and commuting actions #
A typeclass mixin saying that two additive actions on the same space commute.
Instances of this typeclass
- vadd_comm_class_self
- additive.vadd_comm_class
- add_opposite.vadd_comm_class
- add_semigroup.opposite_vadd_comm_class
- add_semigroup.opposite_vadd_comm_class'
- vadd_comm_class.opposite_mid
- prod.vadd_comm_class
- prod.vadd_comm_class_both
- set.vadd_comm_class_set
- set.vadd_comm_class_set'
- set.vadd_comm_class_set''
- set.vadd_comm_class
- add_submonoid.vadd_comm_class_left
- add_submonoid.vadd_comm_class_right
- add_subgroup.vadd_comm_class_left
- add_subgroup.vadd_comm_class_right
- pi.vadd_comm_class
- pi.vadd_comm_class'
- pi.vadd_comm_class''
- function.vadd_comm_class
- finset.vadd_comm_class_finset
- finset.vadd_comm_class_finset'
- finset.vadd_comm_class_finset''
- finset.vadd_comm_class
- filter.vadd_comm_class_filter
- filter.vadd_comm_class_filter'
- filter.vadd_comm_class_filter''
- filter.vadd_comm_class
- continuous_map.vadd_comm_class
- function.embedding.vadd_comm_class
- option.vadd_comm_class
- sigma.vadd_comm_class
- sum.vadd_comm_class
A typeclass mixin saying that two multiplicative actions on the same space commute.
Instances of this typeclass
- smul_comm_class.op_left
- smul_comm_class.op_right
- is_scalar_tower.to_smul_comm_class
- is_scalar_tower.to_smul_comm_class'
- category_theory.Module.smul_comm_class_mk
- smul_comm_class_self
- add_monoid.nat_smul_comm_class
- add_monoid.nat_smul_comm_class'
- add_group.int_smul_comm_class
- add_group.int_smul_comm_class'
- multiplicative.smul_comm_class
- units.smul_comm_class_left
- units.smul_comm_class_right
- units.smul_comm_class'
- non_unital_non_assoc_semiring.nat_smul_comm_class
- non_unital_non_assoc_ring.int_smul_comm_class
- mul_opposite.smul_comm_class
- semigroup.opposite_smul_comm_class
- semigroup.opposite_smul_comm_class'
- smul_comm_class.opposite_mid
- prod.smul_comm_class
- prod.smul_comm_class_both
- smul_comm_class.rat
- smul_comm_class.rat'
- set.smul_comm_class_set
- set.smul_comm_class_set'
- set.smul_comm_class_set''
- set.smul_comm_class
- submonoid.smul_comm_class_left
- submonoid.smul_comm_class_right
- submonoid.center.smul_comm_class_left
- submonoid.center.smul_comm_class_right
- subgroup.smul_comm_class_left
- subgroup.smul_comm_class_right
- subgroup.center.smul_comm_class_left
- subgroup.center.smul_comm_class_right
- subsemiring.smul_comm_class_left
- subsemiring.smul_comm_class_right
- subsemiring.center.smul_comm_class_left
- subsemiring.center.smul_comm_class_right
- subring.smul_comm_class_left
- subring.smul_comm_class_right
- subring.center.smul_comm_class_left
- subring.center.smul_comm_class_right
- pi.smul_comm_class
- pi.smul_comm_class'
- pi.smul_comm_class''
- function.smul_comm_class
- linear_map.smul_comm_class
- module.End.smul_comm_class
- module.End.smul_comm_class'
- linear_map.apply_smul_comm_class
- linear_map.apply_smul_comm_class'
- linear_equiv.apply_smul_comm_class
- linear_equiv.apply_smul_comm_class'
- add_monoid_hom.smul_comm_class
- punit.smul_comm_class
- dfinsupp.smul_comm_class
- finsupp.smul_comm_class
- alg_equiv.apply_smul_comm_class
- alg_equiv.apply_smul_comm_class'
- linear_pmap.smul_comm_class
- submodule.quotient.smul_comm_class
- monoid_algebra.smul_comm_class
- monoid_algebra.smul_comm_class_self
- monoid_algebra.smul_comm_class_symm_self
- add_monoid_algebra.smul_comm_class
- add_monoid_algebra.smul_comm_class_self
- add_monoid_algebra.smul_comm_class_symm_self
- polynomial.smul_comm_class
- finset.smul_comm_class_finset
- finset.smul_comm_class_finset'
- finset.smul_comm_class_finset''
- finset.smul_comm_class
- subalgebra.smul_comm_class_left
- subalgebra.smul_comm_class_right
- mv_polynomial.smul_comm_class
- localization.smul_comm_class
- localization.smul_comm_class_right
- matrix.smul_comm_class
- matrix.semiring.smul_comm_class
- direct_sum.smul_comm_class
- adjoin_root.smul_comm_class
- unitization.smul_comm_class
- conj_act.units_smul_comm_class
- conj_act.units_smul_comm_class'
- conj_act.smul_comm_class₀
- conj_act.smul_comm_class₀'
- conj_act.smul_comm_class
- conj_act.smul_comm_class'
- filter.smul_comm_class_filter
- filter.smul_comm_class_filter'
- filter.smul_comm_class_filter''
- filter.smul_comm_class
- triv_sq_zero_ext.smul_comm_class
- fixed_points.smul_comm_class
- fixed_points.smul_comm_class'
- nnreal.smul_comm_class_left
- nnreal.smul_comm_class_right
- ennreal.smul_comm_class_left
- ennreal.smul_comm_class_right
- uniform_space.completion.smul_comm_class
- complex.smul_comm_class
- continuous_linear_map.smul_comm_class
- continuous_linear_map.apply_smul_comm_class
- continuous_linear_map.apply_smul_comm_class'
- normed_add_group_hom.smul_comm_class
- hahn_series.smul_comm_class
- continuous_map.smul_comm_class
- lie_algebra.smul_comm_class
- submodule.torsion'.smul_comm_class
- continuous_multilinear_map.smul_comm_class
- measure_theory.outer_measure.smul_comm_class
- measure_theory.measure.smul_comm_class
- measure_theory.ae_eq_fun.smul_comm_class
- lp.infty_smul_comm_class
- smul_comm_class_closed_ball_closed_ball_closed_ball
- smul_comm_class_closed_ball_closed_ball_ball
- smul_comm_class_sphere_closed_ball_closed_ball
- smul_comm_class_sphere_closed_ball_ball
- smul_comm_class_sphere_ball_ball
- smul_comm_class_sphere_sphere_closed_ball
- smul_comm_class_sphere_sphere_ball
- smul_comm_class_sphere_sphere_sphere
- function.embedding.smul_comm_class
- option.smul_comm_class
- sigma.smul_comm_class
- sum.smul_comm_class
- pi_tensor_product.smul_comm_class'
- pi_tensor_product.smul_comm_class
- zero_at_infty_continuous_map.smul_comm_class
Frequently, we find ourselves wanting to express a bilinear map M →ₗ[R] N →ₗ[R] P
or an
equivalence between maps (M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N')
where the maps have an associated ring
R
. Unfortunately, using definitions like these requires that R
satisfy comm_semiring R
, and
not just semiring R
. Using M →ₗ[R] N →+ P
and (M →ₗ[R] N) ≃+ (M' →ₗ[R] N')
avoids this
problem, but throws away structure that is useful for when we do have a commutative (semi)ring.
To avoid making this compromise, we instead state these definitions as M →ₗ[R] N →ₗ[S] P
or
(M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N')
and require smul_comm_class S R
on the appropriate modules. When
the caller has comm_semiring R
, they can set S = R
and smul_comm_class_self
will populate the
instance. If the caller only has semiring R
they can still set either R = ℕ
or S = ℕ
, and
add_comm_monoid.nat_smul_comm_class
or add_comm_monoid.nat_smul_comm_class'
will populate
the typeclass, which is still sufficient to recover a ≃+
or →+
structure.
An example of where this is used is linear_map.prod_equiv
.
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.
Commutativity of additive 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 vadd_assoc_class M N α
states that the additive action of M
on α
is
determined by the additive actions of M
on N
and N
on α
.
Instances of this typeclass
- add_semigroup.vadd_assoc_class
- vadd_assoc_class.left
- add_opposite.vadd_assoc_class
- vadd_assoc_class.opposite_mid
- set.vadd_assoc_class
- set.vadd_assoc_class'
- set.vadd_assoc_class''
- finset.vadd_assoc_class
- finset.vadd_assoc_class'
- finset.vadd_assoc_class''
- filter.vadd_assoc_class
- filter.vadd_assoc_class'
- filter.vadd_assoc_class''
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 of this typeclass
- is_scalar_tower.op_left
- is_scalar_tower.op_right
- real.is_scalar_tower
- is_scalar_tower.subsemiring
- semigroup.is_scalar_tower
- is_scalar_tower.left
- units.is_scalar_tower
- units.is_scalar_tower'
- units.is_scalar_tower'_left
- non_unital_non_assoc_semiring.nat_is_scalar_tower
- non_unital_non_assoc_ring.int_is_scalar_tower
- mul_opposite.is_scalar_tower
- is_scalar_tower.opposite_mid
- prod.is_scalar_tower
- prod.is_scalar_tower_both
- add_comm_monoid.nat_is_scalar_tower
- add_comm_group.int_is_scalar_tower
- is_scalar_tower.rat
- set.is_scalar_tower
- set.is_scalar_tower'
- set.is_scalar_tower''
- submonoid.is_scalar_tower
- subgroup.is_scalar_tower
- subsemiring.is_scalar_tower
- subring.is_scalar_tower
- pi.is_scalar_tower
- pi.is_scalar_tower'
- pi.is_scalar_tower''
- linear_map.is_scalar_tower
- module.End.is_scalar_tower
- linear_map.apply_is_scalar_tower
- ulift.is_scalar_tower
- ulift.is_scalar_tower'
- ulift.is_scalar_tower''
- add_monoid_hom.is_scalar_tower
- sub_mul_action.is_scalar_tower
- submodule.is_scalar_tower
- submodule.restrict_scalars.is_scalar_tower
- punit.is_scalar_tower
- dfinsupp.is_scalar_tower
- finsupp.is_scalar_tower
- is_scalar_tower.right
- linear_pmap.is_scalar_tower
- submodule.quotient.is_scalar_tower
- tensor_product.is_scalar_tower_left
- tensor_product.is_scalar_tower_right
- tensor_product.is_scalar_tower
- monoid_algebra.is_scalar_tower
- monoid_algebra.is_scalar_tower_self
- add_monoid_algebra.is_scalar_tower
- add_monoid_algebra.is_scalar_tower_self
- polynomial.is_scalar_tower
- finset.is_scalar_tower
- finset.is_scalar_tower'
- finset.is_scalar_tower''
- ideal.quotient.is_scalar_tower
- subalgebra.is_scalar_tower
- subalgebra.is_scalar_tower_left
- subalgebra.is_scalar_tower_mid
- is_scalar_tower.subalgebra
- is_scalar_tower.subalgebra'
- is_scalar_tower.of_ring_hom
- mv_polynomial.is_scalar_tower
- mv_polynomial.is_scalar_tower'
- localization.is_scalar_tower
- localization.is_scalar_tower_right
- fraction_ring.is_scalar_tower
- restrict_scalars.is_scalar_tower
- matrix.is_scalar_tower
- matrix.semiring.is_scalar_tower
- direct_sum.is_scalar_tower
- algebra.tensor_product.tensor_product.is_scalar_tower
- intermediate_field.is_scalar_tower
- intermediate_field.is_scalar_tower_bot
- intermediate_field.is_scalar_tower_mid
- intermediate_field.is_scalar_tower_mid'
- adjoin_root.is_scalar_tower
- polynomial.splitting_field_aux.is_scalar_tower
- polynomial.splitting_field_aux.scalar_tower'
- polynomial.splitting_field_aux.scalar_tower
- unitization.is_scalar_tower
- filter.is_scalar_tower
- filter.is_scalar_tower'
- filter.is_scalar_tower''
- triv_sq_zero_ext.is_scalar_tower
- intermediate_field.is_scalar_tower_over_bot
- algebraic_closure.step.scalar_tower
- algebraic_closure.is_scalar_tower
- intermediate_field.fixed_field.is_scalar_tower
- nnreal.is_scalar_tower
- ennreal.is_scalar_tower
- uniform_space.completion.is_scalar_tower
- complex.is_scalar_tower
- module.real_complex_tower
- add_group_seminorm.is_scalar_tower
- group_seminorm.is_scalar_tower
- continuous_linear_map.is_scalar_tower
- normed_add_group_hom.is_scalar_tower
- mv_power_series.is_scalar_tower
- power_series.is_scalar_tower
- hahn_series.is_scalar_tower
- ratfunc.is_scalar_tower
- ratfunc.laurent_series.is_scalar_tower
- ideal.quotient.tower_quotient_map_quotient
- continuous_map.is_scalar_tower
- is_localization.localization.at_prime.is_scalar_tower
- algebraic_geometry.function_field_is_scalar_tower
- lie_subalgebra.is_scalar_tower
- lie_algebra.is_scalar_tower
- module.is_torsion_by_set.is_scalar_tower
- submodule.torsion_by_set.is_scalar_tower
- submodule.torsion_by.is_scalar_tower
- continuous_multilinear_map.is_scalar_tower
- measure_theory.outer_measure.is_scalar_tower
- measure_theory.measure.is_scalar_tower
- measure_theory.ae_eq_fun.is_scalar_tower
- weak_bilin.is_scalar_tower
- upper_half_plane.SL_to_GL_tower
- upper_half_plane.subgroup_on_GL_pos
- upper_half_plane.subgroup_to_SL_tower
- seminorm.is_scalar_tower
- lp.is_scalar_tower
- lp.infty_is_scalar_tower
- ideal.cotangent.is_scalar_tower
- local_ring.cotangent_space.is_scalar_tower
- derivation.is_scalar_tower
- kaehler_differential.is_scalar_tower
- kaehler_differential.is_scalar_tower'
- is_scalar_tower_closed_ball_closed_ball_closed_ball
- is_scalar_tower_closed_ball_closed_ball_ball
- is_scalar_tower_sphere_closed_ball_closed_ball
- is_scalar_tower_sphere_closed_ball_ball
- is_scalar_tower_sphere_sphere_closed_ball
- is_scalar_tower_sphere_sphere_ball
- is_scalar_tower_sphere_sphere_sphere
- is_scalar_tower_sphere_ball_ball
- is_scalar_tower_closed_ball_ball_ball
- laurent_polynomial.is_scalar_tower
- polynomial_module.is_scalar_tower
- polynomial_module.is_scalar_tower'
- polynomial.gal.is_scalar_tower
- smooth_functions_tower
- pointed_smooth_map.cont_mdiff_map.is_scalar_tower
- pointed_smooth_map.is_scalar_tower
- function.embedding.is_scalar_tower
- option.is_scalar_tower
- sigma.is_scalar_tower
- sum.is_scalar_tower
- pi_tensor_product.is_scalar_tower'
- pi_tensor_product.is_scalar_tower
- cyclotomic_ring.cyclotomic_field.is_scalar_tower
- ideal.factors.is_scalar_tower
- valuation_subring.of_prime_scalar_tower
- zero_at_infty_continuous_map.is_scalar_tower
- op_smul_eq_smul : ∀ (m : M) (a : α), mul_opposite.op m • a = m • a
A typeclass indicating that the right (aka mul_opposite
) and left actions by M
on α
are
equal, that is that M
acts centrally on α
. This can be thought of as a version of commutativity
for •
.
Instances of this typeclass
- mul_opposite.is_central_scalar
- comm_semigroup.is_central_scalar
- prod.is_central_scalar
- set.is_central_scalar
- submonoid.pointwise_central_scalar
- add_submonoid.pointwise_central_scalar
- pi.is_central_scalar
- linear_map.is_central_scalar
- ulift.is_central_scalar
- add_monoid_hom.is_central_scalar
- sub_mul_action.is_central_scalar
- submodule.is_central_scalar
- punit.is_central_scalar
- dfinsupp.is_central_scalar
- finsupp.is_central_scalar
- submodule.quotient.is_central_scalar
- tensor_product.is_central_scalar
- monoid_algebra.is_central_scalar
- add_monoid_algebra.is_central_scalar
- polynomial.is_central_scalar
- subgroup.pointwise_central_scalar
- add_subgroup.pointwise_central_scalar
- submodule.pointwise_central_scalar
- finset.is_central_scalar
- mv_polynomial.is_central_scalar
- localization.is_central_scalar
- restrict_scalars.is_central_scalar
- matrix.is_central_scalar
- alternating_map.is_central_scalar
- direct_sum.is_central_scalar
- subsemiring.pointwise_central_scalar
- subring.pointwise_central_scalar
- unitization.is_central_scalar
- filter.is_central_scalar
- triv_sq_zero_ext.is_central_scalar
- uniform_space.completion.is_central_scalar
- complex.is_central_scalar
- continuous_linear_map.is_central_scalar
- affine_map.is_central_scalar
- normed_add_group_hom.is_central_scalar
- continuous_map.is_central_scalar
- lie_subalgebra.is_central_scalar
- lie_submodule.is_central_scalar
- free_lie_algebra.is_central_scalar
- lie_submodule.quotient.is_central_scalar
- continuous_multilinear_map.is_central_scalar
- measure_theory.outer_measure.is_central_scalar
- measure_theory.measure.is_central_scalar
- bounded_continuous_function.is_central_scalar
- measure_theory.ae_eq_fun.is_central_scalar
- continuous_affine_map.is_central_scalar
- derivation.is_central_scalar
- function.embedding.is_central_scalar
- option.is_central_scalar
- sigma.is_central_scalar
- sum.is_central_scalar
- valuation_subring.pointwise_central_scalar
- zero_at_infty_continuous_map.is_central_scalar
Auxiliary definition for has_smul.comp
, mul_action.comp_hom
,
distrib_mul_action.comp_hom
, module.comp_hom
, etc.
Equations
- has_smul.comp.smul g n a = g n • a
Auxiliary definition for has_vadd.comp
, add_action.comp_hom
, etc.
Equations
- has_vadd.comp.vadd g n a = g n +ᵥ a
An action of M
on α
and a function N → M
induces an action of N
on α
.
See note [reducible non-instances]. Since this is reducible, we make sure to go via
has_smul.comp.smul
to prevent typeclass inference unfolding too far.
Equations
- has_smul.comp α g = {smul := has_smul.comp.smul g}
An additive action of M
on α
and a function N → M
induces
an additive action of N
on α
Equations
- has_vadd.comp α g = {vadd := has_vadd.comp.vadd g}
Given a tower of scalar actions M → α → β
, if we use has_smul.comp
to pull back both of M
's actions by a map g : N → M
, then we obtain a new
tower of scalar actions N → α → β
.
This cannot be an instance because it can cause infinite loops whenever the has_smul
arguments
are still metavariables.
Given a tower of additive actions M → α → β
, if we use
has_smul.comp
to pull back both of M
's actions by a map g : N → M
, then we obtain a new tower
of scalar actions N → α → β
.
This cannot be an instance because it can cause infinite loops whenever the has_smul
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the has_smul
arguments
are still metavariables.
This cannot be an instance because it can cause infinite loops whenever the has_smul
arguments
are still metavariables.
Note that the smul_comm_class α β β
typeclass argument is usually satisfied by algebra α β
.
Note that the is_scalar_tower α β β
typeclass argument is usually satisfied by algebra α β
.
has_smul
version of one_mul_eq_id
has_vadd
version of zero_add_eq_id
has_smul
version of comp_mul_left
has_vadd
version of comp_add_left
Pullback a multiplicative action along an injective map respecting •
.
See note [reducible non-instances].
Equations
- function.injective.mul_action f hf smul = {to_has_smul := {smul := has_smul.smul _inst_3}, one_smul := _, mul_smul := _}
Pullback an additive action along an injective map respecting +ᵥ
.
Equations
- function.injective.add_action f hf smul = {to_has_vadd := {vadd := has_vadd.vadd _inst_3}, zero_vadd := _, add_vadd := _}
Pushforward an additive action along a surjective map respecting +ᵥ
.
Equations
- function.surjective.add_action f hf smul = {to_has_vadd := {vadd := has_vadd.vadd _inst_3}, zero_vadd := _, add_vadd := _}
Pushforward a multiplicative action along a surjective map respecting •
.
See note [reducible non-instances].
Equations
- function.surjective.mul_action f hf smul = {to_has_smul := {smul := has_smul.smul _inst_3}, one_smul := _, mul_smul := _}
Push forward the action of R
on M
along a compatible surjective map f : R →* S
.
See also function.surjective.distrib_mul_action_left
and function.surjective.module_left
.
Equations
- function.surjective.mul_action_left f hf hsmul = {to_has_smul := {smul := has_smul.smul _inst_6}, one_smul := _, mul_smul := _}
Push forward the action of R
on M
along a compatible
surjective map f : R →+ S
.
Equations
- function.surjective.add_action_left f hf hsmul = {to_has_vadd := {vadd := has_vadd.vadd _inst_6}, zero_vadd := _, add_vadd := _}
The regular action of a monoid on itself by left multiplication.
This is promoted to a module by semiring.to_module
.
Equations
- monoid.to_mul_action M = {to_has_smul := {smul := has_mul.mul (mul_one_class.to_has_mul M)}, one_smul := _, mul_smul := _}
The regular action of a monoid on itself by left addition.
This is promoted to an add_torsor
by add_group_is_add_torsor
.
Equations
- add_monoid.to_add_action M = {to_has_vadd := {vadd := has_add.add (add_zero_class.to_has_add M)}, zero_vadd := _, add_vadd := _}
Note that the is_scalar_tower M α α
and smul_comm_class M α α
typeclass arguments are
usually satisfied by algebra M α
.
Embedding of α
into functions M → α
induced by a multiplicative action of M
on α
.
Embedding of α
into functions M → α
induced by an additive action of M
on α
.
A multiplicative action of M
on α
and a monoid homomorphism N → M
induce
a multiplicative action of N
on α
.
See note [reducible non-instances].
Equations
- mul_action.comp_hom α g = {to_has_smul := {smul := has_smul.comp.smul ⇑g}, one_smul := _, mul_smul := _}
An additive action of M
on α
and an additive monoid homomorphism N → M
induce
an additive action of N
on α
.
See note [reducible non-instances].
Equations
- add_action.comp_hom α g = {to_has_vadd := {vadd := has_vadd.comp.vadd ⇑g}, zero_vadd := _, add_vadd := _}
- to_mul_action : mul_action M A
- smul_add : ∀ (r : M) (x y : A), r • (x + y) = r • x + r • y
- smul_zero : ∀ (r : M), r • 0 = 0
Typeclass for multiplicative actions on additive structures. This generalizes group modules.
Instances of this typeclass
- module.to_distrib_mul_action
- mul_semiring_action.to_distrib_mul_action
- derivation.distrib_mul_action
- add_monoid.End.apply_distrib_mul_action
- units.distrib_mul_action
- mul_opposite.distrib_mul_action
- prod.distrib_mul_action
- add_aut.apply_distrib_mul_action
- ring_hom.apply_distrib_mul_action
- submonoid.distrib_mul_action
- subgroup.distrib_mul_action
- subsemiring.distrib_mul_action
- subring.distrib_mul_action
- pi.distrib_mul_action
- pi.distrib_mul_action'
- linear_map.distrib_mul_action
- linear_equiv.apply_distrib_mul_action
- ulift.distrib_mul_action
- ulift.distrib_mul_action'
- add_monoid_hom.distrib_mul_action
- punit.distrib_mul_action
- dfinsupp.distrib_mul_action
- dfinsupp.distrib_mul_action₂
- finsupp.distrib_mul_action
- submodule.quotient.distrib_mul_action'
- submodule.quotient.distrib_mul_action
- tensor_product.left_distrib_mul_action
- tensor_product.distrib_mul_action
- monoid_algebra.distrib_mul_action
- add_monoid_algebra.distrib_mul_action
- polynomial.distrib_mul_action
- subalgebra.distrib_mul_action
- mv_polynomial.distrib_mul_action
- localization.distrib_mul_action
- self_adjoint.distrib_mul_action
- skew_adjoint.distrib_mul_action
- matrix.distrib_mul_action
- multilinear_map.distrib_mul_action
- alternating_map.distrib_mul_action
- unitization.distrib_mul_action
- conj_act.distrib_mul_action₀
- triv_sq_zero_ext.distrib_mul_action
- order_dual.distrib_mul_action
- nnreal.distrib_mul_action
- ennreal.distrib_mul_action
- complex.distrib_mul_action
- continuous_linear_map.distrib_mul_action
- affine_map.distrib_mul_action
- normed_add_group_hom.distrib_mul_action
- hahn_series.distrib_mul_action
- continuous_map.distrib_mul_action
- bilin_form.distrib_mul_action
- submodule.torsion'.distrib_mul_action
- continuous_multilinear_map.distrib_mul_action
- measure_theory.outer_measure.distrib_mul_action
- measure_theory.measure.distrib_mul_action
- bounded_continuous_function.distrib_mul_action
- filter.germ.distrib_mul_action
- filter.germ.distrib_mul_action'
- measure_theory.ae_eq_fun.distrib_mul_action
- continuous_affine_map.distrib_mul_action
- weak_dual.distrib_mul_action
- uniform_space.completion.distrib_mul_action
- seminorm.distrib_mul_action
- measure_theory.vector_measure.distrib_mul_action
- nnrat.distrib_mul_action
- quadratic_form.distrib_mul_action
- pi_tensor_product.distrib_mul_action'
- locally_constant.distrib_mul_action
Instances of other typeclasses for distrib_mul_action
- distrib_mul_action.has_sizeof_inst
Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].
Equations
- function.injective.distrib_mul_action f hf smul = {to_mul_action := {to_has_smul := {smul := has_smul.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].
Equations
- function.surjective.distrib_mul_action f hf smul = {to_mul_action := {to_has_smul := {smul := has_smul.smul _inst_5}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Push forward the action of R
on M
along a compatible surjective map f : R →* S
.
See also function.surjective.mul_action_left
and function.surjective.module_left
.
Equations
- function.surjective.distrib_mul_action_left f hf hsmul = {to_mul_action := {to_has_smul := {smul := has_smul.smul _inst_8}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Compose a distrib_mul_action
with a monoid_hom
, with action f r' • m
.
See note [reducible non-instances].
Equations
- distrib_mul_action.comp_hom A f = {to_mul_action := {to_has_smul := {smul := has_smul.comp.smul ⇑f}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
Each element of the monoid defines a additive monoid homomorphism.
Equations
- distrib_mul_action.to_add_monoid_hom A x = {to_fun := has_smul.smul x, map_zero' := _, map_add' := _}
Each element of the monoid defines an additive monoid homomorphism.
Equations
- distrib_mul_action.to_add_monoid_End M A = {to_fun := distrib_mul_action.to_add_monoid_hom A _inst_3, map_one' := _, map_mul' := _}
- to_mul_action : mul_action M A
- smul_mul : ∀ (r : M) (x y : A), r • (x * y) = r • x * r • y
- smul_one : ∀ (r : M), r • 1 = 1
Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.
Instances of this typeclass
- mul_semiring_action.to_mul_distrib_mul_action
- units.mul_distrib_mul_action
- units.mul_distrib_mul_action'
- mul_opposite.mul_distrib_mul_action
- prod.mul_distrib_mul_action
- mul_aut.apply_mul_distrib_mul_action
- submonoid.mul_distrib_mul_action
- subgroup.mul_distrib_mul_action
- subsemiring.mul_distrib_mul_action
- subring.mul_distrib_mul_action
- pi.mul_distrib_mul_action
- pi.mul_distrib_mul_action'
- ulift.mul_distrib_mul_action
- ulift.mul_distrib_mul_action'
- punit.mul_distrib_mul_action
- localization.mul_distrib_mul_action
- conj_act.units_mul_distrib_mul_action
- conj_act.mul_distrib_mul_action
- conj_act.subgroup.conj_mul_distrib_mul_action
Instances of other typeclasses for mul_distrib_mul_action
- mul_distrib_mul_action.has_sizeof_inst
Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].
Equations
- function.injective.mul_distrib_mul_action f hf smul = {to_mul_action := {to_has_smul := {smul := has_smul.smul _inst_5}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].
Equations
- function.surjective.mul_distrib_mul_action f hf smul = {to_mul_action := {to_has_smul := {smul := has_smul.smul _inst_5}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
Compose a mul_distrib_mul_action
with a monoid_hom
, with action f r' • m
.
See note [reducible non-instances].
Equations
- mul_distrib_mul_action.comp_hom A f = {to_mul_action := {to_has_smul := {smul := has_smul.comp.smul ⇑f}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
Scalar multiplication by r
as a monoid_hom
.
Equations
- mul_distrib_mul_action.to_monoid_hom A r = {to_fun := has_smul.smul r, map_one' := _, map_mul' := _}
Each element of the monoid defines a monoid homomorphism.
Equations
- mul_distrib_mul_action.to_monoid_End M A = {to_fun := mul_distrib_mul_action.to_monoid_hom A _inst_3, map_one' := _, map_mul' := _}
The monoid of endomorphisms.
Note that this is generalized by category_theory.End
to categories other than Type u
.
Equations
- function.End α = (α → α)
Instances for function.End
Equations
- function.End.monoid α = {mul := function.comp α, mul_assoc := _, one := id α, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (function.End α)), npow_zero' := _, npow_succ' := _}
Equations
- function.End.inhabited α = {default := 1}
The tautological action by function.End α
on α
.
This is generalized to bundled endomorphisms by:
equiv.perm.apply_mul_action
add_monoid.End.apply_distrib_mul_action
add_aut.apply_distrib_mul_action
mul_aut.apply_mul_distrib_mul_action
ring_hom.apply_distrib_mul_action
linear_equiv.apply_distrib_mul_action
linear_map.apply_module
ring_hom.apply_mul_semiring_action
alg_equiv.apply_mul_semiring_action
Equations
- function.End.apply_mul_action = {to_has_smul := {smul := λ (_x : function.End α) (_y : α), _x _y}, one_smul := _, mul_smul := _}
function.End.apply_mul_action
is faithful.
The tautological action by add_monoid.End α
on α
.
This generalizes function.End.apply_mul_action
.
Equations
- add_monoid.End.apply_distrib_mul_action = {to_mul_action := {to_has_smul := {smul := λ (_x : add_monoid.End α) (_y : α), ⇑_x _y}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
add_monoid.End.apply_distrib_mul_action
is faithful.
The monoid hom representing a monoid action.
When M
is a group, see mul_action.to_perm_hom
.
Equations
- mul_action.to_End_hom = {to_fun := has_smul.smul mul_action.to_has_smul, map_one' := _, map_mul' := _}
The monoid action induced by a monoid hom to function.End α
See note [reducible non-instances].
Equations
The tautological additive action by additive (function.End α)
on α
.
Equations
- add_action.function_End = {to_has_vadd := {vadd := λ (_x : additive (function.End α)) (_y : α), _x _y}, zero_vadd := _, add_vadd := _}
The additive monoid hom representing an additive monoid action.
When M
is a group, see add_action.to_perm_hom
.
Equations
- add_action.to_End_hom = {to_fun := has_vadd.vadd add_action.to_has_vadd, map_zero' := _, map_add' := _}
The additive action induced by a hom to additive (function.End α)
See note [reducible non-instances].
Equations
Equations
- additive.has_vadd = {vadd := λ (a : additive α), has_smul.smul (⇑additive.to_mul a)}
Equations
- multiplicative.has_smul = {smul := λ (a : multiplicative α), has_vadd.vadd (⇑multiplicative.to_add a)}
Equations
- additive.add_action = {to_has_vadd := additive.has_vadd mul_action.to_has_smul, zero_vadd := _, add_vadd := _}