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

Main definitions

• NonUnitalAlgHom
• AlgHom.toNonUnitalAlgHom

Tags

non-unital, algebra, morphism

structure NonUnitalAlgHom (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] extends DistribMulActionHom : 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 : A → B
• 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

def «term_→ₙₐ_» : Lean.TrailingParserDescr

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

• «term_→ₙₐ_» = Lean.ParserDescr.trailingNode `term_→ₙₐ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₙₐ ") (Lean.ParserDescr.cat `term 25))

def «term_→ₙₐ[_]_» : Lean.TrailingParserDescr

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.

class NonUnitalAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] extends DistribMulActionHomClass , MulHomClass : Prop

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

instance NonUnitalAlgHomClass.toNonUnitalRingHomClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} : ∀ {x : Monoid R} {x_1 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_2 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction R B] [inst_2 : FunLike F A B] [inst : NonUnitalAlgHomClass F R A B], NonUnitalRingHomClass F A B

Equations

• ⋯ = ⋯

instance NonUnitalAlgHomClass.instLinearMapClassToAddCommMonoidToNonUnitalNonAssocSemiringToAddCommMonoidToNonUnitalNonAssocSemiring {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} : ∀ {x : Semiring R} {x_1 : NonUnitalSemiring A} {x_2 : NonUnitalSemiring B} [inst : Module R A] [inst_1 : Module R B] [inst_2 : FunLike F A B] [inst_3 : NonUnitalAlgHomClass F R A B], LinearMapClass F R A B

Equations

• ⋯ = ⋯

def NonUnitalAlgHomClass.toNonUnitalAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B

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

Equations

• ↑f = let __src := ↑f; { toDistribMulActionHom := { toMulActionHom := { toFun := __src.toFun, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

instance NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] : CoeTC F (A →ₙₐ[R] B)

Equations

• NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHom = { coe := NonUnitalAlgHomClass.toNonUnitalAlgHom }

instance NonUnitalAlgHom.instFunLikeNonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : FunLike (A →ₙₐ[R] B) A B

Equations

• NonUnitalAlgHom.instFunLikeNonUnitalAlgHom = { coe := fun (f : A →ₙₐ[R] B) => f.toFun, coe_injective' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.toFun_eq_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : f.toFun = ⇑f

def NonUnitalAlgHom.Simps.apply {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : A → B

See Note [custom simps projection]

Equations

• NonUnitalAlgHom.Simps.apply f = ⇑f

@[simp]

theorem NonUnitalAlgHom.coe_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {F : Type u_1} [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : ⇑↑f = ⇑f

theorem NonUnitalAlgHom.coe_injective {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : Function.Injective DFunLike.coe

instance NonUnitalAlgHom.instFunLikeNonUnitalAlgHom_1 {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : FunLike (A →ₙₐ[R] B) A B

Equations

• NonUnitalAlgHom.instFunLikeNonUnitalAlgHom_1 = { coe := fun (f : A →ₙₐ[R] B) => f.toFun, coe_injective' := ⋯ }

instance NonUnitalAlgHom.instNonUnitalAlgHomClassNonUnitalAlgHomInstFunLikeNonUnitalAlgHom_1 {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : NonUnitalAlgHomClass (A →ₙₐ[R] B) R A B

Equations

• ⋯ = ⋯

theorem NonUnitalAlgHom.ext {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : ∀ (x : A), f x = g x) : f = g

theorem NonUnitalAlgHom.ext_iff {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} : f = g ↔ ∀ (x : A), f x = g x

theorem NonUnitalAlgHom.congr_fun {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : f = g) (x : A) : f x = g x

@[simp]

theorem NonUnitalAlgHom.coe_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (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), { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) : ⇑{ toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = f

@[simp]

theorem NonUnitalAlgHom.mk_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] 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), { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) : { toDistribMulActionHom := { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = f

instance NonUnitalAlgHom.instCoeOutNonUnitalAlgHomDistribMulActionHomToAddMonoidToAddCommMonoidToAddMonoidToAddCommMonoid {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : CoeOut (A →ₙₐ[R] B) (A →+[R] B)

Equations

• NonUnitalAlgHom.instCoeOutNonUnitalAlgHomDistribMulActionHomToAddMonoidToAddCommMonoidToAddMonoidToAddCommMonoid = { coe := NonUnitalAlgHom.toDistribMulActionHom }

instance NonUnitalAlgHom.instCoeOutNonUnitalAlgHomMulHomToMulToMul {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : CoeOut (A →ₙₐ[R] B) (A →ₙ* B)

Equations

• NonUnitalAlgHom.instCoeOutNonUnitalAlgHomMulHomToMulToMul = { coe := NonUnitalAlgHom.toMulHom }

@[simp]

theorem NonUnitalAlgHom.toDistribMulActionHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : f.toDistribMulActionHom = ↑f

@[simp]

theorem NonUnitalAlgHom.toMulHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : NonUnitalAlgHom.toMulHom f = ↑f

@[simp]

theorem NonUnitalAlgHom.coe_to_distribMulActionHom {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : ⇑↑f = ⇑f

@[simp]

theorem NonUnitalAlgHom.coe_to_mulHom {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : ⇑↑f = ⇑f

theorem NonUnitalAlgHom.to_distribMulActionHom_injective {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : ↑f = ↑g) : f = g

theorem NonUnitalAlgHom.to_mulHom_injective {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : ↑f = ↑g) : f = g

theorem NonUnitalAlgHom.coe_distribMulActionHom_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] 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), { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) : ↑{ toDistribMulActionHom := { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }

theorem NonUnitalAlgHom.coe_mulHom_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] 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), { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun x * { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toFun y) : ↑{ toDistribMulActionHom := { toMulActionHom := { 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} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (c : R) (x : A) : f (c • x) = c • f x

theorem NonUnitalAlgHom.map_add {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (x : A) (y : A) : f (x + y) = f x + f y

theorem NonUnitalAlgHom.map_mul {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (x : A) (y : A) : f (x * y) = f x * f y

theorem NonUnitalAlgHom.map_zero {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) : f 0 = 0

def NonUnitalAlgHom.id (R : Type u_1) (A : Type u_2) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : A →ₙₐ[R] A

The identity map as a NonUnitalAlgHom.

Equations

• NonUnitalAlgHom.id R A = let __src := NonUnitalRingHom.id A; { toDistribMulActionHom := { toMulActionHom := { toFun := id, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.coe_id {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : ⇑(NonUnitalAlgHom.id R A) = id

instance NonUnitalAlgHom.instZeroNonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : Zero (A →ₙₐ[R] B)

Equations

• NonUnitalAlgHom.instZeroNonUnitalAlgHom = { zero := let __src := 0; { toDistribMulActionHom := __src, map_mul' := ⋯ } }

instance NonUnitalAlgHom.instOneNonUnitalAlgHom {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : One (A →ₙₐ[R] A)

Equations

• NonUnitalAlgHom.instOneNonUnitalAlgHom = { one := NonUnitalAlgHom.id R A }

@[simp]

theorem NonUnitalAlgHom.coe_zero {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : ⇑0 = 0

@[simp]

theorem NonUnitalAlgHom.coe_one {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : ⇑1 = id

theorem NonUnitalAlgHom.zero_apply {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (a : A) : 0 a = 0

theorem NonUnitalAlgHom.one_apply {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (a : A) : 1 a = a

instance NonUnitalAlgHom.instInhabitedNonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : Inhabited (A →ₙₐ[R] B)

Equations

• NonUnitalAlgHom.instInhabitedNonUnitalAlgHom = { default := 0 }

def NonUnitalAlgHom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) : A →ₙₐ[R] C

The composition of morphisms is a morphism.

Equations

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

@[simp]

theorem NonUnitalAlgHom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) : ⇑(NonUnitalAlgHom.comp f g) = ⇑f ∘ ⇑g

theorem NonUnitalAlgHom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) (x : A) : (NonUnitalAlgHom.comp f g) x = f (g x)

def NonUnitalAlgHom.inverse {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : B →ₙₐ[R] A

The inverse of a bijective morphism is a morphism.

Equations

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

@[simp]

theorem NonUnitalAlgHom.coe_inverse {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (g : B → A) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ⇑(NonUnitalAlgHom.inverse f g 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) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.fst R A B) self = self.1

@[simp]

theorem NonUnitalAlgHom.fst_apply (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.fst R A B) self = self.1

def NonUnitalAlgHom.fst (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : A × B →ₙₐ[R] A

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

Equations

• NonUnitalAlgHom.fst R A B = { toDistribMulActionHom := { toMulActionHom := { toFun := Prod.fst, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.snd_toFun (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.snd R A B) self = self.2

@[simp]

theorem NonUnitalAlgHom.snd_apply (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.snd R A B) self = self.2

def NonUnitalAlgHom.snd (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : A × B →ₙₐ[R] B

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

Equations

• NonUnitalAlgHom.snd R A B = { toDistribMulActionHom := { toMulActionHom := { toFun := Prod.snd, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.prod_toFun {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) : (NonUnitalAlgHom.prod f g) i = Pi.prod (⇑f) (⇑g) i

@[simp]

theorem NonUnitalAlgHom.prod_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) : (NonUnitalAlgHom.prod f g) i = Pi.prod (⇑f) (⇑g) i

def NonUnitalAlgHom.prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C

The prod of two morphisms is a morphism.

Equations

• NonUnitalAlgHom.prod f g = { toDistribMulActionHom := { toMulActionHom := { toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

theorem NonUnitalAlgHom.coe_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(NonUnitalAlgHom.prod f g) = Pi.prod ⇑f ⇑g

@[simp]

theorem NonUnitalAlgHom.fst_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : NonUnitalAlgHom.comp (NonUnitalAlgHom.fst R B C) (NonUnitalAlgHom.prod f g) = f

@[simp]

theorem NonUnitalAlgHom.snd_prod {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : NonUnitalAlgHom.comp (NonUnitalAlgHom.snd R B C) (NonUnitalAlgHom.prod f g) = g

@[simp]

theorem NonUnitalAlgHom.prod_fst_snd {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : NonUnitalAlgHom.prod (NonUnitalAlgHom.fst R A B) (NonUnitalAlgHom.snd R A B) = 1

@[simp]

theorem NonUnitalAlgHom.prodEquiv_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)) : NonUnitalAlgHom.prodEquiv f = NonUnitalAlgHom.prod f.1 f.2

@[simp]

theorem NonUnitalAlgHom.prodEquiv_symm_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B × C) : NonUnitalAlgHom.prodEquiv.symm f = (NonUnitalAlgHom.comp (NonUnitalAlgHom.fst R B C) f, NonUnitalAlgHom.comp (NonUnitalAlgHom.snd R B C) f)

def NonUnitalAlgHom.prodEquiv {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction 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

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

def NonUnitalAlgHom.inl (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : A →ₙₐ[R] A × B

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

Equations

• NonUnitalAlgHom.inl R A B = NonUnitalAlgHom.prod 1 0

def NonUnitalAlgHom.inr (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : B →ₙₐ[R] A × B

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

Equations

• NonUnitalAlgHom.inr R A B = NonUnitalAlgHom.prod 0 1

@[simp]

theorem NonUnitalAlgHom.coe_inl {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : ⇑(NonUnitalAlgHom.inl R A B) = fun (x : A) => (x, 0)

theorem NonUnitalAlgHom.inl_apply {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (x : A) : (NonUnitalAlgHom.inl R A B) x = (x, 0)

@[simp]

theorem NonUnitalAlgHom.coe_inr {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] : ⇑(NonUnitalAlgHom.inr R A B) = Prod.mk 0

theorem NonUnitalAlgHom.inr_apply {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (x : B) : (NonUnitalAlgHom.inr R A B) x = (0, x)

Interaction with AlgHom

instance AlgHom.instNonUnitalAlgHomClassToMonoidToMonoidWithZeroToSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToNonUnitalNonAssocSemiringToNonAssocSemiringToDistribMulActionToAddCommMonoidToModuleToDistribMulActionToAddCommMonoidToModule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_1} [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B

Equations

• ⋯ = ⋯

def AlgHom.toNonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring 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 NonUnitalAlgHom.

Equations

• ↑f = { toDistribMulActionHom := { toMulActionHom := { toFun := f.toFun, map_smul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }, map_mul' := ⋯ }

instance AlgHom.NonUnitalAlgHom.hasCoe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] : CoeOut (A →ₐ[R] B) (A →ₙₐ[R] B)

Equations

• AlgHom.NonUnitalAlgHom.hasCoe = { coe := AlgHom.toNonUnitalAlgHom }

@[simp]

theorem AlgHom.toNonUnitalAlgHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : ↑f = ↑f

@[simp]

theorem AlgHom.coe_to_nonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : ⇑↑f = ⇑f