Morphisms of non-unital algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
- coe : F → Π (a : A), (λ (_x : A), B) a
- coe_injective' : function.injective non_unital_alg_hom_class.coe
- map_smul : ∀ (f : F) (c : R) (x : A), ⇑f (c • x) = c • ⇑f x
- map_add : ∀ (f : F) (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y
- map_zero : ∀ (f : F), ⇑f 0 = 0
- map_mul : ∀ (f : F) (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y
non_unital_alg_hom_class F R A B asserts
F is a type of bundled algebra homomorphisms
Instances of this typeclass
Instances of other typeclasses for
The composition of morphisms is a morphism.
The inverse of a bijective morphism is a morphism.
The first projection of a product is a non-unital alg_hom.
The second projection of a product is a non-unital alg_hom.
The prod of two morphisms is a morphism.
Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.
The left injection into a product is a non-unital algebra homomorphism.
The right injection into a product is a non-unital algebra homomorphism.
A unital morphism of algebras is a