doc-next-gen

Mathlib.Algebra.Algebra.NonUnitalHom

Module docstring

{"# 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 ","### Operations on the product type

Note that much of this is copied from LinearAlgebra/Prod. ","### Interaction with AlgHom "}

NonUnitalAlgHom structure
[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
Full source 
/-- A morphism respecting addition, multiplication, and scalar multiplication
(denoted as `A →ₛₙₐ[φ] B`, or `A →ₙₐ[R] B` when `φ` is the identity on `R`).
When these arise from algebra structures, this is the same
as a not-necessarily-unital morphism of algebras. -/
structure NonUnitalAlgHom [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
Non-unital algebra homomorphism
Informal description
A non-unital algebra homomorphism is a structure representing a map between two non-unital non-associative semirings \( A \) and \( B \) that preserves addition, multiplication, and scalar multiplication. Here, \( R \) and \( S \) are monoids acting distributively on \( A \) and \( B \) respectively via a monoid homomorphism \( \varphi \colon R \to S \). The homomorphism is denoted as \( A \to_{SNA}[\varphi] B \) or simply \( A \to_{NA}[R] B \) when \( \varphi \) is the identity on \( R \).
term_→ₙₐ_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc NonUnitalAlgHom]
infixr:25 " →ₙₐ " => NonUnitalAlgHom _
Notation for non-unital algebra homomorphisms
Informal description
The notation `→ₙₐ` is used to denote non-unital algebra homomorphisms between two non-unital algebras. Given a monoid homomorphism `φ : R →* S` and non-unital non-associative semirings `A` and `B` with distributive multiplicative actions by `R` and `S` respectively, `A →ₙₐ[φ] B` represents the type of non-unital algebra homomorphisms from `A` to `B` that are compatible with the scalar actions via `φ`.
term_→ₛₙₐ[_]_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc]
notation:25 A " →ₛₙₐ[" φ "] " B => NonUnitalAlgHom φ A B
Non-unital algebra homomorphism notation
Informal description
The notation `A →ₛₙₐ[φ] B` represents the type of non-unital algebra homomorphisms from `A` to `B` with respect to the scalar action `φ`. These are maps that preserve addition, multiplication, and scalar multiplication, but are not required to preserve multiplicative identities or be associative.
NonUnitalAlgSemiHomClass structure
(F : Type*) {R S : outParam Type*} [Monoid R] [Monoid S] (φ : outParam (R →* S)) (A B : outParam Type*) [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction S B] [FunLike F A B] : Prop extends DistribMulActionSemiHomClass F φ A B, MulHomClass F A B
Full source 
/-- `NonUnitalAlgSemiHomClass F φ A B` asserts `F` is a type of bundled algebra homomorphisms
from `A` to `B` which are equivariant with respect to `φ`. -/
class NonUnitalAlgSemiHomClass (F : Type*) {R S : outParam Type*} [Monoid R] [Monoid S]
    (φ : outParam (R →* S)) (A B : outParam Type*)
    [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B]
    [DistribMulAction R A] [DistribMulAction S B] [FunLike F A B] : Prop
    extends DistribMulActionSemiHomClass F φ A B, MulHomClass F A B
Class of Non-Unital Algebra Semi-Homomorphisms with Equivariance
Informal description
The class `NonUnitalAlgSemiHomClass F φ A B` represents a type `F` of bundled algebra homomorphisms from `A` to `B` that are equivariant with respect to a monoid homomorphism `φ : R →* S`. Here, `R` and `S` are monoids acting distributively on the non-unital non-associative semirings `A` and `B` respectively. The homomorphisms in `F` preserve both the multiplicative structure (as per `MulHomClass`) and the scalar multiplication (as per `DistribMulActionSemiHomClass`).
NonUnitalAlgHomClass abbrev
(F : Type*) (R A B : outParam Type*) [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B]
Full source 
/-- `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` -/
abbrev NonUnitalAlgHomClass (F : Type*) (R A B : outParam Type*)
    [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B]
    [DistribMulAction R A] [DistribMulAction R B] [FunLike F A B] :=
  NonUnitalAlgSemiHomClass F (MonoidHom.id R) A B
Class of R-linear Non-Unital Algebra Homomorphisms from A to B
Informal description
The class `NonUnitalAlgHomClass F R A B` asserts that `F` is a type of bundled algebra homomorphisms from `A` to `B` that are `R`-linear, where: - `R` is a monoid acting distributively on the non-unital non-associative semirings `A` and `B` - The homomorphisms preserve both the multiplicative structure and the scalar multiplication - The homomorphisms are `R`-linear with respect to the identity monoid homomorphism on `R`
NonUnitalAlgHomClass.toNonUnitalRingHomClass instance
{F R S A B : Type*} {_ : Monoid R} {_ : Monoid S} {φ : outParam (R →* S)} {_ : NonUnitalNonAssocSemiring A} [DistribMulAction R A] {_ : NonUnitalNonAssocSemiring B} [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] : NonUnitalRingHomClass F A B
Full source 
instance (priority := 100) toNonUnitalRingHomClass
  {F R S A B : Type*} {_ : Monoid R} {_ : Monoid S} {φ : outParam (R →* S)}
    {_ : NonUnitalNonAssocSemiring A} [DistribMulAction R A]
    {_ : NonUnitalNonAssocSemiring B} [DistribMulAction S B] [FunLike F A B]
    [NonUnitalAlgSemiHomClass F φ A B] : NonUnitalRingHomClass F A B :=
  { ‹NonUnitalAlgSemiHomClass F φ A B› with }
Non-Unital Algebra Semi-Homomorphisms are Non-Unital Ring Homomorphisms
Informal description
For any monoids $R$ and $S$, a monoid homomorphism $\phi: R \to S$, non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions of $R$ on $A$ and $S$ on $B$, and a type $F$ of functions from $A$ to $B$ that are non-unital algebra semi-homomorphisms with respect to $\phi$, then $F$ is also a type of non-unital ring homomorphisms from $A$ to $B$.
NonUnitalAlgHomClass.instSemilinearMapClassOfNonUnitalAlgSemiHomClassToMonoidHomRingHom instance
{F R S A B : Type*} {_ : Semiring R} {_ : Semiring S} {φ : R →+* S} {_ : NonUnitalSemiring A} {_ : NonUnitalSemiring B} [Module R A] [Module S B] [FunLike F A B] [NonUnitalAlgSemiHomClass (R := R) (S := S) F φ A B] : SemilinearMapClass F φ A B
Full source 
instance (priority := 100) {F R S A B : Type*}
    {_ : Semiring R} {_ : Semiring S} {φ : R →+* S}
    {_ : NonUnitalSemiring A} {_ : NonUnitalSemiring B} [Module R A] [Module S B] [FunLike F A B]
    [NonUnitalAlgSemiHomClass (R := R) (S := S) F φ A B] :
    SemilinearMapClass F φ A B :=
  { ‹NonUnitalAlgSemiHomClass F φ A B› with map_smulₛₗ := map_smulₛₗ }
Non-Unital Algebra Semi-Homomorphisms as Semilinear Maps
Informal description
For any semirings $R$ and $S$, a ring homomorphism $\varphi: R \to S$, non-unital semirings $A$ and $B$ equipped with module structures over $R$ and $S$ respectively, and a type $F$ of functions from $A$ to $B$ that are non-unital algebra semi-homomorphisms with respect to $\varphi$, the functions in $F$ are also $\varphi$-semilinear maps. This means they preserve addition and satisfy the semilinearity condition $f(r \cdot a) = \varphi(r) \cdot f(a)$ for all $r \in R$ and $a \in A$.
NonUnitalAlgHomClass.instLinearMapClass instance
{F : Type*} [FunLike F A B] [Module R B] [NonUnitalAlgHomClass F R A B] : LinearMapClass F R A B
Full source 
instance (priority := 100) {F : Type*} [FunLike F A B] [Module R B] [NonUnitalAlgHomClass F R A B] :
    LinearMapClass F R A B :=
  { ‹NonUnitalAlgHomClass F R A B› with map_smulₛₗ := map_smulₛₗ }
Non-Unital Algebra Homomorphisms as Linear Maps
Informal description
For any type $F$ of non-unital algebra homomorphisms from $A$ to $B$ over a semiring $R$, where $B$ is a module over $R$, the homomorphisms in $F$ are also $R$-linear maps. This means they preserve addition and scalar multiplication: for any $f \in F$, $x, y \in A$, and $r \in R$, we have $f(x + y) = f(x) + f(y)$ and $f(r \cdot x) = r \cdot f(x)$.
NonUnitalAlgHomClass.toNonUnitalAlgSemiHom definition
{F R S : Type*} [Monoid R] [Monoid S] {φ : R →* S} {A B : Type*} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] (f : F) : A →ₛₙₐ[φ] B
Full source 
/-- 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`. -/
@[coe]
def toNonUnitalAlgSemiHom {F R S : Type*} [Monoid R] [Monoid S] {φ : R →* S} {A B : Type*}
    [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
    [NonUnitalNonAssocSemiring B] [DistribMulAction S B] [FunLike F A B]
    [NonUnitalAlgSemiHomClass F φ A B] (f : F) : A →ₛₙₐ[φ] B :=
  { (f : A →ₙ+* B) with
    toFun := f
    map_smul' := map_smulₛₗ f }
Coercion from non-unital algebra semi-homomorphism class to concrete homomorphism
Informal description
Given monoids $R$ and $S$, a monoid homomorphism $\varphi: R \to S$, and non-unital non-associative semirings $A$ and $B$ equipped with distributive multiplicative actions of $R$ on $A$ and $S$ on $B$ respectively, this function converts an element $f$ of a type $F$ (where $F$ satisfies `NonUnitalAlgSemiHomClass F φ A B`) into an actual non-unital algebra semi-homomorphism $A \to_{SNA}[\varphi] B$. The resulting homomorphism preserves: 1. The additive structure (addition and zero) 2. The multiplicative structure (multiplication) 3. The scalar multiplication via $\varphi$ (i.e., $f(r \cdot a) = \varphi(r) \cdot f(a)$ for all $r \in R$, $a \in A$) This is declared as the default coercion from $F$ to $A \to_{SNA}[\varphi] B$.
NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass instance
{F R S A B : Type*} [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)
Full source 
instance {F R S A B : Type*} [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) :=
  ⟨toNonUnitalAlgSemiHom⟩
Coercion from Non-Unital Algebra Semi-Homomorphism Class to Concrete Homomorphism
Informal description
For any monoids $R$ and $S$, a monoid homomorphism $\varphi: R \to S$, and non-unital non-associative semirings $A$ and $B$ equipped with distributive multiplicative actions of $R$ on $A$ and $S$ on $B$ respectively, any element $f$ of a type $F$ that satisfies `NonUnitalAlgSemiHomClass F φ A B` can be automatically converted into a non-unital algebra semi-homomorphism $A \to_{SNA}[\varphi] B$. This homomorphism preserves addition, multiplication, and scalar multiplication via $\varphi$.
NonUnitalAlgHomClass.toNonUnitalAlgHom definition
{F R : Type*} [Monoid R] {A B : Type*} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B
Full source 
/-- 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`. -/
def toNonUnitalAlgHom {F R : Type*} [Monoid R] {A B : Type*}
    [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
    [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
    [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] B :=
  { (f : A →ₙ+* B) with
    toFun := f
    map_smul' := map_smulₛₗ f }
Coercion from non-unital algebra homomorphism class to concrete homomorphism
Informal description
Given a type `F` satisfying `NonUnitalAlgHomClass F R A B` (i.e., elements of `F` are $R$-linear non-unital algebra homomorphisms between non-unital non-associative semirings `A` and `B`), this function converts an element `f : F` into an actual bundled non-unital algebra homomorphism `A →ₙₐ[R] B`. The resulting homomorphism preserves addition, multiplication, and scalar multiplication by elements of the monoid $R$, where $R$ acts distributively on both $A$ and $B$. This is declared as the default coercion from `F` to `A →ₙₐ[R] B`.
NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomId instance
{F R : Type*} [Monoid R] {A B : Type*} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] : CoeTC F (A →ₙₐ[R] B)
Full source 
instance {F R : Type*} [Monoid R] {A B : Type*}
    [NonUnitalNonAssocSemiring A] [DistribMulAction R A]
    [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
    [FunLike F A B] [NonUnitalAlgHomClass F R A B] :
    CoeTC F (A →ₙₐ[R] B) :=
  ⟨toNonUnitalAlgHom⟩
Coercion from Non-Unital Algebra Homomorphism Class to Concrete Homomorphism
Informal description
For any monoid $R$ and non-unital non-associative semirings $A$ and $B$ with distributive $R$-actions, any type $F$ in the `NonUnitalAlgHomClass F R A B` can be treated as a bundled non-unital algebra homomorphism $A →ₙₐ[R] B$ that preserves addition, multiplication, and scalar multiplication by elements of $R$.
NonUnitalAlgHom.instDFunLike instance
: DFunLike (A →ₛₙₐ[φ] B) A fun _ => B
Full source 
instance : DFunLike (A →ₛₙₐ[φ] B) A fun _ => B where
  coe f := f.toFun
  coe_injective' := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
Non-unital Algebra Homomorphisms as Functions
Informal description
For non-unital algebra homomorphisms $A \to_{SNA}[\varphi] B$, there is a canonical way to treat them as dependent functions from $A$ to $B$.
NonUnitalAlgHom.toFun_eq_coe theorem
(f : A →ₛₙₐ[φ] B) : f.toFun = ⇑f
Full source 
@[simp]
theorem toFun_eq_coe (f : A →ₛₙₐ[φ] B) : f.toFun = ⇑f :=
  rfl
Equality of Underlying Function and Coercion for Non-Unital Algebra Homomorphisms
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$, the underlying function $f$ is equal to its coercion to a function, i.e., $f = \uparrow f$.
NonUnitalAlgHom.Simps.apply definition
(f : A →ₛₙₐ[φ] B) : A → B
Full source 
/-- See Note [custom simps projection] -/
def Simps.apply (f : A →ₛₙₐ[φ] B) : A → B := f
Underlying map of a non-unital algebra homomorphism
Informal description
Given a non-unital algebra homomorphism \( f \colon A \to_{SNA}[\varphi] B \), this function extracts the underlying map \( f \colon A \to B \).
NonUnitalAlgHom.coe_coe theorem
{F : Type*} [FunLike F A B] [NonUnitalAlgSemiHomClass F φ A B] (f : F) : ⇑(f : A →ₛₙₐ[φ] B) = f
Full source 
@[simp]
protected theorem coe_coe {F : Type*} [FunLike F A B]
    [NonUnitalAlgSemiHomClass F φ A B] (f : F) :
    ⇑(f : A →ₛₙₐ[φ] B) = f :=
  rfl
Coercion of Non-Unital Algebra Semi-Homomorphisms Preserves Underlying Function
Informal description
For any type $F$ with a `FunLike` instance and a `NonUnitalAlgSemiHomClass` instance with respect to monoids $R$ and $S$, a monoid homomorphism $\varphi: R \to S$, and non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions of $R$ on $A$ and $S$ on $B$, the coercion of an element $f \in F$ to a non-unital algebra semi-homomorphism $A \to_{SNA}[\varphi] B$ is equal to $f$ itself when viewed as a function from $A$ to $B$.
NonUnitalAlgHom.coe_injective theorem
: @Function.Injective (A →ₛₙₐ[φ] B) (A → B) (↑)
Full source 
theorem coe_injective : @Function.Injective (A →ₛₙₐ[φ] B) (A → B) (↑) := by
  rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
Injectivity of the Canonical Map from Non-Unital Algebra Homomorphisms to Functions
Informal description
The canonical map from the type of non-unital algebra homomorphisms $A \to_{SNA}[\varphi] B$ to the type of functions $A \to B$ is injective. That is, if two non-unital algebra homomorphisms $f, g \colon A \to_{SNA}[\varphi] B$ satisfy $f(x) = g(x)$ for all $x \in A$, then $f = g$.
NonUnitalAlgHom.instFunLike instance
: FunLike (A →ₛₙₐ[φ] B) A B
Full source 
instance : FunLike (A →ₛₙₐ[φ] B) A B where
  coe f := f.toFun
  coe_injective' := coe_injective
Non-Unital Algebra Homomorphisms as Functions
Informal description
For non-unital algebra homomorphisms $A \to_{SNA}[\varphi] B$, there is a canonical way to treat them as functions from $A$ to $B$.
NonUnitalAlgHom.instNonUnitalAlgSemiHomClass instance
: NonUnitalAlgSemiHomClass (A →ₛₙₐ[φ] B) φ A B
Full source 
instance : NonUnitalAlgSemiHomClass (A →ₛₙₐ[φ] B) φ A B where
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  map_mul f := f.map_mul'
  map_smulₛₗ f := f.map_smul'
Non-Unital Algebra Homomorphisms as Semi-Homomorphisms
Informal description
For any monoids $R$ and $S$ with a monoid homomorphism $\varphi: R \to S$, and any non-unital non-associative semirings $A$ and $B$ equipped with distributive multiplicative actions by $R$ and $S$ respectively, the type of non-unital algebra homomorphisms $A \to_{SNA}[\varphi] B$ forms a class of non-unital algebra semi-homomorphisms that are equivariant with respect to $\varphi$ and preserve both the multiplicative and additive structures.
NonUnitalAlgHom.ext theorem
{f g : A →ₛₙₐ[φ] B} (h : ∀ x, f x = g x) : f = g
Full source 
@[ext]
theorem ext {f g : A →ₛₙₐ[φ] B} (h : ∀ x, f x = g x) : f = g :=
  coe_injective <| funext h
Extensionality of Non-Unital Algebra Homomorphisms
Informal description
For any two non-unital algebra homomorphisms $f, g \colon A \to_{SNA}[\varphi] B$, if $f(x) = g(x)$ for all $x \in A$, then $f = g$.
NonUnitalAlgHom.congr_fun theorem
{f g : A →ₛₙₐ[φ] B} (h : f = g) (x : A) : f x = g x
Full source 
theorem congr_fun {f g : A →ₛₙₐ[φ] B} (h : f = g) (x : A) : f x = g x :=
  h ▸ rfl
Function Equality Implies Pointwise Equality for Non-Unital Algebra Homomorphisms
Informal description
For any two non-unital algebra homomorphisms $f, g \colon A \to_{SNA}[\varphi] B$, if $f = g$ as homomorphisms, then for every element $x \in A$, the evaluations $f(x)$ and $g(x)$ are equal.
NonUnitalAlgHom.coe_mk theorem
(f : A → B) (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f
Full source 
@[simp]
theorem coe_mk (f : A → B) (h₁ h₂ h₃ h₄) : ⇑(⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f :=
  rfl
Underlying Function of Constructed Non-Unital Algebra Homomorphism
Informal description
Given a function $f \colon A \to B$ and proofs $h_1, h_2, h_3, h_4$ that $f$ preserves the non-unital algebra structure (addition, scalar multiplication, multiplication, and compatibility with $\varphi$), the underlying function of the constructed non-unital algebra homomorphism $\langle \langle \langle f, h_1 \rangle, h_2, h_3 \rangle, h_4 \rangle \colon A \to_{SNA}[\varphi] B$ is equal to $f$.
NonUnitalAlgHom.mk_coe theorem
(f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) : (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f
Full source 
@[simp]
theorem mk_coe (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) : (⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) = f := by
  rfl
Construction of Non-Unital Algebra Homomorphism Equals Original Function
Informal description
Let $A$ and $B$ be non-unital non-associative semirings equipped with distributive multiplicative actions by monoids $R$ and $S$ respectively, and let $\varphi : R \to S$ be a monoid homomorphism. Given a non-unital algebra homomorphism $f : A \to_{SNA}[\varphi] B$ and proofs $h_1, h_2, h_3, h_4$ that $f$ preserves the relevant operations, the constructed homomorphism $\langle \langle \langle f, h_1 \rangle, h_2, h_3 \rangle, h_4 \rangle$ is equal to $f$.
NonUnitalAlgHom.toDistribMulActionHom_eq_coe theorem
(f : A →ₛₙₐ[φ] B) : f.toDistribMulActionHom = ↑f
Full source 
@[simp]
theorem toDistribMulActionHom_eq_coe (f : A →ₛₙₐ[φ] B) : f.toDistribMulActionHom = ↑f :=
  rfl
Underlying Function of Distributive Multiplicative Action Homomorphism from Non-Unital Algebra Homomorphism
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$, the underlying function of the associated distributive multiplicative action homomorphism $f.toDistribMulActionHom$ is equal to $f$.
NonUnitalAlgHom.toMulHom_eq_coe theorem
(f : A →ₛₙₐ[φ] B) : f.toMulHom = ↑f
Full source 
@[simp]
theorem toMulHom_eq_coe (f : A →ₛₙₐ[φ] B) : f.toMulHom = ↑f :=
  rfl
Underlying multiplicative homomorphism equals the function itself
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$ between non-unital non-associative semirings $A$ and $B$ with compatible scalar actions, the underlying multiplicative homomorphism of $f$ is equal to $f$ itself when viewed as a function.
NonUnitalAlgHom.coe_to_distribMulActionHom theorem
(f : A →ₛₙₐ[φ] B) : ⇑(f : A →ₑ+[φ] B) = f
Full source 
@[simp, norm_cast]
theorem coe_to_distribMulActionHom (f : A →ₛₙₐ[φ] B) : ⇑(f : A →ₑ+[φ] B) = f :=
  rfl
Underlying Function of Non-Unital Algebra Homomorphism as Distributive Action Homomorphism
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$, the underlying function of the associated equivariant additive monoid homomorphism $f \colon A \to_{e+}[\varphi] B$ is equal to $f$ itself.
NonUnitalAlgHom.coe_to_mulHom theorem
(f : A →ₛₙₐ[φ] B) : ⇑(f : A →ₙ* B) = f
Full source 
@[simp, norm_cast]
theorem coe_to_mulHom (f : A →ₛₙₐ[φ] B) : ⇑(f : A →ₙ* B) = f :=
  rfl
Underlying function of multiplicative homomorphism equals the non-unital algebra homomorphism
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$, the underlying function of the multiplicative homomorphism $f \colon A \to^* B$ is equal to $f$ itself.
NonUnitalAlgHom.to_distribMulActionHom_injective theorem
{f g : A →ₛₙₐ[φ] B} (h : (f : A →ₑ+[φ] B) = (g : A →ₑ+[φ] B)) : f = g
Full source 
theorem to_distribMulActionHom_injective {f g : A →ₛₙₐ[φ] B}
    (h : (f : A →ₑ+[φ] B) = (g : A →ₑ+[φ] B)) : f = g := by
  ext a
  exact DistribMulActionHom.congr_fun h a
Injectivity of Non-Unital Algebra Homomorphism Construction from Equivariant Additive Monoid Homomorphism
Informal description
For any two non-unital algebra homomorphisms $f, g \colon A \to_{SNA}[\varphi] B$, if their underlying equivariant additive monoid homomorphisms are equal, then $f$ and $g$ are equal.
NonUnitalAlgHom.to_mulHom_injective theorem
{f g : A →ₛₙₐ[φ] B} (h : (f : A →ₙ* B) = (g : A →ₙ* B)) : f = g
Full source 
theorem to_mulHom_injective {f g : A →ₛₙₐ[φ] B} (h : (f : A →ₙ* B) = (g : A →ₙ* B)) : f = g := by
  ext a
  exact DFunLike.congr_fun h a
Injectivity of Non-Unital Algebra Homomorphism via Multiplicative Homomorphism
Informal description
For any two non-unital algebra homomorphisms $f, g \colon A \to_{SNA}[\varphi] B$, if the underlying multiplicative homomorphisms $f$ and $g$ are equal, then $f = g$.
NonUnitalAlgHom.coe_distribMulActionHom_mk theorem
(f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) : ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₑ+[φ] B) = ⟨⟨f, h₁⟩, h₂, h₃⟩
Full source 
@[norm_cast]
theorem coe_distribMulActionHom_mk (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₑ+[φ] B) = ⟨⟨f, h₁⟩, h₂, h₃⟩ := by
  rfl
Coefficient Extraction for Non-Unital Algebra Homomorphism Construction
Informal description
Let $A$ and $B$ be non-unital non-associative semirings with distributive multiplicative actions by monoids $R$ and $S$ respectively, and let $\varphi: R \to S$ be a monoid homomorphism. For any function $f: A \to B$ and proofs $h_1, h_2, h_3, h_4$ that $f$ preserves the relevant structures, the underlying equivariant additive monoid homomorphism of the constructed non-unital algebra homomorphism $\langle \langle \langle f, h_1 \rangle, h_2, h_3 \rangle, h_4 \rangle : A \to_{SNA}[\varphi] B$ is equal to $\langle \langle f, h_1 \rangle, h_2, h_3 \rangle : A \to_{\varphi}^+ B$.
NonUnitalAlgHom.coe_mulHom_mk theorem
(f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) : ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₙ* B) = ⟨f, h₄⟩
Full source 
@[norm_cast]
theorem coe_mulHom_mk (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₙ* B) = ⟨f, h₄⟩ := by
  rfl
Coercion of Constructed Non-Unital Algebra Homomorphism to Multiplicative Homomorphism
Informal description
Let $A$ and $B$ be non-unital non-associative semirings with distributive multiplicative actions by monoids $R$ and $S$ respectively, and let $\varphi: R \to S$ be a monoid homomorphism. For any function $f: A \to B$ and proofs $h_1, h_2, h_3, h_4$ that $f$ preserves the relevant structures, the underlying multiplicative homomorphism of the constructed non-unital algebra homomorphism $\langle \langle \langle f, h_1 \rangle, h_2, h_3 \rangle, h_4 \rangle: A \to_{SNA}[\varphi] B$ is equal to $\langle f, h_4 \rangle: A \to^* B$.
NonUnitalAlgHom.map_smul theorem
(f : A →ₛₙₐ[φ] B) (c : R) (x : A) : f (c • x) = (φ c) • f x
Full source 
@[simp] -- Marked as `@[simp]` because `MulActionSemiHomClass.map_smulₛₗ` can't be.
protected theorem map_smul (f : A →ₛₙₐ[φ] B) (c : R) (x : A) : f (c • x) = (φ c) • f x :=
  map_smulₛₗ _ _ _
Scalar Multiplication Preservation for Non-Unital Algebra Homomorphisms
Informal description
Let $R$ and $S$ be monoids, and let $\varphi: R \to S$ be a monoid homomorphism. Let $A$ and $B$ be non-unital non-associative semirings equipped with distributive multiplicative actions by $R$ and $S$ respectively. For any non-unital algebra homomorphism $f: A \to_{SNA}[\varphi] B$, scalar $c \in R$, and element $x \in A$, we have: \[ f(c \cdot x) = \varphi(c) \cdot f(x). \]
NonUnitalAlgHom.map_add theorem
(f : A →ₛₙₐ[φ] B) (x y : A) : f (x + y) = f x + f y
Full source 
protected theorem map_add (f : A →ₛₙₐ[φ] B) (x y : A) : f (x + y) = f x + f y :=
  map_add _ _ _
Additivity of Non-Unital Algebra Homomorphisms
Informal description
Let $R$ and $S$ be monoids with a monoid homomorphism $\varphi: R \to S$, and let $A$ and $B$ be non-unital non-associative semirings equipped with distributive multiplicative actions by $R$ and $S$ respectively. For any non-unital algebra homomorphism $f: A \to_{SNA}[\varphi] B$ and any elements $x, y \in A$, we have $f(x + y) = f(x) + f(y)$.
NonUnitalAlgHom.map_mul theorem
(f : A →ₛₙₐ[φ] B) (x y : A) : f (x * y) = f x * f y
Full source 
protected theorem map_mul (f : A →ₛₙₐ[φ] B) (x y : A) : f (x * y) = f x * f y :=
  map_mul _ _ _
Multiplication preservation property of non-unital algebra homomorphisms
Informal description
Let $R$ and $S$ be monoids with a monoid homomorphism $\varphi: R \to S$, and let $A$ and $B$ be non-unital non-associative semirings equipped with distributive multiplicative actions by $R$ and $S$ respectively. For any non-unital algebra homomorphism $f: A \to_{SNA}[\varphi] B$ and any elements $x, y \in A$, we have $f(x * y) = f(x) * f(y)$.
NonUnitalAlgHom.map_zero theorem
(f : A →ₛₙₐ[φ] B) : f 0 = 0
Full source 
protected theorem map_zero (f : A →ₛₙₐ[φ] B) : f 0 = 0 :=
  map_zero _
Non-unital algebra homomorphisms preserve zero
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{SNA}[\varphi] B$ between non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions by monoids $R$ and $S$ respectively (via a monoid homomorphism $\varphi \colon R \to S$), the homomorphism preserves the zero element: $f(0) = 0$.
NonUnitalAlgHom.id definition
(R A : Type*) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] : A →ₙₐ[R] A
Full source 
/-- The identity map as a `NonUnitalAlgHom`. -/
protected def id (R A : Type*) [Monoid R] [NonUnitalNonAssocSemiring A]
    [DistribMulAction R A] : A →ₙₐ[R] A :=
  { NonUnitalRingHom.id A with
    toFun := id
    map_smul' := fun _ _ => rfl }
Identity non-unital algebra homomorphism
Informal description
The identity map as a non-unital algebra homomorphism from a non-unital non-associative semiring \( A \) to itself, where \( A \) is equipped with a distributive multiplicative action by a monoid \( R \). This map preserves addition, multiplication, and scalar multiplication, and is defined by the identity function \( \text{id} \colon A \to A \).
NonUnitalAlgHom.coe_id theorem
: ⇑(NonUnitalAlgHom.id R A) = id
Full source 
@[simp, norm_cast]
theorem coe_id : ⇑(NonUnitalAlgHom.id R A) = id :=
  rfl
Identity Non-Unital Algebra Homomorphism as Identity Function
Informal description
The underlying function of the identity non-unital algebra homomorphism from $A$ to itself (where $A$ is a non-unital non-associative semiring with a distributive multiplicative action by a monoid $R$) is equal to the identity function on $A$.
NonUnitalAlgHom.instZero instance
: Zero (A →ₛₙₐ[φ] B)
Full source 
instance : Zero (A →ₛₙₐ[φ] B) :=
  ⟨{ (0 : A →ₑ+[φ] B) with map_mul' := by simp }⟩
Zero Element in Non-unital Algebra Homomorphisms
Informal description
For any non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions by monoids $R$ and $S$ respectively, and a monoid homomorphism $\varphi: R \to S$, the type of $\varphi$-equivariant non-unital algebra homomorphisms from $A$ to $B$ has a zero element.
NonUnitalAlgHom.instOneId instance
: One (A →ₙₐ[R] A)
Full source 
instance : One (A →ₙₐ[R] A) :=
  ⟨NonUnitalAlgHom.id R A⟩
Identity Non-Unital Algebra Homomorphism as Multiplicative Identity
Informal description
For any monoid $R$ and non-unital non-associative semiring $A$ with a distributive multiplicative action by $R$, the type of non-unital algebra homomorphisms from $A$ to itself has a multiplicative identity element given by the identity map.
NonUnitalAlgHom.coe_zero theorem
: ⇑(0 : A →ₛₙₐ[φ] B) = 0
Full source 
@[simp]
theorem coe_zero : ⇑(0 : A →ₛₙₐ[φ] B) = 0 :=
  rfl
Zero Homomorphism is the Zero Function in Non-Unital Algebra Homomorphisms
Informal description
The zero homomorphism in the space of non-unital algebra homomorphisms from $A$ to $B$ (with respect to a monoid homomorphism $\varphi: R \to S$) is equal to the zero function, i.e., for any $a \in A$, $(0 : A \to_{SNA}[\varphi] B)(a) = 0$.
NonUnitalAlgHom.coe_one theorem
: ((1 : A →ₙₐ[R] A) : A → A) = id
Full source 
@[simp]
theorem coe_one : ((1 : A →ₙₐ[R] A) : A → A) = id :=
  rfl
Identity Non-Unital Algebra Homomorphism as Identity Function
Informal description
For any monoid $R$ and non-unital non-associative semiring $A$ with a distributive multiplicative action by $R$, the identity non-unital algebra homomorphism $1 \colon A \to_{NA}[R] A$ (when viewed as a function from $A$ to $A$) is equal to the identity function $\text{id} \colon A \to A$.
NonUnitalAlgHom.zero_apply theorem
(a : A) : (0 : A →ₛₙₐ[φ] B) a = 0
Full source 
theorem zero_apply (a : A) : (0 : A →ₛₙₐ[φ] B) a = 0 :=
  rfl
Zero Homomorphism Evaluates to Zero
Informal description
For any element $a$ in a non-unital non-associative semiring $A$, the zero homomorphism $0 \colon A \to_{SNA}[\varphi] B$ evaluated at $a$ equals the zero element in the non-unital non-associative semiring $B$.
NonUnitalAlgHom.one_apply theorem
(a : A) : (1 : A →ₙₐ[R] A) a = a
Full source 
theorem one_apply (a : A) : (1 : A →ₙₐ[R] A) a = a :=
  rfl
Identity Non-Unital Algebra Homomorphism Acts as Identity Function
Informal description
For any non-unital non-associative semiring $A$ with a distributive multiplicative action by a monoid $R$, the identity non-unital algebra homomorphism $1 \colon A \to_{NA}[R] A$ satisfies $1(a) = a$ for all $a \in A$.
NonUnitalAlgHom.instInhabited instance
: Inhabited (A →ₛₙₐ[φ] B)
Full source 
instance : Inhabited (A →ₛₙₐ[φ] B) :=
  ⟨0⟩
Inhabited Type of Non-unital Algebra Homomorphisms
Informal description
For any non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions by monoids $R$ and $S$ respectively, and a monoid homomorphism $\varphi: R \to S$, the type of $\varphi$-equivariant non-unital algebra homomorphisms from $A$ to $B$ is inhabited.
NonUnitalAlgHom.comp definition
(f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [κ : MonoidHom.CompTriple φ ψ χ] : A →ₛₙₐ[χ] C
Full source 
/-- The composition of morphisms is a morphism. -/
def comp (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [κ : MonoidHom.CompTriple φ ψ χ] :
    A →ₛₙₐ[χ] C :=
  { (f : B →ₙ* C).comp (g : A →ₙ* B), (f : B →ₑ+[ψ] C).comp (g : A →ₑ+[φ] B) with }
Composition of Non-unital Algebra Homomorphisms
Informal description
Given non-unital non-associative semirings \( A \), \( B \), and \( C \) with distributive multiplicative actions by monoids \( R \), \( S \), and \( T \) respectively, and monoid homomorphisms \( \varphi \colon R \to S \) and \( \psi \colon S \to T \), the composition \( f \circ g \colon A \to C \) of two non-unital algebra homomorphisms \( g \colon A \to B \) and \( f \colon B \to C \) is a non-unital algebra homomorphism with respect to the composition \( \chi = \psi \circ \varphi \). This means that \( f \circ g \) preserves addition, multiplication, and scalar multiplication (i.e., \( (f \circ g)(a + b) = (f \circ g)(a) + (f \circ g)(b) \), \( (f \circ g)(a * b) = (f \circ g)(a) * (f \circ g)(b) \), and \( (f \circ g)(r \cdot a) = \chi(r) \cdot (f \circ g)(a) \) for all \( a, b \in A \) and \( r \in R \)).
NonUnitalAlgHom.coe_comp theorem
(f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] : ⇑(f.comp g) = (⇑f) ∘ (⇑g)
Full source 
@[simp, norm_cast]
theorem coe_comp (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] :
    ⇑(f.comp g) = (⇑f) ∘ (⇑g) := rfl
Composition of Non-unital Algebra Homomorphisms Preserves Underlying Functions
Informal description
Let $A$, $B$, and $C$ be non-unital non-associative semirings with distributive multiplicative actions by monoids $R$, $S$, and $T$ respectively, and let $\varphi \colon R \to S$ and $\psi \colon S \to T$ be monoid homomorphisms. For any non-unital algebra homomorphisms $g \colon A \to B$ (equivariant with respect to $\varphi$) and $f \colon B \to C$ (equivariant with respect to $\psi$), the underlying function of the composition $f \circ g$ equals the composition of the underlying functions of $f$ and $g$.
NonUnitalAlgHom.comp_apply theorem
(f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] (x : A) : f.comp g x = f (g x)
Full source 
theorem comp_apply (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B) [MonoidHom.CompTriple φ ψ χ] (x : A) :
    f.comp g x = f (g x) := rfl
Composition of Non-Unital Algebra Homomorphisms Preserves Evaluation
Informal description
Let $A$, $B$, and $C$ be non-unital non-associative semirings with distributive multiplicative actions by monoids $R$, $S$, and $T$ respectively, and let $\varphi \colon R \to S$ and $\psi \colon S \to T$ be monoid homomorphisms. For any non-unital algebra homomorphisms $g \colon A \to B$ (with respect to $\varphi$) and $f \colon B \to C$ (with respect to $\psi$), and any element $x \in A$, the composition $f \circ g$ evaluated at $x$ equals $f$ applied to $g(x)$, i.e., $(f \circ g)(x) = f(g(x))$.
NonUnitalAlgHom.inverse definition
(f : A →ₙₐ[R] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B₁ →ₙₐ[R] A
Full source 
/-- The inverse of a bijective morphism is a morphism. -/
def inverse (f : A →ₙₐ[R] B₁) (g : B₁ → A)
    (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : B₁ →ₙₐ[R] A :=
  { (f : A →ₙ* B₁).inverse g h₁ h₂, (f : A →+[R] B₁).inverse g h₁ h₂ with }
Inverse of a bijective non-unital algebra homomorphism is a non-unital algebra homomorphism
Informal description
Given a non-unital algebra homomorphism \( f : A \to B \) between non-unital non-associative semirings \( A \) and \( B \) (with a distributive action of a monoid \( R \)), and a function \( g : B \to A \) that is both a left and right inverse of \( f \), the function \( g \) can be equipped with the structure of a non-unital algebra homomorphism from \( B \) to \( A \). This means \( g \) preserves addition, multiplication, and scalar multiplication by elements of \( R \).
NonUnitalAlgHom.coe_inverse theorem
(f : A →ₙₐ[R] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : (inverse f g h₁ h₂ : B₁ → A) = g
Full source 
@[simp]
theorem coe_inverse (f : A →ₙₐ[R] B₁) (g : B₁ → A) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : (inverse f g h₁ h₂ : B₁ → A) = g :=
  rfl
Underlying function of inverse non-unital algebra homomorphism equals its set-theoretic inverse
Informal description
Given a non-unital algebra homomorphism $f \colon A \to B$ between non-unital non-associative semirings $A$ and $B$ with a distributive action of a monoid $R$, and a function $g \colon B \to A$ that is both a left and right inverse of $f$, the underlying function of the inverse homomorphism $\text{inverse}\ f\ g\ h_1\ h_2$ is equal to $g$.
NonUnitalAlgHom.inverse' definition
(f : A →ₛₙₐ[φ] B) (g : B → A) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : B →ₛₙₐ[φ'] A
Full source 
/-- The inverse of a bijective morphism is a morphism. -/
def inverse' (f : A →ₛₙₐ[φ] B) (g : B → A)
    (k : Function.RightInverse φ' φ)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    B →ₛₙₐ[φ'] A :=
  { (f : A →ₙ* B).inverse g h₁ h₂, (f : A →ₑ+[φ] B).inverse' g k h₁ h₂ with
    map_zero' := by
      simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]
      rw [← f.map_zero, h₁]
    map_add' := fun x y ↦ by
      simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]
      rw [← h₂ x, ← h₂ y, ← map_add, h₁, h₂, h₂] }
Inverse of a bijective non-unital algebra homomorphism with right inverse condition
Informal description
Given a non-unital algebra homomorphism \( f : A \to_{SNA}[\varphi] B \) between non-unital non-associative semirings \( A \) and \( B \), where \( \varphi : R \to S \) is a monoid homomorphism, and given a function \( g : B \to A \) that is both a left and right inverse of \( f \), and a function \( \varphi' : S \to R \) that is a right inverse of \( \varphi \), then \( g \) can be equipped with the structure of a non-unital algebra homomorphism \( B \to_{SNA}[\varphi'] A \). This means \( g \) preserves addition, multiplication, and scalar multiplication (with respect to \( \varphi' \)).
NonUnitalAlgHom.coe_inverse' theorem
(f : A →ₛₙₐ[φ] B) (g : B → A) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) : (inverse' f g k h₁ h₂ : B → A) = g
Full source 
@[simp]
theorem coe_inverse' (f : A →ₛₙₐ[φ] B) (g : B → A)
    (k : Function.RightInverse φ' φ)
    (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    (inverse' f g k h₁ h₂ : B → A) = g :=
  rfl
Underlying function of inverse non-unital algebra homomorphism equals its set-theoretic inverse
Informal description
Let $A$ and $B$ be non-unital non-associative semirings with distributive actions of monoids $R$ and $S$ respectively, and let $\varphi: R \to S$ be a monoid homomorphism. Given a non-unital algebra homomorphism $f: A \to_{SNA}[\varphi] B$, a function $g: B \to A$ that is both left and right inverse to $f$, and a right inverse $\varphi': S \to R$ of $\varphi$, then the underlying function of the inverse homomorphism $\text{inverse'}\ f\ g\ k\ h_1\ h_2$ equals $g$.
NonUnitalAlgHom.fst definition
: A × B →ₙₐ[R] A
Full source 
/-- The first projection of a product is a non-unital algebra homomorphism. -/
@[simps]
def fst : A × BA × B →ₙₐ[R] A where
  toFun := Prod.fst
  map_zero' := rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  map_mul' _ _ := rfl
First projection as a non-unital algebra homomorphism
Informal description
The first projection map from the product of two non-unital non-associative semirings $A \times B$ to $A$ is a non-unital algebra homomorphism. Specifically, it preserves addition, multiplication, and scalar multiplication by elements of the monoid $R$.
NonUnitalAlgHom.snd definition
: A × B →ₙₐ[R] B
Full source 
/-- The second projection of a product is a non-unital algebra homomorphism. -/
@[simps]
def snd : A × BA × B →ₙₐ[R] B where
  toFun := Prod.snd
  map_zero' := rfl
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  map_mul' _ _ := rfl
Second projection as a non-unital algebra homomorphism
Informal description
The second projection map from the product $A \times B$ of two non-unital non-associative semirings to $B$ is a non-unital algebra homomorphism. Specifically, it preserves addition, multiplication, and scalar multiplication by elements of the monoid $R$.
NonUnitalAlgHom.prod definition
(f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C
Full source 
/-- The prod of two morphisms is a morphism. -/
@[simps]
def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where
  toFun := Pi.prod f g
  map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero]
  map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
  map_mul' x y := by simp only [Pi.prod, Prod.mk_mul_mk, map_mul]
  map_smul' c x := by simp only [Pi.prod, map_smul, MonoidHom.id_apply, id_eq, Prod.smul_mk]
Product of non-unital algebra homomorphisms
Informal description
Given two non-unital algebra homomorphisms \( f \colon A \to_{NA}[R] B \) and \( g \colon A \to_{NA}[R] C \), their product \( f \times g \) is a non-unital algebra homomorphism from \( A \) to the product algebra \( B \times C \). This homomorphism maps each element \( a \in A \) to the pair \( (f(a), g(a)) \in B \times C \), preserving addition, multiplication, and scalar multiplication.
NonUnitalAlgHom.coe_prod theorem
(f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g
Full source 
theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
  rfl
Underlying Function of Product Homomorphism Equals Component-wise Product
Informal description
For any two non-unital algebra homomorphisms $f \colon A \to_{NA}[R] B$ and $g \colon A \to_{NA}[R] C$, the underlying function of their product homomorphism $f \times g$ is equal to the component-wise product function $\Pi.\text{prod}\,f\,g$, which maps each $a \in A$ to $(f(a), g(a)) \in B \times C$.
NonUnitalAlgHom.fst_prod theorem
(f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (fst R B C).comp (prod f g) = f
Full source 
@[simp]
theorem fst_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (fst R B C).comp (prod f g) = f := by
  rfl
First Projection of Product Homomorphism Equals Original Homomorphism
Informal description
Let $A$, $B$, and $C$ be non-unital non-associative semirings with a distributive multiplicative action by a monoid $R$. For any two non-unital algebra homomorphisms $f \colon A \to B$ and $g \colon A \to C$, the composition of the first projection homomorphism $\text{fst} \colon B \times C \to B$ with the product homomorphism $f \times g \colon A \to B \times C$ equals $f$. In other words, the following diagram commutes: $$\begin{array}{ccc} A & \xrightarrow{f \times g} & B \times C \\ & \searrow{f} & \downarrow{\text{fst}} \\ & & B \end{array}$$
NonUnitalAlgHom.snd_prod theorem
(f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).comp (prod f g) = g
Full source 
@[simp]
theorem snd_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).comp (prod f g) = g := by
  rfl
Second projection of product homomorphism equals second factor
Informal description
For any non-unital algebra homomorphisms $f \colon A \to_{NA}[R] B$ and $g \colon A \to_{NA}[R] C$ over a monoid $R$, the composition of the second projection homomorphism $\mathrm{snd}_{R,B,C} \colon B \times C \to_{NA}[R] C$ with the product homomorphism $f \times g \colon A \to_{NA}[R] B \times C$ equals $g$.
NonUnitalAlgHom.prod_fst_snd theorem
: prod (fst R A B) (snd R A B) = 1
Full source 
@[simp]
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
  coe_injective Pi.prod_fst_snd
Product of Projections is Identity Homomorphism in Non-Unital Algebras
Informal description
The product of the first projection homomorphism $\operatorname{fst} \colon A \times B \to A$ and the second projection homomorphism $\operatorname{snd} \colon A \times B \to B$ equals the identity homomorphism on $A \times B$, i.e., $\operatorname{prod}(\operatorname{fst}, \operatorname{snd}) = \operatorname{id}$.
NonUnitalAlgHom.prodEquiv definition
: (A →ₙₐ[R] B) × (A →ₙₐ[R] C) ≃ (A →ₙₐ[R] B × C)
Full source 
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains. -/
@[simps]
def prodEquiv : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)(A →ₙₐ[R] B) × (A →ₙₐ[R] C) ≃ (A →ₙₐ[R] B × C) where
  toFun f := f.1.prod f.2
  invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence between pairs of non-unital algebra homomorphisms and homomorphisms into product algebras
Informal description
The equivalence between pairs of non-unital algebra homomorphisms $(f \colon A \to_{NA}[R] B, g \colon A \to_{NA}[R] C)$ and single non-unital algebra homomorphisms $A \to_{NA}[R] B \times C$. Specifically, the bijection maps a pair $(f, g)$ to the homomorphism $a \mapsto (f(a), g(a))$, and conversely maps a homomorphism $h \colon A \to B \times C$ to the pair $(h \circ \pi_1, h \circ \pi_2)$, where $\pi_1$ and $\pi_2$ are the projection homomorphisms from $B \times C$ to $B$ and $C$ respectively.
NonUnitalAlgHom.inl definition
: A →ₙₐ[R] A × B
Full source 
/-- The left injection into a product is a non-unital algebra homomorphism. -/
def inl : A →ₙₐ[R] A × B :=
  prod 1 0
Left injection non-unital algebra homomorphism
Informal description
The left injection map from a non-unital non-associative semiring $A$ to the product $A \times B$ of two such semirings, which sends each element $x \in A$ to $(x, 0) \in A \times B$, is a non-unital algebra homomorphism. Here, $R$ is a monoid acting distributively on both $A$ and $B$, and the product $A \times B$ is equipped with the component-wise operations.
NonUnitalAlgHom.inr definition
: B →ₙₐ[R] A × B
Full source 
/-- The right injection into a product is a non-unital algebra homomorphism. -/
def inr : B →ₙₐ[R] A × B :=
  prod 0 1
Right injection non-unital algebra homomorphism
Informal description
The right injection map from a non-unital non-associative semiring $B$ to the product $A \times B$ of non-unital non-associative semirings, which sends each element $b \in B$ to $(0, b)$. This map preserves addition, multiplication, and scalar multiplication by elements of the monoid $R$ acting distributively on $A$ and $B$.
NonUnitalAlgHom.coe_inl theorem
: (inl R A B : A → A × B) = fun x => (x, 0)
Full source 
@[simp]
theorem coe_inl : (inl R A B : A → A × B) = fun x => (x, 0) :=
  rfl
Coefficient form of left injection homomorphism: $\text{inl}_R(x) = (x, 0)$
Informal description
The left injection homomorphism $\text{inl}_R : A \to A \times B$ between non-unital non-associative semirings is equal to the function mapping each $x \in A$ to $(x, 0) \in A \times B$.
NonUnitalAlgHom.inl_apply theorem
(x : A) : inl R A B x = (x, 0)
Full source 
theorem inl_apply (x : A) : inl R A B x = (x, 0) :=
  rfl
Left injection homomorphism maps $x$ to $(x, 0)$
Informal description
For any element $x$ in a non-unital non-associative semiring $A$, the left injection homomorphism $\text{inl}_R : A \to A \times B$ maps $x$ to the pair $(x, 0)$ in the product semiring $A \times B$, where $B$ is another non-unital non-associative semiring and $R$ is a monoid acting distributively on both $A$ and $B$.
NonUnitalAlgHom.coe_inr theorem
: (inr R A B : B → A × B) = Prod.mk 0
Full source 
@[simp]
theorem coe_inr : (inr R A B : B → A × B) = Prod.mk 0 :=
  rfl
Right Injection Map in Non-Unital Algebra Homomorphisms is Zero-Pairing
Informal description
The right injection map $\text{inr} \colon B \to A \times B$ from a non-unital non-associative semiring $B$ to the product semiring $A \times B$ is equal to the function that maps each element $x \in B$ to $(0, x) \in A \times B$.
NonUnitalAlgHom.inr_apply theorem
(x : B) : inr R A B x = (0, x)
Full source 
theorem inr_apply (x : B) : inr R A B x = (0, x) :=
  rfl
Right Injection Homomorphism Maps to $(0, x)$ in Product Semiring
Informal description
For any element $x$ in a non-unital non-associative semiring $B$, the right injection non-unital algebra homomorphism $\mathrm{inr}_{R,A,B}$ maps $x$ to the pair $(0, x)$ in the product semiring $A \times B$.
AlgHom.instNonUnitalAlgHomClassOfAlgHomClass instance
[FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B
Full source 
instance (priority := 100) [FunLike F A B] [AlgHomClass F R A B] : NonUnitalAlgHomClass F R A B :=
  { ‹AlgHomClass F R A B› with map_smulₛₗ := map_smul }
Algebra Homomorphisms as Non-Unital Algebra Homomorphisms
Informal description
For any commutative semiring $R$ and semirings $A$, $B$ equipped with $R$-algebra structures, every $R$-algebra homomorphism from $A$ to $B$ is also a non-unital $R$-algebra homomorphism.
AlgHom.toNonUnitalAlgHom definition
(f : A →ₐ[R] B) : A →ₙₐ[R] B
Full source 
/-- A unital morphism of algebras is a `NonUnitalAlgHom`. -/
@[coe]
def toNonUnitalAlgHom (f : A →ₐ[R] B) : A →ₙₐ[R] B :=
  { f with map_smul' := map_smul f }
Conversion from algebra homomorphism to non-unital algebra homomorphism
Informal description
Given an \( R \)-algebra homomorphism \( f \colon A \to_{R} B \), this definition constructs a non-unital algebra homomorphism \( A \to_{R} B \) by preserving the scalar multiplication structure of \( f \).
AlgHom.NonUnitalAlgHom.hasCoe instance
: CoeOut (A →ₐ[R] B) (A →ₙₐ[R] B)
Full source 
instance NonUnitalAlgHom.hasCoe : CoeOut (A →ₐ[R] B) (A →ₙₐ[R] B) :=
  ⟨toNonUnitalAlgHom⟩
Algebra Homomorphism as Non-Unital Algebra Homomorphism
Informal description
Every $R$-algebra homomorphism $f \colon A \to_{R} B$ can be viewed as a non-unital algebra homomorphism $A \to_{R} B$ by preserving the scalar multiplication structure.
AlgHom.toNonUnitalAlgHom_eq_coe theorem
(f : A →ₐ[R] B) : f.toNonUnitalAlgHom = f
Full source 
@[simp]
theorem toNonUnitalAlgHom_eq_coe (f : A →ₐ[R] B) : f.toNonUnitalAlgHom = f :=
  rfl
Equality of Algebra Homomorphism and its Non-Unital Conversion: $f.\text{toNonUnitalAlgHom} = f$
Informal description
For any $R$-algebra homomorphism $f \colon A \to_{R} B$, the non-unital algebra homomorphism obtained by applying the conversion `toNonUnitalAlgHom` to $f$ is equal to $f$ itself.
NonUnitalAlgHom.restrictScalars definition
(f : A →ₙₐ[S] B) : A →ₙₐ[R] B
Full source 
/-- 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`. -/
def restrictScalars (f : A →ₙₐ[S] B) : A →ₙₐ[R] B :=
  { (f : A →ₙ+* B) with
    map_smul' := fun r x ↦ by have := map_smul f (r • 1) x; simpa }
Restriction of scalars for non-unital algebra homomorphisms
Informal description
Given a non-unital algebra homomorphism $f \colon A \to_{S} B$ between non-unital non-associative semirings $A$ and $B$, where $S$ is a monoid acting distributively on $B$, and given another monoid $R$ acting on $S$ via a monoid homomorphism $\varphi \colon R \to S$, the function `restrictScalars` constructs a new non-unital algebra homomorphism $A \to_{R} B$ by restricting the scalar multiplication action from $S$ to $R$. Specifically, for any $r \in R$ and $x \in A$, the scalar multiplication $r \cdot x$ in the restricted homomorphism is defined as $\varphi(r) \cdot x$ in the original homomorphism. This operation preserves the additive and multiplicative structures of the original homomorphism.
NonUnitalAlgHom.restrictScalars_apply theorem
(f : A →ₙₐ[S] B) (x : A) : f.restrictScalars R x = f x
Full source 
@[simp]
lemma restrictScalars_apply (f : A →ₙₐ[S] B) (x : A) : f.restrictScalars R x = f x := rfl
Application of Scalar-Restricted Non-Unital Algebra Homomorphism Equals Original
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{S} B$ and any element $x \in A$, the application of the scalar-restricted homomorphism $f.\text{restrictScalars}\,R$ to $x$ equals the application of $f$ to $x$, i.e., $(f.\text{restrictScalars}\,R)(x) = f(x)$.
NonUnitalAlgHom.coe_restrictScalars theorem
(f : A →ₙₐ[S] B) : (f.restrictScalars R : A →ₙ+* B) = f
Full source 
lemma coe_restrictScalars (f : A →ₙₐ[S] B) : (f.restrictScalars R : A →ₙ+* B) = f := rfl
Coefficient equality for scalar-restricted non-unital algebra homomorphisms
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{S} B$ between non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions by monoids $S$ and $R$ respectively, the underlying non-unital ring homomorphism of the scalar-restricted homomorphism $f.\text{restrictScalars}\, R$ is equal to $f$ itself.
NonUnitalAlgHom.coe_restrictScalars' theorem
(f : A →ₙₐ[S] B) : (f.restrictScalars R : A → B) = f
Full source 
lemma coe_restrictScalars' (f : A →ₙₐ[S] B) : (f.restrictScalars R : A → B) = f := rfl
Underlying Function Equality for Scalar-Restricted Non-Unital Algebra Homomorphism
Informal description
For any non-unital algebra homomorphism $f \colon A \to_{S} B$ between non-unital non-associative semirings $A$ and $B$ with distributive multiplicative actions by monoids $S$ and $R$ respectively, the underlying function of the scalar-restricted homomorphism $f.\text{restrictScalars}\, R$ is equal to $f$ itself. That is, for all $x \in A$, we have $(f.\text{restrictScalars}\, R)(x) = f(x)$.
NonUnitalAlgHom.restrictScalars_injective theorem
: Function.Injective (restrictScalars R : (A →ₙₐ[S] B) → A →ₙₐ[R] B)
Full source 
theorem restrictScalars_injective :
    Function.Injective (restrictScalars R : (A →ₙₐ[S] B) → A →ₙₐ[R] B) :=
  fun _ _ h ↦ ext (congr_fun h :)
Injectivity of Scalar Restriction for Non-Unital Algebra Homomorphisms
Informal description
The restriction of scalars operation on non-unital algebra homomorphisms is injective. That is, for any two homomorphisms $f, g \colon A \to_{S} B$ between non-unital non-associative semirings $A$ and $B$ with a distributive action of monoid $S$, if their scalar-restricted versions $f.\text{restrictScalars}\, R$ and $g.\text{restrictScalars}\, R$ are equal as homomorphisms $A \to_{R} B$, then $f = g$.