Documentation

Mathlib.Algebra.Star.MonoidHom

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.

Instances For

def «term_→⋆*_» :

Lean.TrailingParserDescr

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

Instances For

@[implicit_reducible]

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]

Instances For

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

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

Instances For

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

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

Instances For

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

The identity as a star monoid homomorphism.

Instances For

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

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

Instances For

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

@[implicit_reducible]

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.

Instances For

def «term_≃⋆*_» :

Lean.TrailingParserDescr

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

Instances For

@[implicit_reducible]

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] :

The identity map as a star monoid isomorphism.

Instances For

@[implicit_reducible]

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

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

Instances For

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]

Instances For

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]

Instances For

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

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

Instances For

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

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

Transitivity of StarMulEquiv.

Instances For

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

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

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.toStarMonoidHom {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [Star A] [Star B] (f : A ≃⋆* B) :

Reinterpret a StarMulEquiv as a StarMonoidHom.

Instances For

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

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

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

Instances For

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

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

Instances For

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