feat(Algebra/Ring/CentroidHom): CentroidHom and algebras (#8699)

Explore the relationship between the Centroid of a ring and algebra:

- A a non-unital, non-associative semiring α is an algebra over the Semiring CentroidHom α
- When the non-unital, non-associative semiring α  is an algebra over the commutative semiring R, then CentroidHom α is a ring over R, provided the range of the natural ring homomorphism from R into CentroidHom α lies in the center of CentroidHom α.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/Ring/CentroidHom.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Christopher Hoskin
 -/
+import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Module.Hom
 import Mathlib.RingTheory.NonUnitalSubsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Basic
@@ -432,6 +433,55 @@ instance : DistribMulAction M (CentroidHom α) :=
 instance : Module R (CentroidHom α) :=
   toEnd_injective.module R (toEndRingHom α).toAddMonoidHom toEnd_smul
 
+/-!
+The following instances show that `α` is a non-unital and non-associative algebra over
+`CentroidHom α`.
+-/
+
+/-- The tautological action by `CentroidHom α` on `α`.
+
+This generalizes `Function.End.applyMulAction`. -/
+instance applyModule : Module (CentroidHom α) α where
+  smul T a := T a
+  add_smul _ _ _ := rfl
+  zero_smul _ := rfl
+  one_smul _ := rfl
+  mul_smul _ _ _:= rfl
+  smul_zero := map_zero
+  smul_add := map_add
+
+@[simp]
+lemma smul_def (T : CentroidHom α) (a : α) : T • a = T a := rfl
+
+instance : SMulCommClass (CentroidHom α) α α where
+  smul_comm _ _ _ := map_mul_left _ _ _
+
+instance : SMulCommClass α (CentroidHom α) α := SMulCommClass.symm _ _ _
+
+instance : IsScalarTower (CentroidHom α) α α where
+  smul_assoc _ _ _ := (map_mul_right _ _ _).symm
+
+/-!
+Let `α` be an algebra over `R`, such that the canonical ring homomorphism of `R` into
+`CentroidHom α` lies in the center of `CentroidHom α`. Then `CentroidHom α` is an algebra over `R`
+-/
+
+variable {R : Type*}
+
+variable [CommSemiring R]
+variable [Module R α] [SMulCommClass R α α] [IsScalarTower R α α]
+
+/-- The natural ring homomorphism from `R` into `CentroidHom α`.
+
+This is a stronger version of `Module.toAddMonoidEnd`. -/
+@[simps! apply_toFun]
+def _root_.Module.toCentroidHom : R →+* CentroidHom α := RingHom.smulOneHom
+
+open Module in
+/-- `CentroidHom α` as an algebra over `R`. -/
+example (h : ∀ (r : R) (T : CentroidHom α), toCentroidHom r * T = T * toCentroidHom r) :
+    Algebra R (CentroidHom α) := toCentroidHom.toAlgebra' h
+
 local notation "L" => AddMonoid.End.mulLeft
 local notation "R" => AddMonoid.End.mulRight