English
A MulAction by a product monoid M × N on α is equivalent to a Sigma-type consisting of a MulAction M on α, a MulAction N on α, and a SMulCommClass M N α. This expresses that an action of the product is the same as two commuting actions by the factors together with a compatibility condition.
Русский
Действие произведения моноидов M × N на α эквивалентно суммарному типу, состоящему из действия M на α, действия N на α и совместимости SMulCommClass M N α. Это выражает, что действие произведения равно двум несовместимо действующим факторам с условием совместимости.
LaTeX
$$$\text{MulAction } (\,M \times N\,) \alpha \ \simeq\ \Sigma' (\text{MulAction } M \alpha) (\text{MulAction } N \alpha) (\text{SMulCommClass } M N \alpha).$$$
Lean4
/-- 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 prodEquiv : MulAction (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 ..
