Theorems · Theorem · ring theory

DirectSum.toAlgebra_apply

∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) {B : Type uB} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (A i)] [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι]
  [inst_4 : DirectSum.GSemiring A] [inst_5 : Semiring B] [inst_6 : DirectSum.GAlgebra R A] [inst_7 : Algebra R B]
  [inst_8 : DecidableEq ι] (f : (i : ι) → A i →ₗ[R] B) (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj)
  (a : DirectSum ι fun i => A i),
  (DirectSum.toAlgebra R A f hone hmul) a = (DirectSum.toSemiring (fun i => (f i).toAddMonoidHom) hone hmul) a

Defined in

Mathlib.Algebra.DirectSum.Algebra

Cited by

0 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddMonoidDirectSum.GSemiringSemiringDirectSum.GAlgebraAlgebraDecidableEq