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)

• toFun : A → B
• map_smul' : ∀ (m : R) (x : A), MulActionHom.toFun s.toMulActionHom (m • x) = m • MulActionHom.toFun s.toMulActionHom x
• map_zero' : MulActionHom.toFun s.toMulActionHom 0 = 0
• map_add' : ∀ (x y : A), MulActionHom.toFun s.toMulActionHom (x + y) = MulActionHom.toFun s.toMulActionHom x + MulActionHom.toFun s.toMulActionHom y
• map_mul' : ∀ (x y : A), MulActionHom.toFun s.toMulActionHom (x * y) = MulActionHom.toFun s.toMulActionHom x * MulActionHom.toFun s.toMulActionHom y

  The proposition that the function preserves multiplication

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.

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] extends DistribMulActionHomClass : Type (max (max u_1 u_3) u_4)

• coe : F → A → B
• coe_injective' : Function.Injective FunLike.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

  The proposition that the function preserves multiplication

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} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalAlgHomClass F R A B] : NonUnitalRingHomClass F A B

Equations

• NonUnitalAlgHomClass.toNonUnitalRingHomClass = let src := inst; NonUnitalRingHomClass.mk (_ : ∀ (f : F) (x y : A), ↑f (x + y) = ↑f x + ↑f y) (_ : ∀ (f : F), ↑f 0 = 0)

instance NonUnitalAlgHomClass.instLinearMapClassToAddCommMonoidToAddCommMonoid (R : Type u) (A : Type v) (B : Type w) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] {F : Type u_1} [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B

Equations

• NonUnitalAlgHomClass.instLinearMapClassToAddCommMonoidToAddCommMonoid R A B = let src := inst; SemilinearMapClass.mk (_ : ∀ (f : F) (c : R) (x : A), ↑f (c • x) = c • ↑f x)

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] [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

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

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] [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 fun x => B

Equations

• NonUnitalAlgHom.instFunLikeNonUnitalAlgHom = { coe := fun f => f.toFun, coe_injective' := (_ : ∀ ⦃a₁ a₂ : A →ₙₐ[R] B⦄, (fun f => f.toFun) a₁ = (fun f => f.toFun) a₂ → a₁ = a₂) }

@[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} [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 FunLike.coe

instance NonUnitalAlgHom.instNonUnitalAlgHomClassNonUnitalAlgHom {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

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

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₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom 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₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom 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₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom 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₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom 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

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

@[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

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

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

@[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.fst

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

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

@[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.snd

@[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.snd

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

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

@[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

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

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_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)

@[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.fst f.snd

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 => (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} [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B

Equations

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

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

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

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