Theorems · Definition · ring theory

DirectSum.toAlgebra

{ι : 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) →
                            (f 0) GradedMonoid.GOne.one = 1 →
                              (∀ {i j : ι} (ai : A i) (aj : A j),
                                  (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) →
                                (DirectSum ι fun i => A i) →ₐ[R] B

A family of LinearMaps preserving DirectSum.GOne.one and DirectSum.GMul.mul describes an AlgHom on ⨁ i, A i. This is a stronger version of DirectSum.toSemiring. Of particular interest is the case when A i are bundled subobjects, f is the family of coercions such as Submodule.subtype (A i), and the [GMonoid A] structure originates from DirectSum.GMonoid.ofAddSubmodules, in which case the proofs about GOne and GMul can be discharged by rfl.

Defined in

Mathlib.Algebra.DirectSum.Algebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddMonoidDirectSum.GSemiringSemiringDirectSum.GAlgebraAlgebraDecidableEq