Documentation

Mathlib.Algebra.Algebra.NonUnitalHom

Morphisms of non-unital algebras #

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

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 #

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 DistribMulActionHom :
Type (max v w)

A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras.

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

    The proposition that the function preserves multiplication

Instances For

    A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras.

    Equations
    Instances For

      A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras.

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

        A morphism respecting addition, multiplication, and scalar multiplication. When these arise from algebra structures, this is the same as a not-necessarily-unital morphism of algebras.

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

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

            Instances
              @[reducible, inline]

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

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

              Equations
              Instances For
                @[instance 100]
                instance NonUnitalAlgHomClass.toNonUnitalRingHomClass {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} :
                ∀ {x : Monoid R} {x_1 : Monoid S} {φ : outParam (R →* S)} {x_2 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_3 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction S B] [inst_2 : FunLike F A B] [inst : 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_1 : Semiring S} {φ : R →+* S} {x_2 : NonUnitalSemiring A} {x_3 : NonUnitalSemiring B} [inst : Module R A] [inst_1 : Module S B] [inst_2 : FunLike F A B] [inst_3 : NonUnitalAlgSemiHomClass F (↑φ) A B], SemilinearMapClass F φ A B
                Equations
                • =
                @[instance 100]
                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) :

                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' := }
                Instances For
                  Equations
                  • NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHomOfNonUnitalAlgSemiHomClass = { coe := NonUnitalAlgHomClass.toNonUnitalAlgSemiHom }

                  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
                  Instances For
                    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
                    @[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) :
                    AB

                    See Note [custom simps projection]

                    Equations
                    Instances For
                      @[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
                      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] :
                      Equations
                      • NonUnitalAlgHom.instFunLike = { coe := fun (f : A →ₛₙₐ[φ] B) => f.toFun, coe_injective' := }
                      theorem NonUnitalAlgHom.ext_iff {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} {g : A →ₛₙₐ[φ] B} :
                      f = g ∀ (x : A), f x = g x
                      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 : A →ₛₙₐ[φ] B} {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 : A →ₛₙₐ[φ] B} {g : A →ₛₙₐ[φ] B} (h : f = g) (x : A) :
                      f x = g x
                      @[simp]
                      theorem NonUnitalAlgHom.coe_mk {R : Type u} {S : Type u₁} [Monoid R] [Monoid S] {φ : R →* S} {A : Type v} {B : Type w} [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction S B] (f : AB) (h₁ : ∀ (m : R) (x : A), f (m x) = φ m f x) (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) :
                      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
                      @[simp]
                      theorem NonUnitalAlgHom.mk_coe {R : Type u} {S : Type u₁} [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
                      Equations
                      • NonUnitalAlgHom.instCoeOutDistribMulActionHom = { coe := NonUnitalAlgHom.toDistribMulActionHom }
                      Equations
                      • NonUnitalAlgHom.instCoeOutMulHom = { coe := NonUnitalAlgHom.toMulHom }
                      @[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 : A →ₛₙₐ[φ] B} {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 : A →ₛₙₐ[φ] B} {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₄ }
                      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 : A) (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 : A) (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

                      The identity map as a NonUnitalAlgHom.

                      Equations
                      • NonUnitalAlgHom.id R A = { toFun := id, map_smul' := , map_zero' := , map_add' := , map_mul' := }
                      Instances For
                        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] :
                        Equations
                        • NonUnitalAlgHom.instZero = { zero := let __src := 0; { toDistribMulActionHom := __src, map_mul' := } }
                        Equations
                        @[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
                        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 ψ χ] :

                        The composition of morphisms is a morphism.

                        Equations
                        • f.comp g = { toFun := ((↑f).comp g).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
                        Instances For
                          @[simp]
                          theorem NonUnitalAlgHom.coe_comp {R : Type u} {S : Type u₁} {T : Type u_1} [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' := }
                          Instances For
                            @[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 : BA) (k : Function.RightInverse φ' φ) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

                            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' := }
                            Instances For
                              @[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 : BA) (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.

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

                              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' := }
                              Instances For
                                @[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

                                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' := }
                                Instances For
                                  @[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
                                  @[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

                                  The prod of two morphisms is a morphism.

                                  Equations
                                  • f.prod g = { toFun := Pi.prod f g, map_smul' := , map_zero' := , map_add' := , map_mul' := }
                                  Instances For
                                    theorem NonUnitalAlgHom.coe_prod {R : Type u} [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.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

                                    Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

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

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

                                      Equations
                                      Instances For

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

                                        Equations
                                        Instances For
                                          @[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)

                                          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] :
                                          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 unital morphism of algebras is a NonUnitalAlgHom.

                                          Equations
                                          • f = { toFun := (↑f.toRingHom).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
                                          Instances For
                                            instance AlgHom.NonUnitalAlgHom.hasCoe {R : Type u_2} [CommSemiring R] {A : Type u_3} {B : Type u_4} [Semiring A] [Semiring B] [Algebra R A] [Algebra 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) :
                                            @[simp]
                                            theorem AlgHom.coe_to_nonUnitalAlgHom {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 = f

                                            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
                                            Instances For