Unitary elements of a star monoid #
This file defines unitary R
, where R
is a star monoid, as the submonoid made of the elements
that satisfy star U * U = 1
and U * star U = 1
, and these form a group.
This includes, for instance, unitary operators on Hilbert spaces.
See also Matrix.UnitaryGroup
for specializations to unitary (Matrix n n R)
.
Tags #
unitary
In a *-monoid, unitary R
is the submonoid consisting of all the elements U
of
R
such that star U * U = 1
and U * star U = 1
.
Equations
Instances For
Equations
- unitary.instInvolutiveStarSubtypeMemSubmonoid = { toStar := unitary.instStarSubtypeMemSubmonoid, star_involutive := ⋯ }
Equations
- unitary.instStarMulSubtypeMemSubmonoid = { toInvolutiveStar := unitary.instInvolutiveStarSubtypeMemSubmonoid, star_mul := ⋯ }
unitary
as a Subgroup
of a group.
Note the group structure on this type is not defeq to the one on unitary
.
This situation naturally arises when considering the unitary elements as a
subgroup of the group of units of a star monoid.
Equations
- unitarySubgroup G = { toSubmonoid := unitary G, inv_mem' := ⋯ }
Instances For
Equations
- unitary.instMulActionSubtypeMemSubmonoid = { toSMul := unitary.instSMulSubtypeMemSubmonoid, one_smul := ⋯, mul_smul := ⋯ }
The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of the underlying star monoids.
Equations
- unitary.map f = { toFun := Subtype.map ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }
Instances For
The star monoid isomorphism between unitary subgroups induced by a star monoid isomorphism of the underlying star monoids.
Equations
- unitary.mapEquiv f = { toFun := ⇑(unitary.map f.toStarMonoidHom), invFun := ⇑(unitary.map f.symm.toStarMonoidHom), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_star' := ⋯ }
Instances For
The unitary subgroup of the units is equivalent to the unitary elements of the monoid.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- unitary.instCommGroupSubtypeMemSubmonoid = { toGroup := inferInstanceAs (Group ↥(unitary R)), mul_comm := ⋯ }
Equations
- unitary.instHasDistribNegSubtypeMemSubmonoid = Function.Injective.hasDistribNeg (fun (a : ↥(unitary R)) => ↑a) ⋯ ⋯ ⋯