Theorems · Definition · nonassociative algebras

NonUnitalAlgHom.comp

{R : Type u} →
  {S : Type u₁} →
    {T : Type u_1} →
      [inst : Monoid R] →
        [inst_1 : Monoid S] →
          [inst_2 : Monoid T] →
            {φ : R →* S} →
              {A : Type v} →
                {B : Type w} →
                  {C : Type w₁} →
                    [inst_3 : NonUnitalNonAssocSemiring A] →
                      [inst_4 : DistribMulAction R A] →
                        [inst_5 : NonUnitalNonAssocSemiring B] →
                          [inst_6 : DistribMulAction S B] →
                            [inst_7 : NonUnitalNonAssocSemiring C] →
                              [inst_8 : DistribMulAction T C] →
                                {ψ : S →* T} →
                                  {χ : R →* T} → (B →ₛₙₐ[ψ] C) → (A →ₛₙₐ[φ] B) → [κ : φ.CompTriple ψ χ] → A →ₛₙₐ[χ] C

The composition of morphisms is a morphism.

Defined in

Mathlib.Algebra.Algebra.NonUnitalHom

Cited by

21 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

MonoidMonoidMonoidNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionNonUnitalNonAssocSemiringDistribMulActionMonoidHom.CompTriple