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 β.

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

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]

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.

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

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

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

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

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

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

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.

instance StarMulEquiv.instInhabited {A : Type u_2} [Mul A] [Star A] : Inhabited (A ≃⋆* 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.

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]

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]

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

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

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

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

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