Theorems · Definition · ring theory

DirectSum.toSemiring

{ι : Type u_1} →
  [inst : DecidableEq ι] →
    {A : ι → Type u_2} →
      {R : Type u_3} →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : DirectSum.GSemiring A] →
              [inst_4 : Semiring R] →
                (f : (i : ι) → A i →+ R) →
                  (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

A family of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul describes a RingHoms on ⨁ i, A i. This is a stronger version of DirectSum.toMonoid. Of particular interest is the case when A i are bundled subobjects, f is the family of coercions such as AddSubmonoid.subtype (A i), and the [GSemiring A] structure originates from DirectSum.gsemiring.ofAddSubmonoids, in which case the proofs about GOne and GMul can be discharged by rfl.

Defined in

Mathlib.Algebra.DirectSum.Ring

Cited by

6 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidAddMonoidDirectSum.GSemiringSemiring