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

## Main definitions #

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

## Main statements #

• DirectSum.Decomposition.isInternal: The link to DirectSum.IsInternal.

## Implementation details #

As we want to talk about different types of decomposition (additive monoids, modules, rings, ...), we choose to avoid heavily bundling DirectSum.decompose, instead making copies for the AddEquiv, LinearEquiv, 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 DirectSum.Decomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
Type (max u_1 u_3)

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 DirectSum.IsInternal which comes with a constructive inverse to the canonical "recomposition" rather than just a proof that the "recomposition" is bijective.

Often it is easier to construct a term of this type via Decomposition.ofAddHom or Decomposition.ofLinearMap.

Instances
theorem DirectSum.Decomposition.left_inv {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] {ℳ : ισ} [self : ] :
Function.LeftInverse () DirectSum.Decomposition.decompose'
theorem DirectSum.Decomposition.right_inv {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] {ℳ : ισ} [self : ] :
Function.RightInverse () DirectSum.Decomposition.decompose'
instance DirectSum.instSubsingletonDecomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :

DirectSum.Decomposition instances, while carrying data, are always equal.

Equations
• =
@[reducible, inline]
abbrev DirectSum.Decomposition.ofAddHom {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (decompose : M →+ DirectSum ι fun (i : ι) => ( i)) (h_left_inv : .comp decompose = ) (h_right_inv : decompose.comp = AddMonoidHom.id (DirectSum ι fun (i : ι) => ( i))) :

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

Equations
Instances For
noncomputable def DirectSum.IsInternal.chooseDecomposition {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (h : ) :

Noncomputably conjure a decomposition instance from a DirectSum.IsInternal proof.

Equations
• = { decompose' := ().symm, left_inv := , right_inv := }
Instances For
theorem DirectSum.Decomposition.isInternal {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
def DirectSum.decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
M DirectSum ι fun (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
• = { toFun := DirectSum.Decomposition.decompose', invFun := , left_inv := , right_inv := }
Instances For
theorem DirectSum.Decomposition.inductionOn {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {p : MProp} (h_zero : p 0) (h_homogeneous : ∀ {i : ι} (m : ( i)), p m) (h_add : ∀ (m m' : M), p mp m'p (m + m')) (m : M) :
p m
@[simp]
theorem DirectSum.Decomposition.decompose'_eq {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
DirectSum.Decomposition.decompose' =
@[simp]
theorem DirectSum.decompose_symm_of {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {i : ι} (x : ( i)) :
.symm ((DirectSum.of (fun (i : ι) => ( i)) i) x) = x
@[simp]
theorem DirectSum.decompose_coe {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {i : ι} (x : ( i)) :
x = (DirectSum.of (fun (i : ι) => ( i)) i) x
theorem DirectSum.decompose_of_mem {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {x : M} {i : ι} (hx : x i) :
x = (DirectSum.of (fun (i : ι) => ( i)) i) x, hx
theorem DirectSum.decompose_of_mem_same {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {x : M} {i : ι} (hx : x i) :
(( x) i) = x
theorem DirectSum.decompose_of_mem_ne {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {x : M} {i : ι} {j : ι} (hx : x i) (hij : i j) :
(( x) j) = 0
theorem DirectSum.degree_eq_of_mem_mem {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {x : M} {i : ι} {j : ι} (hxi : x i) (hxj : x j) (hx : x 0) :
i = j
def DirectSum.decomposeAddEquiv {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
M ≃+ DirectSum ι fun (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
• = (let __src := .symm; { toEquiv := __src, map_add' := }).symm
Instances For
@[simp]
theorem DirectSum.decomposeAddEquiv_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (a : M) :
= a
@[simp]
theorem DirectSum.decomposeAddEquiv_symm_apply {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (a : DirectSum ι fun (i : ι) => ( i)) :
.symm a = .symm a
@[simp]
theorem DirectSum.decompose_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
0 = 0
@[simp]
theorem DirectSum.decompose_symm_zero {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) :
.symm 0 = 0
@[simp]
theorem DirectSum.decompose_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : M) (y : M) :
(x + y) = x + y
@[simp]
theorem DirectSum.decompose_symm_add {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : DirectSum ι fun (i : ι) => ( i)) (y : DirectSum ι fun (i : ι) => ( i)) :
.symm (x + y) = .symm x + .symm y
@[simp]
theorem DirectSum.decompose_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {ι' : Type u_5} (s : Finset ι') (f : ι'M) :
(s.sum fun (i : ι') => f i) = s.sum fun (i : ι') => (f i)
@[simp]
theorem DirectSum.decompose_symm_sum {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) {ι' : Type u_5} (s : Finset ι') (f : ι'DirectSum ι fun (i : ι) => ( i)) :
.symm (s.sum fun (i : ι') => f i) = s.sum fun (i : ι') => .symm (f i)
theorem DirectSum.sum_support_decompose {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) [(i : ι) → (x : ( i)) → Decidable (x 0)] (r : M) :
(().sum fun (i : ι) => (( r) i)) = r
instance DirectSum.addCommGroupSetLike {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [SetLike σ M] [] (ℳ : ισ) :
AddCommGroup (DirectSum ι fun (i : ι) => ( i))

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

This seems to 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
• = inferInstance
@[simp]
theorem DirectSum.decompose_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : M) :
(-x) = - x
@[simp]
theorem DirectSum.decompose_symm_neg {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : DirectSum ι fun (i : ι) => ( i)) :
.symm (-x) = -.symm x
@[simp]
theorem DirectSum.decompose_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : M) (y : M) :
(x - y) = x - y
@[simp]
theorem DirectSum.decompose_symm_sub {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [] [] [SetLike σ M] [] (ℳ : ισ) (x : DirectSum ι fun (i : ι) => ( i)) (y : DirectSum ι fun (i : ι) => ( i)) :
.symm (x - y) = .symm x - .symm y
@[reducible, inline]
abbrev DirectSum.Decomposition.ofLinearMap {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) (decompose : M →ₗ[R] DirectSum ι fun (i : ι) => ( i)) (h_left_inv : ∘ₗ decompose = LinearMap.id) (h_right_inv : decompose ∘ₗ = LinearMap.id) :

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

Equations
Instances For
def DirectSum.decomposeLinearEquiv {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) :
M ≃ₗ[R] DirectSum ι fun (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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DirectSum.decomposeLinearEquiv_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) (m : M) :
@[simp]
theorem DirectSum.decomposeLinearEquiv_symm_apply {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) (m : DirectSum ι fun (i : ι) => ( i)) :
.symm m = .symm m
@[simp]
theorem DirectSum.decompose_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) (r : R) (x : M) :
(r x) = r x
@[simp]
theorem DirectSum.decomposeLinearEquiv_symm_comp_lof {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) (i : ι) :
.symm ∘ₗ DirectSum.lof R ι (fun (x : ι) => ( x)) i = ( i).subtype
theorem DirectSum.decompose_lhom_ext {ι : Type u_1} {R : Type u_2} {M : Type u_3} [] [] [] [Module R M] (ℳ : ι) {N : Type u_5} [] [Module R N] ⦃f : M →ₗ[R] N ⦃g : M →ₗ[R] N (h : ∀ (i : ι), f ∘ₗ ( i).subtype = g ∘ₗ ( i).subtype) :
f = g

Two linear maps from a module with a decomposition agree if they agree on every piece.

Note this cannot be @[ext] as ℳ cannot be inferred.