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_1) [inst : NonUnitalNonAssocSemiring α] extends AddMonoidHom :
Type u_1
  • Commutativity of centroid homomorphims with left multiplication.

    map_mul_left' : ∀ (a b : α), ZeroHom.toFun (toAddMonoidHom) (a * b) = a * ZeroHom.toFun (toAddMonoidHom) b
  • Commutativity of centroid homomorphims with right multiplication.

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

The type of centroid homomorphisms from α to α.

Instances For
    class CentroidHomClass (F : Type u_1) (α : outParam (Type u_2)) [inst : NonUnitalNonAssocSemiring α] extends AddMonoidHomClass :
    Type (maxu_1u_2)
    • Commutativity of centroid homomorphims with left multiplication.

      map_mul_left : ∀ (f : F) (a b : α), f (a * b) = a * f b
    • Commutativity of centroid homomorphims with right multiplication.

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

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

    You should extend this class when you extend CentroidHom.

    Instances
      instance instCoeTCCentroidHom {F : Type u_1} {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst : CentroidHomClass F α] :
      Equations
      • One or more equations did not get rendered due to their size.

      Centroid homomorphisms #

      Equations
      • One or more equations did not get rendered due to their size.
      instance CentroidHom.instCoeFunCentroidHomForAll {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] :
      CoeFun (CentroidHom α) fun x => αα

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

      Equations
      theorem CentroidHom.ext {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {f : CentroidHom α} {g : CentroidHom α} (h : ∀ (a : α), f a = g a) :
      f = g
      @[simp]
      theorem CentroidHom.coe_toAddMonoidHom {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
      f = f
      @[simp]
      theorem CentroidHom.toAddMonoidHom_eq_coe {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
      f.toAddMonoidHom = f
      theorem CentroidHom.coe_toAddMonoidHom_injective {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] :
      Function.Injective AddMonoidHomClass.toAddMonoidHom

      Turn a centroid homomorphism into an additive monoid endomorphism.

      Equations
      def CentroidHom.copy {α : Type u_1} [inst : 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.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CentroidHom.coe_copy {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :
      ↑(CentroidHom.copy f f' h) = f'
      theorem CentroidHom.copy_eq {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :

      id as a CentroidHom.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CentroidHom.coe_id (α : Type u_1) [inst : NonUnitalNonAssocSemiring α] :
      ↑(CentroidHom.id α) = id
      @[simp]
      theorem CentroidHom.id_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) :
      ↑(CentroidHom.id α) a = a
      def CentroidHom.comp {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :

      Composition of CentroidHoms as a CentroidHom.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CentroidHom.coe_comp {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :
      ↑(CentroidHom.comp g f) = g f
      @[simp]
      theorem CentroidHom.comp_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) (a : α) :
      ↑(CentroidHom.comp g f) a = g (f a)
      theorem CentroidHom.cancel_right {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {g₁ : CentroidHom α} {g₂ : CentroidHom α} {f : CentroidHom α} (hf : Function.Surjective f) :
      CentroidHom.comp g₁ f = CentroidHom.comp g₂ f g₁ = g₂
      theorem CentroidHom.cancel_left {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] {g : CentroidHom α} {f₁ : CentroidHom α} {f₂ : CentroidHom α} (hg : Function.Injective g) :
      CentroidHom.comp g f₁ = CentroidHom.comp g f₂ f₁ = f₂
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • CentroidHom.instMulCentroidHom = { mul := CentroidHom.comp }
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CentroidHom.coe_zero {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] :
      0 = 0
      @[simp]
      theorem CentroidHom.coe_one {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] :
      1 = id
      @[simp]
      theorem CentroidHom.coe_add {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
      ↑(f + g) = f + g
      @[simp]
      theorem CentroidHom.coe_mul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
      ↑(f * g) = f g
      @[simp]
      theorem CentroidHom.coe_nsmul {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ) :
      ↑(n f) = n f
      @[simp]
      theorem CentroidHom.zero_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) :
      0 a = 0
      @[simp]
      theorem CentroidHom.one_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (a : α) :
      1 a = a
      @[simp]
      theorem CentroidHom.add_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
      ↑(f + g) a = f a + g a
      @[simp]
      theorem CentroidHom.mul_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
      ↑(f * g) a = f (g a)
      @[simp]
      theorem CentroidHom.nsmul_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α) (n : ) (a : α) :
      ↑(n f) a = n f a
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • CentroidHom.instNatCastCentroidHom = { natCast := fun n => n 1 }
      @[simp]
      theorem CentroidHom.coe_nat_cast {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ) :
      n = ↑(n CentroidHom.id α)
      theorem CentroidHom.nat_cast_apply {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ) (m : α) :
      n m = n m
      @[simp]
      @[simp]
      theorem CentroidHom.toEnd_nat_cast {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (n : ) :
      Equations
      • One or more equations did not get rendered due to their size.
      theorem CentroidHom.comp_mul_comm {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (T : CentroidHom α) (S : CentroidHom α) (a : α) (b : α) :
      (T S) (a * b) = (S T) (a * b)

      Negation of CentroidHoms as a CentroidHom.

      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      instance CentroidHom.hasZsmul {α : Type u_1} [inst : NonUnitalNonAssocRing α] :
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • CentroidHom.instIntCastCentroidHomToNonUnitalNonAssocSemiring = { intCast := fun z => z 1 }
      @[simp]
      theorem CentroidHom.coe_int_cast {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ) :
      z = ↑(z CentroidHom.id α)
      theorem CentroidHom.int_cast_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ) (m : α) :
      z m = z m
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CentroidHom.coe_neg {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) :
      ↑(-f) = -f
      @[simp]
      theorem CentroidHom.coe_sub {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) :
      ↑(f - g) = f - g
      @[simp]
      theorem CentroidHom.neg_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α) :
      ↑(-f) a = -f a
      @[simp]
      theorem CentroidHom.sub_apply {α : Type u_1} [inst : NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
      ↑(f - g) a = f a - g a
      @[simp]
      theorem CentroidHom.toEnd_int_cast {α : Type u_1} [inst : NonUnitalNonAssocRing α] (z : ) :
      Equations
      • One or more equations did not get rendered due to their size.
      def CentroidHom.commRing {α : Type u_1} [inst : NonUnitalRing α] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 b = 0) :

      A prime associative ring has commutative centroid.

      Equations