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 #
CentroidHom
: Maps which preserve left and right multiplication.
Typeclasses #
References #
Tags #
centroid
The type of centroid homomorphisms from α
to α
.
- toFun : α → α
- map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
- 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
Commutativity of centroid homomorphims with left multiplication.
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
.
- map_zero : ∀ (f : F), f 0 = 0
Commutativity of centroid homomorphims with left multiplication.
Commutativity of centroid homomorphims with right multiplication.
Instances
Commutativity of centroid homomorphims with left multiplication.
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' := ⋯ }
Equations
- ⋯ = ⋯
Helper instance for when there's too many metavariables to apply DFunLike.CoeFun
directly.
Equations
- CentroidHom.instCoeFunForall = inferInstanceAs (CoeFun (CentroidHom α) fun (x : CentroidHom α) => α → α)
Turn a centroid homomorphism into an additive monoid endomorphism.
Equations
- f.toEnd = ↑f
Instances For
Copy of a CentroidHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = { toFun := f', map_zero' := ⋯, map_add' := ⋯, map_mul_left' := ⋯, map_mul_right' := ⋯ }
Instances For
id
as a CentroidHom
.
Equations
- CentroidHom.id α = { toAddMonoidHom := AddMonoidHom.id α, map_mul_left' := ⋯, map_mul_right' := ⋯ }
Instances For
Equations
- CentroidHom.instInhabited α = { default := CentroidHom.id α }
Composition of CentroidHom
s as a CentroidHom
.
Equations
- g.comp f = { toAddMonoidHom := g.comp f.toAddMonoidHom, map_mul_left' := ⋯, map_mul_right' := ⋯ }
Instances For
Equations
- CentroidHom.instZero = { zero := let __src := 0; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }
Equations
- CentroidHom.instOne = { one := CentroidHom.id α }
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 }
Equations
- CentroidHom.instSMul = { smul := fun (n : M) (f : CentroidHom α) => let __src := n • ↑f; { toAddMonoidHom := __src, map_mul_left' := ⋯, map_mul_right' := ⋯ } }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- CentroidHom.hasNPowNat = { pow := fun (f : CentroidHom α) (n : ℕ) => { toAddMonoidHom := f.toEnd ^ n, map_mul_left' := ⋯, map_mul_right' := ⋯ } }
Equations
- CentroidHom.instAddCommMonoid = Function.Injective.addCommMonoid AddMonoidHomClass.toAddMonoidHom ⋯ ⋯ ⋯ ⋯
Alias of CentroidHom.coe_natCast
.
Alias of CentroidHom.natCast_apply
.
Alias of CentroidHom.toEnd_natCast
.
Equations
- CentroidHom.instSemiring = Function.Injective.semiring CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
CentroidHom.toEnd
as a RingHom
.
Equations
- CentroidHom.toEndRingHom α = { toFun := CentroidHom.toEnd, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- CentroidHom.instDistribMulAction = Function.Injective.distribMulAction (CentroidHom.toEndRingHom α).toAddMonoidHom ⋯ ⋯
Equations
- CentroidHom.instModule = Function.Injective.module R (CentroidHom.toEndRingHom α).toAddMonoidHom ⋯ ⋯
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
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
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 center of the centroid
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CentroidHom.instFunLikeSubtypeMemSubsemiringCenter = { coe := fun (f : ↥(Subsemiring.center (CentroidHom α))) => (↑(↑f).toAddMonoidHom).toFun, coe_injective' := ⋯ }
The canonical homomorphism from the center into the centroid
Equations
- CentroidHom.centerToCentroid = (SubsemiringClass.subtype (Subsemiring.center (CentroidHom α))).toNonUnitalRingHom.comp CentroidHom.centerToCentroidCenter
Instances For
The canonical isomorphism from the center of a (non-associative) semiring onto its centroid.
Equations
- CentroidHom.centerIsoCentroid = { toFun := CentroidHom.centerToCentroid.toFun, invFun := fun (T : CentroidHom α) => ⟨T 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Negation of CentroidHom
s 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' := ⋯ } }
Alias of CentroidHom.coe_intCast
.
Alias of CentroidHom.intCast_apply
.
Equations
- CentroidHom.instAddCommGroup = Function.Injective.addCommGroup CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Alias of CentroidHom.toEnd_intCast
.
Equations
- CentroidHom.instRing = Function.Injective.ring CentroidHom.toEnd ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A prime associative ring has commutative centroid.