[Merged by Bors] - feat(algebra/{monoid_algebra/basic,free_non_unital_non_assoc_algebra,lie/free}): generalize typeclasses

src/algebra/free_non_unital_non_assoc_algebra.lean

@@ -42,8 +42,7 @@ noncomputable theory
 variables (R : Type u) (X : Type v) [semiring R]
 
 /-- The free non-unital, non-associative algebra on the type `X` with coefficients in `R`. -/
-@[derive [inhabited, non_unital_non_assoc_semiring, module R]]
-def free_non_unital_non_assoc_algebra := monoid_algebra R (free_magma X)
+abbreviation free_non_unital_non_assoc_algebra := monoid_algebra R (free_magma X)
 
 namespace free_non_unital_non_assoc_algebra
 
@@ -53,19 +52,6 @@ variables {X}
 def of : X → free_non_unital_non_assoc_algebra R X :=
 (monoid_algebra.of_magma R _) ∘ free_magma.of
 
-instance : is_scalar_tower R
-  (free_non_unital_non_assoc_algebra R X) (free_non_unital_non_assoc_algebra R X) :=
-monoid_algebra.is_scalar_tower_self R
-
-/-- If the coefficients are commutative amongst themselves, they also commute with the algebra
-multiplication. -/
-instance (R : Type u) [comm_semiring R] : smul_comm_class R
-  (free_non_unital_non_assoc_algebra R X) (free_non_unital_non_assoc_algebra R X) :=
-monoid_algebra.smul_comm_class_self R
-
-instance (R : Type u) [ring R] : add_comm_group (free_non_unital_non_assoc_algebra R X) :=
-module.add_comm_monoid_to_add_comm_group R
-
 variables {A : Type w} [non_unital_non_assoc_semiring A]
 variables [module R A] [is_scalar_tower R A A] [smul_comm_class R A A]
 
@@ -87,18 +73,15 @@ rfl
   F ∘ (of R) = f ↔ F = lift R f :=
 (lift R).symm_apply_eq
 
-attribute [irreducible] of lift
-
 @[simp] lemma lift_of_apply (f : X → A) (x) : lift R f (of R x) = f x :=
-by rw [← function.comp_app (lift R f) (of R) x, of_comp_lift]
+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) :
   lift R (F ∘ (of R)) = F :=
-by rw [← lift_symm_apply, equiv.apply_symm_apply]
+(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}
   (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ :=
-have h' : (lift R).symm F₁ = (lift R).symm F₂, { ext, simp [h], },
-(lift R).symm.injective h'
+(lift R).symm.injective $ funext h
 
 end free_non_unital_non_assoc_algebra

src/algebra/lie/free.lean

@@ -69,18 +69,32 @@ the free Lie algebra. -/
 inductive rel : lib R X → lib R X → Prop
 | lie_self (a : lib R X) : rel (a * a) 0
 | leibniz_lie (a b c : lib R X) : rel (a * (b * c)) (((a * b) * c) + (b * (a * c)))
-| smul (t : R) (a b : lib R X) : rel a b → rel (t • a) (t • b)
-| add_right (a b c : lib R X) : rel a b → rel (a + c) (b + c)
-| mul_left (a b c : lib R X) : rel b c → rel (a * b) (a * c)
-| mul_right (a b c : lib R X) : rel a b → rel (a * c) (b * c)
+| smul (t : R) {a b : lib R X} : rel a b → rel (t • a) (t • b)
+| add_right {a b : lib R X} (c : lib R X) : rel a b → rel (a + c) (b + c)
+| mul_left (a : lib R X) {b c : lib R X} : rel b c → rel (a * b) (a * c)
+| mul_right {a b : lib R X} (c : lib R X) : rel a b → rel (a * c) (b * c)
 
 variables {R X}
 
-lemma rel.add_left (a b c : lib R X) (h : rel R X b c) : rel R X (a + b) (a + c) :=
-by { rw [add_comm _ b, add_comm _ c], exact rel.add_right _ _ _ h, }
+lemma rel.add_left (a : lib R X) {b c : lib R X} (h : rel R X b c) : rel R X (a + b) (a + c) :=
+by { rw [add_comm _ b, add_comm _ c], exact h.add_right _, }
 
-lemma rel.neg (a b : lib R X) (h : rel R X a b) : rel R X (-a) (-b) :=
-h.smul (-1) _ _
+lemma rel.neg {a b : lib R X} (h : rel R X a b) : rel R X (-a) (-b) :=
+by simpa only [neg_one_smul] using h.smul (-1)
+
+lemma rel.sub_left (a : lib R X) {b c : lib R X} (h : rel R X b c) : rel R X (a - b) (a - c) :=
+by simpa only [sub_eq_add_neg] using h.neg.add_left a
+
+lemma rel.sub_right {a b : lib R X} (c : lib R X) (h : rel R X a b) : rel R X (a - c) (b - c) :=
+by simpa only [sub_eq_add_neg] using h.add_right (-c)
+
+lemma rel.smul_of_tower {S : Type*} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R]
+  (t : S) (a b : lib R X)
+  (h : rel R X a b) : rel R X (t • a) (t • b) :=
+begin
+  rw [←smul_one_smul R t a, ←smul_one_smul R t b],
+  exact h.smul _,
+end
 
 end free_lie_algebra
 
@@ -90,29 +104,46 @@ def free_lie_algebra := quot (free_lie_algebra.rel R X)
 
 namespace free_lie_algebra
 
+instance {S : Type*} [monoid S] [distrib_mul_action S R] [is_scalar_tower S R R] :
+  has_scalar S (free_lie_algebra R X) :=
+{ smul := λ t, quot.map ((•) t) (rel.smul_of_tower t) }
+
+instance {S : Type*} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R]
+  [is_scalar_tower S R R] [is_central_scalar S R] :
+  is_central_scalar S (free_lie_algebra R X) :=
+{ op_smul_eq_smul := λ t, quot.ind $ by exact λ a, congr_arg (quot.mk _) (op_smul_eq_smul t a) }
+
+instance : has_zero (free_lie_algebra R X) :=
+{ zero := quot.mk _ 0 }
+
+instance : has_add (free_lie_algebra R X) :=
+{ add := quot.map₂ (+) (λ _ _ _, rel.add_left _) (λ _ _ _, rel.add_right _) }
+
+instance : has_neg (free_lie_algebra R X) :=
+{ neg := quot.map has_neg.neg (λ _ _, rel.neg) }
+
+instance : has_sub (free_lie_algebra R X) :=
+{ sub := quot.map₂ has_sub.sub (λ _ _ _, rel.sub_left _) (λ _ _ _, rel.sub_right _) }
+
+instance : add_group (free_lie_algebra R X) :=
+function.surjective.add_group_smul (quot.mk _) (surjective_quot_mk _)
+  rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
+instance : add_comm_semigroup (free_lie_algebra R X) :=
+function.surjective.add_comm_semigroup (quot.mk _) (surjective_quot_mk _) (λ _ _, rfl)
+
 instance : add_comm_group (free_lie_algebra R X) :=
-{ add            := quot.map₂ (+) rel.add_left rel.add_right,
-  add_comm       := by { rintros ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw add_comm, },
-  add_assoc      := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_assoc, },
-  zero           := quot.mk _ 0,
-  zero_add       := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw zero_add, },
-  add_zero       := by { rintros ⟨a⟩, change quot.mk _ _ = _, rw add_zero, },
-  neg            := quot.map has_neg.neg rel.neg,
-  add_left_neg   := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _ , rw add_left_neg, } }
-
-instance : module R (free_lie_algebra R X) :=
-{ smul      := λ t, quot.map ((•) t) (rel.smul t),
-  one_smul  := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw one_smul, },
-  mul_smul  := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw mul_smul, },
-  add_smul  := by { rintros t₁ t₂ ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw add_smul, },
-  smul_add  := by { rintros t ⟨a⟩ ⟨b⟩, change quot.mk _ _ = quot.mk _ _, rw smul_add, },
-  zero_smul := by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, rw zero_smul, },
-  smul_zero := λ t, by { change quot.mk _ _ = quot.mk _ _, rw smul_zero, }, }
+{ ..free_lie_algebra.add_group R X,
+  ..free_lie_algebra.add_comm_semigroup R X }
+
+instance {S : Type*} [semiring S] [module S R] [is_scalar_tower S R R] :
+  module S (free_lie_algebra R X) :=
+function.surjective.module S ⟨quot.mk _, rfl, λ _ _, rfl⟩ (surjective_quot_mk _) (λ _ _, rfl)
 
 /-- Note that here we turn the `has_mul` coming from the `non_unital_non_assoc_semiring` structure
 on `lib R X` into a `has_bracket` on `free_lie_algebra`. -/
 instance : lie_ring (free_lie_algebra R X) :=
-{ bracket     := quot.map₂ (*) rel.mul_left rel.mul_right,
+{ bracket     := quot.map₂ (*) (λ _ _ _, rel.mul_left _) (λ _ _ _, rel.mul_right _),
   add_lie     := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw add_mul, },
   lie_add     := by { rintros ⟨a⟩ ⟨b⟩ ⟨c⟩, change quot.mk _ _ = quot.mk _ _, rw mul_add, },
   lie_self    := by { rintros ⟨a⟩, exact quot.sound (rel.lie_self a), },

src/algebra/monoid_algebra/basic.lean

@@ -218,12 +218,15 @@ section derived_instances
 instance [semiring k] [subsingleton k] : unique (monoid_algebra k G) :=
 finsupp.unique_of_right
 
-instance [ring k] : add_group (monoid_algebra k G) :=
-finsupp.add_group
+instance [ring k] : add_comm_group (monoid_algebra k G) :=
+finsupp.add_comm_group
+
+instance [ring k] [has_mul G] : non_unital_non_assoc_ring (monoid_algebra k G) :=
+{ .. monoid_algebra.add_comm_group,
+  .. monoid_algebra.non_unital_non_assoc_semiring }
 
 instance [ring k] [monoid G] : ring (monoid_algebra k G) :=
-{ neg := has_neg.neg,
-  add_left_neg := add_left_neg,
+{ .. monoid_algebra.non_unital_non_assoc_ring,
   .. monoid_algebra.semiring }
 
 instance [comm_ring k] [comm_monoid G] : comm_ring (monoid_algebra k G) :=
@@ -423,7 +426,7 @@ end misc_theorems
 /-! #### Non-unital, non-associative algebra structure -/
 section non_unital_non_assoc_algebra
 
-variables {R : Type*} (k) [semiring R] [semiring k] [distrib_mul_action R k] [has_mul G]
+variables {R : Type*} (k) [monoid R] [semiring k] [distrib_mul_action R k] [has_mul G]
 
 instance is_scalar_tower_self [is_scalar_tower R k k] :
   is_scalar_tower R (monoid_algebra k G) (monoid_algebra k G) :=
@@ -953,14 +956,15 @@ section derived_instances
 instance [semiring k] [subsingleton k] : unique (add_monoid_algebra k G) :=
 finsupp.unique_of_right
 
-instance [ring k] : add_group (add_monoid_algebra k G) :=
-finsupp.add_group
+instance [ring k] : add_comm_group (add_monoid_algebra k G) :=
+finsupp.add_comm_group
+
+instance [ring k] [has_add G] : non_unital_non_assoc_ring (add_monoid_algebra k G) :=
+{ .. add_monoid_algebra.add_comm_group,
+  .. add_monoid_algebra.non_unital_non_assoc_semiring }
 
 instance [ring k] [add_monoid G] : ring (add_monoid_algebra k G) :=
-{ neg := has_neg.neg,
-  add_left_neg := add_left_neg,
-  sub := has_sub.sub,
-  sub_eq_add_neg := finsupp.add_group.sub_eq_add_neg,
+{ .. add_monoid_algebra.non_unital_non_assoc_ring,
   .. add_monoid_algebra.semiring }
 
 instance [comm_ring k] [add_comm_monoid G] : comm_ring (add_monoid_algebra k G) :=
@@ -1193,7 +1197,7 @@ variables {k G}
 
 section non_unital_non_assoc_algebra
 
-variables {R : Type*} (k) [semiring R] [semiring k] [distrib_mul_action R k] [has_add G]
+variables {R : Type*} (k) [monoid R] [semiring k] [distrib_mul_action R k] [has_add G]
 
 instance is_scalar_tower_self [is_scalar_tower R k k] :
   is_scalar_tower R (add_monoid_algebra k G) (add_monoid_algebra k G) :=