Unitary elements in a product

The unitary elements of a product of star monoids are the pairs of unitary elements. This file packages that identification as a multiplicative equivalence.

Main definition

• Unitary.prodEquiv: unitary (A × B) is multiplicatively equivalent to unitary A × unitary B.

def Unitary.prodEquiv (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [StarMul A] [StarMul B] : ↥(unitary (A × B)) ≃* ↥(unitary A) × ↥(unitary B)

Unitary elements in a product are pairs of unitary elements.

Equations

• Unitary.prodEquiv A B = (Unitary.equivProdSubmonoid✝ A B).trans ((unitary A).prodEquiv (unitary B))

@[simp]

theorem Unitary.coe_prodEquiv_apply (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [StarMul A] [StarMul B] (u : ↥(unitary (A × B))) : (↑((prodEquiv A B) u).1, ↑((prodEquiv A B) u).2) = ↑u

The product underlying the forward unitary-product equivalence is unchanged.

@[simp]

theorem Unitary.coe_prodEquiv_symm_apply (A : Type u_1) (B : Type u_2) [Monoid A] [Monoid B] [StarMul A] [StarMul B] (u : ↥(unitary A) × ↥(unitary B)) : ↑((prodEquiv A B).symm u) = (↑u.1, ↑u.2)

The product underlying the inverse unitary-product equivalence is the pair of underlying unitary elements.