mathlib3 documentation

algebra.hom.non_unital_alg

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:

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 #

Tags #

non-unital, algebra, morphism

source
@[nolint]
def non_unital_alg_hom.to_mul_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (self : A →ₙₐ[R] B) :
A →ₙ* B
source
structure non_unital_alg_hom (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R 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.

Instances for non_unital_alg_hom
source
@[nolint]
def non_unital_alg_hom.to_distrib_mul_action_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (self : A →ₙₐ[R] B) :
A →+[R] B
source
@[class]
structure non_unital_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] :
Type (max u_1 u_3 u_4)

non_unital_alg_hom_class F R A B asserts F is a type of bundled algebra homomorphisms from A to B.

Instances of this typeclass
Instances of other typeclasses for non_unital_alg_hom_class
  • non_unital_alg_hom_class.has_sizeof_inst
source
@[nolint, instance]
def non_unital_alg_hom_class.to_mul_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] [self : non_unital_alg_hom_class F R A B] :
mul_hom_class F A B
source
@[instance]
def non_unital_alg_hom_class.to_distrib_mul_action_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] [self : non_unital_alg_hom_class F R A B] :
distrib_mul_action_hom_class F R A B
source
@[protected, nolint, instance]
def non_unital_alg_hom_class.non_unital_alg_hom_class.to_non_unital_ring_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_alg_hom_class F R A B] :
non_unital_ring_hom_class F A B
Equations
source
@[protected, instance]
def non_unital_alg_hom_class.linear_map_class (R : Type u) (A : Type v) (B : Type w) [semiring R] [non_unital_non_assoc_semiring A] [module R A] [non_unital_non_assoc_semiring B] [module R B] {F : Type u_1} [non_unital_alg_hom_class F R A B] :
linear_map_class F R A B
Equations
source
@[protected, instance]
def non_unital_alg_hom_class.non_unital_alg_hom.has_coe_t {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_alg_hom_class F R A B] :
has_coe_t F (A →ₙₐ[R] B)
Equations
source
@[protected, instance]
def non_unital_alg_hom.has_coe_to_fun {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
has_coe_to_fun (A →ₙₐ[R] B) (λ (_x : A →ₙₐ[R] B), A → B)

see Note [function coercion]

Equations
source
@[simp]
theorem non_unital_alg_hom.to_fun_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
f.to_fun = ⇑f
source
@[protected, simp]
theorem non_unital_alg_hom.coe_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {F : Type u_1} [non_unital_alg_hom_class F R A B] (f : F) :
⇑↑f = ⇑f
source
theorem non_unital_alg_hom.coe_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
function.injective coe_fn
source
@[protected, instance]
def non_unital_alg_hom.non_unital_alg_hom_class {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
non_unital_alg_hom_class (A →ₙₐ[R] B) R A B
Equations
source
@[ext]
theorem non_unital_alg_hom.ext {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {f g : A →ₙₐ[R] B} (h : ∀ (x : A), ⇑f x = ⇑g x) :
f = g
source
theorem non_unital_alg_hom.ext_iff {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {f g : A →ₙₐ[R] B} :
f = g ↔ ∀ (x : A), ⇑f x = ⇑g x
source
theorem non_unital_alg_hom.congr_fun {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {f g : A →ₙₐ[R] B} (h : f = g) (x : A) :
⇑f x = ⇑g x
source
@[simp]
theorem non_unital_alg_hom.coe_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R 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
source
@[simp]
theorem non_unital_alg_hom.mk_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] 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
source
@[protected, instance]
def non_unital_alg_hom.distrib_mul_action_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
has_coe (A →ₙₐ[R] B) (A →+[R] B)
Equations
source
@[protected, instance]
def non_unital_alg_hom.mul_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
has_coe (A →ₙₐ[R] B) (A →ₙ* B)
Equations
source
@[simp]
theorem non_unital_alg_hom.to_distrib_mul_action_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
f.to_distrib_mul_action_hom = ↑f
source
@[simp]
theorem non_unital_alg_hom.to_mul_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
f.to_mul_hom = ↑f
source
@[simp, norm_cast]
theorem non_unital_alg_hom.coe_to_distrib_mul_action_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
⇑↑f = ⇑f
source
@[simp, norm_cast]
theorem non_unital_alg_hom.coe_to_mul_hom {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
⇑↑f = ⇑f
source
theorem non_unital_alg_hom.to_distrib_mul_action_hom_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {f g : A →ₙₐ[R] B} (h : ↑f = ↑g) :
f = g
source
theorem non_unital_alg_hom.to_mul_hom_injective {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] {f g : A →ₙₐ[R] B} (h : ↑f = ↑g) :
f = g
source
@[norm_cast]
theorem non_unital_alg_hom.coe_distrib_mul_action_hom_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] 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₃}
source
@[norm_cast]
theorem non_unital_alg_hom.coe_mul_hom_mk {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] 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₄}
source
@[protected, simp]
theorem non_unital_alg_hom.map_smul {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) (c : R) (x : A) :
⇑f (c • x) = c • ⇑f x
source
@[protected, simp]
theorem non_unital_alg_hom.map_add {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) (x y : A) :
⇑f (x + y) = ⇑f x + ⇑f y
source
@[protected, simp]
theorem non_unital_alg_hom.map_mul {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) (x y : A) :
⇑f (x * y) = ⇑f x * ⇑f y
source
@[protected, simp]
theorem non_unital_alg_hom.map_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) :
⇑f 0 = 0
source
@[protected, instance]
def non_unital_alg_hom.has_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
has_zero (A →ₙₐ[R] B)
Equations
source
@[protected, instance]
def non_unital_alg_hom.has_one {R : Type u} {A : Type v} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] :
has_one (A →ₙₐ[R] A)
Equations
source
@[simp]
theorem non_unital_alg_hom.coe_zero {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
⇑0 = 0
source
@[simp]
theorem non_unital_alg_hom.coe_one {R : Type u} {A : Type v} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] :
⇑1 = id
source
theorem non_unital_alg_hom.zero_apply {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (a : A) :
⇑0 a = 0
source
theorem non_unital_alg_hom.one_apply {R : Type u} {A : Type v} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] (a : A) :
⇑1 a = a
source
@[protected, instance]
def non_unital_alg_hom.inhabited {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
inhabited (A →ₙₐ[R] B)
Equations
source
def non_unital_alg_hom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) :
A →ₙₐ[R] C

The composition of morphisms is a morphism.

Equations
source
@[simp, norm_cast]
theorem non_unital_alg_hom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) :
⇑(f.comp g) = ⇑f ∘ ⇑g
source
theorem non_unital_alg_hom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) (x : A) :
⇑(f.comp g) x = ⇑f (⇑g x)
source
def non_unital_alg_hom.inverse {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :
B →ₙₐ[R] A

The inverse of a bijective morphism is a morphism.

Equations
source
@[simp]
theorem non_unital_alg_hom.coe_inverse {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (f : A →ₙₐ[R] B) (g : B → A) (h₁ : function.left_inverse g ⇑f) (h₂ : function.right_inverse g ⇑f) :
⇑(f.inverse g h₁ h₂) = g

Operations on the product type #

Note that much of this is copied from linear_algebra/prod.

source
def non_unital_alg_hom.fst (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
A × B →ₙₐ[R] A

The first projection of a product is a non-unital alg_hom.

Equations
source
@[simp]
theorem non_unital_alg_hom.fst_apply (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (self : A × B) :
⇑(non_unital_alg_hom.fst R A B) self = self.fst
source
def non_unital_alg_hom.snd (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
A × B →ₙₐ[R] B

The second projection of a product is a non-unital alg_hom.

Equations
source
@[simp]
theorem non_unital_alg_hom.snd_apply (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (self : A × B) :
⇑(non_unital_alg_hom.snd R A B) self = self.snd
source
def non_unital_alg_hom.prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
A →ₙₐ[R] B × C

The prod of two morphisms is a morphism.

Equations
source
@[simp]
theorem non_unital_alg_hom.prod_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) :
⇑(f.prod g) i = pi.prod ⇑f ⇑g i
source
theorem non_unital_alg_hom.coe_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
⇑(f.prod g) = pi.prod ⇑f ⇑g
source
@[simp]
theorem non_unital_alg_hom.fst_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
(non_unital_alg_hom.fst R B C).comp (f.prod g) = f
source
@[simp]
theorem non_unital_alg_hom.snd_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
(non_unital_alg_hom.snd R B C).comp (f.prod g) = g
source
@[simp]
theorem non_unital_alg_hom.prod_fst_snd {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
(non_unital_alg_hom.fst R A B).prod (non_unital_alg_hom.snd R A B) = 1
source
def non_unital_alg_hom.prod_equiv {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] :
(A →ₙₐ[R] B) × (A →ₙₐ[R] C) ≃ (A →ₙₐ[R] B × C)

Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

Equations
source
@[simp]
theorem non_unital_alg_hom.prod_equiv_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)) :
⇑non_unital_alg_hom.prod_equiv f = f.fst.prod f.snd
source
@[simp]
theorem non_unital_alg_hom.prod_equiv_symm_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] (f : A →ₙₐ[R] B × C) :
⇑(non_unital_alg_hom.prod_equiv.symm) f = ((non_unital_alg_hom.fst R B C).comp f, (non_unital_alg_hom.snd R B C).comp f)
source
def non_unital_alg_hom.inl (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
A →ₙₐ[R] A × B

The left injection into a product is a non-unital algebra homomorphism.

Equations
source
def non_unital_alg_hom.inr (R : Type u) (A : Type v) (B : Type w) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
B →ₙₐ[R] A × B

The right injection into a product is a non-unital algebra homomorphism.

Equations
source
@[simp]
theorem non_unital_alg_hom.coe_inl {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
⇑(non_unital_alg_hom.inl R A B) = λ (x : A), (x, 0)
source
theorem non_unital_alg_hom.inl_apply {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (x : A) :
⇑(non_unital_alg_hom.inl R A B) x = (x, 0)
source
@[simp]
theorem non_unital_alg_hom.coe_inr {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] :
⇑(non_unital_alg_hom.inr R A B) = prod.mk 0
source
theorem non_unital_alg_hom.inr_apply {R : Type u} {A : Type v} {B : Type w} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] (x : B) :
⇑(non_unital_alg_hom.inr R A B) x = (0, x)

Interaction with alg_hom #

source
@[protected, instance]
def alg_hom.non_unital_alg_hom_class {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] {F : Type u_1} [alg_hom_class F R A B] :
non_unital_alg_hom_class F R A B
Equations
source
def alg_hom.to_non_unital_alg_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
A →ₙₐ[R] B

A unital morphism of algebras is a non_unital_alg_hom.

Equations
source
@[protected, instance]
def alg_hom.non_unital_alg_hom.has_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] :
has_coe (A →ₐ[R] B) (A →ₙₐ[R] B)
Equations
source
@[simp]
theorem alg_hom.to_non_unital_alg_hom_eq_coe {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
f.to_non_unital_alg_hom = ↑f
source
@[simp, norm_cast]
theorem alg_hom.coe_to_non_unital_alg_hom {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
⇑↑f = ⇑f