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

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.

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
        class NonUnitalAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] extends DistribMulActionHomClass :
        Type (max (max u_1 u_3) u_4)

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

        • coe : FAB
        • coe_injective' : Function.Injective FunLike.coe
        • map_smul : ∀ (f : F) (c : R) (x : A), f (c x) = c f x
        • map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
        • map_zero : ∀ (f : F), f 0 = 0
        • map_mul : ∀ (f : F) (x y : A), f (x * y) = f x * f y

          The proposition that the function preserves multiplication

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

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • NonUnitalAlgHomClass.instCoeTCNonUnitalAlgHom = { coe := NonUnitalAlgHomClass.toNonUnitalAlgHom }
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]

            See Note [custom simps projection]

            Equations
            Instances For
              @[simp]
              theorem NonUnitalAlgHom.coe_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {F : Type u_1} [NonUnitalAlgHomClass F R A B] (f : F) :
              f = f
              Equations
              • One or more equations did not get rendered due to their size.
              theorem NonUnitalAlgHom.ext {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : ∀ (x : A), f x = g x) :
              f = g
              theorem NonUnitalAlgHom.ext_iff {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} :
              f = g ∀ (x : A), f x = g x
              theorem NonUnitalAlgHom.congr_fun {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : f = g) (x : A) :
              f x = g x
              @[simp]
              theorem NonUnitalAlgHom.coe_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : AB) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) :
              { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = f
              @[simp]
              theorem NonUnitalAlgHom.mk_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) :
              { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = f
              Equations
              • NonUnitalAlgHom.instCoeOutNonUnitalAlgHomDistribMulActionHomToAddMonoidToAddCommMonoidToAddMonoidToAddCommMonoid = { coe := NonUnitalAlgHom.toDistribMulActionHom }
              Equations
              • NonUnitalAlgHom.instCoeOutNonUnitalAlgHomMulHomToMulToMul = { coe := NonUnitalAlgHom.toMulHom }
              @[simp]
              theorem NonUnitalAlgHom.toDistribMulActionHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) :
              f.toDistribMulActionHom = f
              @[simp]
              theorem NonUnitalAlgHom.to_mulHom_injective {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] {f : A →ₙₐ[R] B} {g : A →ₙₐ[R] B} (h : f = g) :
              f = g
              theorem NonUnitalAlgHom.coe_distribMulActionHom_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) :
              { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }
              theorem NonUnitalAlgHom.coe_mulHom_mk {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) :
              { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ } = { toFun := f, map_mul' := h₄ }
              theorem NonUnitalAlgHom.map_smul {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (c : R) (x : A) :
              f (c x) = c f x
              theorem NonUnitalAlgHom.map_add {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (x : A) (y : A) :
              f (x + y) = f x + f y
              theorem NonUnitalAlgHom.map_mul {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (x : A) (y : A) :
              f (x * y) = f x * f y

              The identity map as a NonUnitalAlgHom.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Equations
                @[simp]
                theorem NonUnitalAlgHom.coe_one {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] :
                1 = id
                theorem NonUnitalAlgHom.one_apply {R : Type u} {A : Type v} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (a : A) :
                1 a = a
                Equations
                • NonUnitalAlgHom.instInhabitedNonUnitalAlgHom = { default := 0 }

                The composition of morphisms is a morphism.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def NonUnitalAlgHom.inverse {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

                  The inverse of a bijective morphism is a morphism.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem NonUnitalAlgHom.coe_inverse {R : Type u} {A : Type v} {B : Type w} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (f : A →ₙₐ[R] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                    (NonUnitalAlgHom.inverse f g h₁ h₂) = g

                    Operations on the product type #

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

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

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem NonUnitalAlgHom.snd_apply (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) :
                      (NonUnitalAlgHom.snd R A B) self = self.2
                      @[simp]
                      theorem NonUnitalAlgHom.snd_toFun (R : Type u) (A : Type v) (B : Type w) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] (self : A × B) :
                      (NonUnitalAlgHom.snd R A B) self = self.2

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem NonUnitalAlgHom.prod_toFun {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) :
                        (NonUnitalAlgHom.prod f g) i = Pi.prod (f) (g) i
                        @[simp]
                        theorem NonUnitalAlgHom.prod_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A) :
                        (NonUnitalAlgHom.prod f g) i = Pi.prod (f) (g) i

                        The prod of two morphisms is a morphism.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem NonUnitalAlgHom.prodEquiv_apply {R : Type u} {A : Type v} {B : Type w} {C : Type w₁} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] (f : (A →ₙₐ[R] B) × (A →ₙₐ[R] C)) :
                          NonUnitalAlgHom.prodEquiv f = NonUnitalAlgHom.prod f.1 f.2

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

                                Interaction with AlgHom #

                                def AlgHom.toNonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

                                A unital morphism of algebras is a NonUnitalAlgHom.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  instance AlgHom.NonUnitalAlgHom.hasCoe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                                  Equations
                                  • AlgHom.NonUnitalAlgHom.hasCoe = { coe := AlgHom.toNonUnitalAlgHom }
                                  @[simp]
                                  theorem AlgHom.toNonUnitalAlgHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                                  f = f
                                  @[simp]
                                  theorem AlgHom.coe_to_nonUnitalAlgHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                                  f = f