Theorems · Theorem · ring theory

GradedAlgHom.comp_assoc

∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Semiring D] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra R C] [inst_8 : Algebra R D] [inst_9 : DecidableEq ι] [inst_10 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} {𝒞 : ι → Submodule R C} {𝒟 : ι → Submodule R D}
  [inst_11 : GradedAlgebra 𝒜] [inst_12 : GradedAlgebra ℬ] [inst_13 : GradedAlgebra 𝒞] [inst_14 : GradedAlgebra 𝒟]
  (fCD : 𝒞 →ₐᵍ[R] 𝒟) (fBC : ℬ →ₐᵍ[R] 𝒞) (fAB : 𝒜 →ₐᵍ[R] ℬ), (fCD.comp fBC).comp fAB = fCD.comp (fBC.comp fAB)

Defined in

Mathlib.RingTheory.GradedAlgebra.AlgHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebraDecidableEqAddMonoidGradedAlgebraGradedAlgebraGradedAlgebraGradedAlgebra