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

source

def unitary (R : Type u_1) [Monoid R] [StarMul R] :

Submonoid R

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

unitary R = { carrier := {U : R | star U * U = 1 ∧ U * star U = 1}, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source

theorem unitary.mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :

U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1

source

@[simp]

theorem unitary.star_mul_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :

star U * U = 1

source

@[simp]

theorem unitary.mul_star_self_of_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :

U * star U = 1

source

theorem unitary.star_mem {R : Type u_1} [Monoid R] [StarMul R] {U : R} (hU : U ∈ unitary R) :

star U ∈ unitary R

source

@[simp]

theorem unitary.star_mem_iff {R : Type u_1} [Monoid R] [StarMul R] {U : R} :

star U ∈ unitary R ↔ U ∈ unitary R

source

instance unitary.instStarSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] :

Star ↥(unitary R)

Equations

unitary.instStarSubtypeMemSubmonoid = { star := fun (U : ↥(unitary R)) => ⟨star ↑U, ⋯⟩ }

source

@[simp]

theorem unitary.coe_star {R : Type u_1} [Monoid R] [StarMul R] {U : ↥(unitary R)} :

↑(star U) = star ↑U

source

theorem unitary.coe_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :

star ↑U * ↑U = 1

source

theorem unitary.coe_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :

↑U * ↑(star U) = 1

source

@[simp]

theorem unitary.star_mul_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :

star U * U = 1

source

@[simp]

theorem unitary.mul_star_self {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :

U * star U = 1

source

instance unitary.instGroupSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] :

Group ↥(unitary R)

Equations

One or more equations did not get rendered due to their size.

source

instance unitary.instInvolutiveStarSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] :

InvolutiveStar ↥(unitary R)

Equations

unitary.instInvolutiveStarSubtypeMemSubmonoid = { toStar := unitary.instStarSubtypeMemSubmonoid, star_involutive := ⋯ }

source

instance unitary.instStarMulSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] :

StarMul ↥(unitary R)

Equations

unitary.instStarMulSubtypeMemSubmonoid = { toInvolutiveStar := unitary.instInvolutiveStarSubtypeMemSubmonoid, star_mul := ⋯ }

source

instance unitary.instInhabitedSubtypeMemSubmonoid {R : Type u_1} [Monoid R] [StarMul R] :

Inhabited ↥(unitary R)

Equations

unitary.instInhabitedSubtypeMemSubmonoid = { default := 1 }

source

theorem unitary.star_eq_inv {R : Type u_1} [Monoid R] [StarMul R] (U : ↥(unitary R)) :

star U = U⁻¹

source

theorem unitary.star_eq_inv' {R : Type u_1} [Monoid R] [StarMul R] :

star = Inv.inv

source

def unitary.toUnits {R : Type u_1} [Monoid R] [StarMul R] :

↥(unitary R) →* Rˣ

The unitary elements embed into the units.

Equations

unitary.toUnits = { toFun := fun (x : ↥(unitary R)) => { val := ↑x, inv := ↑x⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem unitary.val_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :

↑(toUnits x) = ↑x

source

@[simp]

theorem unitary.val_inv_toUnits_apply {R : Type u_1} [Monoid R] [StarMul R] (x : ↥(unitary R)) :

↑(toUnits x)⁻¹ = ↑x⁻¹

source

theorem unitary.toUnits_injective {R : Type u_1} [Monoid R] [StarMul R] :

Function.Injective ⇑toUnits

source

theorem IsUnit.mem_unitary_iff_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :

u ∈ unitary R ↔ star u * u = 1

source

theorem IsUnit.mem_unitary_iff_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :

u ∈ unitary R ↔ u * star u = 1

source

theorem IsUnit.mem_unitary_of_star_mul_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :

star u * u = 1 → u ∈ unitary R

Alias of the reverse direction of IsUnit.mem_unitary_iff_star_mul_self.

source

theorem IsUnit.mem_unitary_of_mul_star_self {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : IsUnit u) :

u * star u = 1 → u ∈ unitary R

Alias of the reverse direction of IsUnit.mem_unitary_iff_mul_star_self.

source

theorem unitary.mul_left_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :

x * ↑U = y * ↑U ↔ x = y

For unitary U in a star-monoid R, x * U = y * U if and only if x = y for all x and y in R.

source

theorem unitary.mul_right_inj {R : Type u_1} [Monoid R] [StarMul R] {x y : R} (U : ↥(unitary R)) :

↑U * x = ↑U * y ↔ x = y

For unitary U in a star-monoid R, U * x = U * y if and only if x = y for all x and y in R.

source

theorem unitary.mul_inv_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :

a * b⁻¹ ∈ unitary G ↔ star a * a = star b * b

source

theorem unitary.inv_mul_mem_iff {G : Type u_2} [Group G] [StarMul G] (a b : G) :

a⁻¹ * b ∈ unitary G ↔ a * star a = b * star b

source

theorem Units.unitary_eq {R : Type u_1} [Monoid R] [StarMul R] :

unitary Rˣ = Submonoid.comap (coeHom R) (unitary R)

source

theorem Units.mul_inv_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :

↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

In a star monoid, the product a * b⁻¹ of units is unitary if star a * a = star b * b.

source

theorem Units.inv_mul_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] (a b : Rˣ) :

↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b

In a star monoid, the product a⁻¹ * b of units is unitary if a * star a = b * star b.

source

instance unitary.instIsStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :

IsStarNormal u

source

instance unitary.coe_isStarNormal {R : Type u_1} [Monoid R] [StarMul R] (u : ↥(unitary R)) :

IsStarNormal ↑u

source

theorem isStarNormal_of_mem_unitary {R : Type u_1} [Monoid R] [StarMul R] {u : R} (hu : u ∈ unitary R) :

IsStarNormal u

source

theorem unitary.smul_mem_of_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] {r : R} {a : A} (hr : r ∈ unitary R) (ha : a ∈ unitary A) :

r • a ∈ unitary A

source

theorem unitary.smul_mem {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) {a : A} (ha : a ∈ unitary A) :

r • a ∈ unitary A

source

instance unitary.instSMulSubtypeMemSubmonoid {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :

SMul ↥(unitary R) ↥(unitary A)

Equations

unitary.instSMulSubtypeMemSubmonoid = { smul := fun (r : ↥(unitary R)) (a : ↥(unitary A)) => ⟨r • ↑a, ⋯⟩ }

source

@[simp]

theorem unitary.coe_smul {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] (r : ↥(unitary R)) (a : ↥(unitary A)) :

↑(r • a) = r • ↑a

source

instance unitary.instMulActionSubtypeMemSubmonoid {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :

MulAction ↥(unitary R) ↥(unitary A)

Equations

unitary.instMulActionSubtypeMemSubmonoid = { toSMul := unitary.instSMulSubtypeMemSubmonoid, one_smul := ⋯, mul_smul := ⋯ }

source

instance unitary.instStarModuleSubtypeMemSubmonoid {R : Type u_1} {A : Type u_2} [Monoid R] [Monoid A] [MulAction R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarMul R] [StarMul A] [StarModule R A] :

StarModule ↥(unitary R) ↥(unitary A)

source

instance unitary.instSMulCommClassSubtypeMemSubmonoid {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R A] [MulAction S A] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [SMulCommClass R S A] :

SMulCommClass ↥(unitary R) ↥(unitary S) ↥(unitary A)

source

instance unitary.instIsScalarTowerSubtypeMemSubmonoid {R : Type u_1} {S : Type u_2} {A : Type u_3} [Monoid R] [Monoid S] [Monoid A] [StarMul R] [StarMul S] [StarMul A] [MulAction R S] [MulAction R A] [MulAction S A] [StarModule R S] [StarModule R A] [StarModule S A] [IsScalarTower R A A] [IsScalarTower S A A] [SMulCommClass R A A] [SMulCommClass S A A] [IsScalarTower R S S] [SMulCommClass R S S] [IsScalarTower R S A] :

IsScalarTower ↥(unitary R) ↥(unitary S) ↥(unitary A)

source

theorem unitary.map_mem {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {F : Type u_5} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R} (hr : r ∈ unitary R) :

f r ∈ unitary S

source

def unitary.map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :

↥(unitary R) →⋆* ↥(unitary S)

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

source

@[simp]

theorem unitary.map_coe {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (a✝ : ↥(unitary R)) :

(map f) a✝ = Subtype.map ⇑f ⋯ a✝

source

@[simp]

theorem unitary.coe_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :

↑((map f) x) = f ↑x

source

@[simp]

theorem unitary.coe_map_star {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) (x : ↥(unitary R)) :

↑((map f) (star x)) = f (star ↑x)

source

@[simp]

theorem unitary.map_id {R : Type u_2} [Monoid R] [StarMul R] :

map (StarMonoidHom.id R) = StarMonoidHom.id ↥(unitary R)

source

theorem unitary.map_comp {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (g : S →⋆* T) (f : R →⋆* S) :

map (g.comp f) = (map g).comp (map f)

source

@[simp]

theorem unitary.map_injective {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] {f : R →⋆* S} (hf : Function.Injective ⇑f) :

Function.Injective ⇑(map f)

source

theorem unitary.toUnits_comp_map {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R →⋆* S) :

toUnits.comp (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits

source

def unitary.mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :

↥(unitary R) ≃⋆* ↥(unitary S)

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

source

@[simp]

theorem unitary.mapEquiv_symm_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary S)) :

(mapEquiv f).symm a = (map f.symm.toStarMonoidHom) a

source

@[simp]

theorem unitary.mapEquiv_apply {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) (a : ↥(unitary R)) :

(mapEquiv f) a = (map f.toStarMonoidHom) a

source

@[simp]

theorem unitary.mapEquiv_refl {R : Type u_2} [Monoid R] [StarMul R] :

mapEquiv (StarMulEquiv.refl R) = StarMulEquiv.refl ↥(unitary R)

source

@[simp]

theorem unitary.mapEquiv_symm {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :

mapEquiv f.symm = (mapEquiv f).symm

source

@[simp]

theorem unitary.mapEquiv_trans {R : Type u_2} {S : Type u_3} {T : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [Monoid T] [StarMul T] (f : R ≃⋆* S) (g : S ≃⋆* T) :

mapEquiv (f.trans g) = (mapEquiv f).trans (mapEquiv g)

source

@[simp]

theorem unitary.toMonoidHom_mapEquiv {R : Type u_2} {S : Type u_3} [Monoid R] [StarMul R] [Monoid S] [StarMul S] (f : R ≃⋆* S) :

(mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom

source

instance unitary.instCommGroupSubtypeMemSubmonoid {R : Type u_1} [CommMonoid R] [StarMul R] :

CommGroup ↥(unitary R)

Equations

unitary.instCommGroupSubtypeMemSubmonoid = { toGroup := inferInstanceAs (Group ↥(unitary R)), mul_comm := ⋯ }

source

theorem unitary.mem_iff_star_mul_self {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :

U ∈ unitary R ↔ star U * U = 1

source

theorem unitary.mem_iff_self_mul_star {R : Type u_1} [CommMonoid R] [StarMul R] {U : R} :

U ∈ unitary R ↔ U * star U = 1

source

theorem unitary.coe_inv {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) :

↑U⁻¹ = (↑U)⁻¹

source

theorem unitary.coe_div {R : Type u_1} [GroupWithZero R] [StarMul R] (U₁ U₂ : ↥(unitary R)) :

↑(U₁ / U₂) = ↑U₁ / ↑U₂

source

theorem unitary.coe_zpow {R : Type u_1} [GroupWithZero R] [StarMul R] (U : ↥(unitary R)) (z : ℤ) :

↑(U ^ z) = ↑U ^ z

source

instance unitary.instNegSubtypeMemSubmonoid {R : Type u_1} [Ring R] [StarRing R] :

Neg ↥(unitary R)

Equations

unitary.instNegSubtypeMemSubmonoid = { neg := fun (U : ↥(unitary R)) => ⟨-↑U, ⋯⟩ }

source

theorem unitary.coe_neg {R : Type u_1} [Ring R] [StarRing R] (U : ↥(unitary R)) :

↑(-U) = -↑U

source

instance unitary.instHasDistribNegSubtypeMemSubmonoid {R : Type u_1} [Ring R] [StarRing R] :

HasDistribNeg ↥(unitary R)

Equations

unitary.instHasDistribNegSubtypeMemSubmonoid = Function.Injective.hasDistribNeg (fun (a : ↥(unitary R)) => ↑a) ⋯ ⋯ ⋯

source

@[simp]

theorem unitary.spectrum.unitary_conjugate {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : ↥(unitary A)} :

spectrum R (↑u * a * star ↑u) = spectrum R a

Unitary conjugation preserves the spectrum, star on left.

source

@[simp]

theorem unitary.spectrum.unitary_conjugate' {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [StarMul A] {a : A} {u : ↥(unitary A)} :

spectrum R (star ↑u * a * ↑u) = spectrum R a

Unitary conjugation preserves the spectrum, star on right.

source

theorem IsStarProjection.two_mul_sub_one_mem_unitary {R : Type u_2} [Ring R] [StarRing R] {p : R} (hp : IsStarProjection p) :

2 * p - 1 ∈ unitary R

Documentation

Mathlib.Algebra.Star.Unitary

Unitary elements of a star monoid #

Tags #