# Morphisms of non-unital algebras #

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

• 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 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 NonUnitalAlgHom.

TODO: add NonUnitalAlgEquiv when needed.

## Tags #

non-unital, algebra, morphism

structure NonUnitalAlgHom {R : Type u} {S : Type u₁} [] [] (φ : R →* S) (A : Type v) (B : Type w) [] [] extends :
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.

• toFun : AB
• map_smul' : ∀ (m : R) (x : A), self.toFun (m x) = φ m self.toFun x
• map_zero' : self.toFun 0 = 0
• map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
• map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y

The proposition that the function preserves multiplication

Instances For

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.

Equations
Instances For

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
class NonUnitalAlgSemiHomClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [] [] (φ : outParam (R →* S)) (A : outParam (Type u_4)) (B : outParam (Type u_5)) [] [] [FunLike F A B] extends , :

NonUnitalAlgSemiHomClass F φ A B asserts F is a type of bundled algebra homomorphisms from A to B which are equivariant with respect to φ.

Instances
@[reducible, inline]
abbrev NonUnitalAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [] [] [] [FunLike F A B] :

NonUnitalAlgHomClass F R A B asserts F is a type of bundled algebra homomorphisms from A to B which are R-linear.

This is an abbreviation to NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B

Equations
Instances For
@[instance 100]
instance NonUnitalAlgHomClass.toNonUnitalRingHomClass {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} :
∀ {x : } {x_1 : } {φ : outParam (R →* S)} {x_2 : } [inst : ] {x_3 : } [inst_1 : ] [inst_2 : FunLike F A B] [inst : ],
Equations
• =
@[instance 100]
instance NonUnitalAlgHomClass.instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom {F : Type u_3} {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} :
∀ {x : } {x_1 : } {φ : R →+* S} {x_2 : } {x_3 : } [inst : Module R A] [inst_1 : Module S B] [inst_2 : FunLike F A B] [inst_3 : NonUnitalAlgSemiHomClass F (φ) A B],
Equations
• =
@[instance 100]
instance NonUnitalAlgHomClass.instLinearMapClass {R : Type u} [] {A : Type u_1} {B : Type u_2} [Module R A] {F : Type u_3} [FunLike F A B] [Module R B] [] :
Equations
• =
def NonUnitalAlgHomClass.toNonUnitalAlgSemiHom {F : Type u_3} {R : Type u_4} {S : Type u_5} [] [] {φ : R →* S} {A : Type u_6} {B : Type u_7} [] [] [FunLike F A B] [] (f : F) :

Turn an element of a type F satisfying NonUnitalAlgSemiHomClass F φ A B into an actual NonUnitalAlgHom. This is declared as the default coercion from F to A →ₛₙₐ[φ] B.

Equations
• f = let __src := f; { toFun := f, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
instance NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass {F : Type u_3} {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [] [] {φ : R →* S} [] [] [FunLike F A B] [] :
Equations
• NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass = { coe := NonUnitalAlgHomClass.toNonUnitalAlgSemiHom }
def NonUnitalAlgHomClass.toNonUnitalAlgHom {F : Type u_3} {R : Type u_4} [] {A : Type u_5} {B : Type u_6} [] [] [FunLike F A B] [] (f : F) :

Turn an element of a type F satisfying NonUnitalAlgHomClass F R A B into an actual @[coe] NonUnitalAlgHom. This is declared as the default coercion from F to A →ₛₙₐ[R] B.

Equations
• = let __src := f; { toFun := f, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
instance NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId {F : Type u_3} {R : Type u_4} [] {A : Type u_5} {B : Type u_6} [] [] [FunLike F A B] [] :
Equations
• NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId = { coe := NonUnitalAlgHomClass.toNonUnitalAlgHom }
instance NonUnitalAlgHom.instDFunLike {R : Type u} {S : Type u₁} [] [] (φ : R →* S) (A : Type v) (B : Type w) [] [] :
DFunLike (A →ₛₙₐ[φ] B) A fun (x : A) => B
Equations
• = { coe := fun (f : A →ₛₙₐ[φ] B) => f.toFun, coe_injective' := }
@[simp]
theorem NonUnitalAlgHom.toFun_eq_coe {R : Type u} {S : Type u₁} [] [] (φ : R →* S) (A : Type v) (B : Type w) [] [] (f : A →ₛₙₐ[φ] B) :
f.toFun = f
def NonUnitalAlgHom.Simps.apply {R : Type u} {S : Type u₁} [] [] (φ : R →* S) (A : Type v) (B : Type w) [] [] (f : A →ₛₙₐ[φ] B) :
AB

See Note [custom simps projection]

Equations
• = f
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_coe {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {F : Type u_2} [FunLike F A B] [] (f : F) :
f = f
theorem NonUnitalAlgHom.coe_injective {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Function.Injective DFunLike.coe
instance NonUnitalAlgHom.instFunLike {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• NonUnitalAlgHom.instFunLike = { coe := fun (f : A →ₛₙₐ[φ] B) => f.toFun, coe_injective' := }
instance NonUnitalAlgHom.instNonUnitalAlgSemiHomClass {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• =
theorem NonUnitalAlgHom.ext {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {f : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} (h : ∀ (x : A), f x = g x) :
f = g
theorem NonUnitalAlgHom.ext_iff {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {f : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} :
f = g ∀ (x : A), f x = g x
theorem NonUnitalAlgHom.congr_fun {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {f : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} (h : f = g) (x : A) :
f x = g x
@[simp]
theorem NonUnitalAlgHom.coe_mk {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : AB) (h₁ : ∀ (m : R) (x : A), f (m x) = φ m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) :
{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
@[simp]
theorem NonUnitalAlgHom.mk_coe {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m x) = φ m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) :
{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
instance NonUnitalAlgHom.instCoeOutDistribMulActionHom {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• NonUnitalAlgHom.instCoeOutDistribMulActionHom = { coe := NonUnitalAlgHom.toDistribMulActionHom }
instance NonUnitalAlgHom.instCoeOutMulHom {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• NonUnitalAlgHom.instCoeOutMulHom = { coe := NonUnitalAlgHom.toMulHom }
@[simp]
theorem NonUnitalAlgHom.toDistribMulActionHom_eq_coe {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) :
f.toDistribMulActionHom = f
@[simp]
theorem NonUnitalAlgHom.toMulHom_eq_coe {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) :
f.toMulHom = f
@[simp]
theorem NonUnitalAlgHom.coe_to_distribMulActionHom {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) :
f = f
@[simp]
theorem NonUnitalAlgHom.coe_to_mulHom {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) :
f = f
theorem NonUnitalAlgHom.to_distribMulActionHom_injective {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {f : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} (h : f = g) :
f = g
theorem NonUnitalAlgHom.to_mulHom_injective {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {f : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} (h : f = g) :
f = g
theorem NonUnitalAlgHom.coe_distribMulActionHom_mk {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m x) = φ m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) :
{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }
theorem NonUnitalAlgHom.coe_mulHom_mk {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (h₁ : ∀ (m : R) (x : A), f (m x) = φ m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) :
{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = { toFun := f, map_mul' := h₄ }
theorem NonUnitalAlgHom.map_smul {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (c : R) (x : A) :
f (c x) = φ c f x
theorem NonUnitalAlgHom.map_add {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (x : A) (y : A) :
f (x + y) = f x + f y
theorem NonUnitalAlgHom.map_mul {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) (x : A) (y : A) :
f (x * y) = f x * f y
theorem NonUnitalAlgHom.map_zero {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (f : A →ₛₙₐ[φ] B) :
f 0 = 0
def NonUnitalAlgHom.id (R : Type u_2) (A : Type u_3) [] [] :

The identity map as a NonUnitalAlgHom.

Equations
• = let __src := ; { toFun := id, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_id {R : Type u} [] {A : Type v} [] :
() = id
instance NonUnitalAlgHom.instZero {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• NonUnitalAlgHom.instZero = { zero := let __src := 0; { toDistribMulActionHom := __src, map_mul' := } }
instance NonUnitalAlgHom.instOneId {R : Type u} [] {A : Type v} [] :
Equations
• NonUnitalAlgHom.instOneId = { one := }
@[simp]
theorem NonUnitalAlgHom.coe_zero {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
0 = 0
@[simp]
theorem NonUnitalAlgHom.coe_one {R : Type u} [] {A : Type v} [] :
1 = id
theorem NonUnitalAlgHom.zero_apply {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] (a : A) :
0 a = 0
theorem NonUnitalAlgHom.one_apply {R : Type u} [] {A : Type v} [] (a : A) :
1 a = a
instance NonUnitalAlgHom.instInhabited {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] :
Equations
• NonUnitalAlgHom.instInhabited = { default := 0 }
def NonUnitalAlgHom.comp {R : Type u} {S : Type u₁} {T : Type u_1} [] [] [] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [] [] [] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [κ : φ.CompTriple ψ χ] :

The composition of morphisms is a morphism.

Equations
• f.comp g = let __src := (f).comp g; let __src_1 := (f).comp g; { toFun := __src.toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_comp {R : Type u} {S : Type u₁} {T : Type u_1} [] [] [] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [] [] [] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [φ.CompTriple ψ χ] :
(f.comp g) = f g
theorem NonUnitalAlgHom.comp_apply {R : Type u} {S : Type u₁} {T : Type u_1} [] [] [] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [] [] [] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [φ.CompTriple ψ χ] (x : A) :
(f.comp g) x = f (g x)
def NonUnitalAlgHom.inverse {R : Type u} [] {A : Type v} [] {B₁ : Type u_2} [] (f : A →ₙₐ[R] B₁) (g : B₁A) (h₁ : ) (h₂ : ) :
B₁ →ₙₐ[R] A

The inverse of a bijective morphism is a morphism.

Equations
• f.inverse g h₁ h₂ = let __src := (f).inverse g h₁ h₂; let __src_1 := (f).inverse g h₁ h₂; { toFun := __src.toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_inverse {R : Type u} [] {A : Type v} [] {B₁ : Type u_2} [] (f : A →ₙₐ[R] B₁) (g : B₁A) (h₁ : ) (h₂ : ) :
(f.inverse g h₁ h₂) = g
def NonUnitalAlgHom.inverse' {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {φ' : S →* R} (f : A →ₛₙₐ[φ] B) (g : BA) (k : ) (h₁ : ) (h₂ : ) :

The inverse of a bijective morphism is a morphism.

Equations
• f.inverse' g k h₁ h₂ = let __src := (f).inverse g h₁ h₂; let __src_1 := (f).inverse' g k h₁ h₂; { toFun := __src.toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_inverse' {R : Type u} {S : Type u₁} [] [] {φ : R →* S} {A : Type v} {B : Type w} [] [] {φ' : S →* R} (f : A →ₛₙₐ[φ] B) (g : BA) (k : ) (h₁ : ) (h₂ : ) :
(f.inverse' g k h₁ h₂) = g

### Operations on the product type #

Note that much of this is copied from LinearAlgebra/Prod.

@[simp]
theorem NonUnitalAlgHom.fst_toFun (R : Type u) [] (A : Type v) (B : Type w) [] [] (self : A × B) :
() self = self.1
@[simp]
theorem NonUnitalAlgHom.fst_apply (R : Type u) [] (A : Type v) (B : Type w) [] [] (self : A × B) :
() self = self.1
def NonUnitalAlgHom.fst (R : Type u) [] (A : Type v) (B : Type w) [] [] :

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

Equations
• = { toFun := Prod.fst, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.snd_toFun (R : Type u) [] (A : Type v) (B : Type w) [] [] (self : A × B) :
() self = self.2
@[simp]
theorem NonUnitalAlgHom.snd_apply (R : Type u) [] (A : Type v) (B : Type w) [] [] (self : A × B) :
() self = self.2
def NonUnitalAlgHom.snd (R : Type u) [] (A : Type v) (B : Type w) [] [] :

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

Equations
• = { toFun := Prod.snd, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.prod_apply {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) :
(f.prod g) i = Pi.prod (f) (g) i
@[simp]
theorem NonUnitalAlgHom.prod_toFun {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) :
(f.prod g) i = Pi.prod (f) (g) i
def NonUnitalAlgHom.prod {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :

The prod of two morphisms is a morphism.

Equations
• f.prod g = { toFun := Pi.prod f g, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
theorem NonUnitalAlgHom.coe_prod {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
(f.prod g) = Pi.prod f g
@[simp]
theorem NonUnitalAlgHom.fst_prod {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
().comp (f.prod g) = f
@[simp]
theorem NonUnitalAlgHom.snd_prod {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) :
().comp (f.prod g) = g
@[simp]
theorem NonUnitalAlgHom.prod_fst_snd {R : Type u} [] {A : Type v} {B : Type w} [] [] :
().prod () = 1
@[simp]
theorem NonUnitalAlgHom.prodEquiv_symm_apply {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : A →ₙₐ[R] B × C) :
NonUnitalAlgHom.prodEquiv.symm f = (().comp f, ().comp f)
@[simp]
theorem NonUnitalAlgHom.prodEquiv_apply {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] (f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)) :
NonUnitalAlgHom.prodEquiv f = f.1.prod f.2
def NonUnitalAlgHom.prodEquiv {R : Type u} [] {A : Type v} {B : Type w} {C : Type w₁} [] [] [] :
(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
• One or more equations did not get rendered due to their size.
Instances For
def NonUnitalAlgHom.inl (R : Type u) [] (A : Type v) (B : Type w) [] [] :

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

Equations
Instances For
def NonUnitalAlgHom.inr (R : Type u) [] (A : Type v) (B : Type w) [] [] :

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

Equations
Instances For
@[simp]
theorem NonUnitalAlgHom.coe_inl {R : Type u} [] {A : Type v} {B : Type w} [] [] :
() = fun (x : A) => (x, 0)
theorem NonUnitalAlgHom.inl_apply {R : Type u} [] {A : Type v} {B : Type w} [] [] (x : A) :
() x = (x, 0)
@[simp]
theorem NonUnitalAlgHom.coe_inr {R : Type u} [] {A : Type v} {B : Type w} [] [] :
() =
theorem NonUnitalAlgHom.inr_apply {R : Type u} [] {A : Type v} {B : Type w} [] [] (x : B) :
() x = (0, x)

### Interaction with AlgHom#

@[instance 100]
instance AlgHom.instNonUnitalAlgHomClassOfAlgHomClass {F : Type u_1} {R : Type u_2} [] {A : Type u_3} {B : Type u_4} [] [] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] :
Equations
• =
def AlgHom.toNonUnitalAlgHom {R : Type u_2} [] {A : Type u_3} {B : Type u_4} [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

A unital morphism of algebras is a NonUnitalAlgHom.

Equations
• f = { toFun := (f.toRingHom).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
instance AlgHom.NonUnitalAlgHom.hasCoe {R : Type u_2} [] {A : Type u_3} {B : Type u_4} [] [] [Algebra R A] [Algebra R B] :
Equations
• AlgHom.NonUnitalAlgHom.hasCoe = { coe := AlgHom.toNonUnitalAlgHom }
@[simp]
theorem AlgHom.toNonUnitalAlgHom_eq_coe {R : Type u_2} [] {A : Type u_3} {B : Type u_4} [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
@[simp]
theorem AlgHom.coe_to_nonUnitalAlgHom {R : Type u_2} [] {A : Type u_3} {B : Type u_4} [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
f = f
def NonUnitalAlgHom.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] [] (f : A →ₙₐ[S] B) :

If a monoid R acts on another monoid S, then a non-unital algebra homomorphism over S can be viewed as a non-unital algebra homomorphism over R.

Equations
• = let __src := f; { toFun := __src.toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem NonUnitalAlgHom.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] [] (f : A →ₙₐ[S] B) (x : A) :
= f x
theorem NonUnitalAlgHom.coe_restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] [] (f : A →ₙₐ[S] B) :
= f
theorem NonUnitalAlgHom.coe_restrictScalars' (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] [] (f : A →ₙₐ[S] B) :
= f
theorem NonUnitalAlgHom.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [] [] [] [] [] [] [] [] [] :