Mathlib.Algebra.GroupWithZero.Action.Prod

Prod.smul_zero_mk theorem

{α : Type*} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) : a • ((0 : α), c) = (0, a • c)

Full source

theorem smul_zero_mk {α : Type*} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) :
    a • ((0 : α), c) = (0, a • c) := by rw [Prod.smul_mk, smul_zero]

Scalar Multiplication on Zero Pair: $a \cdot (0, c) = (0, a \cdot c)$

Informal description

Let $M$ be a monoid acting distributively on an additive monoid $\alpha$, and let $\beta$ be an arbitrary type. For any element $a \in M$ and any $c \in \beta$, the scalar multiplication of $a$ on the pair $(0, c)$ satisfies $a \cdot (0, c) = (0, a \cdot c)$.

Prod.smul_mk_zero theorem

{β : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) : a • (b, (0 : β)) = (a • b, 0)

Full source

theorem smul_mk_zero {β : Type*} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) :
    a • (b, (0 : β)) = (a • b, 0) := by rw [Prod.smul_mk, smul_zero]

Scalar Multiplication on Pair with Zero: $a \cdot (b, 0) = (a \cdot b, 0)$

Informal description

Let $M$ be a monoid acting distributively on an additive monoid $\beta$, and let $\alpha$ be an arbitrary type. For any element $a \in M$ and any $b \in \alpha$, the scalar multiplication of $a$ on the pair $(b, 0)$ satisfies $a \cdot (b, 0) = (a \cdot b, 0)$.

Prod.smulZeroClass instance

{R M N : Type*} [Zero M] [Zero N] [SMulZeroClass R M] [SMulZeroClass R N] : SMulZeroClass R (M × N)

Full source

instance smulZeroClass {R M N : Type*} [Zero M] [Zero N] [SMulZeroClass R M] [SMulZeroClass R N] :
    SMulZeroClass R (M × N) where smul_zero _ := by ext <;> exact smul_zero _

Component-wise Scalar Multiplication Preserving Zero on Product Types

Informal description

For any types $M$ and $N$ with zero elements and scalar multiplication operations by elements of type $R$ that preserve zero, the product type $M \times N$ also has a scalar multiplication operation that preserves zero. Specifically, if $R$ acts on $M$ and $N$ via `SMulZeroClass` structures, then $R$ acts on $M \times N$ via the component-wise scalar multiplication $(r \cdot (m, n)) = (r \cdot m, r \cdot n)$.

Prod.distribSMul instance

{R M N : Type*} [AddZeroClass M] [AddZeroClass N] [DistribSMul R M] [DistribSMul R N] : DistribSMul R (M × N)

Full source

instance distribSMul {R M N : Type*} [AddZeroClass M] [AddZeroClass N] [DistribSMul R M]
    [DistribSMul R N] : DistribSMul R (M × N) where
  smul_add _ _ _ := by ext <;> exact smul_add ..

Component-wise Distributive Scalar Multiplication on Product Types

Informal description

For any types $M$ and $N$ with additive zero class structures and scalar multiplication operations by elements of type $R$ that distribute over addition, the product type $M \times N$ also has a scalar multiplication operation that distributes over addition. Specifically, if $R$ acts on $M$ and $N$ via `DistribSMul` structures, then $R$ acts on $M \times N$ via the component-wise scalar multiplication $(r \cdot (m, n)) = (r \cdot m, r \cdot n)$.

Prod.distribMulAction instance

 {R : Type*} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] :
  DistribMulAction R (M × N)

Full source

instance distribMulAction {R : Type*} [Monoid R] [AddMonoid M] [AddMonoid N]
    [DistribMulAction R M] [DistribMulAction R N] : DistribMulAction R (M × N) :=
  { Prod.mulAction, Prod.distribSMul with }

Distributive Multiplicative Action on Product of Additive Monoids

Informal description

For any monoid $R$ and additive monoids $M$ and $N$ with distributive multiplicative actions of $R$, the product type $M \times N$ inherits a component-wise distributive multiplicative action of $R$.

Prod.mulDistribMulAction instance

 {R : Type*} [Monoid R] [Monoid M] [Monoid N] [MulDistribMulAction R M] [MulDistribMulAction R N] :
  MulDistribMulAction R (M × N)

Full source

instance mulDistribMulAction {R : Type*} [Monoid R] [Monoid M] [Monoid N]
    [MulDistribMulAction R M] [MulDistribMulAction R N] : MulDistribMulAction R (M × N) where
  smul_mul _ _ _ := by ext <;> exact smul_mul' ..
  smul_one _ := by ext <;> exact smul_one _

Multiplicative Distributive Action on Product of Monoids

Informal description

For any monoid $R$ and monoids $M$ and $N$ with multiplicative distributive actions of $R$, the product type $M \times N$ inherits a component-wise multiplicative distributive action of $R$.

DistribMulAction.prodOfSMulCommClass abbrev

[DistribMulAction M α] [DistribMulAction N α] [SMulCommClass M N α] : DistribMulAction (M × N) α

Full source

/-- Construct a `DistribMulAction` by a product monoid from `DistribMulAction`s by the factors. -/
abbrev DistribMulAction.prodOfSMulCommClass [DistribMulAction M α] [DistribMulAction N α]
    [SMulCommClass M N α] : DistribMulAction (M × N) α where
  __ := MulAction.prodOfSMulCommClass M N α
  smul_zero mn := by change mn.1 • mn.2 • 0 = (0 : α); rw [smul_zero, smul_zero]
  smul_add mn a a' := by change mn.1 • mn.2 • _ = (_ : α); rw [smul_add, smul_add]; rfl

Distributive Multiplicative Action of Product Monoid on Commuting Actions

Informal description

Given monoids $M$ and $N$ with distributive multiplicative actions on an additive monoid $\alpha$, and assuming these actions commute (i.e., $m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $m \in M$, $n \in N$, $a \in \alpha$), then the product monoid $M \times N$ also has a distributive multiplicative action on $\alpha$ defined componentwise.

DistribMulAction.prodEquiv definition

: DistribMulAction (M × N) α ≃ Σ' (_ : DistribMulAction M α) (_ : DistribMulAction N α), SMulCommClass M N α

Full source

/-- A `DistribMulAction` by a product monoid is equivalent to
  commuting `DistribMulAction`s by the factors. -/
def DistribMulAction.prodEquiv : DistribMulActionDistribMulAction (M × N) α ≃
    Σ' (_ : DistribMulAction M α) (_ : DistribMulAction N α), SMulCommClass M N α where
  toFun _ :=
    letI instM := DistribMulAction.compHom α (.inl M N)
    letI instN := DistribMulAction.compHom α (.inr M N)
    ⟨instM, instN, (MulAction.prodEquiv M N α inferInstance).2.2⟩
  invFun _insts :=
    letI := _insts.1; letI := _insts.2.1; have := _insts.2.2
    DistribMulAction.prodOfSMulCommClass M N α
  left_inv _ := by
    dsimp only; ext ⟨m, n⟩ a
    change (m, (1 : N)) • ((1 : M), n) • a = _
    rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul]; rfl
  right_inv := by
    rintro ⟨_, x, _⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← one_smul N a]); rfl
    congr 1
    · funext i; congr; ext m a; clear i; (conv_rhs => rw [← one_smul N a]); rfl
    · ext n a; (conv_rhs => rw [← one_smul M (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..

Equivalence between product monoid actions and commuting component actions

Informal description

The equivalence states that a distributive multiplicative action by a product monoid $M \times N$ on an additive monoid $\alpha$ is equivalent to the existence of commuting distributive multiplicative actions by $M$ and $N$ on $\alpha$. More precisely, the equivalence is between: 1. The type of distributive multiplicative actions of $M \times N$ on $\alpha$, and 2. The dependent triple consisting of: - A distributive multiplicative action of $M$ on $\alpha$, - A distributive multiplicative action of $N$ on $\alpha$, and - A proof that these actions commute (i.e., $m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $m \in M$, $n \in N$, $a \in \alpha$). The forward direction constructs the component actions via the inclusion homomorphisms $M \to M \times N$ and $N \to M \times N$, while the backward direction combines commuting actions into a product action.

See also