# mathlib3documentation

algebra.direct_sum.decomposition

# Decompositions of additive monoids, groups, and modules into direct sums #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• direct_sum.decomposition ℳ: A typeclass to provide a constructive decomposition from an additive monoid M into a family of additive submonoids ℳ
• direct_sum.decompose ℳ: The canonical equivalence provided by the above typeclass

## Main statements #

• direct_sum.decomposition.is_internal: The link to direct_sum.is_internal.

## Implementation details #

As we want to talk about different types of decomposition (additive monoids, modules, rings, ...), we choose to avoid heavily bundling direct_sum.decompose, instead making copies for the add_equiv, linear_equiv, etc. This means we have to repeat statements that follow from these bundled homs, but means we don't have to repeat statements for different types of decomposition.

@[class]
structure direct_sum.decomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) :
Type (max u_1 u_3)
• decompose' : M (λ (i : ι), (ℳ i))
• left_inv :
• right_inv :

A decomposition is an equivalence between an additive monoid M and a direct sum of additive submonoids ℳ i of that M, such that the "recomposition" is canonical. This definition also works for additive groups and modules.

This is a version of direct_sum.is_internal which comes with a constructive inverse to the canonical "recomposition" rather than just a proof that the "recomposition" is bijective.

Instances of this typeclass
Instances of other typeclasses for direct_sum.decomposition
@[protected, instance]
def direct_sum.decomposition.subsingleton {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) :

direct_sum.decomposition instances, while carrying data, are always equal.

@[protected]
theorem direct_sum.decomposition.is_internal {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
def direct_sum.decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
M (λ (i : ι), (ℳ i))

If M is graded by ι with degree i component ℳ i, then it is isomorphic as to a direct sum of components. This is the canonical spelling of the decompose' field.

Equations
@[protected]
theorem direct_sum.decomposition.induction_on {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {p : M Prop} (h_zero : p 0) (h_homogeneous : {i : ι} (m : (ℳ i)), p m) (h_add : (m m' : M), p m p m' p (m + m')) (m : M) :
p m
@[simp]
theorem direct_sum.decomposition.decompose'_eq {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
@[simp]
theorem direct_sum.decompose_symm_of {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {i : ι} (x : (ℳ i)) :
.symm) ((direct_sum.of (λ {i : ι}, (ℳ i)) i) x) = x
@[simp]
theorem direct_sum.decompose_coe {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {i : ι} (x : (ℳ i)) :
= (direct_sum.of (λ {i : ι}, (ℳ i)) i) x
theorem direct_sum.decompose_of_mem {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {x : M} {i : ι} (hx : x ℳ i) :
= (direct_sum.of (λ (i : ι), (ℳ i)) i) x, hx⟩
theorem direct_sum.decompose_of_mem_same {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {x : M} {i : ι} (hx : x ℳ i) :
( x) i) = x
theorem direct_sum.decompose_of_mem_ne {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {x : M} {i j : ι} (hx : x ℳ i) (hij : i j) :
( x) j) = 0
def direct_sum.decompose_add_equiv {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
M ≃+ (λ (i : ι), (ℳ i))

If M is graded by ι with degree i component ℳ i, then it is isomorphic as an additive monoid to a direct sum of components.

Equations
@[simp]
theorem direct_sum.decompose_add_equiv_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
@[simp]
theorem direct_sum.decompose_add_equiv_symm_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
@[simp]
theorem direct_sum.decompose_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
= 0
@[simp]
theorem direct_sum.decompose_symm_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ)  :
.symm) 0 = 0
@[simp]
theorem direct_sum.decompose_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x y : M) :
(x + y) = +
@[simp]
theorem direct_sum.decompose_symm_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x y : (λ (i : ι), (ℳ i))) :
.symm) (x + y) = .symm) x + .symm) y
@[simp]
theorem direct_sum.decompose_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {ι' : Type u_2} (s : finset ι') (f : ι' M) :
(s.sum (λ (i : ι'), f i)) = s.sum (λ (i : ι'), (f i))
@[simp]
theorem direct_sum.decompose_symm_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) {ι' : Type u_2} (s : finset ι') (f : ι' (λ (i : ι), (ℳ i))) :
.symm) (s.sum (λ (i : ι'), f i)) = s.sum (λ (i : ι'), .symm) (f i))
theorem direct_sum.sum_support_decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) [Π (i : ι) (x : (ℳ i)), decidable (x 0)] (r : M) :
(dfinsupp.support r)).sum (λ (i : ι), ( r) i)) = r
@[protected, instance]
def direct_sum.add_comm_group_set_like {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [ M] [ M] (ℳ : ι σ) :
add_comm_group (λ (i : ι), (ℳ i)))

The - in the statements below doesn't resolve without this line.

This seems to a be a problem of synthesized vs inferred typeclasses disagreeing. If we replace the statement of decompose_neg with @eq (⨁ i, ℳ i) (decompose ℳ (-x)) (-decompose ℳ x) instead of decompose ℳ (-x) = -decompose ℳ x, which forces the typeclasses needed by ⨁ i, ℳ i to be found by unification rather than synthesis, then everything works fine without this instance.

Equations
@[simp]
theorem direct_sum.decompose_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x : M) :
(-x) = -
@[simp]
theorem direct_sum.decompose_symm_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x : (λ (i : ι), (ℳ i))) :
.symm) (-x) = -.symm) x
@[simp]
theorem direct_sum.decompose_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x y : M) :
(x - y) = -
@[simp]
theorem direct_sum.decompose_symm_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [decidable_eq ι] [ M] [ M] (ℳ : ι σ) (x y : (λ (i : ι), (ℳ i))) :
.symm) (x - y) = .symm) x - .symm) y
@[simp]
theorem direct_sum.decompose_linear_equiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [decidable_eq ι] [semiring R] [ M] (ℳ : ι M)  :
def direct_sum.decompose_linear_equiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} [decidable_eq ι] [semiring R] [ M] (ℳ : ι M)  :
M ≃ₗ[R] (λ (i : ι), (ℳ i))

If M is graded by ι with degree i component ℳ i, then it is isomorphic as a module to a direct sum of components.

Equations
@[simp]
theorem direct_sum.decompose_linear_equiv_symm_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [decidable_eq ι] [semiring R] [ M] (ℳ : ι M)  :
@[simp]
theorem direct_sum.decompose_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [decidable_eq ι] [semiring R] [ M] (ℳ : ι M) (r : R) (x : M) :
(r x) = r