prodEquiv — Mathlib

English

There is an equivalence between a DistribMulAction on a product and the data of two commuting DistribMulActions on the factors, together with a commuting class.

Русский

Существует эквивалентность между DistribMulAction на произведении и данными двух коммутирующих DistribMulAction на множителях вместе с классом коммутируемости.

LaTeX

$$$\\text{DistribMulAction}(M \\times N) \\alpha \\simeq (\\text{DistribMulAction } M \\alpha) \\times' (\\text{DistribMulAction } N \\alpha) \\times' SMulCommClass M N \\alpha$$$

Lean4

/-- A `DistribMulAction` by a product monoid is equivalent to
  commuting `DistribMulAction`s by the factors. -/
def prodEquiv :
    DistribMulAction (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 ..

Похожие утверждения