Documentation

Mathlib.Algebra.Ring.CentroidHom

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 DFunLike 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_6) [NonUnitalNonAssocSemiring α] extends AddMonoidHom :
Type u_6

The type of centroid homomorphisms from α to α.

  • toFun : αα
  • map_zero' : (self.toAddMonoidHom).toFun 0 = 0
  • map_add' : ∀ (x y : α), (self.toAddMonoidHom).toFun (x + y) = (self.toAddMonoidHom).toFun x + (self.toAddMonoidHom).toFun y
  • map_mul_left' : ∀ (a b : α), (self.toAddMonoidHom).toFun (a * b) = a * (self.toAddMonoidHom).toFun b

    Commutativity of centroid homomorphims with left multiplication.

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

    Commutativity of centroid homomorphims with right multiplication.

Instances For
    theorem CentroidHom.map_mul_left' {α : Type u_6} [NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a : α) (b : α) :
    (self.toAddMonoidHom).toFun (a * b) = a * (self.toAddMonoidHom).toFun b

    Commutativity of centroid homomorphims with left multiplication.

    theorem CentroidHom.map_mul_right' {α : Type u_6} [NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a : α) (b : α) :
    (self.toAddMonoidHom).toFun (a * b) = (self.toAddMonoidHom).toFun a * b

    Commutativity of centroid homomorphims with right multiplication.

    class CentroidHomClass (F : Type u_6) (α : Type u_7) [NonUnitalNonAssocSemiring α] [FunLike F α α] extends AddMonoidHomClass :

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

    You should extend this class when you extend CentroidHom.

    • 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.

    Instances
      theorem CentroidHomClass.map_mul_left {F : Type u_6} {α : Type u_7} [NonUnitalNonAssocSemiring α] [FunLike F α α] [self : CentroidHomClass F α] (f : F) (a : α) (b : α) :
      f (a * b) = a * f b

      Commutativity of centroid homomorphims with left multiplication.

      theorem CentroidHomClass.map_mul_right {F : Type u_6} {α : Type u_7} [NonUnitalNonAssocSemiring α] [FunLike F α α] [self : CentroidHomClass F α] (f : F) (a : α) (b : α) :
      f (a * b) = f a * b

      Commutativity of centroid homomorphims with right multiplication.

      Equations
      • instCoeTCCentroidHomOfCentroidHomClass = { coe := fun (f : F) => let __src := f; { toFun := f, map_zero' := , map_add' := , map_mul_left' := , map_mul_right' := } }

      Centroid homomorphisms #

      Equations
      • CentroidHom.instFunLike = { coe := fun (f : CentroidHom α) => (f.toAddMonoidHom).toFun, coe_injective' := }
      instance CentroidHom.instCoeFunForall {α : Type u_5} [NonUnitalNonAssocSemiring α] :
      CoeFun (CentroidHom α) fun (x : CentroidHom α) => αα

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

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

      Turn a centroid homomorphism into an additive monoid endomorphism.

      Equations
      • f.toEnd = f
      Instances For
        def CentroidHom.copy {α : Type u_5} [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
        • f.copy f' h = let __src := f.copy f' h; { toFun := f', map_zero' := , map_add' := , map_mul_left' := , map_mul_right' := }
        Instances For
          @[simp]
          theorem CentroidHom.coe_copy {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :
          (f.copy f' h) = f'
          theorem CentroidHom.copy_eq {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (f' : αα) (h : f' = f) :
          f.copy f' h = f

          id as a CentroidHom.

          Equations
          Instances For
            @[simp]
            @[simp]
            theorem CentroidHom.id_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :
            (CentroidHom.id α) a = a

            Composition of CentroidHoms as a CentroidHom.

            Equations
            • g.comp f = let __src := g.comp f.toAddMonoidHom; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := }
            Instances For
              @[simp]
              theorem CentroidHom.coe_comp {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :
              (g.comp f) = g f
              @[simp]
              theorem CentroidHom.comp_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) (a : α) :
              (g.comp f) a = g (f a)
              @[simp]
              theorem CentroidHom.coe_comp_addMonoidHom {α : Type u_5} [NonUnitalNonAssocSemiring α] (g : CentroidHom α) (f : CentroidHom α) :
              (g.comp f) = (g).comp f
              @[simp]
              theorem CentroidHom.comp_assoc {α : Type u_5} [NonUnitalNonAssocSemiring α] (h : CentroidHom α) (g : CentroidHom α) (f : CentroidHom α) :
              (h.comp g).comp f = h.comp (g.comp f)
              @[simp]
              theorem CentroidHom.comp_id {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
              f.comp (CentroidHom.id α) = f
              @[simp]
              theorem CentroidHom.id_comp {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) :
              (CentroidHom.id α).comp f = f
              @[simp]
              theorem CentroidHom.cancel_right {α : Type u_5} [NonUnitalNonAssocSemiring α] {g₁ : CentroidHom α} {g₂ : CentroidHom α} {f : CentroidHom α} (hf : Function.Surjective f) :
              g₁.comp f = g₂.comp f g₁ = g₂
              @[simp]
              theorem CentroidHom.cancel_left {α : Type u_5} [NonUnitalNonAssocSemiring α] {g : CentroidHom α} {f₁ : CentroidHom α} {f₂ : CentroidHom α} (hg : Function.Injective g) :
              g.comp f₁ = g.comp f₂ f₁ = f₂
              Equations
              • CentroidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
              Equations
              Equations
              • CentroidHom.instAdd = { add := fun (f g : CentroidHom α) => let __src := f + g; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
              Equations
              • CentroidHom.instMul = { mul := CentroidHom.comp }
              instance CentroidHom.instSMul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] :
              Equations
              • CentroidHom.instSMul = { smul := fun (n : M) (f : CentroidHom α) => let __src := n f; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
              instance CentroidHom.instIsScalarTower {M : Type u_2} {N : Type u_3} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [Monoid N] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] [DistribMulAction N α] [SMulCommClass N α α] [IsScalarTower N α α] [SMul M N] [IsScalarTower M N α] :
              Equations
              • =
              instance CentroidHom.instSMulCommClass {M : Type u_2} {N : Type u_3} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [Monoid N] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] [DistribMulAction N α] [SMulCommClass N α α] [IsScalarTower N α α] [SMulCommClass M N α] :
              Equations
              • =
              Equations
              • =
              Equations
              • CentroidHom.hasNPowNat = { pow := fun (f : CentroidHom α) (n : ) => { toAddMonoidHom := f.toEnd ^ n, map_mul_left' := , map_mul_right' := } }
              @[simp]
              theorem CentroidHom.coe_zero {α : Type u_5} [NonUnitalNonAssocSemiring α] :
              0 = 0
              @[simp]
              theorem CentroidHom.coe_one {α : Type u_5} [NonUnitalNonAssocSemiring α] :
              1 = id
              @[simp]
              theorem CentroidHom.coe_add {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
              (f + g) = f + g
              @[simp]
              theorem CentroidHom.coe_mul {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) :
              (f * g) = f g
              @[simp]
              theorem CentroidHom.coe_smul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (n : M) (f : CentroidHom α) :
              (n f) = n f
              @[simp]
              theorem CentroidHom.zero_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :
              0 a = 0
              @[simp]
              theorem CentroidHom.one_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :
              1 a = a
              @[simp]
              theorem CentroidHom.add_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
              (f + g) a = f a + g a
              @[simp]
              theorem CentroidHom.mul_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
              (f * g) a = f (g a)
              @[simp]
              theorem CentroidHom.smul_apply {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (n : M) (f : CentroidHom α) (a : α) :
              (n f) a = n f a
              @[simp]
              theorem CentroidHom.toEnd_add {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) :
              (x + y).toEnd = x.toEnd + y.toEnd
              theorem CentroidHom.toEnd_smul {M : Type u_2} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Monoid M] [DistribMulAction M α] [SMulCommClass M α α] [IsScalarTower M α α] (m : M) (x : CentroidHom α) :
              (m x).toEnd = m x.toEnd
              Equations
              Equations
              • CentroidHom.instNatCast = { natCast := fun (n : ) => n 1 }
              @[simp]
              theorem CentroidHom.coe_natCast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ) :
              n = n (CentroidHom.id α)
              theorem CentroidHom.natCast_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ) (m : α) :
              n m = n m
              @[simp]
              theorem CentroidHom.toEnd_mul {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (y : CentroidHom α) :
              (x * y).toEnd = x.toEnd * y.toEnd
              @[simp]
              theorem CentroidHom.toEnd_pow {α : Type u_5} [NonUnitalNonAssocSemiring α] (x : CentroidHom α) (n : ) :
              (x ^ n).toEnd = x.toEnd ^ n
              @[simp]
              theorem CentroidHom.toEnd_natCast {α : Type u_5} [NonUnitalNonAssocSemiring α] (n : ) :
              (n).toEnd = n
              Equations

              CentroidHom.toEnd as a RingHom.

              Equations
              • CentroidHom.toEndRingHom α = { toFun := CentroidHom.toEnd, map_one' := , map_mul' := , map_zero' := , map_add' := }
              Instances For
                theorem CentroidHom.comp_mul_comm {α : Type u_5} [NonUnitalNonAssocSemiring α] (T : CentroidHom α) (S : CentroidHom α) (a : α) (b : α) :
                (T S) (a * b) = (S T) (a * b)
                Equations
                instance CentroidHom.instModule {R : Type u_4} {α : Type u_5} [NonUnitalNonAssocSemiring α] [Semiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] :
                Equations

                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.

                Equations
                @[simp]
                theorem CentroidHom.smul_def {α : Type u_5} [NonUnitalNonAssocSemiring α] (T : CentroidHom α) (a : α) :
                T a = T a

                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

                @[simp]
                theorem Module.toCentroidHom_apply_toFun {α : Type u_5} [NonUnitalNonAssocSemiring α] {R : Type u_6} [CommSemiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] (x : R) (a : α) :
                (Module.toCentroidHom x) a = x a
                def Module.toCentroidHom {α : Type u_5} [NonUnitalNonAssocSemiring α] {R : Type u_6} [CommSemiring R] [Module R α] [SMulCommClass R α α] [IsScalarTower R α α] :

                The natural ring homomorphism from R into CentroidHom α.

                This is a stronger version of Module.toAddMonoidEnd.

                Equations
                • Module.toCentroidHom = RingHom.smulOneHom
                Instances For

                  The canonical homomorphism from the center into the centroid

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem CentroidHom.centerToCentroid_apply {α : Type u_5} [NonUnitalNonAssocSemiring α] (z : (NonUnitalSubsemiring.center α)) (a : α) :
                    (CentroidHom.centerToCentroid z) a = z * a
                    theorem NonUnitalNonAssocSemiring.mem_center_iff {α : Type u_5} [NonUnitalNonAssocSemiring α] (a : α) :
                    a NonUnitalSubsemiring.center α AddMonoid.End.mulRight a = AddMonoid.End.mulLeft a AddMonoid.End.mulLeft a (CentroidHom.toEndRingHom α).rangeS
                    theorem NonUnitalNonAssocCommSemiring.mem_center_iff {α : Type u_5} [NonUnitalNonAssocCommSemiring α] (a : α) :
                    a NonUnitalSubsemiring.center α ∀ (b : α), Commute (AddMonoid.End.mulLeft b) (AddMonoid.End.mulLeft a)

                    The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Negation of CentroidHoms as a CentroidHom.

                      Equations
                      • CentroidHom.instNeg = { neg := fun (f : CentroidHom α) => let __src := -f; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
                      Equations
                      • CentroidHom.instSub = { sub := fun (f g : CentroidHom α) => let __src := f - g; { toAddMonoidHom := __src, map_mul_left' := , map_mul_right' := } }
                      Equations
                      • CentroidHom.instIntCast = { intCast := fun (z : ) => z 1 }
                      @[simp]
                      theorem CentroidHom.coe_intCast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ) :
                      z = z (CentroidHom.id α)
                      theorem CentroidHom.intCast_apply {α : Type u_5} [NonUnitalNonAssocRing α] (z : ) (m : α) :
                      z m = z m
                      @[simp]
                      theorem CentroidHom.toEnd_neg {α : Type u_5} [NonUnitalNonAssocRing α] (x : CentroidHom α) :
                      (-x).toEnd = -x.toEnd
                      @[simp]
                      theorem CentroidHom.toEnd_sub {α : Type u_5} [NonUnitalNonAssocRing α] (x : CentroidHom α) (y : CentroidHom α) :
                      (x - y).toEnd = x.toEnd - y.toEnd
                      Equations
                      @[simp]
                      theorem CentroidHom.coe_neg {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) :
                      (-f) = -f
                      @[simp]
                      theorem CentroidHom.coe_sub {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) :
                      (f - g) = f - g
                      @[simp]
                      theorem CentroidHom.neg_apply {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (a : α) :
                      (-f) a = -f a
                      @[simp]
                      theorem CentroidHom.sub_apply {α : Type u_5} [NonUnitalNonAssocRing α] (f : CentroidHom α) (g : CentroidHom α) (a : α) :
                      (f - g) a = f a - g a
                      @[simp]
                      theorem CentroidHom.toEnd_intCast {α : Type u_5} [NonUnitalNonAssocRing α] (z : ) :
                      (z).toEnd = z
                      Equations
                      @[reducible, inline]
                      abbrev CentroidHom.commRing {α : Type u_5} [NonUnitalRing α] (h : ∀ (a b : α), (∀ (r : α), a * r * b = 0)a = 0 b = 0) :

                      A prime associative ring has commutative centroid.

                      Equations
                      Instances For