# mathlibdocumentation

algebra.non_unital_alg_hom

# Morphisms of non-unital algebras #

This file defines morphisms between two types, each of which carries:

• a multiplication,
• a scalar action.

The multiplications are not assumed to be associative or unital, or even to be compatible with the scalar actions. In a typical application, the operations will satisfy compatibility conditions making them into algebras (albeit possibly non-associative and/or non-unital) but such conditions are not required to make this definition.

This notion of morphism should be useful for any category of non-unital algebras. The motivating application at the time it was introduced was to be able to state the adjunction property for magma algebras. These are non-unital, non-associative algebras obtained by applying the group-algebra construction except where we take a type carrying just has_mul instead of group.

For a plausible future application, one could take the non-unital algebra of compactly-supported functions on a non-compact topological space. A proper map between a pair of such spaces (contravariantly) induces a morphism between their algebras of compactly-supported functions which will be a non_unital_alg_hom.

TODO: add non_unital_alg_equiv when needed.

## Main definitions #

• non_unital_alg_hom
• alg_hom.to_non_unital_alg_hom

## Tags #

non-unital, algebra, morphism

@[nolint]
def non_unital_alg_hom.to_mul_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (self : B) :
B
structure non_unital_alg_hom (R : Type u) (A : Type v) (B : Type w) [monoid R] [ A] [ B] :
Type (max v w)

A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras.

@[nolint]
def non_unital_alg_hom.to_distrib_mul_action_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (self : B) :
A →+[R] B
@[instance]
def non_unital_alg_hom.has_coe_to_fun {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
Equations
@[simp]
theorem non_unital_alg_hom.to_fun_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
theorem non_unital_alg_hom.coe_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
@[ext]
theorem non_unital_alg_hom.ext {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] {f g : B} (h : ∀ (x : A), f x = g x) :
f = g
theorem non_unital_alg_hom.ext_iff {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] {f g : B} :
f = g ∀ (x : A), f x = g x
theorem non_unital_alg_hom.congr_fun {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] {f g : B} (h : f = g) (x : A) :
f x = g x
@[simp]
theorem non_unital_alg_hom.coe_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : A → B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = (f x) * f y) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄} = f
@[simp]
theorem non_unital_alg_hom.mk_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = (f x) * f y) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄} = f
@[instance]
def non_unital_alg_hom.distrib_mul_action_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
has_coe B) (A →+[R] B)
Equations
@[instance]
def non_unital_alg_hom.mul_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
has_coe B) (mul_hom A B)
Equations
@[simp]
theorem non_unital_alg_hom.to_distrib_mul_action_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
@[simp]
theorem non_unital_alg_hom.to_mul_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
@[simp]
theorem non_unital_alg_hom.coe_to_distrib_mul_action_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
@[simp]
theorem non_unital_alg_hom.coe_to_mul_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
theorem non_unital_alg_hom.to_distrib_mul_action_hom_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] {f g : B} (h : f = g) :
f = g
theorem non_unital_alg_hom.to_mul_hom_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] {f g : B} (h : f = g) :
f = g
theorem non_unital_alg_hom.coe_distrib_mul_action_hom_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = (f x) * f y) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄} = {to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃}
theorem non_unital_alg_hom.coe_mul_hom_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = (f x) * f y) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄} = {to_fun := f, map_mul' := h₄}
@[simp]
theorem non_unital_alg_hom.map_smul {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (c : R) (x : A) :
f (c x) = c f x
@[simp]
theorem non_unital_alg_hom.map_add {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (x y : A) :
f (x + y) = f x + f y
@[simp]
theorem non_unital_alg_hom.map_mul {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (x y : A) :
f (x * y) = (f x) * f y
@[simp]
theorem non_unital_alg_hom.map_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) :
f 0 = 0
@[instance]
def non_unital_alg_hom.has_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
Equations
@[instance]
def non_unital_alg_hom.has_one {R : Type u} {A : Type v} [monoid R] [ A] :
Equations
@[simp]
theorem non_unital_alg_hom.coe_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
0 = 0
@[simp]
theorem non_unital_alg_hom.coe_one {R : Type u} {A : Type v} [monoid R] [ A] :
theorem non_unital_alg_hom.zero_apply {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (a : A) :
0 a = 0
theorem non_unital_alg_hom.one_apply {R : Type u} {A : Type v} [monoid R] [ A] (a : A) :
1 a = a
@[instance]
def non_unital_alg_hom.inhabited {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] :
Equations
def non_unital_alg_hom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [ A] [ B] [ C] (f : C) (g : B) :
C

The composition of morphisms is a morphism.

Equations
@[simp]
theorem non_unital_alg_hom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [ A] [ B] [ C] (f : C) (g : B) :
(f.comp g) = f g
theorem non_unital_alg_hom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [ A] [ B] [ C] (f : C) (g : B) (x : A) :
(f.comp g) x = f (g x)
def non_unital_alg_hom.inverse {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (g : B → A) (h₁ : f) (h₂ : f) :
A

The inverse of a bijective morphism is a morphism.

Equations
@[simp]
theorem non_unital_alg_hom.coe_inverse {R : Type u} {A : Type v} {B : Type w} [monoid R] [ A] [ B] (f : B) (g : B → A) (h₁ : f) (h₂ : f) :
(f.inverse g h₁ h₂) = g
def alg_hom.to_non_unital_alg_hom {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) :
B

A unital morphism of algebras is a non_unital_alg_hom.

Equations
@[instance]
def alg_hom.non_unital_alg_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] :
has_coe (A →ₐ[R] B) B)
Equations
@[simp]
theorem alg_hom.to_non_unital_alg_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) :
@[simp]
theorem alg_hom.coe_to_non_unital_alg_hom {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) :