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} {S : Type u₁} [Monoid R] [Monoid S] (φ : R →* S) (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] extends A →ₑ+[φ] B, A →ₙ* 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.

• 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

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.

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 NonUnitalAlgSemiHomClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [Monoid R] [Monoid S] (φ : outParam (R →* S)) (A : outParam (Type u_4)) (B : outParam (Type u_5)) [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction S B] [FunLike F A B] extends DistribMulActionSemiHomClass F (⇑φ) A B, MulHomClass F A B : Prop

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

• 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

@[reducible, inline]

abbrev 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] : Prop

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

• NonUnitalAlgHomClass F R A B = NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B

@[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✝ : Monoid R} {x✝¹ : Monoid S} {φ : outParam (R →* S)} {x✝² : NonUnitalNonAssocSemiring A} [DistribMulAction R A] {x✝³ : NonUnitalNonAssocSemiring B} [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] : NonUnitalRingHomClass F A B

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✝ : Semiring R} {x✝¹ : Semiring S} {φ : R →+* S} {x✝² : NonUnitalSemiring A} {x✝³ : NonUnitalSemiring B} [Module R A] [Module S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F (↑φ) A B] : SemilinearMapClass F φ A B

Equations

• ⋯ = ⋯

@[instance 100]

instance NonUnitalAlgHomClass.instLinearMapClass {R : Type u} [Semiring R] {A : Type u_1} {B : Type u_2} [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] {F : Type u_3} [FunLike F A B] [Module R B] [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B

Equations

• ⋯ = ⋯

def NonUnitalAlgHomClass.toNonUnitalAlgSemiHom {F : Type u_3} {R : Type u_4} {S : Type u_5} [Monoid R] [Monoid S] {φ : R →* S} {A : Type u_6} {B : Type u_7} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] (f : F) : A →ₛₙₐ[φ] B

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 = { toFun := ⇑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

instance NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass {F : Type u_3} {R : Type u_4} {S : Type u_5} {A : Type u_6} {B : Type u_7} [Monoid R] [Monoid S] {φ : R →* S} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] : CoeTC F (A →ₛₙₐ[φ] B)

Equations

• NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass = { coe := NonUnitalAlgHomClass.toNonUnitalAlgSemiHom }

def NonUnitalAlgHomClass.toNonUnitalAlgHom {F : Type u_3} {R : Type u_4} [Monoid R] {A : Type u_5} {B : Type u_6} [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 @[coe] NonUnitalAlgHom. This is declared as the default coercion from F to A →ₛₙₐ[R] B.

Equations

• NonUnitalAlgHomClass.toNonUnitalAlgHom f = { toFun := ⇑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

instance NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId {F : Type u_3} {R : Type u_4} [Monoid R] {A : Type u_5} {B : Type u_6} [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.instCoeTCNonUnitalAlgHomId = { coe := NonUnitalAlgHomClass.toNonUnitalAlgHom }

instance NonUnitalAlgHom.instDFunLike {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] (φ : R →* S) (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] : DFunLike (A →ₛₙₐ[φ] B) A fun (x : A) => B

Equations

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

@[simp]

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

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

See Note [custom simps projection]

Equations

• NonUnitalAlgHom.Simps.apply φ A B f = ⇑f

@[simp]

theorem NonUnitalAlgHom.coe_coe {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] {F : Type u_2} [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] (f : F) : ⇑↑f = ⇑f

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

instance NonUnitalAlgHom.instFunLike {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] : FunLike (A →ₛₙₐ[φ] B) A B

Equations

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

instance NonUnitalAlgHom.instNonUnitalAlgSemiHomClass {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] : NonUnitalAlgSemiHomClass (A →ₛₙₐ[φ] B) φ A B

Equations

• ⋯ = ⋯

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

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

@[simp]

theorem NonUnitalAlgHom.coe_mk {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S 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), { 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₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S 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), { 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.toDistribMulActionHom_eq_coe {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] (f : A →ₛₙₐ[φ] B) : f.toDistribMulActionHom = ↑f

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem NonUnitalAlgHom.coe_distribMulActionHom_mk {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S 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), { 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₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S 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), { 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₄ }

@[simp]

theorem NonUnitalAlgHom.map_smul {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] (f : A →ₛₙₐ[φ] B) (c : R) (x : A) : f (c • x) = φ c • f x

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

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

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

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

The identity map as a NonUnitalAlgHom.

Equations

• NonUnitalAlgHom.id R A = { toFun := id, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

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

instance NonUnitalAlgHom.instZero {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] : Zero (A →ₛₙₐ[φ] B)

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

instance NonUnitalAlgHom.instInhabited {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] : Inhabited (A →ₛₙₐ[φ] B)

Equations

• NonUnitalAlgHom.instInhabited = { default := 0 }

def NonUnitalAlgHom.comp {R : Type u} {S : Type u₁} {T : Type u_1} [Monoid R] [Monoid S] [Monoid T] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [NonUnitalNonAssocSemiring C] [DistribMulAction T C] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [κ : φ.CompTriple ψ χ] : A →ₛₙₐ[χ] C

The composition of morphisms is a morphism.

Equations

• f.comp g = { toFun := ((↑f).comp ↑g).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.coe_comp {R : Type u} {S : Type u₁} {T : Type u_1} [Monoid R] [Monoid S] [Monoid T] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [NonUnitalNonAssocSemiring C] [DistribMulAction T C] {ψ : 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} [Monoid R] [Monoid S] [Monoid T] {φ : R →* S} {A : Type v} {B : Type w} {C : Type w₁} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [NonUnitalNonAssocSemiring C] [DistribMulAction T C] {ψ : 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} [Monoid R] {A : Type v} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {B₁ : Type u_2} [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

• f.inverse g h₁ h₂ = { toFun := ((↑f).inverse g h₁ h₂).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

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

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

The inverse of a bijective morphism is a morphism.

Equations

• f.inverse' g k h₁ h₂ = { toFun := ((↑f).inverse g h₁ h₂).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.coe_inverse' {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] {φ' : S →* R} (f : A →ₛₙₐ[φ] B) (g : B → A) (k : Function.RightInverse ⇑φ' ⇑φ) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) : ⇑(f.inverse' g k h₁ h₂) = g

Operations on the product type

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

def NonUnitalAlgHom.fst (R : Type u) [Monoid R] (A : Type v) (B : Type w) [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 = { toFun := Prod.fst, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.fst_toFun (R : Type u) [Monoid R] (A : Type v) (B : Type w) [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) [Monoid R] (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.fst R A B) self = self.1

def NonUnitalAlgHom.snd (R : Type u) [Monoid R] (A : Type v) (B : Type w) [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 = { toFun := Prod.snd, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.snd_toFun (R : Type u) [Monoid R] (A : Type v) (B : Type w) [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) [Monoid R] (A : Type v) (B : Type w) [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) : (NonUnitalAlgHom.snd R A B) self = self.2

def NonUnitalAlgHom.prod {R : Type u} [Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [NonUnitalNonAssocSemiring C] [DistribMulAction R B] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × 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' := ⋯ }

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

def NonUnitalAlgHom.inl (R : Type u) [Monoid R] (A : Type v) (B : Type w) [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) [Monoid R] (A : Type v) (B : Type w) [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} [Monoid R] {A : Type v} {B : Type w} [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} [Monoid R] {A : Type v} {B : Type w} [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} [Monoid R] {A : Type v} {B : Type w} [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} [Monoid R] {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (x : B) : (NonUnitalAlgHom.inr R A B) x = (0, x)

Interaction with AlgHom

@[instance 100]

instance AlgHom.instNonUnitalAlgHomClassOfAlgHomClass {F : Type u_1} {R : Type u_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B

Equations

• ⋯ = ⋯

def AlgHom.toNonUnitalAlgHom {R : Type u_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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 = { toFun := (↑↑f.toRingHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

instance AlgHom.NonUnitalAlgHom.hasCoe {R : Type u_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [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_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : ↑f = NonUnitalAlgHomClass.toNonUnitalAlgHom f

def NonUnitalAlgHom.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₙₐ[S] B) : A →ₙₐ[R] 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

• NonUnitalAlgHom.restrictScalars R f = { toFun := (↑f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₙₐ[S] B) (x : A) : (NonUnitalAlgHom.restrictScalars R f) x = f x

theorem NonUnitalAlgHom.coe_restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₙₐ[S] B) : ↑(NonUnitalAlgHom.restrictScalars R f) = ↑f

theorem NonUnitalAlgHom.coe_restrictScalars' (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →ₙₐ[S] B) : ⇑(NonUnitalAlgHom.restrictScalars R f) = ⇑f

theorem NonUnitalAlgHom.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] : Function.Injective (NonUnitalAlgHom.restrictScalars R)