feat(algebra/algebra/basic): define alg_hom_class and `non_unital_a…

…lg_hom_class` (#14679)

This PR defines `alg_hom_class` and `non_unital_alg_hom_class` as part of the morphism refactor.

src/algebra/algebra/basic.lean

@@ -484,6 +484,30 @@ run_cmd tactic.add_doc_string `alg_hom.to_ring_hom "Reinterpret an `alg_hom` as
 infixr ` →ₐ `:25 := alg_hom _
 notation A ` →ₐ[`:25 R `] ` B := alg_hom R A B
 
+/-- `alg_hom_class F R A B` asserts `F` is a type of bundled algebra homomorphisms
+from `A` to `B`.  -/
+class alg_hom_class (F : Type*) (R : out_param Type*) (A : out_param Type*) (B : out_param Type*)
+  [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
+  extends ring_hom_class F A B :=
+(commutes : ∀ (f : F) (r : R), f (algebra_map R A r) = algebra_map R B r)
+
+-- `R` becomes a metavariable but that's fine because it's an `out_param`
+attribute [nolint dangerous_instance] alg_hom_class.to_ring_hom_class
+
+attribute [simp] alg_hom_class.commutes
+
+namespace alg_hom_class
+
+variables {R : Type*} {A : Type*} {B : Type*} [comm_semiring R] [semiring A] [semiring B]
+  [algebra R A] [algebra R B]
+
+@[priority 100] -- see Note [lower instance priority]
+instance {F : Type*} [alg_hom_class F R A B] : linear_map_class F R A B :=
+{ map_smulₛₗ := λ f r x, by simp only [algebra.smul_def, map_mul, commutes, ring_hom.id_apply],
+  ..‹alg_hom_class F R A B› }
+
+end alg_hom_class
+
 namespace alg_hom
 
 variables {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁}
@@ -499,13 +523,14 @@ initialize_simps_projections alg_hom (to_fun → apply)
 
 @[simp] lemma to_fun_eq_coe (f : A →ₐ[R] B) : f.to_fun = f := rfl
 
-instance : ring_hom_class (A →ₐ[R] B) A B :=
+instance : alg_hom_class (A →ₐ[R] B) R A B :=
 { coe := to_fun,
   coe_injective' := λ f g h, by { cases f, cases g, congr' },
   map_add := map_add',
   map_zero := map_zero',
   map_mul := map_mul',
-  map_one := map_one' }
+  map_one := map_one',
+  commutes := λ f, f.commutes' }
 
 instance coe_ring_hom : has_coe (A →ₐ[R] B) (A →+* B) := ⟨alg_hom.to_ring_hom⟩
 
@@ -560,26 +585,22 @@ theorem commutes (r : R) : φ (algebra_map R A r) = algebra_map R B r := φ.comm
 theorem comp_algebra_map : (φ : A →+* B).comp (algebra_map R A) = algebra_map R B :=
 ring_hom.ext $ φ.commutes
 
-lemma map_add (r s : A) : φ (r + s) = φ r + φ s := map_add _ _ _
-lemma map_zero : φ 0 = 0 := map_zero _
-lemma map_mul (x y) : φ (x * y) = φ x * φ y := map_mul _ _ _
-lemma map_one : φ 1 = 1 := map_one _
-lemma map_pow (x : A) (n : ℕ) : φ (x ^ n) = (φ x) ^ n :=
-map_pow _ _ _
+protected lemma map_add (r s : A) : φ (r + s) = φ r + φ s := map_add _ _ _
+protected lemma map_zero : φ 0 = 0 := map_zero _
+protected lemma map_mul (x y) : φ (x * y) = φ x * φ y := map_mul _ _ _
+protected lemma map_one : φ 1 = 1 := map_one _
+protected lemma map_pow (x : A) (n : ℕ) : φ (x ^ n) = (φ x) ^ n := map_pow _ _ _
 
-@[simp] lemma map_smul (r : R) (x : A) : φ (r • x) = r • φ x :=
-by simp only [algebra.smul_def, map_mul, commutes]
+@[simp] protected lemma map_smul (r : R) (x : A) : φ (r • x) = r • φ x := map_smul _ _ _
 
-lemma map_sum {ι : Type*} (f : ι → A) (s : finset ι) :
-  φ (∑ x in s, f x) = ∑ x in s, φ (f x) :=
-φ.to_ring_hom.map_sum f s
+protected lemma map_sum {ι : Type*} (f : ι → A) (s : finset ι) :
+  φ (∑ x in s, f x) = ∑ x in s, φ (f x) := map_sum _ _ _
 
-lemma map_finsupp_sum {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A) :
-  φ (f.sum g) = f.sum (λ i a, φ (g i a)) :=
-φ.map_sum _ _
+protected lemma map_finsupp_sum {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A) :
+  φ (f.sum g) = f.sum (λ i a, φ (g i a)) := map_finsupp_sum _ _ _
 
-lemma map_bit0 (x) : φ (bit0 x) = bit0 (φ x) := map_bit0 _ _
-lemma map_bit1 (x) : φ (bit1 x) = bit1 (φ x) := map_bit1 _ _
+protected lemma map_bit0 (x) : φ (bit0 x) = bit0 (φ x) := map_bit0 _ _
+protected lemma map_bit1 (x) : φ (bit1 x) = bit1 (φ x) := map_bit1 _ _
 
 /-- If a `ring_hom` is `R`-linear, then it is an `alg_hom`. -/
 def mk' (f : A →+* B) (h : ∀ (c : R) x, f (c • x) = c • f x) : A →ₐ[R] B :=
@@ -630,8 +651,8 @@ ext $ λ x, rfl
 /-- R-Alg ⥤ R-Mod -/
 def to_linear_map : A →ₗ[R] B :=
 { to_fun := φ,
-  map_add' := φ.map_add,
-  map_smul' := φ.map_smul }
+  map_add' := map_add _,
+  map_smul' := map_smul _ }
 
 @[simp] lemma to_linear_map_apply (p : A) : φ.to_linear_map p = φ p := rfl
 
@@ -697,17 +718,14 @@ section comm_semiring
 variables [comm_semiring R] [comm_semiring A] [comm_semiring B]
 variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 
-lemma map_multiset_prod (s : multiset A) :
-  φ s.prod = (s.map φ).prod :=
-φ.to_ring_hom.map_multiset_prod s
+protected lemma map_multiset_prod (s : multiset A) :
+  φ s.prod = (s.map φ).prod := map_multiset_prod _ _
 
-lemma map_prod {ι : Type*} (f : ι → A) (s : finset ι) :
-  φ (∏ x in s, f x) = ∏ x in s, φ (f x) :=
-φ.to_ring_hom.map_prod f s
+protected lemma map_prod {ι : Type*} (f : ι → A) (s : finset ι) :
+  φ (∏ x in s, f x) = ∏ x in s, φ (f x) := map_prod _ _ _
 
-lemma map_finsupp_prod {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A) :
-  φ (f.prod g) = f.prod (λ i a, φ (g i a)) :=
-φ.map_prod _ _
+protected lemma map_finsupp_prod {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A) :
+  φ (f.prod g) = f.prod (λ i a, φ (g i a)) := map_finsupp_prod _ _ _
 
 end comm_semiring
 
@@ -716,8 +734,8 @@ section ring
 variables [comm_semiring R] [ring A] [ring B]
 variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 
-lemma map_neg (x) : φ (-x) = -φ x := map_neg _ _
-lemma map_sub (x y) : φ (x - y) = φ x - φ y := map_sub _ _ _
+protected lemma map_neg (x) : φ (-x) = -φ x := map_neg _ _
+protected lemma map_sub (x y) : φ (x - y) = φ x - φ y := map_sub _ _ _
 
 @[simp] lemma map_int_cast (n : ℤ) : φ n = n :=
 φ.to_ring_hom.map_int_cast n
@@ -757,6 +775,30 @@ attribute [nolint doc_blame] alg_equiv.to_mul_equiv
 
 notation A ` ≃ₐ[`:50 R `] ` A' := alg_equiv R A A'
 
+/-- `alg_equiv_class F R A B` states that `F` is a type of algebra structure preserving
+  equivalences. You should extend this class when you extend `alg_equiv`. -/
+class alg_equiv_class (F : Type*) (R A B : out_param Type*)
+  [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
+  extends ring_equiv_class F A B :=
+(commutes : ∀ (f : F) (r : R), f (algebra_map R A r) = algebra_map R B r)
+
+-- `R` becomes a metavariable but that's fine because it's an `out_param`
+attribute [nolint dangerous_instance] alg_equiv_class.to_ring_equiv_class
+
+namespace alg_equiv_class
+
+@[priority 100] -- See note [lower instance priority]
+instance to_alg_hom_class (F R A B : Type*)
+  [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
+  [h : alg_equiv_class F R A B] : alg_hom_class F R A B :=
+{ coe := coe_fn,
+  coe_injective' := fun_like.coe_injective,
+  map_zero := map_zero,
+  map_one := map_one,
+  .. h }
+
+end alg_equiv_class
+
 namespace alg_equiv
 
 variables {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁}
@@ -767,12 +809,13 @@ variables [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃]
 variables [algebra R A₁] [algebra R A₂] [algebra R A₃]
 variables (e : A₁ ≃ₐ[R] A₂)
 
-instance : ring_equiv_class (A₁ ≃ₐ[R] A₂) A₁ A₂ :=
+instance : alg_equiv_class (A₁ ≃ₐ[R] A₂) R A₁ A₂ :=
 { coe := to_fun,
   inv := inv_fun,
   coe_injective' := λ f g h₁ h₂, by { cases f, cases g, congr' },
   map_add := map_add',
   map_mul := map_mul',
+  commutes := commutes',
   left_inv := left_inv,
   right_inv := right_inv }
 
@@ -856,7 +899,7 @@ lemma coe_alg_hom_injective : function.injective (coe : (A₁ ≃ₐ[R] A₂) 
 lemma coe_ring_hom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) :=
 rfl
 
-protected lemma map_pow : ∀ (x : A₁) (n : ℕ), e (x ^ n) = (e x) ^ n := e.to_alg_hom.map_pow
+protected lemma map_pow : ∀ (x : A₁) (n : ℕ), e (x ^ n) = (e x) ^ n := map_pow _
 protected lemma injective : function.injective e := equiv_like.injective e
 protected lemma surjective : function.surjective e := equiv_like.surjective e
 protected lemma bijective : function.bijective e := equiv_like.bijective e
@@ -1136,11 +1179,11 @@ variables [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂)
 
 lemma map_prod {ι : Type*} (f : ι → A₁) (s : finset ι) :
   e (∏ x in s, f x) = ∏ x in s, e (f x) :=
-e.to_alg_hom.map_prod f s
+map_prod _ f s
 
 lemma map_finsupp_prod {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A₁) :
   e (f.prod g) = f.prod (λ i a, e (g i a)) :=
-e.to_alg_hom.map_finsupp_prod f g
+map_finsupp_prod _ f g
 
 end comm_semiring
 

src/algebra/hom/non_unital_alg.lean

@@ -60,6 +60,30 @@ 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
 
+/-- `non_unital_alg_hom_class F R A B` asserts `F` is a type of bundled algebra homomorphisms
+from `A` to `B`.  -/
+class non_unital_alg_hom_class (F : Type*) (R : out_param Type*) (A : out_param Type*)
+  (B : out_param Type*) [monoid R]
+  [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B]
+  [distrib_mul_action R A] [distrib_mul_action R B]
+  extends distrib_mul_action_hom_class F R A B, mul_hom_class F A B
+
+-- `R` becomes a metavariable but that's fine because it's an `out_param`
+attribute [nolint dangerous_instance] non_unital_alg_hom_class.to_mul_hom_class
+
+namespace non_unital_alg_hom_class
+
+variables [semiring R]
+  [non_unital_non_assoc_semiring A] [module R A]
+  [non_unital_non_assoc_semiring B] [module R B]
+
+@[priority 100] -- see Note [lower instance priority]
+instance {F : Type*} [non_unital_alg_hom_class F R A B] : linear_map_class F R A B :=
+{ map_smulₛₗ := distrib_mul_action_hom_class.map_smul,
+  ..‹non_unital_alg_hom_class F R A B› }
+
+end non_unital_alg_hom_class
+
 namespace non_unital_alg_hom
 
 variables {R A B C} [monoid R]
@@ -78,6 +102,14 @@ lemma coe_injective :
   @function.injective (A →ₙₐ[R] B) (A → B) coe_fn :=
 by rintro ⟨f, _⟩ ⟨g, _⟩ ⟨h⟩; congr
 
+instance : non_unital_alg_hom_class (A →ₙₐ[R] B) R A B :=
+{ coe := to_fun,
+  coe_injective' := coe_injective,
+  map_smul := λ f, f.map_smul',
+  map_add := λ f, f.map_add',
+  map_zero := λ f, f.map_zero',
+  map_mul := λ f, f.map_mul' }
+
 @[ext] lemma ext {f g : A →ₙₐ[R] B} (h : ∀ x, f x = g x) : f = g :=
 coe_injective $ funext h
 
@@ -131,20 +163,16 @@ by { ext, refl, }
   ((⟨f, h₁, h₂, h₃, h₄⟩ : A →ₙₐ[R] B) : A →ₙ* B) = ⟨f, h₄⟩ :=
 by { ext, refl, }
 
-@[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] protected lemma map_smul (f : A →ₙₐ[R] B) (c : R) (x : A) :
+  f (c • x) = c • f x := map_smul _ _ _
 
-@[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] protected lemma map_add (f : A →ₙₐ[R] B) (x y : A) :
+  f (x + y) = (f x) + (f y) := map_add _ _ _
 
-@[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] protected lemma map_mul (f : A →ₙₐ[R] B) (x y : A) :
+  f (x * y) = (f x) * (f y) := map_mul _ _ _
 
-@[simp] lemma map_zero (f : A →ₙₐ[R] B) : f 0 = 0 :=
-f.to_distrib_mul_action_hom.map_zero
+@[simp] protected lemma map_zero (f : A →ₙₐ[R] B) : f 0 = 0 := map_zero _
 
 instance : has_zero (A →ₙₐ[R] B) :=
 ⟨{ map_mul' := by simp,
@@ -263,9 +291,14 @@ namespace alg_hom
 
 variables {R A B} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
 
+@[priority 100] -- see Note [lower instance priority]
+instance {F : Type*} [alg_hom_class F R A B] : non_unital_alg_hom_class F R A B :=
+{ map_smul := map_smul,
+  ..‹alg_hom_class F R A B› }
+
 /-- A unital morphism of algebras is a `non_unital_alg_hom`. -/
 def to_non_unital_alg_hom (f : A →ₐ[R] B) : A →ₙₐ[R] B :=
-{ map_smul' := f.map_smul, .. f, }
+{ map_smul' := map_smul f, .. f, }
 
 instance non_unital_alg_hom.has_coe : has_coe (A →ₐ[R] B) (A →ₙₐ[R] B) :=
 ⟨to_non_unital_alg_hom⟩