Theorems · Definition · ring theory

DirectSum.liftRingHom

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

Families of AddMonoidHoms preserving DirectSum.One.one and DirectSum.Mul.mul are isomorphic to RingHoms on ⨁ i, A i. This is a stronger version of DFinsupp.liftAddHom.

Defined in

Mathlib.Algebra.DirectSum.Ring

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidAddMonoidDirectSum.GSemiringSemiring