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
instance
unitary.instStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
instance
unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
unitary.instInvolutiveStarSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
InvolutiveStar { x // x ∈ unitary R }
instance
unitary.instStarSemigroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitaryToSemigroupToSemigroupToMulMemClassInstSubmonoidClassSubmonoidInstSetLikeSubmonoid
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
StarSemigroup { x // x ∈ unitary R }
Equations
- One or more equations did not get rendered due to their size.
instance
unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
Equations
- unitary.instInhabitedSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary = { default := 1 }
theorem
unitary.star_eq_inv'
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
star = Inv.inv
@[simp]
theorem
unitary.toUnits_apply_val
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
(x : { x // x ∈ unitary R })
:
↑(↑unitary.toUnits x) = ↑x
@[simp]
theorem
unitary.toUnits_apply_inv
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
(x : { x // x ∈ unitary R })
:
The unitary elements embed into the units.
Equations
- One or more equations did not get rendered due to their size.
theorem
unitary.to_units_injective
{R : Type u_1}
[inst : Monoid R]
[inst : StarSemigroup R]
:
Function.Injective ↑unitary.toUnits
instance
unitary.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidUnitary
{R : Type u_1}
[inst : CommMonoid R]
[inst : StarSemigroup R]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
unitary.mem_iff_star_mul_self
{R : Type u_1}
[inst : CommMonoid R]
[inst : StarSemigroup R]
{U : R}
:
theorem
unitary.mem_iff_self_mul_star
{R : Type u_1}
[inst : CommMonoid R]
[inst : StarSemigroup R]
{U : R}
:
theorem
unitary.coe_inv
{R : Type u_1}
[inst : GroupWithZero R]
[inst : StarSemigroup R]
(U : { x // x ∈ unitary R })
:
theorem
unitary.coe_div
{R : Type u_1}
[inst : GroupWithZero R]
[inst : StarSemigroup R]
(U₁ : { x // x ∈ unitary R })
(U₂ : { x // x ∈ unitary R })
:
theorem
unitary.coe_zpow
{R : Type u_1}
[inst : GroupWithZero R]
[inst : StarSemigroup R]
(U : { x // x ∈ unitary R })
(z : ℤ)
:
instance
unitary.instNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarSemigroupToNonUnitalSemiringToNonUnitalRing
{R : Type u_1}
[inst : Ring R]
[inst : StarRing R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
unitary.instHasDistribNegSubtypeMemSubmonoidToMulOneClassToMonoidToMonoidWithZeroToSemiringInstMembershipInstSetLikeSubmonoidUnitaryToStarSemigroupToNonUnitalSemiringToNonUnitalRingMul
{R : Type u_1}
[inst : Ring R]
[inst : StarRing R]
:
HasDistribNeg { x // x ∈ unitary R }
Equations
- One or more equations did not get rendered due to their size.