doc-next-gen

Mathlib.Algebra.Group.Action.Prod

Module docstring

{"# Prod instances for additive and multiplicative actions

This file defines instances for binary product of additive and multiplicative actions and provides scalar multiplication as a homomorphism from α × β to β.

Main declarations

  • smulMulHom/smulMonoidHom: Scalar multiplication bundled as a multiplicative/monoid homomorphism.

See also

  • Mathlib.Algebra.Group.Action.Option
  • Mathlib.Algebra.Group.Action.Pi
  • Mathlib.Algebra.Group.Action.Sigma
  • Mathlib.Algebra.Group.Action.Sum

Porting notes

The to_additive attribute can be used to generate both the smul and vadd lemmas from the corresponding pow lemmas, as explained on zulip here: https://leanprover.zulipchat.com/#narrow/near/316087838

This was not done as part of the port in order to stay as close as possible to the mathlib3 code. ","### Scalar multiplication as a homomorphism "}

Prod.isScalarTower instance
[SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (α × β)
Full source 
@[to_additive]
instance isScalarTower [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] :
    IsScalarTower M N (α × β) where
  smul_assoc _ _ _ := by ext <;> exact smul_assoc ..
Scalar Tower Structure on Product Types
Informal description
For types $M$, $N$, $\alpha$, and $\beta$, if $M$ acts on $N$ and $N$ acts on both $\alpha$ and $\beta$ in a compatible way (i.e., the actions form a scalar tower), then the product type $\alpha \times \beta$ also forms a scalar tower with respect to these actions. This means that for any $m \in M$, $n \in N$, and $(a, b) \in \alpha \times \beta$, the action satisfies $m \cdot (n \cdot (a, b)) = (m \cdot n) \cdot (a, b)$.
Prod.smulCommClass instance
[SMulCommClass M N α] [SMulCommClass M N β] : SMulCommClass M N (α × β)
Full source 
@[to_additive]
instance smulCommClass [SMulCommClass M N α] [SMulCommClass M N β] : SMulCommClass M N (α × β) where
  smul_comm _ _ _ := by ext <;> exact smul_comm ..
Commutativity of Scalar Multiplication on Product Types
Informal description
For types $M$, $N$, $\alpha$, and $\beta$, if the scalar multiplication operations of $M$ and $N$ commute on both $\alpha$ and $\beta$, then they also commute on the product type $\alpha \times \beta$. In other words, if for all $m \in M$, $n \in N$, $a \in \alpha$ we have $m \cdot (n \cdot a) = n \cdot (m \cdot a)$, and similarly for $\beta$, then the same property holds for pairs $(a, b) \in \alpha \times \beta$.
Prod.isCentralScalar instance
[SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] : IsCentralScalar M (α × β)
Full source 
@[to_additive]
instance isCentralScalar [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] :
    IsCentralScalar M (α × β) where
  op_smul_eq_smul _ _ := Prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)
Central Scalar Multiplication on Product Types
Informal description
For types $M$, $\alpha$, and $\beta$, if $\alpha$ and $\beta$ are both equipped with scalar multiplication by $M$ and its opposite $M^{\text{op}}$, and the scalar multiplication by $M$ is central on both $\alpha$ and $\beta$, then the scalar multiplication by $M$ is also central on the product type $\alpha \times \beta$. This means that for any $m \in M$ and $(a, b) \in \alpha \times \beta$, the scalar multiplication satisfies $m \cdot (a, b) = (m \cdot a, m \cdot b) = (a \cdot m, b \cdot m)$.
Prod.faithfulSMulLeft instance
[FaithfulSMul M α] [Nonempty β] : FaithfulSMul M (α × β)
Full source 
@[to_additive]
instance faithfulSMulLeft [FaithfulSMul M α] [Nonempty β] : FaithfulSMul M (α × β) where
  eq_of_smul_eq_smul h :=
    let ⟨b⟩ := ‹Nonempty β›
    eq_of_smul_eq_smul fun a : α => by injection h (a, b)
Faithful Scalar Multiplication on Left Component of Product Types
Informal description
For any type $M$ with a faithful scalar multiplication action on $\alpha$ and a nonempty type $\beta$, the scalar multiplication action of $M$ on the product type $\alpha \times \beta$ is also faithful.
Prod.faithfulSMulRight instance
[Nonempty α] [FaithfulSMul M β] : FaithfulSMul M (α × β)
Full source 
@[to_additive]
instance faithfulSMulRight [Nonempty α] [FaithfulSMul M β] : FaithfulSMul M (α × β) where
  eq_of_smul_eq_smul h :=
    let ⟨a⟩ := ‹Nonempty α›
    eq_of_smul_eq_smul fun b : β => by injection h (a, b)
Faithful Scalar Multiplication on Right Component of Product Types
Informal description
For any type $\alpha$ that is nonempty and any type $M$ with a faithful scalar multiplication action on $\beta$, the scalar multiplication action of $M$ on the product type $\alpha \times \beta$ is also faithful.
Prod.smulCommClassBoth instance
[Mul N] [Mul P] [SMul M N] [SMul M P] [SMulCommClass M N N] [SMulCommClass M P P] : SMulCommClass M (N × P) (N × P)
Full source 
@[to_additive]
instance smulCommClassBoth [Mul N] [Mul P] [SMul M N] [SMul M P] [SMulCommClass M N N]
    [SMulCommClass M P P] : SMulCommClass M (N × P) (N × P) where
  smul_comm c x y := by simp [smul_def, mul_def, mul_smul_comm]
Commutativity of Scalar Multiplication on Product Types
Informal description
For types $N$ and $P$ equipped with multiplication operations, and a type $M$ with scalar multiplication actions on both $N$ and $P$, if $M$ commutes with scalar multiplication on $N$ and $P$ individually, then $M$ also commutes with scalar multiplication on the product type $N \times P$.
Prod.isScalarTowerBoth instance
[Mul N] [Mul P] [SMul M N] [SMul M P] [IsScalarTower M N N] [IsScalarTower M P P] : IsScalarTower M (N × P) (N × P)
Full source 
instance isScalarTowerBoth [Mul N] [Mul P] [SMul M N] [SMul M P] [IsScalarTower M N N]
    [IsScalarTower M P P] : IsScalarTower M (N × P) (N × P) where
  smul_assoc c x y := by simp [smul_def, mul_def, smul_mul_assoc]
Scalar Tower Structure on Product Types
Informal description
For types $M$, $N$, and $P$ where $N$ and $P$ are equipped with multiplication operations, and $M$ acts on both $N$ and $P$ via scalar multiplication, if $M$ forms a scalar tower over $N$ (i.e., the scalar multiplication is compatible with the multiplication in $N$) and similarly for $P$, then $M$ also forms a scalar tower over the product type $N \times P$.
Prod.mulAction instance
[Monoid M] [MulAction M α] [MulAction M β] : MulAction M (α × β)
Full source 
@[to_additive]
instance mulAction [Monoid M] [MulAction M α] [MulAction M β] : MulAction M (α × β) where
  mul_smul _ _ _ := by ext <;> exact mul_smul ..
  one_smul _ := by ext <;> exact one_smul ..
Multiplicative Action on Product Types
Informal description
For any monoid $M$ and types $\alpha$ and $\beta$ with multiplicative actions of $M$, the product type $\alpha \times \beta$ inherits a multiplicative action of $M$ defined componentwise.
smulMulHom definition
[Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : α × β →ₙ* β
Full source 
/-- Scalar multiplication as a multiplicative homomorphism. -/
@[simps]
def smulMulHom [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] :
    α × βα × β →ₙ* β where
  toFun a := a.1 • a.2
  map_mul' _ _ := (smul_mul_smul_comm _ _ _ _).symm
Scalar multiplication as a multiplicative homomorphism
Informal description
Given a monoid $\alpha$ and a multiplicative structure $\beta$ with a multiplicative action of $\alpha$ on $\beta$ such that $\alpha$ forms a scalar tower over $\beta$ and the actions of $\alpha$ and $\beta$ commute, the function $\text{smulMulHom}$ maps a pair $(a, b) \in \alpha \times \beta$ to the scalar product $a \cdot b \in \beta$, and this function is a multiplicative homomorphism.
smulMonoidHom definition
[Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] : α × β →* β
Full source 
/-- Scalar multiplication as a monoid homomorphism. -/
@[simps]
def smulMonoidHom [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β]
    [SMulCommClass α β β] : α × βα × β →* β :=
  { smulMulHom with map_one' := one_smul _ _ }
Scalar multiplication as a monoid homomorphism
Informal description
Given a monoid $\alpha$ and a multiplicative monoid $\beta$ with a multiplicative action of $\alpha$ on $\beta$ such that $\alpha$ forms a scalar tower over $\beta$ and the actions of $\alpha$ and $\beta$ commute, the function $\text{smulMonoidHom}$ maps a pair $(a, b) \in \alpha \times \beta$ to the scalar product $a \cdot b \in \beta$. This function is a monoid homomorphism, meaning it preserves the multiplicative identity and the operation.
MulAction.prodOfSMulCommClass abbrev
[MulAction M α] [MulAction N α] [SMulCommClass M N α] : MulAction (M × N) α
Full source 
/-- Construct a `MulAction` by a product monoid from `MulAction`s by the factors.
  This is not an instance to avoid diamonds for example when `α := M × N`. -/
@[to_additive AddAction.prodOfVAddCommClass
"Construct an `AddAction` by a product monoid from `AddAction`s by the factors.
This is not an instance to avoid diamonds for example when `α := M × N`."]
abbrev MulAction.prodOfSMulCommClass [MulAction M α] [MulAction N α] [SMulCommClass M N α] :
    MulAction (M × N) α where
  smul mn a := mn.1 • mn.2 • a
  one_smul a := (one_smul M _).trans (one_smul N a)
  mul_smul x y a := by
    change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
    rw [mul_smul, mul_smul, smul_comm y.1 x.2]
Product Monoid Action from Commuting Actions
Informal description
Given monoids $M$ and $N$ acting multiplicatively on a type $\alpha$, and assuming these actions commute (i.e., $[SMulCommClass M N \alpha]$), there exists a multiplicative action of the product monoid $M \times N$ on $\alpha$ defined by $(m, n) \cdot a = m \cdot (n \cdot a) = n \cdot (m \cdot a)$ for all $(m, n) \in M \times N$ and $a \in \alpha$.
MulAction.prodEquiv definition
: MulAction (M × N) α ≃ Σ' (_ : MulAction M α) (_ : MulAction N α), SMulCommClass M N α
Full source 
/-- A `MulAction` by a product monoid is equivalent to commuting `MulAction`s by the factors. -/
@[to_additive AddAction.prodEquiv
"An `AddAction` by a product monoid is equivalent to commuting `AddAction`s by the factors."]
def MulAction.prodEquiv :
    MulActionMulAction (M × N) α ≃ Σ' (_ : MulAction M α) (_ : MulAction N α), SMulCommClass M N α where
  toFun _ :=
    letI instM := MulAction.compHom α (.inl M N)
    letI instN := MulAction.compHom α (.inr M N)
    ⟨instM, instN,
    { smul_comm := fun m n a ↦ by
        change (m, (1 : N)) • ((1 : M), n) • a = ((1 : M), n) • (m, (1 : N)) • a
        simp_rw [smul_smul, Prod.mk_mul_mk, mul_one, one_mul] }⟩
  invFun _insts :=
    letI := _insts.1; letI := _insts.2.1; have := _insts.2.2
    MulAction.prodOfSMulCommClass M N α
  left_inv := by
    rintro ⟨-, hsmul⟩; dsimp only; ext ⟨m, n⟩ a
    change (m, (1 : N)) • ((1 : M), n) • a = _
    rw [← hsmul, Prod.mk_mul_mk, mul_one, one_mul]; rfl
  right_inv := by
    rintro ⟨hM, hN, -⟩
    dsimp only; congr 1
    · ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    congr 1
    · funext; congr; ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl
    · ext n a; (conv_rhs => rw [← hM.one_smul (SMul.smul n a)]); rfl
    · exact proof_irrel_heq ..
Equivalence between product monoid actions and commuting actions
Informal description
The equivalence states that a multiplicative action of the product monoid $M \times N$ on a type $\alpha$ is equivalent to a pair of commuting multiplicative actions of $M$ and $N$ on $\alpha$. More precisely, the equivalence maps a multiplicative action of $M \times N$ on $\alpha$ to the following data: 1. A multiplicative action of $M$ on $\alpha$ obtained by composing with the left inclusion homomorphism $M \to M \times N$ (sending $m \mapsto (m,1)$) 2. A multiplicative action of $N$ on $\alpha$ obtained by composing with the right inclusion homomorphism $N \to M \times N$ (sending $n \mapsto (1,n)$) 3. 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$) Conversely, given such commuting actions of $M$ and $N$, we can reconstruct the action of $M \times N$ via $(m,n) \cdot a = m \cdot (n \cdot a) = n \cdot (m \cdot a)$.