Theorems · Definition · ring theory

GradedAlgHom.comp

{R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {C : Type u_8} →
        {ι : Type u_10} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Semiring B] →
                [inst_3 : Semiring C] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra R B] →
                      [inst_6 : Algebra R C] →
                        [inst_7 : DecidableEq ι] →
                          [inst_8 : AddMonoid ι] →
                            {𝒜 : ι → Submodule R A} →
                              {ℬ : ι → Submodule R B} →
                                {𝒞 : ι → Submodule R C} →
                                  [inst_9 : GradedAlgebra 𝒜] →
                                    [inst_10 : GradedAlgebra ℬ] →
                                      [inst_11 : GradedAlgebra 𝒞] → (ℬ →ₐᵍ[R] 𝒞) → (𝒜 →ₐᵍ[R] ℬ) → 𝒜 →ₐᵍ[R] 𝒞

If g and f are R-linear graded algebra homomorphisms with the domain of g equal to the codomain of f, then g.comp f is the graded algebra homomorphism x ↦ g (f x).

Defined in

Mathlib.RingTheory.GradedAlgebra.AlgHom

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraDecidableEqAddMonoidGradedAlgebraGradedAlgebraGradedAlgebra