feat(algebra/hom/non_unital_alg): introduce notation for non-unital a…

…lgebra homomorphisms (#13470)

This introduces the notation `A →ₙₐ[R] B` for `non_unital_alg_hom R A B` to mirror that of `non_unital_ring_hom R S` as `R →ₙ+* S` from #13430. Here, the `ₙ` stands for "non-unital".

src/algebra/algebra/unitization.lean

@@ -467,7 +467,7 @@ section coe
 realized as a non-unital algebra homomorphism. -/
 @[simps]
 def coe_non_unital_alg_hom (R A : Type*) [comm_semiring R] [non_unital_semiring A] [module R A] :
-  non_unital_alg_hom R A (unitization R A) :=
+  A →ₙₐ[R] unitization R A :=
 { to_fun := coe,
   map_smul' := coe_smul R,
   map_zero' := coe_zero R,
@@ -505,7 +505,7 @@ alg_hom_ext (non_unital_alg_hom.congr_fun h) (by simp [alg_hom.commutes])
 /-- Non-unital algebra homomorphisms from `A` into a unital `R`-algebra `C` lift uniquely to
 `unitization R A →ₐ[R] C`. This is the universal property of the unitization. -/
 @[simps apply_apply]
-def lift : non_unital_alg_hom R A C ≃ (unitization R A →ₐ[R] C) :=
+def lift : (A →ₙₐ[R] C) ≃ (unitization R A →ₐ[R] C) :=
 { to_fun := λ φ,
   { to_fun := λ x, algebra_map R C x.fst + φ x.snd,
     map_one' := by simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero],

src/algebra/free_non_unital_non_assoc_algebra.lean

@@ -58,29 +58,29 @@ variables [module R A] [is_scalar_tower R A A] [smul_comm_class R A A]
 /-- The functor `X ↦ free_non_unital_non_assoc_algebra R X` from the category of types to the
 category of non-unital, non-associative algebras over `R` is adjoint to the forgetful functor in the
 other direction. -/
-def lift : (X → A) ≃ non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A :=
+def lift : (X → A) ≃ (free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :=
 free_magma.lift.trans (monoid_algebra.lift_magma R)
 
-@[simp] lemma lift_symm_apply (F : non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A) :
+@[simp] lemma lift_symm_apply (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
   (lift R).symm F = F ∘ (of R) :=
 rfl
 
 @[simp] lemma of_comp_lift (f : X → A) : (lift R f) ∘ (of R) = f :=
 (lift R).left_inv f
 
 @[simp] lemma lift_unique
-  (f : X → A) (F : non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A) :
+  (f : X → A) (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
   F ∘ (of R) = f ↔ F = lift R f :=
 (lift R).symm_apply_eq
 
 @[simp] lemma lift_of_apply (f : X → A) (x) : lift R f (of R x) = f x :=
 congr_fun (of_comp_lift _ f) x
 
-@[simp] lemma lift_comp_of (F : non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A) :
+@[simp] lemma lift_comp_of (F : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A) :
   lift R (F ∘ (of R)) = F :=
 (lift R).apply_symm_apply F
 
-@[ext] lemma hom_ext {F₁ F₂ : non_unital_alg_hom R (free_non_unital_non_assoc_algebra R X) A}
+@[ext] lemma hom_ext {F₁ F₂ : free_non_unital_non_assoc_algebra R X →ₙₐ[R] A}
   (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ :=
 (lift R).symm.injective $ funext h
 

src/algebra/hom/non_unital_alg.lean

@@ -54,6 +54,9 @@ structure non_unital_alg_hom [monoid R]
   [non_unital_non_assoc_semiring B] [distrib_mul_action R B]
   extends A →+[R] B, A →ₙ* B
 
+infixr ` →ₙₐ `:25 := non_unital_alg_hom _
+notation A ` →ₙₐ[`:25 R `] ` B := non_unital_alg_hom R A B
+
 attribute [nolint doc_blame] non_unital_alg_hom.to_distrib_mul_action_hom
 attribute [nolint doc_blame] non_unital_alg_hom.to_mul_hom
 
@@ -65,123 +68,123 @@ variables [non_unital_non_assoc_semiring B] [distrib_mul_action R B]
 variables [non_unital_non_assoc_semiring C] [distrib_mul_action R C]
 
 /-- see Note [function coercion] -/
-instance : has_coe_to_fun (non_unital_alg_hom R A B) (λ _, A → B) := ⟨to_fun⟩
+instance : has_coe_to_fun (A →ₙₐ[R] B) (λ _, A → B) := ⟨to_fun⟩
 
-@[simp] lemma to_fun_eq_coe (f : non_unital_alg_hom R A B) : f.to_fun = ⇑f := rfl
+@[simp] lemma to_fun_eq_coe (f : A →ₙₐ[R] B) : f.to_fun = ⇑f := rfl
 
 initialize_simps_projections non_unital_alg_hom (to_fun → apply)
 
 lemma coe_injective :
-  @function.injective (non_unital_alg_hom R A B) (A → B) coe_fn :=
+  @function.injective (A →ₙₐ[R] B) (A → B) coe_fn :=
 by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr
 
-@[ext] lemma ext {f g : non_unital_alg_hom R A B} (h : ∀ x, f x = g x) : f = g :=
+@[ext] lemma ext {f g : A →ₙₐ[R] B} (h : ∀ x, f x = g x) : f = g :=
 coe_injective $ funext h
 
-lemma ext_iff {f g : non_unital_alg_hom R A B} : f = g ↔ ∀ x, f x = g x :=
+lemma ext_iff {f g : A →ₙₐ[R] B} : f = g ↔ ∀ x, f x = g x :=
 ⟨by { rintro rfl x, refl }, ext⟩
 
-lemma congr_fun {f g : non_unital_alg_hom R A B} (h : f = g) (x : A) : f x = g x := h ▸ rfl
+lemma congr_fun {f g : A →ₙₐ[R] B} (h : f = g) (x : A) : f x = g x := h ▸ rfl
 
 @[simp] lemma coe_mk (f : A → B) (h₁ h₂ h₃ h₄) :
-  ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A → B) = f :=
+  ((⟨f, h₁, h₂, h₃, h₄⟩ : A →ₙₐ[R] B) : A → B) = f :=
 rfl
 
-@[simp] lemma mk_coe (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) :
-  (⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) = f :=
+@[simp] lemma mk_coe (f : A →ₙₐ[R] B) (h₁ h₂ h₃ h₄) :
+  (⟨f, h₁, h₂, h₃, h₄⟩ : A →ₙₐ[R] B) = f :=
 by { ext, refl, }
 
-instance : has_coe (non_unital_alg_hom R A B) (A →+[R] B) :=
+instance : has_coe (A →ₙₐ[R] B) (A →+[R] B) :=
 ⟨to_distrib_mul_action_hom⟩
 
-instance : has_coe (non_unital_alg_hom R A B) (A →ₙ* B) := ⟨to_mul_hom⟩
+instance : has_coe (A →ₙₐ[R] B) (A →ₙ* B) := ⟨to_mul_hom⟩
 
-@[simp] lemma to_distrib_mul_action_hom_eq_coe (f : non_unital_alg_hom R A B) :
+@[simp] lemma to_distrib_mul_action_hom_eq_coe (f : A →ₙₐ[R] B) :
   f.to_distrib_mul_action_hom = ↑f :=
 rfl
 
-@[simp] lemma to_mul_hom_eq_coe (f : non_unital_alg_hom R A B) : f.to_mul_hom = ↑f :=
+@[simp] lemma to_mul_hom_eq_coe (f : A →ₙₐ[R] B) : f.to_mul_hom = ↑f :=
 rfl
 
-@[simp, norm_cast] lemma coe_to_distrib_mul_action_hom (f : non_unital_alg_hom R A B) :
+@[simp, norm_cast] lemma coe_to_distrib_mul_action_hom (f : A →ₙₐ[R] B) :
   ((f : A →+[R] B) : A → B) = f :=
 rfl
 
-@[simp, norm_cast] lemma coe_to_mul_hom (f : non_unital_alg_hom R A B) :
+@[simp, norm_cast] lemma coe_to_mul_hom (f : A →ₙₐ[R] B) :
   ((f : A →ₙ* B) : A → B) = f :=
 rfl
 
-lemma to_distrib_mul_action_hom_injective {f g : non_unital_alg_hom R A B}
+lemma to_distrib_mul_action_hom_injective {f g : A →ₙₐ[R] B}
   (h : (f : A →+[R] B) = (g : A →+[R] B)) : f = g :=
 by { ext a, exact distrib_mul_action_hom.congr_fun h a, }
 
-lemma to_mul_hom_injective {f g : non_unital_alg_hom R A B}
+lemma to_mul_hom_injective {f g : A →ₙₐ[R] B}
   (h : (f : A →ₙ* B) = (g : A →ₙ* B)) : f = g :=
 by { ext a, exact mul_hom.congr_fun h a, }
 
-@[norm_cast] lemma coe_distrib_mul_action_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) :
-  ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A →+[R] B) =
+@[norm_cast] lemma coe_distrib_mul_action_hom_mk (f : A →ₙₐ[R] B) (h₁ h₂ h₃ h₄) :
+  ((⟨f, h₁, h₂, h₃, h₄⟩ : A →ₙₐ[R] B) : A →+[R] B) =
   ⟨f, h₁, h₂, h₃⟩ :=
 by { ext, refl, }
 
-@[norm_cast] lemma coe_mul_hom_mk (f : non_unital_alg_hom R A B) (h₁ h₂ h₃ h₄) :
-  ((⟨f, h₁, h₂, h₃, h₄⟩ : non_unital_alg_hom R A B) : A →ₙ* B) = ⟨f, h₄⟩ :=
+@[norm_cast] lemma coe_mul_hom_mk (f : A →ₙₐ[R] B) (h₁ h₂ h₃ h₄) :
+  ((⟨f, h₁, h₂, h₃, h₄⟩ : A →ₙₐ[R] B) : A →ₙ* B) = ⟨f, h₄⟩ :=
 by { ext, refl, }
 
-@[simp] lemma map_smul (f : non_unital_alg_hom R A B) (c : R) (x : A) :
+@[simp] lemma map_smul (f : A →ₙₐ[R] B) (c : R) (x : A) :
   f (c • x) = c • f x :=
 f.to_distrib_mul_action_hom.map_smul c x
 
-@[simp] lemma map_add (f : non_unital_alg_hom R A B) (x y : A) :
+@[simp] lemma map_add (f : A →ₙₐ[R] B) (x y : A) :
   f (x + y) = (f x) + (f y) :=
 f.to_distrib_mul_action_hom.map_add x y
 
-@[simp] lemma map_mul (f : non_unital_alg_hom R A B) (x y : A) :
+@[simp] lemma map_mul (f : A →ₙₐ[R] B) (x y : A) :
   f (x * y) = (f x) * (f y) :=
 f.to_mul_hom.map_mul x y
 
-@[simp] lemma map_zero (f : non_unital_alg_hom R A B) : f 0 = 0 :=
+@[simp] lemma map_zero (f : A →ₙₐ[R] B) : f 0 = 0 :=
 f.to_distrib_mul_action_hom.map_zero
 
-instance : has_zero (non_unital_alg_hom R A B) :=
+instance : has_zero (A →ₙₐ[R] B) :=
 ⟨{ map_mul' := by simp,
    .. (0 : A →+[R] B) }⟩
 
-instance : has_one (non_unital_alg_hom R A A) :=
+instance : has_one (A →ₙₐ[R] A) :=
 ⟨{ map_mul' := by simp,
    .. (1 : A →+[R] A) }⟩
 
-@[simp] lemma coe_zero : ((0 : non_unital_alg_hom R A B) : A → B) = 0 := rfl
+@[simp] lemma coe_zero : ((0 : A →ₙₐ[R] B) : A → B) = 0 := rfl
 
-@[simp] lemma coe_one : ((1 : non_unital_alg_hom R A A) : A → A) = id := rfl
+@[simp] lemma coe_one : ((1 : A →ₙₐ[R] A) : A → A) = id := rfl
 
-lemma zero_apply (a : A) : (0 : non_unital_alg_hom R A B) a = 0 := rfl
+lemma zero_apply (a : A) : (0 : A →ₙₐ[R] B) a = 0 := rfl
 
-lemma one_apply (a : A) : (1 : non_unital_alg_hom R A A) a = a := rfl
+lemma one_apply (a : A) : (1 : A →ₙₐ[R] A) a = a := rfl
 
-instance : inhabited (non_unital_alg_hom R A B) := ⟨0⟩
+instance : inhabited (A →ₙₐ[R] B) := ⟨0⟩
 
 /-- The composition of morphisms is a morphism. -/
-def comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) : non_unital_alg_hom R A C :=
+def comp (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) : A →ₙₐ[R] C :=
 { .. (f : B →ₙ* C).comp (g : A →ₙ* B),
   .. (f : B →+[R] C).comp (g : A →+[R] B) }
 
-@[simp, norm_cast] lemma coe_comp (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) :
+@[simp, norm_cast] lemma coe_comp (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) :
   (f.comp g : A → C) = (f : B → C) ∘ (g : A → B) :=
 rfl
 
-lemma comp_apply (f : non_unital_alg_hom R B C) (g : non_unital_alg_hom R A B) (x : A) :
+lemma comp_apply (f : B →ₙₐ[R] C) (g : A →ₙₐ[R] B) (x : A) :
   f.comp g x = f (g x) :=
 rfl
 
 /-- The inverse of a bijective morphism is a morphism. -/
-def inverse (f : non_unital_alg_hom R A B) (g : B → A)
+def inverse (f : A →ₙₐ[R] B) (g : B → A)
   (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
-  non_unital_alg_hom R B A :=
+  B →ₙₐ[R] A :=
 { .. (f : A →ₙ* B).inverse g h₁ h₂,
   .. (f : A →+[R] B).inverse g h₁ h₂ }
 
-@[simp] lemma coe_inverse (f : non_unital_alg_hom R A B) (g : B → A)
+@[simp] lemma coe_inverse (f : A →ₙₐ[R] B) (g : B → A)
   (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) :
   (inverse f g h₁ h₂ : B → A) = g :=
 rfl
@@ -193,17 +196,17 @@ namespace alg_hom
 variables {R A B} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
 
 /-- A unital morphism of algebras is a `non_unital_alg_hom`. -/
-def to_non_unital_alg_hom (f : A →ₐ[R] B) : non_unital_alg_hom R A B :=
+def to_non_unital_alg_hom (f : A →ₐ[R] B) : A →ₙₐ[R] B :=
 { map_smul' := f.map_smul, .. f, }
 
-instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (non_unital_alg_hom R A B) :=
+instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (A →ₙₐ[R] B) :=
 ⟨to_non_unital_alg_hom⟩
 
 @[simp] lemma to_non_unital_alg_hom_eq_coe (f : A →ₐ[R] B) : f.to_non_unital_alg_hom = f :=
 rfl
 
 @[simp, norm_cast] lemma coe_to_non_unital_alg_hom (f : A →ₐ[R] B) :
-  ((f : non_unital_alg_hom R A B) : A → B) = f :=
+  ((f : A →ₙₐ[R] B) : A → B) = f :=
 rfl
 
 end alg_hom

src/algebra/lie/free.lean

@@ -201,7 +201,7 @@ begin
 end
 
 /-- The quotient map as a `non_unital_alg_hom`. -/
-def mk : non_unital_alg_hom R (lib R X) (free_lie_algebra R X) :=
+def mk : lib R X →ₙₐ[R] free_lie_algebra R X :=
 { to_fun    := quot.mk (rel R X),
   map_smul' := λ t a, rfl,
   map_zero' := rfl,

src/algebra/lie/non_unital_non_assoc_algebra.lean

@@ -66,14 +66,14 @@ variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂]
 /-- Regarding the `lie_ring` of a `lie_algebra` as a `non_unital_non_assoc_semiring`, we can
 regard a `lie_hom` as a `non_unital_alg_hom`. -/
 @[simps]
-def to_non_unital_alg_hom (f : L →ₗ⁅R⁆ L₂) : non_unital_alg_hom R L L₂ :=
+def to_non_unital_alg_hom (f : L →ₗ⁅R⁆ L₂) : L →ₙₐ[R] L₂ :=
 { to_fun := f,
   map_zero' := f.map_zero,
   map_mul'  := f.map_lie,
   ..f }
 
 lemma to_non_unital_alg_hom_injective :
-  function.injective (to_non_unital_alg_hom : _ → non_unital_alg_hom R L L₂) :=
+  function.injective (to_non_unital_alg_hom : _ → (L →ₙₐ[R] L₂)) :=
 λ f g h, ext $ non_unital_alg_hom.congr_fun h
 
 end lie_hom

src/algebra/monoid_algebra/basic.lean

@@ -495,22 +495,22 @@ variables {A : Type u₃} [non_unital_non_assoc_semiring A]
 /-- A non_unital `k`-algebra homomorphism from `monoid_algebra k G` is uniquely defined by its
 values on the functions `single a 1`. -/
 lemma non_unital_alg_hom_ext [distrib_mul_action k A]
-  {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A}
+  {φ₁ φ₂ : monoid_algebra k G →ₙₐ[k] A}
   (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
 non_unital_alg_hom.to_distrib_mul_action_hom_injective $
   finsupp.distrib_mul_action_hom_ext' $
   λ a, distrib_mul_action_hom.ext_ring (h a)
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext] lemma non_unital_alg_hom_ext' [distrib_mul_action k A]
-  {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A}
+  {φ₁ φ₂ : monoid_algebra k G →ₙₐ[k] A}
   (h : φ₁.to_mul_hom.comp (of_magma k G) = φ₂.to_mul_hom.comp (of_magma k G)) : φ₁ = φ₂ :=
 non_unital_alg_hom_ext k $ mul_hom.congr_fun h
 
 /-- The functor `G ↦ monoid_algebra k G`, from the category of magmas to the category of non-unital,
 non-associative algebras over `k` is adjoint to the forgetful functor in the other direction. -/
 @[simps] def lift_magma [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :
-  (G →ₙ* A) ≃ non_unital_alg_hom k (monoid_algebra k G) A :=
+  (G →ₙ* A) ≃ (monoid_algebra k G →ₙₐ[k] A) :=
 { to_fun    := λ f,
     { to_fun    := λ a, a.sum (λ m t, t • f m),
       map_smul' :=  λ t' a,
@@ -1307,25 +1307,25 @@ variables {A : Type u₃} [non_unital_non_assoc_semiring A]
 /-- A non_unital `k`-algebra homomorphism from `add_monoid_algebra k G` is uniquely defined by its
 values on the functions `single a 1`. -/
 lemma non_unital_alg_hom_ext [distrib_mul_action k A]
-  {φ₁ φ₂ : non_unital_alg_hom k (add_monoid_algebra k G) A}
+  {φ₁ φ₂ : add_monoid_algebra k G →ₙₐ[k] A}
   (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
 @monoid_algebra.non_unital_alg_hom_ext k (multiplicative G) _ _ _ _ _ φ₁ φ₂ h
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext] lemma non_unital_alg_hom_ext' [distrib_mul_action k A]
-  {φ₁ φ₂ : non_unital_alg_hom k (add_monoid_algebra k G) A}
+  {φ₁ φ₂ : add_monoid_algebra k G →ₙₐ[k] A}
   (h : φ₁.to_mul_hom.comp (of_magma k G) = φ₂.to_mul_hom.comp (of_magma k G)) : φ₁ = φ₂ :=
 @monoid_algebra.non_unital_alg_hom_ext' k (multiplicative G) _ _ _ _ _ φ₁ φ₂ h
 
 /-- The functor `G ↦ add_monoid_algebra k G`, from the category of magmas to the category of
 non-unital, non-associative algebras over `k` is adjoint to the forgetful functor in the other
 direction. -/
 @[simps] def lift_magma [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :
-  (multiplicative G →ₙ* A) ≃ non_unital_alg_hom k (add_monoid_algebra k G) A :=
+  (multiplicative G →ₙ* A) ≃ (add_monoid_algebra k G →ₙₐ[k] A) :=
 { to_fun := λ f, { to_fun := λ a, sum a (λ m t, t • f (multiplicative.of_add m)),
                    .. (monoid_algebra.lift_magma k f : _)},
   inv_fun := λ F, F.to_mul_hom.comp (of_magma k G),
-  .. (monoid_algebra.lift_magma k : (multiplicative G →ₙ* A) ≃ non_unital_alg_hom k _ A) }
+  .. (monoid_algebra.lift_magma k : (multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)) }
 
 end non_unital_non_assoc_algebra
 

src/topology/algebra/module/character_space.lean

@@ -63,7 +63,7 @@ def to_clm (φ : character_space 𝕜 A) : A →L[𝕜] 𝕜 := (φ : weak_dual
 lemma to_clm_apply (φ : character_space 𝕜 A) (x : A) : φ x = to_clm φ x := rfl
 
 /-- An element of the character space, as an non-unital algebra homomorphism. -/
-@[simps] def to_non_unital_alg_hom (φ : character_space 𝕜 A) : non_unital_alg_hom 𝕜 A 𝕜 :=
+@[simps] def to_non_unital_alg_hom (φ : character_space 𝕜 A) : A →ₙₐ[𝕜] 𝕜 :=
 { to_fun := (φ : A → 𝕜),
   map_mul' := φ.prop.2,
   map_smul' := (to_clm φ).map_smul,

src/topology/continuous_function/zero_at_infty.lean

@@ -521,7 +521,7 @@ def comp_linear_map [add_comm_monoid δ] [has_continuous_add δ] {R : Type*}
 /-- Composition as a non-unital algebra homomorphism. -/
 def comp_non_unital_alg_hom {R : Type*} [semiring R] [non_unital_non_assoc_semiring δ]
   [topological_semiring δ] [module R δ] [has_continuous_const_smul R δ] (g : β →co γ) :
-  non_unital_alg_hom R C₀(γ, δ) C₀(β, δ) :=
+  C₀(γ, δ) →ₙₐ[R] C₀(β, δ) :=
 { to_fun := λ f, f.comp g,
   map_smul' := λ r f, rfl,
   map_zero' := rfl,