Morphisms of non-unital algebras #
This file defines morphisms between two types, each of which carries:
- an addition,
- an additive zero,
- 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
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_equiv when needed.
Main definitions #
non-unital, algebra, morphism
- to_fun : A → B
- map_smul' : ∀ (m : R) (x : A), self.to_fun (m • x) = m • self.to_fun x
- map_zero' : self.to_fun 0 = 0
- map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
- map_mul' : ∀ (x y : A), self.to_fun (x * y) = (self.to_fun x) * self.to_fun y
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.
The composition of morphisms is a morphism.
The inverse of a bijective morphism is a morphism.
A unital morphism of algebras is a