Documentation

Mathlib.Algebra.Hom.Centroid

Centroid homomorphisms #

Let A be a (non unital, non associative) algebra. The centroid of A is the set of linear maps T on A such that T commutes with left and right multiplication, that is to say, for all a and b in A, $$ T(ab) = (Ta)b, T(ab) = a(Tb). $$ In mathlib we call elements of the centroid "centroid homomorphisms" (CentroidHom) in keeping with AddMonoidHom etc.

We use the FunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

Types of morphisms #

Typeclasses #

References #

Tags #

centroid

structure CentroidHom (α : Type u_3) [NonUnitalNonAssocSemiring α] extends AddMonoidHom :
Type u_3
  • toFun : αα
  • map_zero' : ZeroHom.toFun (s.toAddMonoidHom) 0 = 0
  • map_add' : ∀ (x y : α), ZeroHom.toFun (s.toAddMonoidHom) (x + y) = ZeroHom.toFun (s.toAddMonoidHom) x + ZeroHom.toFun (s.toAddMonoidHom) y
  • map_mul_left' : ∀ (a b : α), ZeroHom.toFun (s.toAddMonoidHom) (a * b) = a * ZeroHom.toFun (s.toAddMonoidHom) b

    Commutativity of centroid homomorphims with left multiplication.

  • map_mul_right' : ∀ (a b : α), ZeroHom.toFun (s.toAddMonoidHom) (a * b) = ZeroHom.toFun (s.toAddMonoidHom) a * b

    Commutativity of centroid homomorphims with right multiplication.

The type of centroid homomorphisms from α to α.

Instances For
    class CentroidHomClass (F : Type u_3) (α : outParam (Type u_4)) [NonUnitalNonAssocSemiring α] extends AddMonoidHomClass :
    Type (max u_3 u_4)
    • coe : Fαα
    • coe_injective' : Function.Injective FunLike.coe
    • map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y
    • map_zero : ∀ (f : F), f 0 = 0
    • map_mul_left : ∀ (f : F) (a b : α), f (a * b) = a * f b

      Commutativity of centroid homomorphims with left multiplication.

    • map_mul_right : ∀ (f : F) (a b : α), f (a * b) = f a * b

      Commutativity of centroid homomorphims with right multiplication.

    CentroidHomClass F α states that F is a type of centroid homomorphisms.

    You should extend this class when you extend CentroidHom.

    Instances

      Centroid homomorphisms #

      Helper instance for when there's too many metavariables to apply FunLike.CoeFun directly.

      theorem CentroidHom.toFun_eq_coe {α : Type u_2} [NonUnitalNonAssocSemiring α] {f : CentroidHom α} :
      f.toFun = f
      theorem CentroidHom.ext {α : Type u_2} [NonUnitalNonAssocSemiring α] {f : CentroidHom α} {g : CentroidHom α} (h : ∀ (a : α), f a = g a) :
      f = g
      @[simp]
      theorem CentroidHom.coe_toAddMonoidHom {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
      f = f
      @[simp]
      theorem CentroidHom.toAddMonoidHom_eq_coe {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
      f.toAddMonoidHom = f

      Turn a centroid homomorphism into an additive monoid endomorphism.

      Instances For
        def CentroidHom.copy {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :

        Copy of a CentroidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

        Instances For
          @[simp]
          theorem CentroidHom.coe_copy {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :
          ↑(CentroidHom.copy f f' h) = f'
          theorem CentroidHom.copy_eq {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :
          @[simp]
          @[simp]
          theorem CentroidHom.id_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (a : α) :
          ↑(CentroidHom.id α) a = a

          Composition of CentroidHoms as a CentroidHom.

          Instances For
            @[simp]
            theorem CentroidHom.coe_comp {α : Type u_2} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :
            ↑(CentroidHom.comp g f) = g f
            @[simp]
            theorem CentroidHom.comp_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) (a : α) :
            ↑(CentroidHom.comp g f) a = g (f a)
            @[simp]
            theorem CentroidHom.cancel_right {α : Type u_2} [NonUnitalNonAssocSemiring α] {g₁ : CentroidHom α} {g₂ : CentroidHom α} {f : CentroidHom α} (hf : Function.Surjective f) :
            CentroidHom.comp g₁ f = CentroidHom.comp g₂ f g₁ = g₂
            @[simp]
            theorem CentroidHom.cancel_left {α : Type u_2} [NonUnitalNonAssocSemiring α] {g : CentroidHom α} {f₁ : CentroidHom α} {f₂ : CentroidHom α} (hg : Function.Injective g) :
            CentroidHom.comp g f₁ = CentroidHom.comp g f₂ f₁ = f₂
            @[simp]
            theorem CentroidHom.coe_zero {α : Type u_2} [NonUnitalNonAssocSemiring α] :
            0 = 0
            @[simp]
            theorem CentroidHom.coe_one {α : Type u_2} [NonUnitalNonAssocSemiring α] :
            1 = id
            @[simp]
            theorem CentroidHom.coe_add {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
            ↑(f + g) = f + g
            @[simp]
            theorem CentroidHom.coe_mul {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
            ↑(f * g) = f g
            @[simp]
            theorem CentroidHom.coe_nsmul {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ) :
            ↑(n f) = n f
            @[simp]
            theorem CentroidHom.zero_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (a : α) :
            0 a = 0
            @[simp]
            theorem CentroidHom.one_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (a : α) :
            1 a = a
            @[simp]
            theorem CentroidHom.add_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
            ↑(f + g) a = f a + g a
            @[simp]
            theorem CentroidHom.mul_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
            ↑(f * g) a = f (g a)
            @[simp]
            theorem CentroidHom.nsmul_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ) (a : α) :
            ↑(n f) a = n f a
            @[simp]
            theorem CentroidHom.coe_nat_cast {α : Type u_2} [NonUnitalNonAssocSemiring α] (n : ) :
            n = ↑(n CentroidHom.id α)
            theorem CentroidHom.nat_cast_apply {α : Type u_2} [NonUnitalNonAssocSemiring α] (n : ) (m : α) :
            n m = n m
            theorem CentroidHom.comp_mul_comm {α : Type u_2} [NonUnitalNonAssocSemiring α] (T : CentroidHom α) (S : CentroidHom α) (a : α) (b : α) :
            (T S) (a * b) = (S T) (a * b)
            @[simp]
            theorem CentroidHom.coe_int_cast {α : Type u_2} [NonUnitalNonAssocRing α] (z : ) :
            z = ↑(z CentroidHom.id α)
            theorem CentroidHom.int_cast_apply {α : Type u_2} [NonUnitalNonAssocRing α] (z : ) (m : α) :
            z m = z m
            @[simp]
            theorem CentroidHom.coe_neg {α : Type u_2} [NonUnitalNonAssocRing α] (f : CentroidHom α) :
            ↑(-f) = -f
            @[simp]
            theorem CentroidHom.coe_sub {α : Type u_2} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) :
            ↑(f - g) = f - g
            @[simp]
            theorem CentroidHom.neg_apply {α : Type u_2} [NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α) :
            ↑(-f) a = -f a
            @[simp]
            theorem CentroidHom.sub_apply {α : Type u_2} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
            ↑(f - g) a = f a - g a
            @[simp]
            @[reducible]
            def CentroidHom.commRing {α : Type u_2} [NonUnitalRing α] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 b = 0) :

            A prime associative ring has commutative centroid.

            Instances For