Theorems · Definition · group theory

DirectSum.Decomposition.ofAddHom

{ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : SetLike σ M] →
            [inst_3 : AddSubmonoidClass σ M] →
              (ℳ : ι → σ) →
                (decompose : M →+ DirectSum ι fun i => ↥(ℳ i)) →
                  (DirectSum.coeAddMonoidHom ℳ).comp decompose = AddMonoidHom.id M →
                    decompose.comp (DirectSum.coeAddMonoidHom ℳ) = AddMonoidHom.id (DirectSum ι fun i => ↥(ℳ i)) →
                      DirectSum.Decomposition ℳ

A convenience method to construct a decomposition from an AddMonoidHom, such that the proofs of left and right inverse can be constructed via ext.

Defined in

Mathlib.Algebra.DirectSum.Decomposition

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidSetLikeAddSubmonoidClass