chore(RingTheory/Bialgebra/MonoidAlgebra): use to_additive (leanprover-community#33452)

Author: YaelDillies

Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

@@ -36,6 +36,7 @@ namespace MonoidAlgebra
 variable [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] [Monoid O]
 
 variable (R A M) in
+@[to_additive (dont_translate := R A) (relevant_arg := M)]
 instance instBialgebra : Bialgebra R A[M] where
   counit_one := by simp only [one_def, counit_single, Bialgebra.counit_one]
   mul_compr₂_counit := by ext; simp
@@ -51,70 +52,37 @@ instance instBialgebra : Bialgebra R A[M] where
       LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
       Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]
 
+-- TODO: Generalise to `A[M] →ₐc[R] A[N]` under `Bialgebra R A`
+variable (R) [AddMonoid M] [AddMonoid N] in
+/-- If `f : M → N` is a monoid hom, then `AddMonoidAlgebra.mapDomain f` is a bialgebra hom between
+their additive monoid algebras. -/
+noncomputable def _root_.AddMonoidAlgebra.mapDomainBialgHom (f : M →+ N) :
+    AddMonoidAlgebra R M →ₐc[R] AddMonoidAlgebra R N :=
+  .ofAlgHom (AddMonoidAlgebra.mapDomainAlgHom R R f) (by ext; simp) (by ext; simp)
+
 -- TODO: Generalise to `A[M] →ₐc[R] A[N]` under `Bialgebra R A`
 variable (R) in
 /-- If `f : M → N` is a monoid hom, then `MonoidAlgebra.mapDomain f` is a bialgebra hom between
 their monoid algebras. -/
-@[simps!]
+@[to_additive existing (attr := simps!)]
 noncomputable def mapDomainBialgHom (f : M →* N) : R[M] →ₐc[R] R[N] :=
   .ofAlgHom (mapDomainAlgHom R R f) (by ext; simp) (by ext; simp)
 
-@[simp] lemma mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id R R[M] := by ext; simp
+@[to_additive (attr := simp)]
+lemma mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id R R[M] := by ext; simp
 
-@[simp]
+@[to_additive (attr := simp)]
 lemma mapDomainBialgHom_comp (f : N →* O) (g : M →* N) :
     mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g) := by
   ext; simp [Finsupp.mapDomain_comp]
 
+@[to_additive]
 lemma mapDomainBialgHom_mapDomainBialgHom (f : N →* O) (g : M →* N) (x : R[M]) :
     mapDomainBialgHom R f (mapDomainBialgHom R g x) = mapDomainBialgHom R (f.comp g) x := by
   ext; simp
 
 end MonoidAlgebra
 
-namespace AddMonoidAlgebra
-variable [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] [AddMonoid O]
-
-variable (R A M) in
-instance instBialgebra : Bialgebra R A[M] where
-  counit_one := by simp only [one_def, counit_single, Bialgebra.counit_one]
-  mul_compr₂_counit := by ext; simp [single_mul_single]
-  comul_one := by
-    simp only [one_def, comul_single, Bialgebra.comul_one, Algebra.TensorProduct.one_def,
-      TensorProduct.map_tmul, lsingle_apply]
-  mul_compr₂_comul := by
-    ext a b c d
-    simp only [Function.comp_apply, LinearMap.coe_comp, LinearMap.compr₂_apply,
-      LinearMap.mul_apply', single_mul_single, comul_single, Bialgebra.comul_mul,
-      ← (Coalgebra.Repr.arbitrary R b).eq, ← (Coalgebra.Repr.arbitrary R d).eq, Finset.sum_mul_sum,
-      Algebra.TensorProduct.tmul_mul_tmul, map_sum, TensorProduct.map_tmul, lsingle_apply,
-      LinearMap.compl₁₂_apply, LinearMap.coe_sum, Finset.sum_apply,
-      Finset.sum_comm (s := (Coalgebra.Repr.arbitrary R b).index)]
-
--- TODO: Generalise to `A[M] →ₐc[R] A[N]` under `Bialgebra R A`
-variable (R) in
-/-- If `f : M → N` is a monoid hom, then `AddMonoidAlgebra.mapDomain f` is a bialgebra hom between
-their monoid algebras. -/
-@[simps]
-noncomputable def mapDomainBialgHom (f : M →+ N) : R[M] →ₐc[R] R[N] where
-  __ := mapDomainAlgHom R R f
-  map_smul' m x := by simp
-  counit_comp := by ext; simp
-  map_comp_comul := by ext; simp
-
-@[simp] lemma mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id _ _ := by ext; simp
-
-@[simp]
-lemma mapDomainBialgHom_comp (f : N →+ O) (g : M →+ N) :
-    mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g) := by
-  ext; simp
-
-lemma mapDomainBialgHom_mapDomainBialgHom (f : N →+ O) (g : M →+ N) (x : R[M]) :
-    mapDomainBialgHom R f (mapDomainBialgHom R g x) = mapDomainBialgHom R (f.comp g) x := by
-  ext; simp
-
-end AddMonoidAlgebra
-
 namespace LaurentPolynomial
 
 open AddMonoidAlgebra

Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean

@@ -36,15 +36,17 @@ variable {R A : Type*} [CommSemiring R] [Semiring A] [HopfAlgebra R A]
 variable {G : Type*} [Group G]
 
 variable (R A G) in
+@[to_additive (dont_translate := R) (relevant_arg := G)]
 instance instHopfAlgebraStruct : HopfAlgebraStruct R A[G] where
   antipode := Finsupp.lsum R fun g => Finsupp.lsingle g⁻¹ ∘ₗ antipode R
 
-@[simp]
+@[to_additive (attr := simp)]
 lemma antipode_single (g : G) (a : A) :
     antipode R (single g a) = single g⁻¹ (antipode R a) := by
   simp [MonoidAlgebra, antipode]
 
 open Coalgebra in
+@[to_additive (dont_translate := R A) (relevant_arg := G)]
 instance instHopfAlgebra : HopfAlgebra R A[G] where
   mul_antipode_rTensor_comul := by
     ext a b : 2
@@ -57,33 +59,6 @@ instance instHopfAlgebra : HopfAlgebra R A[G] where
 
 end MonoidAlgebra
 
-namespace AddMonoidAlgebra
-
-variable {R A : Type*} [CommSemiring R] [Semiring A] [HopfAlgebra R A]
-variable {G : Type*} [AddGroup G]
-
-variable (R A G) in
-instance instHopfAlgebraStruct : HopfAlgebraStruct R A[G] where
-  antipode := Finsupp.lsum R fun g => Finsupp.lsingle (-g) ∘ₗ antipode R
-
-@[simp]
-lemma antipode_single (g : G) (a : A) :
-    antipode R (single g a) = single (-g) (antipode R a) := by
-  simp [AddMonoidAlgebra, antipode]
-
-open Coalgebra in
-instance instHopfAlgebra : HopfAlgebra R A[G] where
-  mul_antipode_rTensor_comul := by
-    ext a b : 2
-    simpa [← (ℛ R b).eq, single_mul_single] using congr(lsingle (R := R) (0 : G)
-      $(sum_antipode_mul_eq_algebraMap_counit (ℛ R b)))
-  mul_antipode_lTensor_comul := by
-    ext a b : 2
-    simpa [← (ℛ R b).eq, single_mul_single] using congr(lsingle (R := R) (0 : G)
-      $(sum_mul_antipode_eq_algebraMap_counit (ℛ R b)))
-
-end AddMonoidAlgebra
-
 namespace LaurentPolynomial
 
 open Finsupp