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

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.

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))

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' := ⋯ }

instance StarMonoidHom.instMonoidHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] : MonoidHomClass (A →⋆* B) A B

instance StarMonoidHom.instStarHomClass {A : Type u_2} {B : Type u_3} [Monoid A] [Star A] [Monoid B] [Star B] : StarHomClass (A →⋆* B) A B

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

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' := ⋯ }

@[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

@[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

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

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

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' := ⋯ }

@[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'

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

@[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

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' := ⋯ }

@[simp]

theorem StarMonoidHom.coe_id (A : Type u_2) [Monoid A] [Star A] : ⇑(StarMonoidHom.id A) = id

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' := ⋯ }

@[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

@[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)

@[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)

@[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

@[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

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 := ⋯ }

@[simp]

theorem StarMonoidHom.coe_one {A : Type u_2} [Monoid A] [Star A] : ⇑1 = id

theorem StarMonoidHom.one_apply {A : Type u_2} [Monoid A] [Star A] (a : A) : 1 a = a

Star monoid equivalences

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.

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))

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' := ⋯ }

instance StarMulEquiv.instMulEquivClass {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] : MulEquivClass (A ≃⋆* B) A B

instance StarMulEquiv.instStarHomClass {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] : StarHomClass (A ≃⋆* B) A B

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

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

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' := ⋯ }

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

Equations

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

@[simp]

theorem StarMulEquiv.coe_refl {A : Type u_2} [Mul A] [Star A] : ⇑(StarMulEquiv.refl A) = id

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' := ⋯ }

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

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

@[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

@[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

theorem StarMulEquiv.symm_bijective {A : Type u_2} {B : Type u_3} [Mul A] [Mul B] [Star A] [Star B] : Function.Bijective symm

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

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' := ⋯ }

@[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✝

@[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

@[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

@[simp]

theorem StarMulEquiv.refl_symm {A : Type u_2} [Mul A] [Star A] : (StarMulEquiv.refl A).symm = StarMulEquiv.refl A

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' := ⋯ }

@[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

@[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

@[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)

@[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₁

@[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)

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

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

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' := ⋯ }

@[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

@[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

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' := ⋯ }

@[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

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