# Morphisms of star monoids #

This file defines the type of morphisms `StarMonoidHom` between monoids `A` and `B` where both `A` and `B` are equipped with a `star` operation. These morphisms are star-preserving monoid homomorphisms and are equipped with the notation `A →⋆* B`.

The primary motivation for these morphisms is to provide a target type for morphisms which induce a corresponding morphism between the unitary groups in a star monoid.

## Main definitions #

- `StarMonoidHom`
- `StarMulEquiv`

## Tags #

monoid, star

### Star monoid homomorphisms #

source
structure StarMonoidHom (A : Type u_6) (B : Type u_7) [Monoid A] [Star A] [Monoid B] [Star B] extends A →* B :
Type (max u_6 u_7)

A star monoid homomorphism is a monoid homomorphism which is `star`-preserving.

- toFun : A → B
- map_one' : (↑self.toMonoidHom).toFun 1 = 1
- map_mul' (x y : A) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
- map_star' (a : A) : (↑self.toMonoidHom).toFun (star a) = star ((↑self.toMonoidHom).toFun a)

  By definition, a star monoid homomorphism preserves the `star` operation.

Instances For

source
def «term_→⋆*_» :
Lean.TrailingParserDescr

`α →⋆* β` denotes the type of star monoid homomorphisms from `α` to `β`.

Equations

- «term_→⋆*_» = Lean.ParserDescr.trailingNode `«term_→⋆*_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →⋆* ") (Lean.ParserDescr.cat `term 25))

Instances For

source
instance StarMonoidHom.instFunLike {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] :
FunLike (A →⋆* B) A B
Equations

- StarMonoidHom.instFunLike = { coe := fun (f : A →⋆* B) => (↑f.toMonoidHom).toFun, coe_injective' := ⋯ }

source
instance StarMonoidHom.instMonoidHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] :
MonoidHomClass (A →⋆* B) A B
source
instance StarMonoidHom.instStarHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] :
StarHomClass (A →⋆* B) A B
source
def StarMonoidHom.Simps.coe {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) :
A → B

See Note [custom simps projection]

Equations

- StarMonoidHom.Simps.coe f = ⇑f

Instances For

source
def StarMonoidHom.ofClass {F : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] [FunLike F A B] [MonoidHomClass F A B] [StarHomClass F A B] (f : F) :
A →⋆* B

Construct a `StarMonoidHom` from a morphism in some type which preserves `1`, `*` and `star`.

Equations

- StarMonoidHom.ofClass f = { toFun := ⇑f, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMonoidHom.ofClass_coe {F : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] [FunLike F A B] [MonoidHomClass F A B] [StarHomClass F A B] (f : F) (a : A) :
(ofClass f) a = f a
source
@[simp]
theorem StarMonoidHom.coe_toMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) :
⇑f.toMonoidHom = ⇑f
source
theorem StarMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] {f g : A →⋆* B} (h : ∀ (x : A), f x = g x) :
f = g
source
theorem StarMonoidHom.ext_iff {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] {f g : A →⋆* B} :
f = g ↔ ∀ (x : A), f x = g x
source
def StarMonoidHom.copy {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) (f' : A → B) (h : f' = ⇑f) :
A →⋆* B

Copy of a `StarMonoidHom` with a new `toFun` equal to the old one. Useful to fix definitional equalities.

Equations

- f.copy f' h = { toFun := f', map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMonoidHom.coe_copy {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) (f' : A → B) (h : f' = ⇑f) :
⇑(f.copy f' h) = f'
source
theorem StarMonoidHom.copy_eq {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) (f' : A → B) (h : f' = ⇑f) :
f.copy f' h = f
source
@[simp]
theorem StarMonoidHom.coe_mk {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →* B) (h : ∀ (a : A), (↑f).toFun (star a) = star ((↑f).toFun a)) :
⇑{ toMonoidHom := f, map_star' := h } = ⇑f
source
def StarMonoidHom.id (A : Type u_2) [Monoid A] [Star A] :
A →⋆* A

The identity as a star monoid homomorphism.

Equations

- StarMonoidHom.id A = { toMonoidHom := MonoidHom.id A, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMonoidHom.coe_id (A : Type u_2) [Monoid A] [Star A] :
⇑(StarMonoidHom.id A) = id
source
def StarMonoidHom.comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Star A] [Monoid B] [Star B] [Monoid C] [Star C] (f : B →⋆* C) (g : A →⋆* B) :
A →⋆* C

The composition of star monoid homomorphisms, as a star monoid homomorphism.

Equations

- f.comp g = { toMonoidHom := f.comp g.toMonoidHom, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMonoidHom.coe_comp {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Star A] [Monoid B] [Star B] [Monoid C] [Star C] (f : B →⋆* C) (g : A →⋆* B) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
@[simp]
theorem StarMonoidHom.comp_apply {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Star A] [Monoid B] [Star B] [Monoid C] [Star C] (f : B →⋆* C) (g : A →⋆* B) (a : A) :
(f.comp g) a = f (g a)
source
@[simp]
theorem StarMonoidHom.comp_assoc {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Star A] [Monoid B] [Star B] [Monoid C] [Star C] [Monoid D] [Star D] (f : C →⋆* D) (g : B →⋆* C) (h : A →⋆* B) :
(f.comp g).comp h = f.comp (g.comp h)
source
@[simp]
theorem StarMonoidHom.id_comp {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) :
(StarMonoidHom.id B).comp f = f
source
@[simp]
theorem StarMonoidHom.comp_id {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] (f : A →⋆* B) :
f.comp (StarMonoidHom.id A) = f
source
instance StarMonoidHom.instMonoid {A : Type u_2} [Monoid A] [Star A] :
Monoid (A →⋆* A)
Equations

- StarMonoidHom.instMonoid = { mul := StarMonoidHom.comp, mul_assoc := ⋯, one := StarMonoidHom.id A, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

source
@[simp]
theorem StarMonoidHom.coe_one {A : Type u_2} [Monoid A] [Star A] :
⇑1 = id
source
theorem StarMonoidHom.one_apply {A : Type u_2} [Monoid A] [Star A] (a : A) :
1 a = a

### Star monoid equivalences #

source
structure StarMulEquiv (A : Type u_6) (B : Type u_7) [Mul A] [Mul B] [Star A] [Star B] extends A ≃* B :
Type (max u_6 u_7)

A star monoid equivalence is an equivalence preserving multiplication and the star operation.

- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y
- map_star' (a : A) : self.toFun (star a) = star (self.toFun a)

  By definition, a star monoid equivalence preserves the `star` operation.

Instances For

source
def «term_≃⋆*_» :
Lean.TrailingParserDescr

A star monoid equivalence is an equivalence preserving multiplication and the star operation.

Equations

- «term_≃⋆*_» = Lean.ParserDescr.trailingNode `«term_≃⋆*_» 25 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃⋆* ") (Lean.ParserDescr.cat `term 0))

Instances For

source
instance StarMulEquiv.instEquivLike {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] :
EquivLike (A ≃⋆* B) A B
Equations

- StarMulEquiv.instEquivLike = { coe := fun (e : A ≃⋆* B) => e.toFun, inv := fun (e : A ≃⋆* B) => e.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source
instance StarMulEquiv.instMulEquivClass {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] :
MulEquivClass (A ≃⋆* B) A B
source
instance StarMulEquiv.instStarHomClass {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] :
StarHomClass (A ≃⋆* B) A B
source
theorem StarMulEquiv.ext {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] {f g : A ≃⋆* B} (h : ∀ (a : A), f a = g a) :
f = g
source
theorem StarMulEquiv.ext_iff {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] {f g : A ≃⋆* B} :
f = g ↔ ∀ (a : A), f a = g a
source
def StarMulEquiv.refl (A : Type u_2) [Mul A] [Star A] :
A ≃⋆* A

The identity map as a star monoid isomorphism.

Equations

- StarMulEquiv.refl A = { toMulEquiv := MulEquiv.refl A, map_star' := ⋯ }

Instances For

source
instance StarMulEquiv.instInhabited {A : Type u_2} [Mul A] [Star A] :
Inhabited (A ≃⋆* A)
Equations

- StarMulEquiv.instInhabited = { default := StarMulEquiv.refl A }

source
@[simp]
theorem StarMulEquiv.coe_refl {A : Type u_2} [Mul A] [Star A] :
⇑(StarMulEquiv.refl A) = id
source
def StarMulEquiv.symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
B ≃⋆* A

The inverse of a star monoid isomorphism is a star monoid isomorphism.

Equations

- e.symm = { toMulEquiv := e.symm, map_star' := ⋯ }

Instances For

source
def StarMulEquiv.Simps.apply {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
A → B

See Note [custom simps projection]

Equations

- StarMulEquiv.Simps.apply e = ⇑e

Instances For

source
def StarMulEquiv.Simps.symm_apply {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
B → A

See Note [custom simps projection]

Equations

- StarMulEquiv.Simps.symm_apply e = ⇑e.symm

Instances For

source
@[simp]
theorem StarMulEquiv.invFun_eq_symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] {e : A ≃⋆* B} :
EquivLike.inv e = ⇑e.symm
source
@[simp]
theorem StarMulEquiv.symm_symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
e.symm.symm = e
source
theorem StarMulEquiv.symm_bijective {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] :
Function.Bijective symm
source
theorem StarMulEquiv.coe_mk {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)) :
⇑{ toMulEquiv := e, map_star' := h₁ } = ⇑e
source
def StarMulEquiv.ofClass {F : Type u_1} {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] [EquivLike F A B] [MulEquivClass F A B] [StarHomClass F A B] (f : F) :
A ≃⋆* B

Construct a `StarMulEquiv` from an equivalence in some type which preserves `*` and `star`.

Equations

- StarMulEquiv.ofClass f = { toFun := ⇑f, invFun := EquivLike.inv f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMulEquiv.ofClass_apply {F : Type u_1} {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] [EquivLike F A B] [MulEquivClass F A B] [StarHomClass F A B] (f : F) (a : A) :
(ofClass f) a = f a
source
@[simp]
theorem StarMulEquiv.ofClass_symm_apply {F : Type u_1} {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] [EquivLike F A B] [MulEquivClass F A B] [StarHomClass F A B] (f : F) (a✝ : B) :
(ofClass f).symm a✝ = EquivLike.inv f a✝
source
@[simp]
theorem StarMulEquiv.coe_toMulEquiv {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (f : A ≃⋆* B) :
⇑f.toMulEquiv = ⇑f
source
@[simp]
theorem StarMulEquiv.toMulEquiv_symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (f : A ≃⋆* B) :
f.symm.toMulEquiv = f.symm
source
@[simp]
theorem StarMulEquiv.refl_symm {A : Type u_2} [Mul A] [Star A] :
(StarMulEquiv.refl A).symm = StarMulEquiv.refl A
source
def StarMulEquiv.trans {A : Type u_2} {B : Type u_3} {C : Type u_4} [Mul A] [Mul B] [Mul C] [Star A] [Star B] [Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) :
A ≃⋆* C

Transitivity of `StarMulEquiv`.

Equations

- e₁.trans e₂ = { toMulEquiv := e₁.trans e₂.toMulEquiv, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMulEquiv.apply_symm_apply {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) (x : B) :
e (e.symm x) = x
source
@[simp]
theorem StarMulEquiv.symm_apply_apply {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) (x : A) :
e.symm (e x) = x
source
@[simp]
theorem StarMulEquiv.symm_trans_apply {A : Type u_2} {B : Type u_3} {C : Type u_4} [Mul A] [Mul B] [Mul C] [Star A] [Star B] [Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) (x : C) :
(e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
source
@[simp]
theorem StarMulEquiv.coe_trans {A : Type u_2} {B : Type u_3} {C : Type u_4} [Mul A] [Mul B] [Mul C] [Star A] [Star B] [Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
@[simp]
theorem StarMulEquiv.trans_apply {A : Type u_2} {B : Type u_3} {C : Type u_4} [Mul A] [Mul B] [Mul C] [Star A] [Star B] [Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) (x : A) :
(e₁.trans e₂) x = e₂ (e₁ x)
source
@[simp]
theorem StarMulEquiv.toMulEquiv_trans {A : Type u_2} {B : Type u_3} {C : Type u_4} [Mul A] [Mul B] [Mul C] [Star A] [Star B] [Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) :
(e₁.trans e₂).toMulEquiv = e₁.trans e₂.toMulEquiv
source
theorem StarMulEquiv.leftInverse_symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
Function.LeftInverse ⇑e.symm ⇑e
source
theorem StarMulEquiv.rightInverse_symm {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] (e : A ≃⋆* B) :
Function.RightInverse ⇑e.symm ⇑e
source
def StarMulEquiv.toStarMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A ≃⋆* B) :
A →⋆* B

Reinterpret a `StarMulEquiv` as a `StarMonoidHom`.

Equations

- f.toStarMonoidHom = { toFun := ⇑f, map_one' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMulEquiv.toStarMonoidHom_coe {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A ≃⋆* B) (a : A) :
f.toStarMonoidHom a = f a
source
def StarMulEquiv.ofStarMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A →⋆* B) (g : B →⋆* A) (h₁ : g.comp f = StarMonoidHom.id A) (h₂ : f.comp g = StarMonoidHom.id B) :
A ≃⋆* B

If a star monoid morphism has an inverse, it is an isomorphism of star monoids.

Equations

- StarMulEquiv.ofStarMonoidHom f g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMulEquiv.ofStarMonoidHom_apply {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A →⋆* B) (g : B →⋆* A) (h₁ : g.comp f = StarMonoidHom.id A) (h₂ : f.comp g = StarMonoidHom.id B) (a : A) :
(ofStarMonoidHom f g h₁ h₂) a = f a
source
@[simp]
theorem StarMulEquiv.ofStarMonoidHom_symm_apply {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A →⋆* B) (g : B →⋆* A) (h₁ : g.comp f = StarMonoidHom.id A) (h₂ : f.comp g = StarMonoidHom.id B) (a : B) :
(ofStarMonoidHom f g h₁ h₂).symm a = g a
source
noncomputable def StarMulEquiv.ofBijective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A →⋆* B) (hf : Function.Bijective ⇑f) :
A ≃⋆* B

Promote a bijective star monoid homomorphism to a star monoid equivalence.

Equations

- StarMulEquiv.ofBijective f hf = { toFun := ⇑f, invFun := (MulEquiv.ofBijective f hf).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_star' := ⋯ }

Instances For

source
@[simp]
theorem StarMulEquiv.coe_ofBijective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] {f : A →⋆* B} (hf : Function.Bijective ⇑f) :
⇑(ofBijective f hf) = ⇑f
source
theorem StarMulEquiv.ofBijective_apply {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] {f : A →⋆* B} (hf : Function.Bijective ⇑f) (a : A) :
(ofBijective f hf) a = f a