Mathlib.GroupTheory.GroupAction.DomAct.Basic

Module docstring

{"# Type tags for right action on the domain of a function

By default, M acts on α → β if it acts on β, and the action is given by (c • f) a = c • (f a).

In some cases, it is useful to consider another action: if M acts on α on the left, then it acts on α → β on the right so that (c • f) a = f (c • a). E.g., this action is used to reformulate the Mean Ergodic Theorem in terms of an operator on $L^2$.

Main definitions

DomMulAct M (notation: Mᵈᵐᵃ): type synonym for Mᵐᵒᵖ; if M multiplicatively acts on α, then Mᵈᵐᵃ acts on α → β for any type β;
DomAddAct M (notation: Mᵈᵃᵃ): the additive version.

We also define actions of Mᵈᵐᵃ on:

α → β provided that M acts on α;
A →* B provided that M acts on A by a MulDistribMulAction;
A →+ B provided that M acts on A by a DistribMulAction.

Implementation details

Motivation

Right action can be represented in mathlib as an action of the opposite group Mᵐᵒᵖ. However, this \"domain shift\" action cannot be an instance because this would create a \"diamond\" (a.k.a. ambiguous notation): if M is a monoid, then how does Mᵐᵒᵖ act on M → M? On the one hand, Mᵐᵒᵖ acts on M by c • a = a * c.unop, thus we have an action (c • f) a = f a * c.unop. On the other hand, M acts on itself by multiplication on the left, so with this new instance we would have (c • f) a = f (c.unop * a). Clearly, these are two different actions, so both of them cannot be instances in the library.

To overcome this difficulty, we introduce a type synonym DomMulAct M := Mᵐᵒᵖ (notation: Mᵈᵐᵃ). This new type carries the same algebraic structures as Mᵐᵒᵖ but acts on α → β by this new action. So, e.g., Mᵈᵐᵃ acts on (M → M) → M by DomMulAct.mk c • F f = F (fun a ↦ c • f a) while (Mᵈᵐᵃ)ᵈᵐᵃ (which is isomorphic to M) acts on (M → M) → M by DomMulAct.mk (DomMulAct.mk c) • F f = F (fun a ↦ f (c • a)).

Action on bundled homomorphisms

If the action of M on A preserves some structure, then Mᵈᵐᵃ acts on bundled homomorphisms from A to any type B that preserve the same structure. Examples (some of them are not yet in the library) include:

a MulDistribMulAction generates an action on A →* B;
a DistribMulAction generates an action on A →+ B;
an action on α that commutes with action of some other monoid N generates an action on α →[N] β;
a DistribMulAction on an R-module that commutes with scalar multiplications by c : R generates an action on R-linear maps from this module;
a continuous action on X generates an action on C(X, Y);
a measurable action on X generates an action on { f : X → Y // Measurable f };
a quasi measure preserving action on X generates an action on X →ₘ[μ] Y;
a measure preserving action generates an isometric action on MeasureTheory.Lp _ _ _.

Left action vs right action

It is common in the literature to consider the left action given by (c • f) a = f (c⁻¹ • a) instead of the action defined in this file. However, this left action is defined only if c belongs to a group, not to a monoid, so we decided to go with the right action.

The left action can be written in terms of DomMulAct as (DomMulAct.mk c)⁻¹ • f. As for higher level dynamics objects (orbits, invariant functions etc), they coincide for the left and for the right action, so lemmas can be formulated in terms of DomMulAct.

Keywords

group action, function, domain ","### Copy instances from Mᵐᵒᵖ "}

DomMulAct definition

(M : Type*)

Full source

/-- If `M` multiplicatively acts on `α`, then `DomMulAct M` acts on `α → β` as well as some
bundled maps from `α`. This is a type synonym for `MulOpposite M`, so this corresponds to a right
action of `M`. -/
@[to_additive "If `M` additively acts on `α`, then `DomAddAct M` acts on `α → β` as
well as some bundled maps from `α`. This is a type synonym for `AddOpposite M`, so this corresponds
to a right action of `M`."]
def DomMulAct (M : Type*) := MulOpposite M

Domain Multiplication Action Type

Informal description

The type `DomMulAct M` (notation: `Mᵈᵐᵃ`) is a type synonym for the opposite monoid `Mᵐᵒᵖ`. When `M` has a multiplicative left action on a type `α`, then `DomMulAct M` naturally obtains a right action on function spaces `α → β` for any type `β`, defined by `(c • f) a = f (c • a)`. This construction is particularly useful for ergodic theory and operator algebras.

term_ᵈᵐᵃ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] postfix:max "ᵈᵐᵃ" => DomMulAct

Domain multiplicative action notation

Informal description

The notation `Mᵈᵐᵃ` is defined as a postfix notation for `DomMulAct M`, which is a type synonym for the opposite monoid `Mᵐᵒᵖ`. This notation is used to represent right actions on the domain of functions, where `M` acts on `α` and thus `Mᵈᵐᵃ` acts on `α → β` for any type `β`.

term_ᵈᵃᵃ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] postfix:max "ᵈᵃᵃ" => DomAddAct

Additive domain action notation

Informal description

The notation `Mᵈᵃᵃ` represents the additive version of the domain action type synonym, which is used to define right actions on function domains. It is equivalent to `Mᵃᵒᵖ` (the opposite additive monoid) but specifically designed for actions on function spaces where the action is applied to the domain rather than the codomain.

DomMulAct.mk definition

: M ≃ Mᵈᵐᵃ

Full source

/-- Equivalence between `M` and `Mᵈᵐᵃ`. -/
@[to_additive "Equivalence between `M` and `Mᵈᵐᵃ`."]
def mk : M ≃ Mᵈᵐᵃ := MulOpposite.opEquiv

Equivalence between monoid and its domain multiplication action type

Informal description

The function `DomMulAct.mk` is an equivalence between a monoid `M` and its domain multiplication action type `Mᵈᵐᵃ`, which is a type synonym for the opposite monoid `Mᵐᵒᵖ`. This equivalence allows converting elements of `M` to elements of `Mᵈᵐᵃ` and vice versa.

DomMulAct.instMulOfMulOpposite instance

[Mul Mᵐᵒᵖ] : Mul Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Multiplication Operation on Domain Multiplication Action Type

Informal description

The type `DomMulAct M` inherits a multiplication operation from the opposite monoid `Mᵐᵒᵖ`. Specifically, if `Mᵐᵒᵖ` has a multiplication operation, then `DomMulAct M` is equipped with the same multiplication operation.

DomMulAct.instOneOfMulOpposite instance

[One Mᵐᵒᵖ] : One Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

One Element Inheritance for Domain Multiplication Action Type

Informal description

The type `DomMulAct M` (notation: `Mᵈᵐᵃ`) inherits a one element from the opposite monoid `Mᵐᵒᵖ`. Specifically, if `Mᵐᵒᵖ` has a one element, then `DomMulAct M` is equipped with the same one element.

DomMulAct.instInvOfMulOpposite instance

[Inv Mᵐᵒᵖ] : Inv Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Inversion Operation on Domain Multiplication Action Type

Informal description

For any type $M$ with an inversion operation on its opposite monoid $M^\text{op}$, the domain multiplication action type $M^\text{dma}$ also inherits an inversion operation.

DomMulAct.instSemigroupOfMulOpposite instance

[Semigroup Mᵐᵒᵖ] : Semigroup Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Semigroup Structure on Domain Multiplication Action Type

Informal description

For any monoid $M$, the type $M^\text{dma}$ (domain multiplication action) inherits a semigroup structure from the opposite monoid $M^\text{op}$.

DomMulAct.instCommSemigroupOfMulOpposite instance

[CommSemigroup Mᵐᵒᵖ] : CommSemigroup Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Commutative Semigroup Structure on Domain Multiplication Action Type

Informal description

For any commutative semigroup $M$, the opposite monoid $M^\text{op}$ is also a commutative semigroup, and thus the domain multiplication action type $M^\text{dma}$ inherits this commutative semigroup structure.

DomMulAct.instLeftCancelSemigroupOfMulOpposite instance

[LeftCancelSemigroup Mᵐᵒᵖ] : LeftCancelSemigroup Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Left-Cancellative Semigroup Structure on Domain Multiplication Action Type

Informal description

For any left-cancellative semigroup $M$, the domain multiplication action type $M^{dma}$ is also a left-cancellative semigroup.

DomMulAct.instRightCancelSemigroupOfMulOpposite instance

[RightCancelSemigroup Mᵐᵒᵖ] : RightCancelSemigroup Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Right-Cancellative Semigroup Structure on Domain Multiplication Action Type

Informal description

For any right-cancellative semigroup $M$, the domain multiplication action type $M^{dma}$ is also a right-cancellative semigroup.

DomMulAct.instMulOneClassOfMulOpposite instance

[MulOneClass Mᵐᵒᵖ] : MulOneClass Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Multiplicative Structure Inheritance for Domain Multiplication Action

Informal description

For any type `M` with a multiplicative structure `MulOneClass` on its opposite monoid `Mᵐᵒᵖ`, the domain multiplication action type `Mᵈᵐᵃ` inherits the same multiplicative structure.

DomMulAct.instMonoidOfMulOpposite instance

[Monoid Mᵐᵒᵖ] : Monoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Monoid Structure on Domain Multiplication Action Type

Informal description

For any monoid $M$, the type $M^\text{dma}$ (domain multiplication action) inherits a monoid structure from the opposite monoid $M^\text{op}$.

DomMulAct.instCommMonoidOfMulOpposite instance

[CommMonoid Mᵐᵒᵖ] : CommMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Commutative Monoid Structure on Domain Multiplication Action Type

Informal description

For any commutative monoid $M$, the domain multiplication action type $M^\text{dma}$ is also a commutative monoid.

DomMulAct.instLeftCancelMonoidOfMulOpposite instance

[LeftCancelMonoid Mᵐᵒᵖ] : LeftCancelMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Left-Cancelative Monoid Structure on Domain Multiplication Action Type

Informal description

For any left-cancelative monoid $M$, the domain multiplication action type $M^{dma}$ (a type synonym for the opposite monoid $M^{op}$) inherits a left-cancelative monoid structure.

DomMulAct.instRightCancelMonoidOfMulOpposite instance

[RightCancelMonoid Mᵐᵒᵖ] : RightCancelMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Right-Cancelative Monoid Structure on Domain Multiplication Action Type

Informal description

For any right-cancelative monoid $M$, the domain multiplication action type $M^{dma}$ is also a right-cancelative monoid.

DomMulAct.instCancelMonoidOfMulOpposite instance

[CancelMonoid Mᵐᵒᵖ] : CancelMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Domain Multiplication Action Type Inherits Cancellation Property from Opposite Monoid

Informal description

For any monoid $M$, if the opposite monoid $M^\text{op}$ is a cancel monoid, then the domain multiplication action type $M^\text{dma}$ is also a cancel monoid.

DomMulAct.instCancelCommMonoidOfMulOpposite instance

[CancelCommMonoid Mᵐᵒᵖ] : CancelCommMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Commutative Cancellation Property of Domain Multiplication Action Type

Informal description

For any commutative cancel monoid $M$, the domain multiplication action type $M^\text{dma}$ is also a commutative cancel monoid.

DomMulAct.instInvolutiveInvOfMulOpposite instance

[InvolutiveInv Mᵐᵒᵖ] : InvolutiveInv Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Involutive Inversion on Domain Multiplication Action Type

Informal description

For any monoid $M$, if the opposite monoid $M^\text{op}$ has an involutive inversion operation, then the domain multiplication action type $M^\text{dma}$ also has an involutive inversion operation. This means that for any $c \in M^\text{dma}$, the double inversion $(c^{-1})^{-1}$ equals $c$.

DomMulAct.instDivInvMonoidOfMulOpposite instance

[DivInvMonoid Mᵐᵒᵖ] : DivInvMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Division Monoid Structure on Domain Multiplication Action Type

Informal description

For any type $M$ such that the opposite monoid $M^\text{op}$ is a division monoid, the domain multiplication action type $M^\text{dma}$ is also a division monoid.

DomMulAct.instInvOneClassOfMulOpposite instance

[InvOneClass Mᵐᵒᵖ] : InvOneClass Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Inversion and Identity Structure on Domain Multiplication Action Type

Informal description

For any monoid $M$ with an involutive inversion operation and a multiplicative identity, the type $M^{dma}$ (domain multiplication action) also forms an `InvOneClass`, meaning it inherits the inversion operation and multiplicative identity structure from the opposite monoid $M^{op}$.

DomMulAct.instDivInvOneMonoidOfMulOpposite instance

[DivInvOneMonoid Mᵐᵒᵖ] : DivInvOneMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Domain Multiplication Action as Division Monoid with One

Informal description

For any monoid $M$, if the opposite monoid $M^{\text{op}}$ is a division monoid with one (i.e., it has a division operation and a multiplicative identity), then the domain multiplication action type $M^{\text{dma}}$ is also a division monoid with one.

DomMulAct.instDivisionMonoidOfMulOpposite instance

[DivisionMonoid Mᵐᵒᵖ] : DivisionMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Domain Multiplication Action Type as Division Monoid

Informal description

For any monoid $M$, if the opposite monoid $M^{\text{op}}$ is a division monoid, then the domain multiplication action type $M^{\text{dma}}$ is also a division monoid.

DomMulAct.instDivisionCommMonoidOfMulOpposite instance

[DivisionCommMonoid Mᵐᵒᵖ] : DivisionCommMonoid Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Domain Multiplication Action Type as Division Commutative Monoid

Informal description

For any monoid $M$, if the opposite monoid $M^{\text{op}}$ is a division commutative monoid, then the domain multiplication action type $M^{\text{dma}}$ is also a division commutative monoid.

DomMulAct.instGroupOfMulOpposite instance

[Group Mᵐᵒᵖ] : Group Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Group Structure on Domain Multiplication Action Type

Informal description

For any monoid $M$, if the opposite monoid $M^\text{op}$ is a group, then the domain multiplication action type $M^\text{dma}$ is also a group.

DomMulAct.instCommGroupOfMulOpposite instance

[CommGroup Mᵐᵒᵖ] : CommGroup Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Commutative Group Structure on Domain Multiplication Action Type

Informal description

For any commutative group $M$, the domain multiplication action type $M^\text{dma}$ is also a commutative group.

DomMulAct.instNonAssocSemiringOfMulOpposite instance

[NonAssocSemiring Mᵐᵒᵖ] : NonAssocSemiring Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Non-Associative Semiring Structure on Domain Multiplication Action Type

Informal description

For any type `M`, if the opposite monoid `Mᵐᵒᵖ` has a non-associative semiring structure, then the domain multiplication action type `DomMulAct M` (notation: `Mᵈᵐᵃ`) also inherits a non-associative semiring structure.

DomMulAct.instNonUnitalSemiringOfMulOpposite instance

[NonUnitalSemiring Mᵐᵒᵖ] : NonUnitalSemiring Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Non-Unital Semiring Structure on Domain Multiplication Action Type

Informal description

For any non-unital semiring structure on the opposite monoid $M^{\text{op}}$, the type $M^{\text{dma}}$ (domain multiplication action type) inherits a non-unital semiring structure.

DomMulAct.instSemiringOfMulOpposite instance

[Semiring Mᵐᵒᵖ] : Semiring Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Semiring Structure on Domain Multiplication Action Type

Informal description

For any type $M$ where the opposite monoid $M^{\text{op}}$ has a semiring structure, the domain multiplication action type $M^{\text{dma}}$ also inherits a semiring structure.

DomMulAct.instRingOfMulOpposite instance

[Ring Mᵐᵒᵖ] : Ring Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Ring Structure on Domain Multiplication Action Type

Informal description

For any type $M$ where the opposite monoid $M^{\text{op}}$ has a ring structure, the domain multiplication action type $M^{\text{dma}}$ also inherits a ring structure.

DomMulAct.instCommRingOfMulOpposite instance

[CommRing Mᵐᵒᵖ] : CommRing Mᵈᵐᵃ

Full source

run_cmdrun_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
    `Ring, `CommRing].map Lean.mkIdent do
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
  ))

Commutative Ring Structure on Domain Multiplication Action Type

Informal description

For any type $M$ where the opposite monoid $M^{\text{op}}$ has a commutative ring structure, the domain multiplication action type $M^{\text{dma}}$ also inherits a commutative ring structure.

DomMulAct.instIsLeftCancelMulOfMulOpposite instance

[Mul Mᵐᵒᵖ] [IsLeftCancelMul Mᵐᵒᵖ] : IsLeftCancelMul Mᵈᵐᵃ

Full source

@[to_additive] instance [Mul Mᵐᵒᵖ] [IsLeftCancelMul Mᵐᵒᵖ] : IsLeftCancelMul Mᵈᵐᵃ := ‹_›

Left-Cancellative Multiplication on Domain Multiplication Action Type

Informal description

For any monoid $M$ where the opposite monoid $M^{\text{op}}$ has a left-cancellative multiplication, the domain multiplication action type $M^{\text{dma}}$ also has a left-cancellative multiplication.

DomMulAct.instIsRightCancelMulOfMulOpposite instance

[Mul Mᵐᵒᵖ] [IsRightCancelMul Mᵐᵒᵖ] : IsRightCancelMul Mᵈᵐᵃ

Full source

@[to_additive] instance [Mul Mᵐᵒᵖ] [IsRightCancelMul Mᵐᵒᵖ] : IsRightCancelMul Mᵈᵐᵃ := ‹_›

Right-Cancellative Multiplication on Domain Multiplication Action Type

Informal description

For any type $M$ where the opposite monoid $M^{\text{op}}$ has a right-cancellative multiplication, the domain multiplication action type $M^{\text{dma}}$ also has a right-cancellative multiplication.

DomMulAct.instIsCancelMulOfMulOpposite instance

[Mul Mᵐᵒᵖ] [IsCancelMul Mᵐᵒᵖ] : IsCancelMul Mᵈᵐᵃ

Full source

@[to_additive] instance [Mul Mᵐᵒᵖ] [IsCancelMul Mᵐᵒᵖ] : IsCancelMul Mᵈᵐᵃ := ‹_›

Cancellative Multiplication on Domain Multiplication Action Type

Informal description

For any monoid $M$ where the opposite monoid $M^{\text{op}}$ has a cancellative multiplication, the domain multiplication action type $M^{\text{dma}}$ also has a cancellative multiplication.

DomMulAct.mk_one theorem

[One M] : mk (1 : M) = 1

Full source

@[to_additive (attr := simp)]
lemma mk_one [One M] : mk (1 : M) = 1 := rfl

Identity Preservation under Domain Multiplication Action Equivalence: $\text{mk}(1_M) = 1_{Mᵈᵐᵃ}$

Informal description

For any monoid $M$ with a multiplicative identity element $1$, the equivalence map `DomMulAct.mk` sends the identity element of $M$ to the identity element of $Mᵈᵐᵃ$, i.e., $\text{mk}(1_M) = 1_{Mᵈᵐᵃ}$.

DomMulAct.symm_mk_one theorem

[One M] : mk.symm (1 : Mᵈᵐᵃ) = 1

Full source

@[to_additive (attr := simp)]
lemma symm_mk_one [One M] : mk.symm (1 : Mᵈᵐᵃ) = 1 := rfl

Inverse Equivalence Preserves Identity: $\text{mk.symm}(1_{Mᵈᵐᵃ}) = 1_M$

Informal description

For any monoid $M$ with a multiplicative identity element $1$, the inverse of the equivalence map `DomMulAct.mk` evaluated at the identity element of $Mᵈᵐᵃ$ returns the identity element of $M$, i.e., $\text{mk.symm}(1_{Mᵈᵐᵃ}) = 1_M$.

DomMulAct.mk_mul theorem

[Mul M] (a b : M) : mk (a * b) = mk b * mk a

Full source

@[to_additive (attr := simp)]
lemma mk_mul [Mul M] (a b : M) : mk (a * b) = mk b * mk a := rfl

Equivalence Reverses Multiplication: $\text{mk}(a * b) = \text{mk}(b) * \text{mk}(a)$

Informal description

For any monoid $M$ with a multiplication operation and any elements $a, b \in M$, the equivalence map `DomMulAct.mk` satisfies $\text{mk}(a * b) = \text{mk}(b) * \text{mk}(a)$ in $Mᵈᵐᵃ$.

DomMulAct.symm_mk_mul theorem

[Mul M] (a b : Mᵈᵐᵃ) : mk.symm (a * b) = mk.symm b * mk.symm a

Full source

@[to_additive (attr := simp)]
lemma symm_mk_mul [Mul M] (a b : Mᵈᵐᵃ) : mk.symm (a * b) = mk.symm b * mk.symm a := rfl

Inverse Equivalence Reverses Multiplication in Domain Action Type: $\text{mk.symm}(a * b) = \text{mk.symm}(b) * \text{mk.symm}(a)$

Informal description

For any monoid $M$ with a multiplication operation and any elements $a, b \in M^\text{dma}$, the inverse of the equivalence map $\text{mk}$ satisfies $\text{mk.symm}(a * b) = \text{mk.symm}(b) * \text{mk.symm}(a)$ in $M$.

DomMulAct.mk_inv theorem

[Inv M] (a : M) : mk (a⁻¹) = (mk a)⁻¹

Full source

@[to_additive (attr := simp)]
lemma mk_inv [Inv M] (a : M) : mk (a⁻¹) = (mk a)⁻¹ := rfl

Inversion Preserved under Domain Multiplication Action Equivalence: $\text{mk}(a^{-1}) = (\text{mk}(a))^{-1}$

Informal description

For any monoid $M$ with an inversion operation and any element $a \in M$, the equivalence map $\text{mk}$ satisfies $\text{mk}(a^{-1}) = (\text{mk}(a))^{-1}$ in $M^\text{dma}$.

DomMulAct.symm_mk_inv theorem

[Inv M] (a : Mᵈᵐᵃ) : mk.symm (a⁻¹) = (mk.symm a)⁻¹

Full source

@[to_additive (attr := simp)]
lemma symm_mk_inv [Inv M] (a : Mᵈᵐᵃ) : mk.symm (a⁻¹) = (mk.symm a)⁻¹ := rfl

Inversion Preserved under Inverse Domain Action Equivalence: $\text{mk.symm}(a^{-1}) = (\text{mk.symm}(a))^{-1}$

Informal description

For any monoid $M$ with an inversion operation and any element $a \in M^\text{dma}$, the inverse of the equivalence map $\text{mk}$ satisfies $\text{mk.symm}(a^{-1}) = (\text{mk.symm}(a))^{-1}$ in $M$.

DomMulAct.mk_pow theorem

[Monoid M] (a : M) (n : ℕ) : mk (a ^ n) = mk a ^ n

Full source

@[to_additive (attr := simp)]
lemma mk_pow [Monoid M] (a : M) (n : ℕ) : mk (a ^ n) = mk a ^ n := rfl

Power Preservation under Domain Multiplication Action Equivalence: $\text{mk}(a^n) = (\text{mk}(a))^n$

Informal description

For any monoid $M$, element $a \in M$, and natural number $n$, the equivalence map $\text{mk} : M \to M^\text{dma}$ satisfies $\text{mk}(a^n) = (\text{mk}(a))^n$.

DomMulAct.symm_mk_pow theorem

[Monoid M] (a : Mᵈᵐᵃ) (n : ℕ) : mk.symm (a ^ n) = mk.symm a ^ n

Full source

@[to_additive (attr := simp)]
lemma symm_mk_pow [Monoid M] (a : Mᵈᵐᵃ) (n : ℕ) : mk.symm (a ^ n) = mk.symm a ^ n := rfl

Power Preservation under Domain Multiplication Action Equivalence

Informal description

For any monoid $M$ and any element $a$ of the domain multiplication action type $M^\text{dma}$, and for any natural number $n$, the inverse of the equivalence map `mk` satisfies $\text{mk.symm}(a^n) = (\text{mk.symm}(a))^n$.

DomMulAct.mk_zpow theorem

[DivInvMonoid M] (a : M) (n : ℤ) : mk (a ^ n) = mk a ^ n

Full source

@[to_additive (attr := simp)]
lemma mk_zpow [DivInvMonoid M] (a : M) (n : ℤ) : mk (a ^ n) = mk a ^ n := rfl

Power Preservation under Domain Multiplication Action Equivalence for Integer Exponents

Informal description

For any division monoid $M$, any element $a \in M$, and any integer $n$, the equivalence map $\text{mk} : M \to M^\text{dma}$ satisfies $\text{mk}(a^n) = (\text{mk}(a))^n$.

DomMulAct.symm_mk_zpow theorem

[DivInvMonoid M] (a : Mᵈᵐᵃ) (n : ℤ) : mk.symm (a ^ n) = mk.symm a ^ n

Full source

@[to_additive (attr := simp)]
lemma symm_mk_zpow [DivInvMonoid M] (a : Mᵈᵐᵃ) (n : ℤ) : mk.symm (a ^ n) = mk.symm a ^ n := rfl

Power Preservation under Domain Multiplication Action Equivalence for Integer Exponents

Informal description

For any division monoid $M$, any element $a$ of the domain multiplication action type $M^\text{dma}$, and any integer $n$, the inverse of the equivalence map $\text{mk}$ satisfies $\text{mk.symm}(a^n) = (\text{mk.symm}(a))^n$.

DomMulAct.instSMulForall instance

[SMul M α] : SMul Mᵈᵐᵃ (α → β)

Full source

@[to_additive]
instance [SMul M α] : SMul Mᵈᵐᵃ (α → β) where
  smul c f a := f (mk.symm c • a)

Right Action of Domain Multiplication on Function Spaces

Informal description

For any type $M$ with a left scalar multiplication action on a type $\alpha$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a right scalar multiplication action on the function space $\alpha \to \beta$ for any type $\beta$. This action is defined by $(c \cdot f)(a) = f(c^{-1} \cdot a)$ for $c \in M^\text{dma}$ and $f \in \alpha \to \beta$.

DomMulAct.smul_apply theorem

[SMul M α] (c : Mᵈᵐᵃ) (f : α → β) (a : α) : (c • f) a = f (mk.symm c • a)

Full source

@[to_additive]
theorem smul_apply [SMul M α] (c : Mᵈᵐᵃ) (f : α → β) (a : α) : (c • f) a = f (mk.symm c • a) := rfl

Action Formula for Domain Multiplication on Functions: $(c \cdot f)(a) = f(c^{-1} \cdot a)$

Informal description

For any type $M$ with a left scalar multiplication action on a type $\alpha$, any element $c$ of the domain multiplication action type $M^\text{dma}$, any function $f \colon \alpha \to \beta$, and any element $a \in \alpha$, the action of $c$ on $f$ evaluated at $a$ satisfies $(c \cdot f)(a) = f((\text{mk.symm}\, c) \cdot a)$.

DomMulAct.instSMulCommClassForall instance

[SMul M α] [SMul N β] : SMulCommClass Mᵈᵐᵃ N (α → β)

Full source

@[to_additive]
instance [SMul M α] [SMul N β] : SMulCommClass Mᵈᵐᵃ N (α → β) where
  smul_comm _ _ _ := rfl

Commutation of Domain Multiplication and Scalar Actions on Function Spaces

Informal description

For any types $M$ and $N$ with left scalar multiplication actions on types $\alpha$ and $\beta$ respectively, the right scalar multiplication actions of $M^\text{dma}$ (the domain multiplication action type for $M$) and $N$ commute on the function space $\alpha \to \beta$. That is, for any $c \in M^\text{dma}$, $n \in N$, and $f \in \alpha \to \beta$, we have $c \cdot (n \cdot f) = n \cdot (c \cdot f)$.

DomMulAct.instSMulCommClassForall_1 instance

[SMul M α] [SMul N β] : SMulCommClass N Mᵈᵐᵃ (α → β)

Full source

@[to_additive]
instance [SMul M α] [SMul N β] : SMulCommClass N Mᵈᵐᵃ (α → β) where
  smul_comm _ _ _ := rfl

Commutation of Right Actions on Function Spaces

Informal description

For any types $M$ and $N$ with left scalar multiplication actions on types $\alpha$ and $\beta$ respectively, the right scalar multiplication actions of $N$ and $M^\text{dma}$ (the domain multiplication action type for $M$) commute on the function space $\alpha \to \beta$. That is, for any $n \in N$, $c \in M^\text{dma}$, and $f \in \alpha \to \beta$, we have $n \cdot (c \cdot f) = c \cdot (n \cdot f)$.

DomMulAct.instSMulCommClassForall_2 instance

[SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α → β)

Full source

@[to_additive]
instance [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α → β) where
  smul_comm _ _ f := funext fun _ ↦ congr_arg f (smul_comm _ _ _).symm

Commuting Right Actions of Domain Multiplication on Function Spaces

Informal description

For any types $M$ and $N$ with commuting left scalar multiplication actions on a type $\alpha$, the domain multiplication action types $M^\text{dma}$ and $N^\text{dma}$ (type synonyms for the opposite monoids $M^\text{op}$ and $N^\text{op}$) have commuting right scalar multiplication actions on the function space $\alpha \to \beta$ for any type $\beta$. This means that for any $c \in M^\text{dma}$, $d \in N^\text{dma}$, and $f \in \alpha \to \beta$, we have $(c \cdot (d \cdot f)) = (d \cdot (c \cdot f))$.

DomMulAct.instFaithfulSMulForallOfNontrivial instance

[SMul M α] [FaithfulSMul M α] [Nontrivial β] : FaithfulSMul Mᵈᵐᵃ (α → β)

Full source

@[to_additive]
instance [SMul M α] [FaithfulSMul M α] [Nontrivial β] : FaithfulSMul Mᵈᵐᵃ (α → β) where
  eq_of_smul_eq_smul {c₁ c₂} h := mk.symm.injective <| eq_of_smul_eq_smul fun a : α ↦ by
    rcases exists_pair_ne β with ⟨x, y, hne⟩
    contrapose! hne
    haveI := Classical.decEq α
    replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
    simpa [smul_apply, hne] using h

Faithfulness of Right Action on Function Spaces via Domain Multiplication

Informal description

For any type $M$ with a faithful left scalar multiplication action on a type $\alpha$ and any nontrivial type $\beta$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a faithful right scalar multiplication action on the function space $\alpha \to \beta$. This means that if two elements $c_1, c_2 \in M^\text{dma}$ satisfy $c_1 \cdot f = c_2 \cdot f$ for all $f \in \alpha \to \beta$, then $c_1 = c_2$.

DomMulAct.instSMulZeroClassForallOfSMul instance

[SMul M α] [Zero β] : SMulZeroClass Mᵈᵐᵃ (α → β)

Full source

instance [SMul M α] [Zero β] : SMulZeroClass Mᵈᵐᵃ (α → β) where
  smul_zero _ := rfl

Zero-Preserving Right Action of Domain Multiplication on Function Spaces

Informal description

For any type $M$ with a left scalar multiplication action on a type $\alpha$ and any type $\beta$ with a zero element, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a scalar multiplication action on the function space $\alpha \to \beta$ that preserves the zero function. This means that for any $c \in M^\text{dma}$, we have $c \cdot 0 = 0$, where $0$ denotes the zero function in $\alpha \to \beta$.

DomMulAct.instDistribSMulForallOfSMul instance

{A : Type*} [SMul M α] [AddZeroClass A] : DistribSMul Mᵈᵐᵃ (α → A)

Full source

instance {A : Type*} [SMul M α] [AddZeroClass A] : DistribSMul Mᵈᵐᵃ (α → A) where
  smul_add _ _ _ := rfl

Distributive Right Action on Function Spaces via Domain Multiplication

Informal description

For any type $M$ with a left scalar multiplication action on a type $\alpha$ and any additive monoid $A$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a distributive scalar multiplication action on the function space $\alpha \to A$. This means that for any $c \in M^\text{dma}$ and functions $f, g \in \alpha \to A$, we have $c \cdot (f + g) = c \cdot f + c \cdot g$.

DomMulAct.instMulActionForall instance

[Monoid M] [MulAction M α] : MulAction Mᵈᵐᵃ (α → β)

Full source

@[to_additive]
instance [Monoid M] [MulAction M α] : MulAction Mᵈᵐᵃ (α → β) where
  one_smul f := funext fun _ ↦ congr_arg f (one_smul _ _)
  mul_smul _ _ f := funext fun _ ↦ congr_arg f (mul_smul _ _ _)

Multiplicative Action of Domain Multiplication on Function Spaces

Informal description

For any monoid $M$ with a multiplicative action on a type $\alpha$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a multiplicative action on the function space $\alpha \to \beta$ for any type $\beta$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$ and $f \in \alpha \to \beta$.

DomMulAct.instDistribMulActionForallOfMulAction instance

{A : Type*} [Monoid M] [MulAction M α] [AddMonoid A] : DistribMulAction Mᵈᵐᵃ (α → A)

Full source

instance {A : Type*} [Monoid M] [MulAction M α] [AddMonoid A] : DistribMulAction Mᵈᵐᵃ (α → A) where
  smul_zero _ := rfl
  smul_add _ _ _ := rfl

Distributive Multiplicative Action on Function Spaces via Domain Multiplication

Informal description

For any monoid $M$ with a multiplicative action on a type $\alpha$, and any additive monoid $A$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a distributive multiplicative action on the function space $\alpha \to A$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$ and $f \in \alpha \to A$.

DomMulAct.instMulDistribMulActionForallOfMulAction instance

{A : Type*} [Monoid M] [MulAction M α] [Monoid A] : MulDistribMulAction Mᵈᵐᵃ (α → A)

Full source

instance {A : Type*} [Monoid M] [MulAction M α] [Monoid A] : MulDistribMulAction Mᵈᵐᵃ (α → A) where
  smul_mul _ _ _ := rfl
  smul_one _ := rfl

Multiplicative Distributive Action on Function Spaces via Domain Multiplication

Informal description

For any monoid $M$ with a multiplicative action on a type $\alpha$, and any monoid $A$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a multiplicative distributive action on the function space $\alpha \to A$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$ and $f \in \alpha \to A$.

DomMulAct.instSMulMonoidHom instance

: SMul Mᵈᵐᵃ (A →* B)

Full source

instance : SMul Mᵈᵐᵃ (A →* B) where
  smul c f := f.comp (MulDistribMulAction.toMonoidHom _ (mk.symm c))

Scalar Multiplication Action on Monoid Homomorphisms via Domain Multiplication Action

Informal description

For any monoid $M$ acting on a monoid $A$ via a multiplicative distributive action, and any monoid $B$, the domain multiplication action type $M^{dma}$ (a type synonym for the opposite monoid $M^{op}$) has a scalar multiplication action on the set of monoid homomorphisms from $A$ to $B$. This action is defined by $(c \cdot f)(a) = f(c^{-1} \cdot a)$ for $c \in M^{dma}$, $f \in A \to^* B$, and $a \in A$.

DomMulAct.instSMulCommClassMonoidHom instance

[Monoid M'] [MulDistribMulAction M' A] [SMulCommClass M M' A] : SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →* B)

Full source

instance [Monoid M'] [MulDistribMulAction M' A] [SMulCommClass M M' A] :
    SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →* B) :=
  DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Commuting Right Actions on Monoid Homomorphisms via Domain Multiplication

Informal description

For any monoids $M$ and $M'$ with multiplicative distributive actions on a monoid $A$ that commute with each other, the domain multiplication action types $M^\text{dma}$ and $M'^\text{dma}$ have commuting right scalar multiplication actions on the space of monoid homomorphisms from $A$ to any monoid $B$.

DomMulAct.smul_monoidHom_apply theorem

(c : Mᵈᵐᵃ) (f : A →* B) (a : A) : (c • f) a = f (mk.symm c • a)

Full source

theorem smul_monoidHom_apply (c : Mᵈᵐᵃ) (f : A →* B) (a : A) : (c • f) a = f (mk.symm c • a) :=
  rfl

Action Formula for Monoid Homomorphisms via Domain Multiplication: $(c \cdot f)(a) = f(c^{-1} \cdot a)$

Informal description

For any element $c$ in the domain multiplication action type $M^{dma}$, any monoid homomorphism $f \colon A \to B$, and any element $a \in A$, the action of $c$ on $f$ satisfies $(c \cdot f)(a) = f(c^{-1} \cdot a)$, where $c^{-1}$ is the inverse of $c$ in $M^{dma}$.

DomMulAct.mk_smul_monoidHom_apply theorem

(c : M) (f : A →* B) (a : A) : (mk c • f) a = f (c • a)

Full source

@[simp]
theorem mk_smul_monoidHom_apply (c : M) (f : A →* B) (a : A) : (mk c • f) a = f (c • a) := rfl

Domain Multiplication Action on Monoid Homomorphisms: $(c \cdot f)(a) = f(c \cdot a)$

Informal description

For any monoid element $c \in M$, any monoid homomorphism $f \colon A \to B$, and any element $a \in A$, the action of $c$ on $f$ via the domain multiplication action satisfies $(c \cdot f)(a) = f(c \cdot a)$.

DomMulAct.instMulActionMonoidHom instance

: MulAction Mᵈᵐᵃ (A →* B)

Full source

instance : MulAction Mᵈᵐᵃ (A →* B) := DFunLike.coe_injective.mulAction (⇑) fun _ _ ↦ rfl

Multiplicative Action of Domain Multiplication on Monoid Homomorphisms

Informal description

For any monoid $M$ acting on a monoid $A$ via a multiplicative distributive action, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a multiplicative action on the set of monoid homomorphisms from $A$ to any monoid $B$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$, $f \in A \to^* B$, and $a \in A$.

DomMulAct.instSMulAddMonoidHom instance

: SMul Mᵈᵐᵃ (A →+ B)

Full source

instance : SMul Mᵈᵐᵃ (A →+ B) where
  smul c f := f.comp (DistribSMul.toAddMonoidHom _ (mk.symm c))

Scalar Action of Domain Multiplication on Additive Homomorphisms

Informal description

For any additive monoid homomorphisms $A \to B$, the type $M^\text{dma}$ (the domain multiplication action type) has a scalar multiplication action defined by $(c \cdot f)(a) = f(c \cdot a)$, where $c \in M^\text{dma}$, $f \colon A \to B$ is an additive homomorphism, and $a \in A$.

DomMulAct.instSMulCommClassAddMonoidHom instance

[DistribSMul M' A] [SMulCommClass M M' A] : SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+ B)

Full source

instance [DistribSMul M' A] [SMulCommClass M M' A] : SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →+ B) :=
  DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Commutation of Domain Multiplication Actions on Additive Homomorphisms

Informal description

For any additive monoid homomorphisms $A \to B$, if $M$ and $M'$ have commuting left scalar multiplication actions on $A$ that are distributive over addition, then the domain multiplication action types $M^\text{dma}$ and $M'^\text{dma}$ have commuting right scalar multiplication actions on the space of additive homomorphisms $A \to B$. That is, for any $c \in M^\text{dma}$, $d \in M'^\text{dma}$, and $f \in A \to B$, we have $(c \cdot (d \cdot f)) = (d \cdot (c \cdot f))$.

DomMulAct.instSMulCommClassAddMonoidHom_1 instance

[DistribSMul M' B] : SMulCommClass Mᵈᵐᵃ M' (A →+ B)

Full source

instance [DistribSMul M' B] : SMulCommClass Mᵈᵐᵃ M' (A →+ B) :=
  DFunLike.coe_injective.smulCommClass (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Commutation of Domain Multiplication and Scalar Actions on Additive Homomorphisms

Informal description

For any additive monoid homomorphisms $A \to B$ and a type $M'$ with a distributive scalar multiplication action on $B$, the right scalar multiplication actions of $M^\text{dma}$ (the domain multiplication action type for $M$) and $M'$ commute on the space of additive homomorphisms $A \to B$. That is, for any $c \in M^\text{dma}$, $m' \in M'$, and $f \in A \to B$, we have $c \cdot (m' \cdot f) = m' \cdot (c \cdot f)$.

DomMulAct.smul_addMonoidHom_apply theorem

(c : Mᵈᵐᵃ) (f : A →+ B) (a : A) : (c • f) a = f (mk.symm c • a)

Full source

theorem smul_addMonoidHom_apply (c : Mᵈᵐᵃ) (f : A →+ B) (a : A) : (c • f) a = f (mk.symm c • a) :=
  rfl

Action Formula for Domain Multiplication on Additive Homomorphisms: $(c \cdot f)(a) = f(\text{mk.symm}(c) \cdot a)$

Informal description

For any element $c$ in the domain multiplication action type $M^\text{dma}$, any additive monoid homomorphism $f \colon A \to B$, and any element $a \in A$, the action of $c$ on $f$ evaluated at $a$ is equal to $f$ evaluated at the action of the inverse image of $c$ (under the equivalence `DomMulAct.mk`) on $a$. In other words, $(c \cdot f)(a) = f(\text{mk.symm}(c) \cdot a)$.

DomMulAct.mk_smul_addMonoidHom_apply theorem

(c : M) (f : A →+ B) (a : A) : (mk c • f) a = f (c • a)

Full source

@[simp]
theorem mk_smul_addMonoidHom_apply (c : M) (f : A →+ B) (a : A) : (mk c • f) a = f (c • a) := rfl

Action of Domain Multiplication on Additive Homomorphisms: $(c \cdot f)(a) = f(c \cdot a)$

Informal description

For any monoid element $c \in M$, additive monoid homomorphism $f \colon A \to B$, and element $a \in A$, the action of the domain multiplication type on $f$ satisfies $(c \cdot f)(a) = f(c \cdot a)$, where $c \cdot f$ denotes the scalar multiplication of $f$ by $c$ under the domain multiplication action.

DomMulAct.coe_smul_addMonoidHom theorem

(c : Mᵈᵐᵃ) (f : A →+ B) : ⇑(c • f) = c • ⇑f

Full source

theorem coe_smul_addMonoidHom (c : Mᵈᵐᵃ) (f : A →+ B) : ⇑(c • f) = c • ⇑f :=
  rfl

Compatibility of Scalar Action with Underlying Function for Additive Homomorphisms

Informal description

For any element $c$ in the domain multiplication action type $M^\text{dma}$ and any additive monoid homomorphism $f \colon A \to B$, the underlying function of the scalar multiple $c \cdot f$ is equal to the scalar multiple of the underlying function of $f$ under the domain multiplication action, i.e., $(c \cdot f)(a) = (c \cdot \tilde{f})(a)$ for all $a \in A$, where $\tilde{f}$ denotes the underlying function of $f$.

DomMulAct.instMulActionAddMonoidHomOfDistribMulAction instance

[Monoid M] [AddMonoid A] [DistribMulAction M A] [AddZeroClass B] : MulAction Mᵈᵐᵃ (A →+ B)

Full source

instance [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddZeroClass B] :
    MulAction Mᵈᵐᵃ (A →+ B) := DFunLike.coe_injective.mulAction (⇑) fun _ _ ↦ rfl

Multiplicative Action on Additive Homomorphisms via Domain Multiplication

Informal description

For any monoid $M$ with a distributive multiplicative action on an additive monoid $A$, and any additive monoid with zero $B$, the domain multiplication action type $M^\text{dma}$ has a multiplicative action on the space of additive monoid homomorphisms $A \to B$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$, $f \in A \to B$, and $a \in A$.

DomMulAct.instDistribMulActionAddMonoidHom instance

[Monoid M] [AddMonoid A] [DistribMulAction M A] [AddCommMonoid B] : DistribMulAction Mᵈᵐᵃ (A →+ B)

Full source

instance [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddCommMonoid B] :
    DistribMulAction Mᵈᵐᵃ (A →+ B) :=
  DFunLike.coe_injective.distribMulAction (AddMonoidHom.coeFn A B) fun _ _ ↦ rfl

Distributive Multiplicative Action on Additive Homomorphisms via Domain Multiplication

Informal description

For any monoid $M$ with a distributive multiplicative action on an additive monoid $A$, and any additive commutative monoid $B$, the domain multiplication action type $M^\text{dma}$ has a distributive multiplicative action on the space of additive monoid homomorphisms $A \to B$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$, $f \in A \to B$, and $a \in A$.

DomMulAct.instMulDistribMulActionMonoidHom instance

[Monoid M] [Monoid A] [MulDistribMulAction M A] [CommMonoid B] : MulDistribMulAction Mᵈᵐᵃ (A →* B)

Full source

instance [Monoid M] [Monoid A] [MulDistribMulAction M A] [CommMonoid B] :
    MulDistribMulAction Mᵈᵐᵃ (A →* B) :=
  DFunLike.coe_injective.mulDistribMulAction (MonoidHom.coeFn A B) fun _ _ ↦ rfl

Multiplicative Distributive Action on Monoid Homomorphisms via Domain Multiplication

Informal description

For any monoid $M$ acting on a monoid $A$ via a multiplicative distributive action, and any commutative monoid $B$, the domain multiplication action type $M^\text{dma}$ (a type synonym for the opposite monoid $M^\text{op}$) has a multiplicative distributive action on the space of monoid homomorphisms $A \to B$. This action is defined by $(c \cdot f)(a) = f(c \cdot a)$ for $c \in M^\text{dma}$, $f \in A \to B$, and $a \in A$.