Theorems · Definition · group theory

DirectSum.fromAddMonoid

{ι : Type v} →
  {β : ι → Type w} →
    [inst : (i : ι) → AddCommMonoid (β i)] →
      [DecidableEq ι] →
        {γ : Type u₁} → [inst_2 : AddCommMonoid γ] → (DirectSum ι fun i => γ →+ β i) →+ γ →+ DirectSum ι fun i => β i

fromAddMonoid φ is the natural homomorphism from γ to ⨁ i, β i induced by a family φ of homomorphisms γ → β i. Note that this is not an isomorphism. Not every homomorphism γ →+ ⨁ i, β i arises in this way.

Defined in

Mathlib.Algebra.DirectSum.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEqAddCommMonoid